Unanswered Questions
25 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
15
votes
0
answers
216
views
Code generation from Locales and Sublocales in Isabelle
Problem Description
I stumbled on this limitation/misunderstanding several times when using locales and sublocales in Isabelle. As a minimal example, let us extend the locale from the example in ...
- 1,128
13
votes
0
answers
369
views
Unintentionally proven false theorem with type-in-type outside logic and foundations?
We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
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
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
42
views
Implementing object-logics in Isabelle Best Practices?
I'm patching up Isabelle/Mizar to work with Isabelle2023, and I am wondering what are the best practices for implementing an object logic in Isabelle? (Usually there is great documentation for ...
- 1,574
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
3
votes
0
answers
56
views
Why are modules also rings in the HOL-Algebra library?
We would like to use vectors and matrices (2x2 and 3x3) in a project, and have found the Jordan Normal Form AFP entry (Matrix.thy) which provides a concrete ...
- 131
2
votes
1
answer
52
views
Extract explicit value from Isabelle proof
How can I extract an explicit value for a schematic variable in Isabelle after using it in a proof? For
example, in the following goal, I’m looking to extract a numerical value for ...
- 221