All Questions
Tagged with coq calculus-of-inductive-constructions
5
questions
6
votes
1
answer
409
views
What are the principal differences between Agda's core type theory and Coq's?
Agda is said to be based on Luo's unifying theory of dependent types while Coq is based on the Calculus of Inductive Constructions. Both of these as I understand it extend the impredicative ...
3
votes
2
answers
222
views
Universe inconsistency errors when using ZF model in Coq
I am trying to use a formal logic system I recently implemented in Coq to study ZF set theory. In order to do this, I need to define a type representing the domain in question, and then prove that ...
- 195
0
votes
1
answer
162
views
Why inductive types (or variants) are so rigid in terms of the set of constructors
An inductive type definition normally carries a set of constructors C, but I am not so sure why the set of constructors C is always once-for-all statically defined.
For instance:
...
- 125
13
votes
3
answers
827
views
Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?
Question
Is CiC stronger than CoC, in terms of proof strength?
Context
To illustrate the kind of confusion I am in, and what I'd like to learn from the answer, here is part of my inner monologue:
If I ...
- 139
26
votes
4
answers
1k
views
What are the differences between MLTT and CIC?
In the theory and design of proof assistants based upon dependent types, I feel like there’s a somewhat cultural divide between the "MLTT" world (with Agda as the main representative proof ...
- 5,455