A sequence in the hierarchy of universes

Question

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.

Answer 1

I think you'll find that your definition of $T$ doesn't require as many universes as you think. It's mainly unclear because you've elided subscripts. For instance, what if you wrote:

$$ T : ℕ → \mathcal{U}_1 \\ T(0) = ℕ \\ T(n+1) = T(n) → \mathcal{U}_0 $$

That's a valid way of assigning subscripts, and it only requires two universes. I would guess Idris is doing something like that (where the result of $T$ is one larger than the universe referred to in the second case of $T$).

If the subscript is not internal, there's no way to write something where the subscript would vary depending on the value of the argument to $T$. It could vary based on how many cases you write down for $T$ and related definitions, but you can only write finitely many of those, and don't need something like $\mathcal{U}_ω$ to handle that.

There are type theories with universes that can be thought of as having universes indexed by $ω$ and beyond, although those universes are indexed internally in the examples I'm familiar with.

Answer 2

I'm now a little bit smarter about that and thanks to Dan Doel's answer, I figured out my misconception. What would actually force $\mathcal U_\omega$ to exist, were a $\operatorname{typeof}$ operator, i.e. for any universe index $i$, a function $$\operatorname{typeof}\colon\mathcal U_i\to \mathcal U_{i+1}$$ that maps objects to their types. I (for some reason) thought that $X \to \mathcal U$ would kind of do that, but it doesn't. Using that hypothetical $\operatorname{typeof}$ operator, one could define by induction (leaving universe levels open for the moment) $$ \begin{align} T\colon\mathbb N & \to \mathcal U \\ 0 &\mapsto \mathbb N \\ n+1 &\mapsto \operatorname{typeof}(T(n) \to \mathcal U) \end{align} $$ If I'm correct, that would necessarily bump universe levels each step. So $T\colon\mathbb N \to \mathcal U_i$ is an impossible assignment for a finite $i$. But since no $\operatorname{typeof}$ operator exists in HoTT (or dependent-type programming languages I know) or could be replicated, such a definition is impossible. In HoTT and similar languages, $\operatorname{typeof}$ still exists outside the language, i.e. we, from outside, can see that any object has a type, but there's no way internal to HoTT to get from an object to its type.