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: 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 (“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; 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 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 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 for some further clarifications);
the various answers to this other Proof Assistants question about 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) 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 discusses both “lambda cube” theories and MLTT, but as the title suggests, it says very little.