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.

Filter by
Sorted by
Tagged with
13 votes
3 answers
668 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 ...
6 votes
2 answers
182 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. ...
  • 518
8 votes
1 answer
168 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 ...
10 votes
2 answers
122 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 &...
  • 896
18 votes
1 answer
912 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 ...
  • 455
3 votes
1 answer
86 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 ...
  • 896
8 votes
1 answer
207 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 ...
  • 5,223
15 votes
2 answers
265 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
24 votes
4 answers
654 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 ...