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
- 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
Leveltype, instead of reusing the already present
- How does one type-check and perform normalization-by-evaluation on universe levels?
- What are the subtleties one should be aware of when implementing universes?
- 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