References on implementing universe levels over MLTT?
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) -&gt; 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?


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).
You need to compare levels for equality and less than relation. So, your compiler should know max(x, y) &gt;= x, max(x, y, z) &gt;= max(x, y), etc.
There are many styles of universe hierarchy. You can peek cumulativity, impredicativity (be careful, it may lead to inconsistency), typical ambiguity, etc.
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.