8
$\begingroup$

It seems that universe levels are just a type generated by a zero constant and a successor constructor (like in Agda), so why don't we adapt natural numbers as universe levels?

In Lean, it is also similar: one can find the maximum of two levels, add a level variable with a constant (which is just a sugared version of applying successors), and constants.

$\endgroup$
5
  • $\begingroup$ I actually wonder why we can't index universes with natural numbers rather than having a different type for universe levels... $\endgroup$
    – Couchy
    Feb 20, 2022 at 21:07
  • $\begingroup$ @Couchy my conjecture is that if you can unlift the level of something (which is possible with naturals) you might be able to construct the Girard's paradox $\endgroup$
    – ice1000
    Feb 20, 2022 at 21:15
  • $\begingroup$ What do you mean by unlifting a level? $\endgroup$
    – Couchy
    Feb 20, 2022 at 21:22
  • $\begingroup$ @Couchy reduce the level of something. Thought about this for a while and I feel like I was probably making no sense. Please don't take it seriously :-) $\endgroup$
    – ice1000
    Feb 20, 2022 at 21:36
  • $\begingroup$ I was under the impression you needed ordinals/limits for useful universes? $\endgroup$ May 2, 2022 at 0:13

4 Answers 4

8
$\begingroup$

One of the things that make universe levels “just work”, to some extent, is that they satisfy the idempotent commutative monoid laws judgementally. This means that any elimination form of a universe level would also have to satisfy those laws judgementally. However, this would be basically unusable because there are no other idempotent commutative monoids in standard type theories for it to eliminate into (this contrasts to judgemental monoids and categories, which exist thanks to simple functions equipped with β- and η-laws). In particular, I don't see how such a type could be proven isomorphic to the ordinary zero-suc-based natural numbers, and as such it wouldn't make sense to call them the “natural numbers”.

$\endgroup$
1
  • 3
    $\begingroup$ Also note @ice1000 answer: there is no eliminator from levels to types. That is another important difference. $\endgroup$ Feb 21, 2022 at 7:53
10
$\begingroup$

Modularity.

Clearly, universe levels must form a semi-lattice with a successor. But there is no need to force it to be the set of natural numbers. Doing so would actually result in spurious constraints between unrelated universes, artificially constrained to collapse to some linearly ordered value. By taking a system of free relations, unrelated constraints cannot interfere with one another.

This is as if definitions were forced numbered instead of being given user names. Clearly, it does not endanger the formal expressivity, but it would make the system virtually unusable. (Remember the good old days of BASIC line numbering?)

$\endgroup$
1
  • 3
    $\begingroup$ I certainly agree that demanding that universe levels fit exactly the natural numbers is a bit much. We need to know what < means to test inhabitation and <= for cumulativity. And we also need to know that that's all we need to know, in order to transport constructions homomorphically between systems of universe levels. Modularity is absolutely the thing to care about! $\endgroup$
    – pigworker
    Feb 22, 2022 at 19:14
5
$\begingroup$

The biggest syntactic difference in the given two languages is that universe levels do not have an eliminator as natural numbers do. For instance, you can pattern match over a natural number, and you have equality decider function on natural numbers (say, we can define decEq : (a b : Nat) -> (a = b) \/ (a = b -> ⊥)), while these are all absent from universe levels.

This is also why Level in Agda and levels in Lean are not first-class types (they're built-in types instead). For instance, in Agda Level does not live in a regular universe.

$\endgroup$
1
  • 3
    $\begingroup$ I am confused. You asked a question and then gave the most significant answer. Is this part of "let us seed the site with good stuff"? $\endgroup$ Feb 21, 2022 at 7:52
2
$\begingroup$

At some point in history, Agda's universe levels were just an inductive type like the naturals, but with different accompanying BUILTIN declarations so that they could have extra judgmental equalities (mentioned in other answers). So, you could do 'weirder' things than you can do now, like define families that depended on the level, rather than being parametric in the level.

I suspect this doesn't cause any foundational problems. Set theorists don't have any issues indexing their universes by ordinals whose fine structure is observable. Also, I don't think it's impossible to have judgmental associativity/commutativity/idempotence of on the naturals, as Agda already has some support for adding additional judgmental equalities like that, and I think they're hoping to extend it further.

However, at the time, it made people uneasy to be able to do the 'weird' stuff mentioned above, it wasn't the intended purpose of the first-class universe levels, and the judgmental equality stuff was not really conceived of. So it definitely made sense at the time to make it a bit less like the natural numbers. And it still probably makes sense, for some of these, and other mentioned reasons.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.