<p>IMHO universe hierarchy is particularly complicated to implement while the benefit is <em>very small</em>. It complicates programming in the language <em>and</em> 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.</p>
<p>Here are some answers to your questions. I don't know much type theory -- I can't answer everything, sorry.</p>
<blockquote>
<p>Why not simply reuse the natural numbers for universe levels?</p>
</blockquote>
<p><code>Nat</code> has an eliminator. You shouldn't be able to pattern match on a level. In fact, introducing <code>Level</code> as a type (not to mention an inductive type) already causes problem. Imagine the following function:</p>
<pre><code>Ty : (ell : Level) -&gt; Set (lsuc ell)
Ty l = Set l
</code></pre>
<p>What is the universe level of the type of <code>Ty</code>? Also, what's the universe level of the type of <code>Level</code>? 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).</p>
<blockquote>
<p>How does one type-check and perform normalization-by-evaluation on universe levels?</p>
</blockquote>
<p>I guess just like <code>Nat</code>. The relevant operations are strict subset of <code>Nat</code>.</p>
<blockquote>
<p>What are the subtleties one should be aware of when implementing universes?</p>
</blockquote>
<ol start="0">
<li><code>Level</code> is actually not a type. I personally don't like Agda's approach (but prefer Lean's, Arend's approach, where <code>Level</code> is not a type).</li>
<li>You need to <em>compare</em> levels for equality and <em>less than</em> relation. So, your compiler should know <code>max(x, y) &gt;= x</code>, <code>max(x, y, z) &gt;= max(x, y)</code>, etc.</li>
<li>There are many <em>styles</em> of universe hierarchy. You can peek <a href="https://stackoverflow.com/q/33686403/7083401">cumulativity</a>, impredicativity (be careful, it may lead to inconsistency), typical ambiguity, etc.</li>
<li>You may want to implement a <em>solver</em> for level equations (if you have implicit inference mechanism), but that's very complicated.</li>
</ol>
<blockquote>
<p>How should I test that my universe hierarchy implementation is correct?</p>
</blockquote>
<p>Try to refute the construction of the Girard paradox. It's everywhere on the internet. Also, there is <a href="https://github.com/AndrasKovacs/elaboration-zoo/blob/9599e7ecca77262b6d11a363647e833aaa5cb4c7/04-implicit-args/example.txt#L110-L111" rel="nofollow noreferrer">another example</a> which I believe that it won't work with universe levels.</p>
<p>I'm also implementing universe polymorphism on <a href="https://github.com/aya-prover/aya-dev" rel="nofollow noreferrer">a little programming language</a>, but the code is kinda messy.</p>

CC BY-SA 4.0
2021-05-19T20:13:39.230Z
One benefit of a consistent universe hierarchy I want to mention is that you can erase proofs.
Labbekak
CC BY-SA 4.0
2021-05-20T01:11:53.977Z
I think you can do that even without universe hierarchy, no? Idris2 now has type-in-type but it has a lot of erasure
ice1000
CC BY-SA 4.0
2021-05-20T06:49:35.293Z
No if you erase proofs with type-in-type your language is no longer type-safe, because you can inhabit any proof `A = B` with an infinite loop and cast any (unrelated) `A` to a `B`. You have to evaluate the proof in order to be type-safe, because then the program would run forever, but at least not cast `A` to `B`. Please see https://stackoverflow.com/questions/61930740/in-a-dependently-typed-programming-language-is-type-in-type-practical-for-progra
Labbekak
CC BY-SA 4.0
2021-05-19T07:34:30.917Z
2021-05-19T07:34:30.917Z
ice1000
<p>I've followed the tutorial on <a href="http://davidchristiansen.dk/tutorials/nbe/" rel="nofollow noreferrer">Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen</a>, where we implement a small dependently typed kernel with the axiom <code>Univ : Univ</code>. The &quot;Projects&quot; section of the tutorial provides a project on replacing this with a universe hieararchy:</p>
<blockquote>
<p>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.</p>
</blockquote>
<p>I've looked around a little, and it seems like both Agda and Lean implement a universe hierarchy using <em>levels</em>, which have <a href="https://agda.readthedocs.io/en/latest/language/universe-levels.html" rel="nofollow noreferrer">the following operations</a>:</p>
<pre><code>lzero : Level
lsuc  : (n : Level) → Level
_⊔_   : (n m : Level) → Level
</code></pre>
<ol>
<li>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 <em>reason</em> to introduce a new <code>Level</code> type, instead of reusing the already present <code>Nat</code>?</li>
<li>How does one type-check and perform normalization-by-evaluation on universe levels?</li>
<li>What are the subtleties one should be aware of when implementing universes?</li>
<li>How should I <em>test</em> 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?</li>
</ol>
<p>I am hesitant to try my hand at naively implementing universes based on my intuition, because all the references I have read (<a href="https://www.cis.upenn.edu/%7Ebcpierce/attapl/" rel="nofollow noreferrer">ATAPL</a>, <a href="http://www.cse.chalmers.se/%7Ebengt/papers/GKminiTT.pdf" rel="nofollow noreferrer">MiniTT</a>, 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 <a href="https://github.com/bollu/minitt/blob/master/Christiansen7.hs" rel="nofollow noreferrer">the kernel I now have</a></p>

CC BY-SA 4.0
2021-05-19T07:16:18.213Z
[Coq reference](https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf)
ice1000
CC BY-SA 4.0
2021-05-19T07:24:08.140Z
@ice1000 Thanks for the link! The abstract says "However, the structure and hierarchy of universes is more complex than bare polymorphic type variables.".  In what sense is it more complex? This is in some sense the source of my confusion; I don't see _why_ universes are subtle.
Siddharth Bhat
CC BY-SA 4.0
2021-05-19T07:35:08.927Z
I wrote an answer (:
ice1000
<dependent-type><normalization>
References on implementing universe levels over MLTT?
Siddharth Bhat
# References on implementing universe levels over MLTT?

(Asked by: username_0 on 2021-05-19)

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 Level type, instead of reusing the already present Nat?
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

**Tags:** dependent-type, normalization
> **Comments:**
> **username_1**: [Coq reference](https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf)  
> **username_0**: @ice1000 Thanks for the link! The abstract says "However, the structure and hierarchy of universes is more complex than bare polymorphic type variables.".  In what sense is it more complex? This is in some sense the source of my confusion; I don't see _why_ universes are subtle.  
> **username_1**: I wrote an answer (:  

---

## 1 answers

### Answer by username_1 on 2021-05-19. Score: 2 | Accepted answer

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?


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) >= x, max(x, y, z) >= 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.

> **Comments:**
> **username_2**: One benefit of a consistent universe hierarchy I want to mention is that you can erase proofs.  
> **username_1**: I think you can do that even without universe hierarchy, no? Idris2 now has type-in-type but it has a lot of erasure  
> **username_2**: No if you erase proofs with type-in-type your language is no longer type-safe, because you can inhabit any proof `A = B` with an infinite loop and cast any (unrelated) `A` to a `B`. You have to evaluate the proof in order to be type-safe, because then the program would run forever, but at least not cast `A` to `B`. Please see https://stackoverflow.com/questions/61930740/in-a-dependently-typed-programming-language-is-type-in-type-practical-for-progra  

---

