10
$\begingroup$

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?

$\endgroup$
  • $\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 Klimpel Jul 24 '15 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 Berger Jul 24 '15 at 9:48
  • 2
    $\begingroup$ @MartinBerger: CiC has identity types as well! $\endgroup$ – cody Jul 24 '15 at 17:24
  • $\begingroup$ @Cody True, I had forgotten that you can define them inductively! $\endgroup$ – Martin Berger Jul 24 '15 at 18:15
  • 2
    $\begingroup$ @AndrejBauer If I was witty enough I'd come up with a brexit joke, but unfortunately I'm not. :-P $\endgroup$ – user Feb 18 '17 at 1:59
16
$\begingroup$

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:

  1. 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.

  2. 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.

  3. 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.

  4. Axiom K: this comes for free with certain versions of dependent pattern matching.

  5. 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.

  6. 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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.