Is Martin-Löf type theory basically the predicative Calculus of inductive Constructions without impredicative $\mathtt{Prop}$?
If they're closely related but with more differences than just $\mathtt{Prop}$, what are those differences?
6
-
$\begingroup$ In my book, MLTT is an (old and established) intuitionistic dependent type theory, while I associate the Calculus of Constructions with the Coq proof assistant. But I may be wrong. $\endgroup$– Thomas KlimpelCommented Jul 24, 2015 at 8:42
-
1$\begingroup$ MLTT uses identity types to deal with equality. What would be equality in the predicative fragment of the CiC? $\endgroup$– Martin BergerCommented Jul 24, 2015 at 9:48
-
2$\begingroup$ @MartinBerger: CiC has identity types as well! $\endgroup$– codyCommented Jul 24, 2015 at 17:24
-
1$\begingroup$ This is a bit like asking whether UK is EU without the other 27 member states :-) $\endgroup$– Andrej BauerCommented Feb 17, 2017 at 9:50
-
3$\begingroup$ @AndrejBauer If I was witty enough I'd come up with a brexit joke, but unfortunately I'm not. :-P $\endgroup$– userCommented Feb 18, 2017 at 1:59
|
Show 1 more comment
1 Answer
$\begingroup$
$\endgroup$
The short answer is yes, MLTT can reasonably be equated with CIC without impredicative Prop.
The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense to remove Prop, as one doesn't have either Set or universes of Type.
The main variations one can consider in either of these theories are:
Universes: how many, and how are they defined (Palmgren, On Universes in Type Theory, discusses many inequivalent variations), and whether or not universe polymorphism is admitted.
Which inductive types/families: Agda admits Inductive-Recursive types, but there are many more mundane variations depending on how "large" the types in the constructors and eliminators are allowed, handling parameters vs indices, etc.
Injectivity of type constructors. This leads to a system inconsistent with EM in Agda. Of course Epigram has a more extreme "Observational Type Theory", but this can be considered something different altogether.
Axiom K: this comes for free with certain versions of dependent pattern matching.
Intentional vs Extensional: this is a huge difference, where essentially a new conversion rule is added in the extensional systems $$ \frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B} $$ Which makes type-checking undecidable (but much more powerful!). Martin-Löf himself seems to have considered both types of systems.
The presence of coinductive types and associated elimination principles.
All of the above variations (except OTT) have been considered in the literature and associated with the name "Martin-Löf Type Theory" or "Calculus of Inductive Constructions", mostly because of their association with the Agda and Coq systems, respectively.
So the long answer is that there is no consensus about what the exact definition of either of these systems is.
