<p><em>I am lost in a maze of twisty little type theories, all different.</em></p>
<p>There are a number of works (textbooks and papers) that discuss pure type theories, and specifically the ones constituting the <a href="https://en.wikipedia.org/wiki/Lambda_cube" rel="nofollow noreferrer">Barendregt lambda cube</a>: these works generally do a decent job of explaining how the various type theories therein relate to each other, and how they differ, and what each one's expressive power is.  But they rarely say anything about Martin-Löf's type theories except a bare mention of their existence.</p>
<p>Conversely, there are a (smaller) number of works that discuss Martin-Löf's various flavors of <a href="https://en.wikipedia.org/wiki/Intuitionistic_type_theory" rel="nofollow noreferrer">intuitionistic type theory</a> (“MLTT”).  But they rarely say anything beyond that.</p>
<p>So I'm left very puzzled as to how the two above sets compare to each other.  I can see some differences, of course, but I'm not sure exactly what is relevant and what is just presentational ornament.  Specifically, how do MLTTs compare with the theories in the lambda cube in terms of predicativity, expressive power (interpretability) and arithmetical strength (e.g., expressible total functions, consistency strength)?</p>
<p>The only text I found which puts at least some effort in comparing the two sets is the paper by <a href="https://link.springer.com/article/10.1023/A:1011286100450" rel="nofollow noreferrer">Fairouz Kamareddine &amp; Twan Laan, “A Correspondence between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems”, <em>J. of Log., Lang. Inf.</em> <strong>10</strong> (2001), 375–402</a>; this does clarify things somewhat, but it still fails to really address the (maybe obvious?) question of where MLTT theories sit wrt the lambda cube and how powerful they are; also, the appearance of Russell's ramified theory of types adds another room to the maze.</p>
<p>So, could somebody suggest a place where the precise relation between MLTT and the “lambda cube” theories is discussed, or at least provide a summary of what such a discussion would look like?</p>
<hr />
<p><strong>Edit</strong> (2023-11-11): Various bits of answer I've managed to find after asking the question, which do clarify things somewhat even if they don't amount to a full answer, are:</p>
<ul>
<li><p><a href="https://cstheory.stackexchange.com/questions/32071/is-mltt-effectively-pcic-without-prop/32076#32076">this answer by cody</a> in this StackExchange, confirming that “MLTT can reasonably be equated with CIC without impredicative <code>Prop</code>” but then pointing out a number of technical issues, including many variations that can be considered in these theories;</p>
</li>
<li><p><a href="https://proofassistants.stackexchange.com/questions/1201/proof-theoretic-comparison-table/1210#1210">this very comprehensive answer by Loïc Pujet</a> on the “Proof Assistants” StackExckange, comparing the (proof-theoretic) logical strength of a number of variants of both MLTT and CC (in short the former are below second-order arithmetic whereas the latter are above, but there are subtleties: see Loïc's full answer, as well as <a href="https://cstheory.stackexchange.com/questions/37013/relative-consistency-of-pa-and-some-type-theories/37016#37016">this older one by cody</a> for some further clarifications);</p>
</li>
<li><p>the various answers to <a href="https://proofassistants.stackexchange.com/questions/267/what-are-the-differences-between-mltt-and-cic">this other Proof Assistants question about differences between MLTT and CIC</a> (which is <em>sort</em> of a duplicate of the present one) have interesting things to say, even if they go in all sorts of different directions.</p>
</li>
</ul>
<p>There seems to be very little scholarly work devoted to comparing theories on the “MLTT” side and on the “lambda cube” (/“CoC”) side (e.g., I could find nothing concerning interpretability of fragments of one side in the other side — maybe this is a stupid question).  I'd be happy to be proved wrong.  In fact, there seems to be a dearth of scholarly work even <em>mentioning</em> both sides.  Still, <a href="https://perso.eleves.ens-rennes.fr/%7Esboul434/thesis/thesis-boulier-latest.pdf" rel="nofollow noreferrer">Simon Boulier's thesis, <em>Extending type theory with syntactic models</em> (2018)</a> deals with both (and has some remarks pertaining to the present question, e.g., in §1.2).  The survey <a href="https://arxiv.org/abs/1411.1029" rel="nofollow noreferrer">“An overview of type theories” by Nino Guallart</a> discusses both “lambda cube” theories and MLTT, but as the title suggests, it says very little.</p>

CC BY-SA 4.0
2023-11-09T23:17:31.120Z
One difficulty you'll find is that nobody can seem to agree on what makes a type theory a Martin-Loef type theory. Usually it is completely predicative, but beyond that there's no consensus. W-tyoes? Maybe. Cumulative universes? Maybe. Could be Tarski universes, could be Russell. You might have better luck searching "Calculus of Constructions vs MLTT"
Joey Eremondi
CC BY-SA 4.0
2023-11-10T12:57:34.547Z
The novel feature of MLTT are *identity types*, which ML introduced so he can keep the his type-theory predicative. (You need impredicativity to do equality using Leibniz' *"principium identitatis indiscernibilium"*). So maybe: MLTT can be summarised as: any dependently typed, predicative type theory with identity types?
Martin Berger
CC BY-SA 4.0
2023-11-10T20:10:50.207Z
One difficulty you'll find is that there are no widely accepted definitions of morphisms between type theories, which makes it difficult to compare them.
Andrej Bauer
CC BY-SA 4.0
2023-11-11T09:33:55.243Z
@AndrejBauer Indeed, it's not at all clear to me what sort of interpretability relation one might hope to define (and I was sort of hoping someone would enlighten me in passing). Still, at the very least, one can consider the arithmetical statements “$T$ has strong normalization” for various type theories $T$ of the MLTT or lambda-cube side, and ask for the implications between them (over, say, Peano or Heyting arithmetic): unless I am mistaken, this is a well-defined question (and at least partially answered by Loïc Pujet's answer I've just added a link to).
Gro-Tsen
CC BY-SA 4.0
2023-11-11T10:08:48.900Z
@MartinBerger: saying that the indentity types are "the" novel feature of MLTT is not really fair. It's "a" novel feature.
Andrej Bauer
CC BY-SA 4.0
2023-11-11T11:18:00.887Z
@AndrejBauer What other features have you got in mind? (I'm not a historian of TT, so I'm not totally sure who invented what.)
Martin Berger
CC BY-SA 4.0
2023-11-11T20:14:51.577Z
If Wikipedia is to be trusted, then Martin-Löf invented dependent types, although I don't think this is quite fair, as Automath also had notions of dependency. [These slides](https://www.cse.chalmers.se/~coquand/ndw.pdf) by Theirry Coquand have lots of interesting information. He claims Martin-Löf invented the dependent sum. He certainly cleared up a lot of confusion (such as Automath's equating $\lambda$ and $\Pi$), not to mention that Martin-Löf early on pointed out the  significance of type theory for computer science (on that note, it's amazing that Bishop almost invented type theory).
Andrej Bauer
CC BY-SA 4.0
2023-11-11T20:18:51.400Z
The significance of Martin-Löf's work is so pervasive that it's difficult to see at times: intensional vs. extensional, type theory as a programming language, conceptuaal and mathematical significance of strong normalization (as opposed to a mere technique). I believe all these originate from Martin-Löf, although history is a tricky subject.
Andrej Bauer
CC BY-SA 4.0
2023-12-27T15:25:19.930Z
Cheating a little, I found the following chaperter to have the clearest comparison of MTLL and CoC.  Some of the exercises prove and motivate the differences in proof strangh: Martin Hofmann. Syntax and Semantics of Dependent Types, pages 79-130. Publications of the Newton Institute. Cambridge University Press, 1997.
user833970
CC BY-SA 4.0
2023-12-27T17:36:22.943Z
@user833970 That looks like a very decent answer! One should note, however, that there appear to be two texts with the same title by the same author and the same year of publication (), namely [this one](https://doi.org/10.1017/CBO9780511526619.004) and [this one](https://doi.org/10.1007/978-1-4471-0963-1_2). I think you mean the former, but the latter may be interesting as well.
Gro-Tsen
CC BY-SA 4.0
2023-12-28T00:33:55.360Z
Sorry i did mean the book chapter!
user833970
CC BY-SA 4.0
2023-12-28T09:53:04.393Z
@user833970 Both are book chapters. It really is confusing.
Gro-Tsen
CC BY-SA 4.0
2023-12-28T17:51:32.073Z
Right.  The first link was intended
user833970
<lo.logic><type-theory><big-picture><typed-lambda-calculus>
Is there a text that discusses both the “lambda cube” of pure type theories and Martin-Löf's intuitionistic type theories, and compares them?
Gro-Tsen
# Is there a text that discusses both the “lambda cube” of pure type theories and Martin-Löf's intuitionistic type theories, and compares them?

(Asked by: username_0 on 2023-11-09)

*I am lost in a maze of twisty little type theories, all different.*

There are a number of works (textbooks and papers) that discuss pure type theories, and specifically the ones constituting the [Barendregt lambda cube](https://en.wikipedia.org/wiki/Lambda_cube): these works generally do a decent job of explaining how the various type theories therein relate to each other, and how they differ, and what each one's expressive power is. But they rarely say anything about Martin-Löf's type theories except a bare mention of their existence.

Conversely, there are a (smaller) number of works that discuss Martin-Löf's various flavors of [intuitionistic type theory](https://en.wikipedia.org/wiki/Intuitionistic_type_theory) (“MLTT”). But they rarely say anything beyond that.

So I'm left very puzzled as to how the two above sets compare to each other. I can see some differences, of course, but I'm not sure exactly what is relevant and what is just presentational ornament. Specifically, how do MLTTs compare with the theories in the lambda cube in terms of predicativity, expressive power (interpretability) and arithmetical strength (e.g., expressible total functions, consistency strength)?

The only text I found which puts at least some effort in comparing the two sets is the paper by [Fairouz Kamareddine & Twan Laan, “A Correspondence between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems”, *J. of Log., Lang. Inf.* **10** (2001), 375–402](https://link.springer.com/article/10.1023/A:1011286100450); this does clarify things somewhat, but it still fails to really address the (maybe obvious?) question of where MLTT theories sit wrt the lambda cube and how powerful they are; also, the appearance of Russell's ramified theory of types adds another room to the maze.

So, could somebody suggest a place where the precise relation between MLTT and the “lambda cube” theories is discussed, or at least provide a summary of what such a discussion would look like?

---

**Edit** (2023-11-11): Various bits of answer I've managed to find after asking the question, which do clarify things somewhat even if they don't amount to a full answer, are:

* [this answer by cody](https://cstheory.stackexchange.com/questions/32071/is-mltt-effectively-pcic-without-prop/32076#32076) in this StackExchange, confirming that “MLTT can reasonably be equated with CIC without impredicative `Prop`” but then pointing out a number of technical issues, including many variations that can be considered in these theories;
* [this very comprehensive answer by Loïc Pujet](https://proofassistants.stackexchange.com/questions/1201/proof-theoretic-comparison-table/1210#1210) on the “Proof Assistants” StackExckange, comparing the (proof-theoretic) logical strength of a number of variants of both MLTT and CC (in short the former are below second-order arithmetic whereas the latter are above, but there are subtleties: see Loïc's full answer, as well as [this older one by cody](https://cstheory.stackexchange.com/questions/37013/relative-consistency-of-pa-and-some-type-theories/37016#37016) for some further clarifications);
* the various answers to [this other Proof Assistants question about differences between MLTT and CIC](https://proofassistants.stackexchange.com/questions/267/what-are-the-differences-between-mltt-and-cic) (which is *sort* of a duplicate of the present one) have interesting things to say, even if they go in all sorts of different directions.

There seems to be very little scholarly work devoted to comparing theories on the “MLTT” side and on the “lambda cube” (/“CoC”) side (e.g., I could find nothing concerning interpretability of fragments of one side in the other side — maybe this is a stupid question). I'd be happy to be proved wrong. In fact, there seems to be a dearth of scholarly work even *mentioning* both sides. Still, [Simon Boulier's thesis, *Extending type theory with syntactic models* (2018)](https://perso.eleves.ens-rennes.fr/%7Esboul434/thesis/thesis-boulier-latest.pdf) deals with both (and has some remarks pertaining to the present question, e.g., in §1.2). The survey [“An overview of type theories” by Nino Guallart](https://arxiv.org/abs/1411.1029) discusses both “lambda cube” theories and MLTT, but as the title suggests, it says very little.

**Tags:** lo.logic, type-theory, big-picture, typed-lambda-calculus
> **Comments:**
> **username_1**: One difficulty you'll find is that nobody can seem to agree on what makes a type theory a Martin-Loef type theory. Usually it is completely predicative, but beyond that there's no consensus. W-tyoes? Maybe. Cumulative universes? Maybe. Could be Tarski universes, could be Russell. You might have better luck searching "Calculus of Constructions vs MLTT"  
> **username_2**: The novel feature of MLTT are *identity types*, which ML introduced so he can keep the his type-theory predicative. (You need impredicativity to do equality using Leibniz' *"principium identitatis indiscernibilium"*). So maybe: MLTT can be summarised as: any dependently typed, predicative type theory with identity types?  
> **username_3**: One difficulty you'll find is that there are no widely accepted definitions of morphisms between type theories, which makes it difficult to compare them.  
> **username_0**: @AndrejBauer Indeed, it's not at all clear to me what sort of interpretability relation one might hope to define (and I was sort of hoping someone would enlighten me in passing). Still, at the very least, one can consider the arithmetical statements “$T$ has strong normalization” for various type theories $T$ of the MLTT or lambda-cube side, and ask for the implications between them (over, say, Peano or Heyting arithmetic): unless I am mistaken, this is a well-defined question (and at least partially answered by Loïc Pujet's answer I've just added a link to).  
> **username_3**: @MartinBerger: saying that the indentity types are "the" novel feature of MLTT is not really fair. It's "a" novel feature.  
> **username_2**: @AndrejBauer What other features have you got in mind? (I'm not a historian of TT, so I'm not totally sure who invented what.)  
> **username_3**: If Wikipedia is to be trusted, then Martin-Löf invented dependent types, although I don't think this is quite fair, as Automath also had notions of dependency. [These slides](https://www.cse.chalmers.se/~coquand/ndw.pdf) by Theirry Coquand have lots of interesting information. He claims Martin-Löf invented the dependent sum. He certainly cleared up a lot of confusion (such as Automath's equating $\lambda$ and $\Pi$), not to mention that Martin-Löf early on pointed out the  significance of type theory for computer science (on that note, it's amazing that Bishop almost invented type theory).  
> **username_3**: The significance of Martin-Löf's work is so pervasive that it's difficult to see at times: intensional vs. extensional, type theory as a programming language, conceptuaal and mathematical significance of strong normalization (as opposed to a mere technique). I believe all these originate from Martin-Löf, although history is a tricky subject.  
> **username_4**: Cheating a little, I found the following chaperter to have the clearest comparison of MTLL and CoC.  Some of the exercises prove and motivate the differences in proof strangh: Martin Hofmann. Syntax and Semantics of Dependent Types, pages 79-130. Publications of the Newton Institute. Cambridge University Press, 1997.  
> **username_0**: @user833970 That looks like a very decent answer! One should note, however, that there appear to be two texts with the same title by the same author and the same year of publication (), namely [this one](https://doi.org/10.1017/CBO9780511526619.004) and [this one](https://doi.org/10.1007/978-1-4471-0963-1_2). I think you mean the former, but the latter may be interesting as well.  
> **username_4**: Sorry i did mean the book chapter!  
> **username_0**: @user833970 Both are book chapters. It really is confusing.  
> **username_4**: Right.  The first link was intended  

---

## 0 answers

