Here are a few comparisons of dependent type theories with fragments of Peano arithmetic and set theories that I know of:
Predicative systems (the MLTT family)
Predicative systems are comparable with small fragments of second-order arithmetic. Their strength is measured by which inductive definitions are allowed:
- When there is only a type of natural numbers, we get the strength of ATR₀, in the sense that both theories prove the same Π⁰₂ statements about arithmetic (proved in the paper you mention). ATR₀ is a small fragment of PA2 which plays an important role in reverse mathematics.
- Adding W-types makes the system stronger than Δ¹₂-CA but weaker than Π¹₂-CA, which are slightly larger fragments of PA2.
- Induction-recursion is still a bit stronger, but is expected to be bounded above by KPM+ (see here) which is still weaker than Π¹₂-CA, I believe. This is more or less the theory of Agda.
The order can be refined by taking into account the number of predicative universes : MLTT₁ < MLTT₂ < ... < MLTTω < MLTT₁ + W < ... MLTTω + W < MLTT₁ + IR < ...
A detailed table that also includes ordinal notations and references can be found on the nLab.
Extensionality axioms such as function extensionality, proposition extensionality, UIP, univalence, equality reflection... do not add any logical strength to the system. The full law of excluded middle, however, is another story: now any type is either inhabited or not, which basically makes Bool an impredicative universe of propositions — and impredicative systems are much stronger. In fact, MLTT + LEM has the same strength as CIC + LEM.
Impredicative systems (System F, CC, CIC)
The introduction of an impredicative universe adds a tremendous amount of logical strength to a system. We jump from small fragments of second-order arithmetic to systems which are at least as strong as the full PA2.
- System F has the strength of second-order arithmetic, in the sense that an integer function is provably total in PA2 if and only if it can be defined in system F (standard reference).
- CC, the calculus of constructions (which has an impredicative universe Prop which sits inside the predicative universe Type) has the strength of higher-order arithmetic.
- CCω, which adds a hierarchy of predicative universes, is stronger than Zermelo set theory (proved here), but weaker than ZF set theory (as witnessed by the normalization proof).
Note that the strength comparison theorems are about definable functions, not provable arithmetic statements as before. Indeed, all of these systems have no inductive types at all, so even the integers need to be encoded with impredicativity. And while you can define very complex functions on these impredicative integers, predicates cannot tell them apart: you can't even prove 0≠1. If we want to do such things, we need to add inductive types with large elimination, which results in CIC, the calculus of inductive constructions.
- If we restrict large elimination in the impredicative universe to sub-singleton inductive types, then we can lift functions that are defined on impredicative integers to predicative, inductive integers while remaining compatible with classical set-theoretic semantics. This is more or less the theory of Coq.
- If we allow large elimination for all inductive types in the impredicative universe, then the system becomes incompatible with classical logic.
- Finally, if you add LEM and a variant of the axiom of choice to CIC, then it becomes comparable with ZFC set theory (proved here)
