François G. Dorais

Research in Logic and Foundations of Mathematics


On the structure of universes in HoTT

In this post, I want to outline some subtle and interesting aspects and issues with respect to universes in HoTT. Some of these issues were brought up in a comment discussion with Mike Shulman some time ago and they came up again more recently in a comment discussion with Andrej Bauer and Alexander Kuklev. I will use the HoTT book as a reference though this post is not intended as a criticism of the handling of universes in the book. Indeed, to serve its purpose, the book is deliberately vague about the exact handling of universes in HoTT. In fact, this post is a good illustration why this is necessary!

Also note that the issues I bring up are mostly irrelevant to conducting everyday mathematics in HoTT. While this post is largely for people interested in technical aspects of HoTT, I will nevertheless try to keep the the post at a medium level of technicality since these aspects of HoTT do come occasionally up in everyday mathematics.

In section 1.3, the HoTT book introduces universes as follows:

[W]e introduce a hierarchy of universes

where every universe is an element of the next universe . Moreover, we assume that our universes are cumulative, that is that all the elements of the th universe are also elements of the st universe, i.e. if then also

In the comment discussion mentioned in the preamble, I expressed concerns with the nature of the subscripts in this description. As a result of this discussion, some minor clarification were made to the book. In particular, the following paragraph was added at the end of section 1.3:

As a non-example, in our version of type theory there is no type family “”. Indeed, there is no universe large enough to be its codomain. Moreover, we do not even identify the indices of the universes with the natural numbers of type theory (the latter to be introduced in §1.9).

And further remarks were added in the notes to chapter 1. The purpose of this post is to explain why this matters and also to explain how fiddling with the structure of universes affects HoTT. I will focus on Classical HoTT (HoTT with the Axiom of Choice for sets and hence the Law of Excluded Middle for propositions) though comparable issues arise without these assumptions.

To illustrate the issue, let’s peek at chapter 10 and in particular at section 10.5, where the book describes the interpretation of the cumulative hierarchy of sets inside HoTT. In any universe one can find a type that faithfully interprets the cumulative hierarchy and (since we are working in Classical HoTT) Theorem 10.5.11 shows that is a model ZFC. In particular, HoTT proves the consistency of ZFC. In fact, HoTT proves the consistency of even stronger theories! With some work, one can show that each is a level of whose ordinal rank is an inaccessible cardinal in Therefore, for each Classical HoTT proves the consistency of where abbreviates the statement “there are at least inaccessible cardinals.”

Does this mean that Classical HoTT proves ? No, it doesn’t. To understand this, remember that is a purely arithmetical statement which basically states that there is no proof of from the axioms of Hence is also an arithmetical statement. The only way for HoTT to make sense of this is for to range over the type of natural numbers This is explicitly excluded by the remark quoted above from the end of section 1.3.

The reason for this exclusion becomes more visible if we use an alternative way to handle universes, replacing the hierarchy with a rule which simply says that any two types are contained in a common universe. More precisely (but still suppressing many technical details) given any two types we can introduce a universe type such that The above argument showing that Classical HoTT proves the consistency of requires applications of this rule in order to obtain a sufficiently long chain of universes. Since proofs are finite, a proof can only use the above universe rule finitely often. Therefore, this process does not lead to a proof of in Classical HoTT.

In order to get an actual proof of in we need to have a hierarchy of universes indexed by More formally, we need a type family which will allow us to use induction on to obtain an actual proof of Doing so, we inadvertently obtain more than we set out. The type family must live in some universe and the cumulative hierarchy associated with this satisfies where says that there are infinitely many inaccessible cardinals. Therefore Classical HoTT with the hypothesis of such a family proves which is much stronger than what we set out to do.

In fact, Classical HoTT with proves and so on. Why stop there? What if we have a family for every wellordering ? Can we go beyond? These “large universe hypotheses” are direct analogues of large cardinal hypotheses from set theory. These may seem frivolous at first but such hypotheses necessarily come into play to answer concrete mathematical questions in Classical HoTT such as whether it is possible to extend Lebesgue measure to all subsets of

Let me use this opportunity to point out a feature of the alternative way to handle universes using a rule as outlined above: the rule implies that every type belongs to some universe. The book handles this with this brief remark in section 1.3:

When we say that is a type, we mean that it inhabits some universe

This is a clever workaround that unfortunately has some side effects. There is no way to formally say “every type belongs to some .” The universes are named constants which means that there is no way to quantify over them. Thus effect of the remark is not to prohibit other types but only to declare anything else to be an “illegetimate” type. The intent is to simplify technical issues but it makes types like illegitimate and effectively blocks the possibility of large universe hypotheses as described above.

Mike Shulman suggested a band-aid for this problem in the discussion mentioned earlier, pointing out that there could be universes, even legitimate ones, other than the named universes For example, we could introduce an infinite hierarchy of universes in if we wanted to. This is true but I do not find this fix fully satisfactory. Universes are very special types that are equipped with a lot of technical machinery to allow elements of universes to become actual types and much more. The book mostly suppresses this machinery, and rightfully so since there are many options which are all very technical and not particularly enlightening. Nevertheless, this machinery is implicitly present and it does not appear on its own. My reading of the syntactic hierarchy used in the book is that this machinery is instantiated for each named universe specifically. To say that there might be other universe suggests that players don’t have all the rules of the game, which is disconcerting. My alternative proposal with a rule to introduce a universe containing any two types implicitly assumes that there is some form of additional judgment for universes (or similar device) and that this judgment instantiates all the machinery to make a universe. I find this kind of approach more satisfactory since it allows one to add hypotheses such as the existence of without changing the rules of the game.

Let me close by mentioning that there are plenty of alternatives for these issues. For example, it is not necessarily desirable for every type to belong to a universe. While formalizing a proof above, we accidentally proved a lot more because had to live in some universe. If doesn’t live in a universe, but induction on still works for such types, we can still prove but we can’t necessarily prove as we did above. In fact, there is no need for a single solution: and other set theories have always coexisted pleasantly. However, there is a need to discuss these solutions and to appropriately identify them so that there is no pointless confusion when such aspects of HoTT do matter.


CC0 Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.


Comments