Unanswered Questions
23 questions with no upvoted or accepted answers
23
votes
0
answers
571
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 3,200
12
votes
0
answers
169
views
Rules for mutual inductive/coinductive types
Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
- 3,200
10
votes
0
answers
187
views
Is there a proof assistant (or an embedding) for the (co)end calculus?
A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
- 2,846
9
votes
0
answers
309
views
Alternatives to universe levels
All of the type theory based proof assistants that I have seen have an infinite hierarchy of type universes to avoid the type of types being a term of itself. Are there alternative systems which could ...
- 91
6
votes
0
answers
114
views
Is every logical theory embeddable in a dependently typed extensional type theory?
In category theory by the Yoneda embedding every category $\mathcal{C}$ is a subcategory of a category of presheafs $[\mathcal{C}^{\text{op}}, \text{Set}]$. Every category of presheafs is a topos and ...
- 2,868
5
votes
0
answers
246
views
Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination
Setup
Current Understanding
I've recently been trying to learn about the interaction of Impredicative Polymorphism, Large Elimination and Excluded Middle (notably, inconsistency). Notably, this is ...
- 73
5
votes
0
answers
168
views
What are the conditions for Agda to detect that induction-recursion has a least fixed point?
This is a 3rd in a series of questions, spurred by my attempts to encode an argument by Danielsson [1] [2] regarding existence of syntactically non-strictly positive datatype.
The idea (rephrased):
...
- 107
5
votes
0
answers
95
views
What is the relation of $\lambda^\to$ and $\lambda^{\to\times}$ to cartesian closed categories?
I am learning about the categorical semantics of type theory. I've written some preliminary results in Agda. In particular, I partially proved that the contexts and substitutions of simply-typed ...
- 4,025
4
votes
0
answers
122
views
Proving "proof methods" as theorems in type-theory based proof systems
For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as
add_assoc : forall (x y : T), x + y + z = x + (y + z).
We can thus prove ...
- 41
4
votes
0
answers
107
views
Independence of function extensionality
Who first realized that function extensionality cannot be proved within vanilla MLTT, or some variations of it? Now to my knowledge the simplest way to show this is by syntactic models. But surely ...
- 4,025
3
votes
0
answers
97
views
Limitations of simple type theory proof assistants for undergraduate-level mathematics?
I'm interested in understanding the practical power and limitations of simple type theory, particularly as compared with dependent type theory, in supporting formalized proofs of theorems liable to ...
- 345
2
votes
0
answers
68
views
Tool for typing mathematical physics, e.g. differential geometry
Many expressions in mathematical physics use a rather sloppy notation, e.g. the Lie bracket on a vector field is defined using ambiguous notation, where $X : M \rightarrow TM$ is first defined as a ...
- 4,025
2
votes
0
answers
62
views
Elimination rules of inductive types
Why does the elimination rule of inductive types sometimes allow the target type to depend on the inductive type and sometimes not? I am confused by that. Is it correct that it makes no difference in ...
- 722
1
vote
0
answers
108
views
Proving Quine's notion that identity belongs to logic within type-constrained proof assistants
I'm having difficulty generalizing the following proof to permit predicates of any finite arity.
Consider the following axioms of identity consistent with W. V. O. Quine's argument that relative ...
- 111
1
vote
0
answers
70
views
Heterogeneous lists, large indices
Recently I had cause to define a type of heterogeneous lists in Lean, and wrote
...
- 111