I started to read the HoTT book. I'm now on chapter 1 and I have several questions concerning not even homotopical, but "regular" type theory.


1. On page 24, where the universes are introduced, there is a sequence:


$$\mathcal U\_0:\mathcal U\_1:\mathcal U\_2:\cdots$$


Everything here makes sense, but I don't understand what is $\mathcal{U}\_0$. Maybe I've glossed over the definition?
2. Later in the same section it is stated that there is no type containing all $\mathcal{U}\_i$. Since I'm not yet free from the set-theoretic perspective, I can't help but wonder: can we define something like $\mathcal{U}\_{\omega\_0}$ and so on?
3. Finally, I have a more vague question. I've got some experience with C++ and so I explained to myself Martin-Löf types using data types from C++. However, I have doubts that this approach is even remotely correct. Can somebody help me to understand if this analogy is correct or not?



3 questions about basics of Martin-Löf type theory
Universe levels usually trip up newcomers to type theory since there is no straightforward intuition for them. What I found helpful is to think of them as a *merely technical device to prevent impredicativity*, and only dive deeper into the technicalities when necessary.


The first recognition is that we need a universe: A basic judgment of MLTT is that something is a type: $A \ type$. When making a statement about all types, we need to refer to a collection of types, i.e., a universe $\mathcal{U}$. Consider the type $B :\equiv \Pi\_{A:\mathcal{U}} \mathsf{Id}\_\mathcal{U}(A, A \times \top)$. If we assumed that types like $B$ also lived in $\mathcal{U}$, we could devise devious Russell-style paradoxes, so hence we let $B$ live in a different universe $\mathcal{U}'$. It is no problem to assume that $A$ also lives in $\mathcal{U}'$.


Renaming both universes to $\mathcal{U}\_0$ and $\mathcal{U}\_1$ and repeating these considerations leads to a *cumulative hierarchy of universes* $\mathcal{U}\_0, \mathcal{U}\_1, \mathcal{U}\_2, ...$. So to answer your first question directly: $\mathcal{U}\_0$ is the *basic universe*, and universes later in the hierarchy are introduced at will to prevent impredicativity. Note that cumulativity means that there is a difference between the term-type and the type-universe relationship: Any term lives in exactly one type, e.g., $0 : \mathbb{N}$. A type $A : \mathcal{U}\_i$ lives in infinitely many universes, namely all $\mathcal{U}\_j$ for $j \geq i$.


There are different approaches to formally introduce universes and manage the relation to the typing judgment, most common are ["Tarski-" and "Russell-style" approaches](https://ncatlab.org/homotopytypetheory/show/universe). You probably don't have to worry about that, as the exact implementation is mostly irrelevant when using universe levels in a formalization project.


I'm not aware of any rigorous approaches to introduce something like $\mathcal{U}\_{\omega\_0}$. Since few type theorists are enthusiastic set theorists, I don't think anyone has had the motivation to do such a thing. Paradoxes abound very quickly, and one has to be very careful to not introduce Girard- and Hurkens-style paradoxes. (Dan has pointed out that people around Michael Rathjen and Anton Setzer have worked on the proof-theoretic strength of various type theories, and consider more interesting universe hierarchies in this context.)


If you are an avid C++ programmer, it's completely fine to test out your intuitions in that language. You can't expect any formal rigour, but [Bartosz Milewski](https://bartoszmilewski.com/) has written a whole book expressing some more abstract programming languages principles in C++, and that seems to work surprisingly well. This book also introduces all examples in Haskell, which might provide a nice bridge to languages that have a richer type theoretic foundation.


