Questions tagged [calculus-of-inductive-constructions]
Calculus of (co)Inductive Constructions is a pure type system (Coquand, Huet) equipped with addition types: arbitrary (co)inductive types implementing general (co)inductive schemes; universes as a cumulative hierarchy of predicative types of types; and an impredicative type of propositions.
12
questions
3
votes
2
answers
186
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
127
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
1
vote
0
answers
61
views
Can you help me lay out the different variations of CoC and their generalizations?
I am learning the typed lambda-calculus and looking into the Calculus of Constructions. It was going well until I was slapped in the face with variations, and now I'm confused about the layout of all ...
- 446
13
votes
3
answers
754
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
6
votes
2
answers
230
views
How to prove in Lean that sums are distributive?
Assume we are given three types in Lean.
constants A B C : Type
There is a canonical map of the following form.
...
- 722
8
votes
1
answer
194
views
What should be cited for "the Calculus of inductive Constructions"?
The history of dependent data types spans decades and is a bit confusing. I have seen some implausible claims about which documents present what. I would like to get it right for my own work without ...
- 443
10
votes
2
answers
149
views
What's "predicative" about pC(u)IC?
Timany and Sozeau's Predicative Calculus of Cumulative Inductive Constructions (pCuIC) [1] adds extra cumulativity to the inductive types of (Lee and Werner's [2], I think?) pCIC. But what does the &...
- 906
21
votes
1
answer
1k
views
Proof-theoretic comparison table?
I read this CSTheory SE post, which suggests that it is often not clear what variant of MLTT or CIC is being referred to. But I would like to know the proof-theoretic strengths of the various ...
- 485
3
votes
1
answer
90
views
Is unguarded fixpoint reduction consistent?
In Coq, there are two restrictions on fixpoints to retain normalization:
Recursive calls can only be done on structurally smaller arguments, enforced by a guard condition during type checking; and
...
- 906
8
votes
1
answer
387
views
How does Metamath Zero handle CIC as in Lean or Coq?
Metamath Zero (MM0) is a proof assistant developed by Mario Carneiro. It has a metalogic very similar to the metalogic of MetaMath, but it also borrows design choices from Lean (and maybe other ...
- 6,995
15
votes
2
answers
319
views
Are Logics Based on Dependent Types Stronger Than Ones Without?
There have been several times during I came across statements like Isabelle/HOL's logic is not rich enough to formalize X on various places online and in during personal discussions. Or similar ...
- 1,088
25
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 ...
- 4,098