3 questions about basics of Martin-Löf type theory 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.

*

*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?


*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?


*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?
 A: 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. 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 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.
