Consistency strength of HoTT

Question

What is the consistency strength of Homotopy type theory (HoTT) relative to various set theories (e.g., are there any known set theories that it can interpret)? Does this question even make sense?

Answer 1

The proof theoretic strength of HoTT was studied by Rathjen in Proof Theory of Constructive Systems: Inductive Types and Univalence. The paper surveys a number of long known results on the relative strength of type theory and set theory, and then observes that the cubical set model of HoTT works in a sufficient constructive metatheory that the same observations apply. In particular, we can read off the following results:

1. Martin-Löf type theory with a countable hierarchy of univalent universes has the same proof theoretic strength as

   1. $\mathbf{CZF}$ with for each $n$, an axiom asserting there is an increasing sequence of inaccessibles of length $n$.
   2. $\mathbf{CZF}$ with inaccessibles as above but also the presentation axiom and other choice principles.
   3. $\mathbf{CZF}$ with inaccessibles as above but also $\mathbf{LPO}$.
   4. Kripke-Platek set theory with for each $n > 0$, an axiom asserting there are at least $n$ recursively inaccessible ordinals.

2. Removing W-types from type theory lowers the proof theoretic strength quite a bit. Martin-Löf type theory with a countable hierarchy of univalent universes but without W types has the same consistency strength as

   1. $\mathbf{CZF}$ without $\in$-induction (but with infinity strengthened), inaccessibles as above, and $\mathbf{RDC}$.
   2. Kripke-Platek without $\in$-induction, but with infinity strengthened, and every set is an element of an admissible set.
   3. $\mathbf{ATR}_0$

I'll add to this that looking at the construction of HITs in Coquand, Huber, Mörtberg On Higher Inductive Types in Cubical Type Theory we can see that the construction of the standard examples of HITs (let's say pushouts, W-types and localization) only requires inductive types that are known to exist in $\mathbf{CZF}$ given enough inaccessibles, so exactly the same remarks apply to type theory with HITs as well as univalence. We can also see that the construction of finitary HITs only requires finitary inductive types in the metatheory, and so e.g. type theory with univalence, a natural number type and pushouts has the same strength as the weaker set theories above.

As people pointed out in the comments, there is an interpretation of $\mathbf{ZFC}$ in the HoTT book. This requires assuming the axiom of choice in type theory to work. However, the law of excluded middle is sufficient to get a model of $\mathbf{ZF}$, which has the same consistency strength as $\mathbf{ZFC}$ using Gödel's $L$. On the other hand the simplicial set model in Kapulkin, Lumsdaine, (after Voevodsky), The simplicial model of Univalent Foundations can be carried out in $\mathbf{ZFC}$ with sufficiently many inaccessibles. This gives type theory with excluded middle, univalence and HITs the same consistency strength as $\mathbf{ZFC}$ together with the same inaccessible set axioms as above for $\mathbf{CZF}$.

This just leaves the case of HoTT with propositional resizing. In the HIT cumulative hierarchy interpretation of set theory in HoTT, propositional resizing is only enough to get a model of $\mathbf{IZF}_R$, which is not known to have the same consistency strength as $\mathbf{ZF}$.

However, we can give an alternative construction, assuming the existence of a suitable HIT and combining the HIT cumulative hierarchy with double negation sheafification, as in Rijke, Shulman, Spitters, Modalities in homotopy type theory to get a model of $\mathbf{ZF}$, as follows. Note that we can interpret type theory into the reflective subuniverse for an accessible lex modality, as in Quirin, Lawvere-Tierney sheafification in homotopy type theory, to get an interpretation of type theory with univalence where the law of excluded middle holds. It remains to show that this interpretation contains a cumulative hierarchy HIT. Following Gylterud, From multisets to sets in homotopy type theory, the HIT cumulative hierarchy can be constructed as a retract of the Aczel cumulative hierarchy, which is just a W type, so we only need to show how to construct W types in the reflective subuniverse. We will use the free injective HIT denoted $\mathcal{J}_F$ by Rijke, Shulman and Spitters. It can be used to construct sheafification, as they showed, but note that W-types are also a special case of the free injective. For any W-type (including the Aczel hierarchy) we can combine the constructors for the W-type with the constructors for sheafification to get a HIT that does both simultaneously, to get a type which is an algebra for the polynomial associated to the W-type, a sheaf, and the initial such type, and so constructs the W-type in the reflective subuniverse as we needed.

I'll leave it open whether type theory with univalence and propositional resizing, but without assuming free injectives has the same consistency strength as $\mathbf{ZF}$.