0
$\begingroup$

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.

$\endgroup$
9
  • 1
    $\begingroup$ When you say that "$T : \mathbb{N} \to \mathcal{U}$ ... is a valid definition", what do you mean by that? (a) that $T$ is a type family inside type theory, or (b) $T$ is a function at the meta-level, i.e., outside of type theory. Which is it? $\endgroup$ – Andrej Bauer Oct 11 '19 at 18:31
  • $\begingroup$ Since the universe indexing is at the meta-level I don't see how $T$ is problematic: it doesn't make sense internally, but how is that relevant? (Of course I can't speak to whether $\omega$-many universes is actually enough for HoTT, since I essentially know nothing about it, but the particular point you raise here doesn't seem to be an issue.) $\endgroup$ – Noah Schweber Oct 11 '19 at 18:32
  • 1
    $\begingroup$ @NoahSchweber: it's enough. And for many purposes one can be a bit more subtle and get away with two universes for many purposes (akin to sets and classes). $\endgroup$ – Andrej Bauer Oct 11 '19 at 18:42
  • $\begingroup$ @AndrejBauer Ah, thanks. (In retrospect I think I did know that the consistency strength was $\le$ two universes, although that's not quite the same thing a priori.) $\endgroup$ – Noah Schweber Oct 11 '19 at 18:43
  • 1
    $\begingroup$ @AndrejBauer I pointed out on your blog that conflating universe levels with the internal natural numbers does strictly increase the consistency level of Classical HoTT. (For plain HoTT, the question is more subtle and I never investigated it.) $\endgroup$ – François G. Dorais Oct 17 '19 at 2:10
1
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.