Skip to main content
27 votes

Proof-theoretic comparison table?

Here are a few comparisons of dependent type theories with fragments of Peano arithmetic and set theories that I know of: Predicative systems (the MLTT family) Predicative systems are comparable with ...
Loïc Pujet's user avatar
  • 1,479
22 votes

What are the differences between MLTT and CIC?

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it ...
Neel Krishnaswami's user avatar
18 votes

What are the differences between MLTT and CIC?

The short answer is: $\mathbf{MLTT}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$, and $\mathbf{CiC}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, ...
Namdak Tönpa's user avatar
12 votes

What are the differences between MLTT and CIC?

The technical answers are correct, but they completely overlook the philosophical differences between the two formalisms. Martin-Löf type theory closely reflects Arendt Heyting's explanations of the ...
Lawrence Paulson's user avatar
11 votes

What are the differences between MLTT and CIC?

Apart from judgmental equality, MLTT and CIC also differ in the following: The existence of an impredicative universe. CIC has Prop, and that's what makes it a part of the lambda cube. This universe ...
ice1000's user avatar
  • 6,256
10 votes

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

Meven's answer explains that without inductive types, you cannot hope to recover a natural number object with proper induction principles. You can interpret this as saying that you lose some ...
Loïc Pujet's user avatar
  • 1,479
9 votes
Accepted

How does Metamath Zero handle CIC as in Lean or Coq?

All three of your possibilities are potential options for future directions, although they get progressively more "future" as you go down the list. Extract the full proof from a modified ...
Mario Carneiro's user avatar
7 votes

What's "predicative" about pC(u)IC?

As an additional bit of trivia: I found the following in Chapter 4 of the Coq Reference Manual, V8.4: For Cᴏǫ version V7, this Calculus was known as the Calculus of (Co)Inductive Constructions (Cɪᴄ ...
ionchy's user avatar
  • 1,026
7 votes
Accepted

What are the principal differences between Agda's core type theory and Coq's?

I will answer the headline question and ignore UTT (I believe thinking of Agda as UTT causes more confusion than it solves). There are very many differences between the theories Agda and Coq implement,...
James Wood's user avatar
  • 1,053
7 votes

Universe inconsistency errors when using ZF model in Coq

Here is how I would go about formalizing first-order logic and models, with a small fragment of ZF as an example. Note that we can still carry out Gödel coding by natural numbers, so long as the types ...
Andrej Bauer's user avatar
  • 9,553
6 votes

Are Logics Based on Dependent Types Stronger Than Ones Without?

Pretty much always, it means "this gadget is more annoying to formalise in HOL", not "this gadget is not possible to formalise in HOL." A simple example of this is formalising ...
Neel Krishnaswami's user avatar
5 votes

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

In complement to Meven Lennon-Bertrand's answer, it is shown in From realizability to induction via dependent intersection by Aaron Stump that by extending $\lambda P2$ (or CoC) with dependent ...
Couchy's user avatar
  • 2,241
5 votes

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

There is a paper by Geuvers constructing a model showing that Induction is not derivable in second order logic. The name is pretty explicit, but to reformulate, the main result is that while you can ...
Meven Lennon-Bertrand's user avatar
5 votes
Accepted

Is unguarded fixpoint reduction consistent?

This is consistent. First, this equality holds propositionally by eta-expansion of the constructor. Thus, if your type theory had equality reflection, it would also hold definitionally. Since ...
Pierre-Marie Pédrot's user avatar
4 votes
Accepted

Why inductive types (or variants) are so rigid in terms of the set of constructors

There are two components to your question. The first, corresponds to the idea of constructor subtyping (actually, non-empty lists are the first example of the paper). I don't think there are any hard ...
Meven Lennon-Bertrand's user avatar
4 votes
Accepted

Are Logics Based on Dependent Types Stronger Than Ones Without?

For completeness I'm adding the specific example that the OP is asking for, turning my comment above and Jason Rute's into an answer. One thing that make type theories occurring in most PAs strictly ...
Pedro Sánchez Terraf's user avatar
4 votes
Accepted

What's "predicative" about pC(u)IC?

As far as I know, the "Predicative" part refers to the existence of the type hierarchy. But the CIC/PCIC/PCUIC terminologies are not very fixed, and they can vary quite a lot between article…...
Meven Lennon-Bertrand's user avatar
4 votes
Accepted

How to prove in Lean that sums are distributive?

Likely the most idiomatic option is the equation compiler: ...
It'sNotALie.'s user avatar
  • 1,445
2 votes

How to prove in Lean that sums are distributive?

I have figured out how to write the inverse using @sum.cases_on. The rules of @sum.cases_on in lean are nearly identical as the rules of match in Jacobs book. The code is: ...
Nico's user avatar
  • 722
2 votes

What should be cited for "the Calculus of inductive Constructions"?

It depends on what you're willing to accept, right? It could be: Th. Coquand and C. Paulin-Mohring, "Inductively defined types". In P. Martin-Lof and G. Mints, editors, Proceedings of Colog’...
Alex Nelson's user avatar
  • 1,564
1 vote
Accepted

Universe inconsistency errors when using ZF model in Coq

Not sure exactly how your problem appears since you do not give the code up to the point where you get your failures so I cannot reproduce. But here is a self-contained example that should do the ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible