Universes in dependent type theory

Question

I am reading about dependent types theory in the Homotopy Type Theory online book.

In section 1.3 of the Type Theory chapter, it introduces the notion of hierarchy of Universes: $\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : \cdots$, where

every universe $\mathcal{U}_i$ is an element of the next universe $\mathcal{U}_{i+1}$. Moreover, we assume that our universes are cumulative, that is that all the elements of the $i^{\mathrm{th}}$ universe are also elements of the $(i+1)^{\mathrm{th}}$ universe.

Yet, when I look at the formation rules for the various types in appendix A, at first glance, if a universe appears above the bar as a premise, the same universe appears below. For instance for the coproduct types formation rule:

$$\dfrac{\Gamma \vdash A : \mathcal{U}_i \quad \Gamma \vdash B : \mathcal{U}i}{\Gamma \vdash A + B : \mathcal{U}_i}(+\mbox{-}FORM)$$

So my question is why is a hierarchy necessary? Under what circumstances do you need to jump from a universe to one higher in the hierarchy? It is really not obvious to me how given any combination of $A_m: \mathcal{U}_i$, you can end up with a type $B$ that is not in $\mathcal{U}_i$. In more details: the formation rules in sections of the appendix A.2.4, A.2.5, A.2.6, A.2.7, A.2.8, A.2.9, A.2.10, A.3.2, either mention $\mathcal{U}_i$ in the premise and judgement, or just in the judgement.

The book also hints that there is a formal way to assign universes:

If there is any doubt about whether an argument is correct, the way to check it is to try to assign levels consistently to all universes appearing in it.

What is the process for assigning levels consistently?

$\mathcal{U}:\mathcal{U}$ would lead to the Russell paradox. Avoiding the Russell paradox is explicitly mentioned in the book (page 24). It also goes into more details page 54, 55 that is uses “Russell-style universes” rather than “Tarski-style universes”. So at a very high level, I take for granted that the theory wants to avoid the paradox. Unfortunately I don't have the background to make sense of out that directly. What I am after in this question, is really just scratching the surface by getting some examples of things in $\mathcal{U}_j$ and not in $\mathcal{U}_i$ for $j > i$ and may be anything else that give me a feel for how the hierarchies work.

Answer 1

The question under what circumstances we need to jump from a universe to one higher in the hierarchy is a good one. Having the hierarchy and the ability to climb it is important. You need to jump levels when you want to treat a universe as a type or as part of a type. For example to define functions of (non-dependent) type $$ A \rightarrow \mathcal{U}_i $$ you must show that $A \rightarrow \mathcal{U}_i$ is in a universe. But that cannot be $\mathcal{U}_i$ or some smaller universe. So what do we do? To deal with the problem (without using the unsound $\mathcal{U}_i : \mathcal{U}_i$), we need to jump up a universe. The rule that enables us to make this jump is $\mathcal{U}$-Intro $$ \frac{\vdash \Gamma : ctx}{\Gamma \vdash \mathcal{U}_i : \mathcal{U}_{i+1}}, $$ given in Appendix A.2.3. The very point of the hierarchy of universes is that we can do this. This can be seen as a safe approximation of having universes contain themselves.

Answer 2

I will slightly amend Martin's answer to explain where cumulativity comes in (the rule which says that $X : \mathcal{U}_i$ and $i \leq j$ entail $X : \mathcal{U}_j$). Suppose we have $A : \mathcal{U}_{42}$ and we would like to give a type to $A \to \mathcal{U}_{99}$. The formation rule for $\to$ is this: $$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_i}{\Gamma \vdash (X \to Y) : \mathcal{U}_i}$$ (If $X \to Y$ is a shorthand for $\Pi_{x : X} Y$ then the above rule could be derived from the formation rule for $\Pi$, but let us not worry about it.) In order to use this rule, both types involved in the formation of the function type must be in the same universe. In our case we have $A$ in $\mathcal{U}_{42}$ and $\mathcal{U}_{99}$ in $\mathcal{U}_{100}$. So we first use cummulativity to deduce that $A : \mathcal{U}_{100}$ as well, and then proceed to show that $A \to \mathcal{U}_{99}$ has the type $\mathcal{U}_{100}$.

We could get rid of cummulativity, but then the rules become more complex. For example, formation of $\to$ would read $$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_j}{\Gamma \vdash (X \to Y) : \mathcal{U}_{\max(i,j)}}$$ or $$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_j \qquad i \leq k \qquad j \leq k}{\Gamma \vdash (X \to Y) : \mathcal{U}_k}$$ In any case, type theory has many subtle variations, and getting them all to play together nicely seems to be a bit of an art.