<p>I am wondering about relative consistency of various Martin-Löf type theories, when compared to one another, I will use MLTT for the intensional Martin-Löf type theory with <span class="math-container">$\Pi$</span>, <span class="math-container">$\Sigma$</span>, <span class="math-container">$\mathbb{N}$</span>, Id, unit and empty types.</p>
<p>Let's formulate consistency as lack of term of empty type and relative consistency being a proof that given the rules of itself T1 and assumption that they are consistent, we can deduce that another type theory T2 is consistent.
So here are the variants.</p>
<ol>
<li>MLTT + Predicative Set universes  (ala Agda without induction recursion)</li>
<li>MLTT + Predicative (S)Prop and Set universes (ala Agda without induction recursion and with -prop)</li>
<li>MLTT + Impredicative (S)Prop (ala Coq)</li>
<li>MLTT + Impredicative Set at the bottom (ala Coq with -impredicative-set but without Prop)</li>
<li>MLTT + Impredicative (S)Prop + Impredicative Set (ala Coq with -impredicative-set)</li>
<li>Combinations of the above with large (agda-style) induction-recursion</li>
</ol>
<p>In the last case I am not even aware of consistency results for the combination with impredicative universes.
Related question seems to be:
<a href="https://cstheory.stackexchange.com/questions/37013/relative-consistency-of-pa-and-some-type-theories">Relative consistency of PA and some type theories</a>, but the answer there does not take into account universes.
I am mostly looking for references discussing the relative consistency of these.</p>

CC BY-SA 4.0
2021-03-11T13:02:18.760Z
It's odd to call it "Martin-Löf type theory" without having the identity types also. Did you just forget them, or is there a reason for excluding them?
Andrej Bauer
CC BY-SA 4.0
2021-03-11T13:03:46.577Z
@AndrejBauer just forgot thanks for catching that
Ilk
CC BY-SA 4.0
2021-03-11T13:04:44.207Z
It might also be worth spelling out what you mean by "relative consistency", precisely. Presumably you'd also explain what consistency is in this case, is it "there is no closed term of type $\mathtt{empty}$?
Andrej Bauer
<reference-request><type-theory><proof-theory>
Relative consistency of various Martin-Löf style type theories
Ilk
# Relative consistency of various Martin-Löf style type theories

(Asked by: username_0 on 2021-03-11)

I am wondering about relative consistency of various Martin-Löf type theories, when compared to one another, I will use MLTT for the intensional Martin-Löf type theory with $\Pi$, $\Sigma$, $\mathbb{N}$, Id, unit and empty types.

Let's formulate consistency as lack of term of empty type and relative consistency being a proof that given the rules of itself T1 and assumption that they are consistent, we can deduce that another type theory T2 is consistent.
So here are the variants.

1. MLTT + Predicative Set universes (ala Agda without induction recursion)
2. MLTT + Predicative (S)Prop and Set universes (ala Agda without induction recursion and with -prop)
3. MLTT + Impredicative (S)Prop (ala Coq)
4. MLTT + Impredicative Set at the bottom (ala Coq with -impredicative-set but without Prop)
5. MLTT + Impredicative (S)Prop + Impredicative Set (ala Coq with -impredicative-set)
6. Combinations of the above with large (agda-style) induction-recursion

In the last case I am not even aware of consistency results for the combination with impredicative universes.
Related question seems to be:
[Relative consistency of PA and some type theories](https://cstheory.stackexchange.com/questions/37013/relative-consistency-of-pa-and-some-type-theories), but the answer there does not take into account universes.
I am mostly looking for references discussing the relative consistency of these.

**Tags:** reference-request, type-theory, proof-theory

> **Comments:**
> **username_1**: It's odd to call it "Martin-Löf type theory" without having the identity types also. Did you just forget them, or is there a reason for excluding them?  
> **username_0**: @AndrejBauer just forgot thanks for catching that  
> **username_1**: It might also be worth spelling out what you mean by "relative consistency", precisely. Presumably you'd also explain what consistency is in this case, is it "there is no closed term of type $\mathtt{empty}$?  

---

## 0 answers

