Cumulativity of the universe hierarchy

[FernandoChu]

The book postulates the following rules

However, I think these don't imply that if $A : \mathcal{U}_i$, and $B : \mathcal{U}_j$ there is a $k$ such that $A,B : \mathcal{U}_k$; since $\mathcal{U}$-CUMUL only works for successors. Though we need such a $k$ for $\Pi$ form, for example. Such a $k$ can be proved to exist outside the theory, but we need it inside it too for "uniformly" introducing functions (and other types).

I think a least upper bound operator ($\sqcup$) on indices would be sufficient, and that $i \sqcup (i+1) = i+1$, etc. Not sure if there's an easier way out.

[mikeshulman]

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.

[FernandoChu]

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.

[mikeshulman]

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

[FernandoChu]

Thanks!