The [HoTT Book](https://homotopytypetheory.org/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.



A sequence in the hierarchy of universes
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.


