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
11 votes
3 answers
587 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 ...
user avatar
5 votes
2 answers
152 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. ...
user avatar
  • 433
8 votes
1 answer
155 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 ...
user avatar
10 votes
2 answers
111 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 &...
user avatar
  • 856
18 votes
1 answer
817 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 ...
user avatar
  • 421
3 votes
1 answer
78 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 ...
user avatar
  • 856
8 votes
1 answer
139 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 ...
user avatar
  • 3,355
15 votes
2 answers
237 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 ...
user avatar
  • 898
24 votes
4 answers
531 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 ...
user avatar