Sort as a function

Stream: new members

[Caroline]

I notice that we can't make λ n : Nat => Sort n (which would be of type ∀ n : Nat. Sort (n + 1) universe levels are a special kind of sub-language rather than being able to be arbitrary naturals, including parameters.
Why does that limitation exist? What would go wrong if Sort n (with n a variable passed in from a lambda) was allowed?

[Notification Bot]

Eric Rodriguez has marked this topic as resolved.

[Notification Bot]

Eric Rodriguez has marked this topic as unresolved.

[Eric Rodriguez]

what universe would that live in?

[Caroline]

oh, i see, indeed, one wouldn't be able to give the type of ∀ n : Nat. Sort (n + 1). There isn't a k such that (∀ n : Nat. Sort (n + 1)) : Sort k. thanks!

[Eric Wieser]

Note that universe levels live in docs#Lean.Level (at least, in the meta-theory), and are not Nats (which are Exprs in the meta-theory)

[Arthur Adjedj]

Agda supports first-class levels, and types like ∀ n : Nat. Set n live in an "inaccessible" sort Setω

[Niels Voss]

In Lean, Sort levels are not really natural numbers (or at least they aren't Nat), as they don't really exists within the theory at all. If you aren't careful, allowing first-class levels can lead to proofs of False. Obviously since Agda supports first-class levels it is possible to make them work but Lean doesn't support them.
Out of curiosity, is there an actual problem you have that would be solved easier if such a function was constructable?