<p>The short answer is yes, MLTT can reasonably be equated with CIC without impredicative <code>Prop</code>.</p>

<p>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 <code>Prop</code>, as one doesn't have either <code>Set</code> or universes of <code>Type</code>.</p>

<p>The main variations one can consider in either of these theories are:</p>

<ol>
<li><p><strong>Universes</strong>: how many, and how are they defined (Palmgren, <em>On Universes in Type Theory</em>, discusses many inequivalent variations), and whether or not <em>universe polymorphism</em> is admitted.</p></li>
<li><p><strong>Which inductive types/families</strong>: 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.</p></li>
<li><p><strong>Injectivity of type constructors</strong>. 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.</p></li>
<li><p><strong>Axiom K</strong>: this comes for free with certain versions of dependent pattern matching.</p></li>
<li><p><strong>Intentional vs Extensional</strong>: 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.</p></li>
<li><p>The presence of <strong>coinductive types</strong> and associated elimination principles.</p></li>
</ol>

<p>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.</p>

<p>So the long answer is that there is no consensus about what the exact definition of either of these systems is.</p>

CC BY-SA 3.0
2015-07-24T17:45:45.283Z
2017-02-17T08:27:45.493Z
2017-02-17T08:27:45.493Z
cody
<p>Is Martin-Löf type theory basically the predicative Calculus of inductive Constructions without impredicative $\mathtt{Prop}$?</p>

<p>If they're closely related but with more differences than just $\mathtt{Prop}$, what are those differences?</p>

CC BY-SA 3.0
2015-07-24T08:42:37.117Z
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.
Thomas Klimpel
CC BY-SA 3.0
2015-07-24T09:48:19.837Z
MLTT uses identity types to deal with equality. What would be equality in the predicative fragment of the CiC?
Martin Berger
CC BY-SA 3.0
2015-07-24T17:24:53.320Z
@MartinBerger: CiC has identity types as well!
cody
CC BY-SA 3.0
2015-07-24T18:15:48.257Z
@Cody True, I had forgotten that you can define them inductively!
Martin Berger
CC BY-SA 3.0
2017-02-17T09:50:44.110Z
This is a bit like asking whether UK is EU without the other 27 member states :-)
Andrej Bauer
CC BY-SA 3.0
2017-02-18T01:59:43.213Z
@AndrejBauer If I was witty enough I'd come up with a brexit joke, but unfortunately I'm not. :-P
user
<type-theory><calculus-of-constructions>
Is MLTT effectively pCiC without Prop?
user
# Is MLTT effectively pCiC without Prop?

(Asked by: username_0 on 2015-07-24)

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?

**Tags:** type-theory, calculus-of-constructions

> **Comments:**
> **username_1**: 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.  
> **username_2**: MLTT uses identity types to deal with equality. What would be equality in the predicative fragment of the CiC?  
> **username_3**: @MartinBerger: CiC has identity types as well!  
> **username_2**: @Cody True, I had forgotten that you can define them inductively!  
> **username_4**: This is a bit like asking whether UK is EU without the other 27 member states :-)  
> **username_0**: @AndrejBauer If I was witty enough I'd come up with a brexit joke, but unfortunately I'm not. :-P  

---

## 1 answers

### Answer by username_3 on 2015-07-24. Score: 24 | Accepted answer

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.


---

