12
$\begingroup$

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?

$\endgroup$
5
  • 1
    $\begingroup$ $U_0$ is just the initial step in the ladder of the universes (if the number $0$ scares you in principle you could shift all the indices by $1$ and nothing would change). I don't understand your point 2 (the set-theoretic analog of this observation is that there is no set of all sets). In 3 what analogy are you using? Curry-Howard correspondence is valid and there is a lot of reading material on it on the Internet. $\endgroup$
    – Faris
    Commented Jan 27, 2021 at 10:26
  • $\begingroup$ @Faris Thank you for your comment! So, $\mathcal{U}_0$ could be chosen to be any type? My matter is not with the index, but with the substance: what is $\mathcal{U}_0?$ I understand that the type of all types does not exist, but I thought that maybe this hierarchy of universes could be extended transfinitely by some wizardry. Apparently not. And huge thanks once again for your prompt response. $\endgroup$ Commented Jan 27, 2021 at 10:31
  • 7
    $\begingroup$ Transfinite universe hierarchies are completely fine, they are usually not considered because countable universes is enough for most practical purposes. The ordinal notation convention would be more appropriate, since universe levels must be ordered, so we'd write $\omega_0$. If we have $U_{\omega_0}$, that enables quantification over all finite levels. $\endgroup$ Commented Jan 27, 2021 at 10:44
  • 3
    $\begingroup$ A couple of months ago, Agda (you play Agda without installing it at the Agdapad) obtained universes up to $\mathcal{U}_{\omega\cdot2}$, whereas before we just had $\mathcal{U}_\omega$. So yes, iterating this beyond $\omega$ is definitely possible, and in some circumstances also useful. (Why stop at $\omega\cdot2$? It's the smallest extension such that every type has a type and such that we can quantify over the levels below $\omega$.) $\endgroup$ Commented Jan 28, 2021 at 1:03
  • $\begingroup$ $\mathcal{U}_0$ is the "set of sets", in set-theoretic parlance. You know from naive set theory that this is not a good idea, so it could not be a "regular" set. $\endgroup$
    – xuq01
    Commented Aug 4, 2021 at 18:45

1 Answer 1

16
$\begingroup$

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.

$\endgroup$
1
  • 8
    $\begingroup$ If you want to see more elaborate universe hierarchies, you can look at work by Anton Setzer. He has material working up to universes that correspond to $Π_3$ reflecting ordinals. Also in Agda every numbered universe is Mahlo, which makes it possible to define ordinal-indexed hierarchies within each one. See e.g. here. $\endgroup$
    – Dan Doel
    Commented Jan 27, 2021 at 17:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .