The HoTT Book states in the first chapter that universes are cumulative and that every universe is in some other universe.

Obviously, there needs to be an infinite number of universes then, but universes indexed by natural numbers a-priori seem to suffice.

It also states that $\lambda (i:\mathbb N).\ \mathcal U_i$ does not exist, because indices of universes are not the natural numbers in the theory but assigned outside by the meta-theory. It makes me wonder whether – in the meta-theory – the indices of the universes are natural numbers or not. They cannot be, if $T:\mathbb N \to \mathcal U$ with $$ T(0) = \mathbb N \quad\text{and}\quad T(n+1) = (T(n) \to \mathcal U) $$ is a valid definition. Maybe I'm wrong, but as far as I know, a type family $P: A \to \mathcal U_i$ cannot live in $\mathcal U_i$, but must be in some universe larger than $\mathcal U_i$. Assuming $\mathbb N$ lives in $\mathcal U_0$, $T(n+1)$ must live in a universe at last $\mathcal U_{n+1}$. I'm well aware that here, the universe index isn't a natural number of the theory, but the argument to $T$ is. I'm just seeing that there is a necessity for some universe $\mathcal U_\omega$ for $T$ to live in (where $\omega$ is the well known ordinal). It would have the property to contain an infinite stack of universes, but still doesn't contain itself.

I just wonder if my reasoning is correct or if I got something horribly wrong.

internally, but how is that relevant? (Of course I can't speak to whether $\omega$-many universes is actually enough for HoTT, since I essentially know nothing about it, but the particular point you raise here doesn't seem to be an issue.) $\endgroup$ – Noah Schweber Oct 11 '19 at 18:324more comments