Cumulativity of the universe hierarchy about book HOT 4 CLOSED

I think your second paragraph is right. There are no "universe variables" in the formal system of the book.

from book.

I'm not sure what you mean by "uniformly" introducing functions. There are certainly better ways to set up a theory of universes if you're going to implement it in a proof assistant, but I believe that in the Book the subscripts on universes are literally metatheoretic natural numbers, so they do have least upper bounds. The treatment of universes in the definition of things like function-types is, well, ambiguous, because it uses typical ambiguity, but I think the intent was that all types involved live in the same universe.

from book.

Thanks for the comment. To give a concrete example: if we have $A : \mathcal{U}_i$ and $B: \mathcal{U}j$, we can't use the given rules to form $\Pi{x:A}B(x)$, since Pi-Form requires A and B to be in the same universe. And there is no way to show that $A$ and $B$ can be lifted up to the same universe (i.e. write a derivation tree), at least not for "variable indices".

Or maybe what I'm misunderstanding is the use of "variable indices", and a theorem involving them as in the book was meant to be a theorem schema involving every (metatheoretical) natural number.

That's what I meant by "uniformly" defining functions, doing so for every pair of variable indices, not just a pair of concrete ones. To be clear, I understand that metatheoretically we can show that we can do so for every concrete pair (and therefore all pairs), but, at least to me, one of the advantages of DTT was being able to internalize these sort of things through dependent protducts.

from book.

Thanks!

from book.