References on implementing universe levels over MLTT?

Question

I've followed the tutorial on Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we implement a small dependently typed kernel with the axiom Univ : Univ. The "Projects" section of the tutorial provides a project on replacing this with a universe hieararchy:

7.Replace U with an infinite number of universes and a cumulativity relation. To do this, type equality checks should be replaced by a subsumption check, where each type constructor has variance rules similar to other systems with subtyping.

I've looked around a little, and it seems like both Agda and Lean implement a universe hierarchy using levels, which have the following operations:

lzero : Level
lsuc  : (n : Level) → Level
_⊔_   : (n m : Level) → Level

1. Who came up with this encoding of universes based on levels originally? Why not simply reuse the natural numbers for universe levels? There must be some reason to introduce a new Level type, instead of reusing the already present Nat?
2. How does one type-check and perform normalization-by-evaluation on universe levels?
3. What are the subtleties one should be aware of when implementing universes?
4. How should I test that my universe hierarchy implementation is correct? Are there short, well-known theorems that depend on a universe hierarchy, which I should try to encode?

I am hesitant to try my hand at naively implementing universes based on my intuition, because all the references I have read (ATAPL, MiniTT, and the above tutorial) all stop short of explaining universe levels. I get the feeling that there is non-triviality which I am unable to see, and thus would like to know how to (a) implement, and (b) test universes, on top of the kernel I now have

Answer 1

IMHO universe hierarchy is particularly complicated to implement while the benefit is very small. It complicates programming in the language and the implementation of the language. The only benefit is to ensure the logical consistency. I guess that's why everybody is not writing about it.

Here are some answers to your questions. I don't know much type theory -- I can't answer everything, sorry.

Why not simply reuse the natural numbers for universe levels?

Nat has an eliminator. You shouldn't be able to pattern match on a level. In fact, introducing Level as a type (not to mention an inductive type) already causes problem. Imagine the following function:

Ty : (ell : Level) -> Set (lsuc ell)
Ty l = Set l

What is the universe level of the type of Ty? Also, what's the universe level of the type of Level? If we don't have a type for levels (but instead built it into the syntax, to eliminate these cases) we could avoid these problems (but then you become less flexible ofc).

How does one type-check and perform normalization-by-evaluation on universe levels?

I guess just like Nat. The relevant operations are strict subset of Nat.

What are the subtleties one should be aware of when implementing universes?

0. Level is actually not a type. I personally don't like Agda's approach (but prefer Lean's, Arend's approach, where Level is not a type).
1. You need to compare levels for equality and less than relation. So, your compiler should know max(x, y) >= x, max(x, y, z) >= max(x, y), etc.
2. There are many styles of universe hierarchy. You can peek cumulativity, impredicativity (be careful, it may lead to inconsistency), typical ambiguity, etc.
3. You may want to implement a solver for level equations (if you have implicit inference mechanism), but that's very complicated.

How should I test that my universe hierarchy implementation is correct?

Try to refute the construction of the Girard paradox. It's everywhere on the internet. Also, there is another example which I believe that it won't work with universe levels.

I'm also implementing universe polymorphism on a little programming language, but the code is kinda messy.