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
3 votes
2 answers

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 ...
Circuit Craft's user avatar
0 votes
1 answer

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: ...
Tiago Campos's user avatar
1 vote
0 answers

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 ...
Alex Byard's user avatar
13 votes
3 answers

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 ...
Max Kubierschky's user avatar
6 votes
2 answers

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. ...
Nico's user avatar
  • 722
8 votes
1 answer

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 ...
user833970's user avatar
10 votes
2 answers

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 &...
ionchy's user avatar
  • 906
21 votes
1 answer

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 ...
user21820's user avatar
  • 485
3 votes
1 answer

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 ...
ionchy's user avatar
  • 906
8 votes
1 answer

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 ...
Jason Rute's user avatar
  • 6,995
15 votes
2 answers

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 ...
Wno-all's user avatar
  • 1,088
25 votes
4 answers

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 ...
Meven Lennon-Bertrand's user avatar