universe polymorphism

Stream: general

[Fernando Chu]

Hello, I'm new to lean but I have some experience on agda. Since there's universe polymorphism, is there a Type ω such that all other types Type n are in there? (for n natural)

[Anatole Dedecker]

No we only have one tower of universes. However you can declare universe variables or use Type* to get polymorphism

[Anatole Dedecker]

But it really is « copy paste polymorphism » in the sense that the « same definition » at two different universe levels are really two different definitions from the point of view of the type theory

[Anatole Dedecker]

Also in Lean each term has a unique type so we couldn’t really have such a definition

[Fernando Chu]

Thanks! I'm new to this « copy paste polymorphism » . From the book, I have

universe u
def F (α : Type u) : Type u := Prod α α

Not that it's useful, but is it possible to get define make F particular to a universe? def G' (α : Type 1) : Type 1 := F α works because lean correctly unifies, but I'm wondering if there's a more explicit way to point out the universe level

[Kevin Buzzard]

You can use F.{u}

[Fernando Chu]

I see, thank you, I didn't know that worked for "application" too. Just to be super sure, terms like Type 10 are simple terms, right? I.e. there is no function application in it, the space is just part of the syntax for the term.

[Kyle Miller]

Yes, Type 10 is not function application. It's a "sort expression," where 10 is a level expression (not a nat).

[Fernando Chu]

great, thank you all!

[Kyle Miller]

By the way, to explicitly quantify the universes in a definition the syntax is

def {u} F (α : Type u) : Type u := Prod α α

[Kyle Miller]

The universes declaration causes the universe level variables that you actually use in a definition to automatically be added there.

[Fernando Chu]

ohh that's interesting, that notation only works for level expressions, right? They seem to be treated in a very special way with their own syntax

[Kyle Miller]

https://leanprover.github.io/reference/expressions.html#universes (that's not a complete specification; you can write things like Type (max u v w))

[Fernando Chu]

thank you, I hadn't found that reference, was checking https://leanprover.github.io/lean4/doc/whatIsLean.html instead. I suppose that reference is for Lean3 but probably most applies for Lean4

[Kevin Buzzard]

This is a lean 3 stream -- questions about lean 4 go in the lean4 stream but as far as I know nothing changed here