I still can't grasp universes

Stream: new members

[Huỳnh Trần Khanh]

I couldn't understand universes even though I've read https://leanprover.github.io/reference/expressions.html several times, can anyone explain this to me in simple terms, or at least give me some context as to why this is needed

[Horatiu Cheval]

In Lean everything is a term and has type. So things like int, bool ... have to have a type, for which we might introduce Type, the type of types, so nat : Type, bool : Type, ... . And then you ask well, Type too has to have a type, so what's the type of Type? One might think to set the type of Type to be Type itself, since it is in the end a type, and Type is the type of all types. The problem with having Type : Type is that it is known to be inconsistent. See for example, Girard's paradox, for which also have a formalization in Lean: https://github.com/leanprover-community/mathlib/blob/master/counterexamples/girard.lean

So instead of this, for the type of Type, we introduce a larger type, and we call it Type 1. And then this continues forever, for the type Type 1 we introduce Type 2 and so on. So that we have Type : Type 1 : Type 2 : ...

[Horatiu Cheval]

That's my intuition at least

[Horatiu Cheval]

And of course, as you might know, in Lean we also have Prop which goes below the first Type 0. So the hierarchy is actually Sort 0 : Sort 1 : Sort 2 ..., where Prop is a notation for Sort 0 and Type u for Sort u + 1

[Huỳnh Trần Khanh]

Then what is the difference between Sort and Type? (answered sorry) And why are there weird functions (+, max, imax) on universe levels? I can't understand the purpose of them (except + 1, I fail to see why adding an arbitrary number is needed)

[Huỳnh Trần Khanh]

Especially imax. The definition is extremely weird.

[Max]

If you have a tuple of two elements in universe level i and j, then the tuple itself is of a type which is in the most-high-up (= max i j) universe. That's a fellow newbie's intuition so take it with a grain of salt :)

[Horatiu Cheval]

imax is for Props . One of the main differences between Prop and Type* is how they behave with respective too universes in Pi-types. Any quantification into Prop stays in Prop.

universes u v
variables (β : Type u → Type v) (p : Type u → Prop)
#check ∀ α : Type u, β α
-- Π (α : Type u), β α : Type (max (u+1) v)
#check ∀ α : Type u, p α
-- ∀ (α : Type u), p α : Prop

[Horatiu Cheval]

imax is so that you can include both cases above in a single formula

[Horatiu Cheval]

So the general rule, take from the Lean reference manual, can be expressed, for \a : Sort u and \b : Sort v, as (Π x : α, β) : Sort (imax u v), with the help of imax, otherwise you would need to write two cases, for Sort 0 and Sort u, u > 0

[Huỳnh Trần Khanh]

Wait.

The last one denotes the universe level 0 if v is 0, and max u v otherwise.

Why doesn't that sentence read

The last one denotes the universe level 0 if either u or v is 0, and max u v otherwise.

[Huỳnh Trần Khanh]

Yes, your explanation helps, but your explanation generates even more questions :joy:

[Horatiu Cheval]

Because it doesn't work that way in the other direction.

universes u
variables α : Type u
variables p : Prop
#check p → α
-- p → α : Sort (u + 1) = Sort (max 0 (u + 1))
--                = Sort (imax 0 (u + 1)) ≠ Sort (your_alternative_imax 0 (u + 1)) = Sort 0
#check α → p
-- α → p : Sort 0 = Sort (imax ((u + 1) 0) ≠ Sort (max (u + 1) 0) = u + 1

[Horatiu Cheval]

Actually only the first #check is relevant to the last question, the second one is just for exemplification

[Huỳnh Trần Khanh]

OK so this is getting even more confusing... Why can I do this?

universe u
variables α : Type u

def x := α
def y := x α
def z := y α

[Huỳnh Trần Khanh]

This can go on forever...

[Huỳnh Trần Khanh]

I know this is not "proper mathematics" but this is proper type theory. I need help :joy:

[Huỳnh Trần Khanh]

And yes I did that because I made a def for fun and I checked its type and I saw Type u_1 \im Type u_1 and I was like oh this is a function and I used it...

[Huỳnh Trần Khanh]

Foundations is so confusing. I swear if foundations was a subject at school I would drop out to avoid severe brain damage.

[Horatiu Cheval]

Here it's not a matter of foundations at all actually, just of Lean syntax. Declaring a variable basically tells Lean "consider this as an argument for all future definition, wherever needed".
So your x for example, is the same as if you wrote

universes u
def x (α : Type u) : Type u := α

So, with x you just defined the identity function at Type u, that takes an argument and just returns. It makes no different that the argument is of type Type u. It could have been int and everything would have worked the same.

[Kyle Miller]

Huỳnh Trần Khanh said:

if foundations was a subject at school I would drop out to avoid severe brain damage.

This might be foundations-induced brain damage, but I found it helpful to think about universe variables as a way to give an (infinite) family of definitions/theorems simultaneously, without having to repeat yourself for all possible combinations of universes you might want to use in practice. The universe variable arithmetic expressions are there to help you define useful families, and Lean guarantees that any substitution of universe levels for the universe variables gives well-typed terms (given the above example, you can do x.{37} to get the instantiation of that definition with the type Type 37 -> Type 37, substituting 37 for u.)

Something this point of view helped me understand is why you can't have types that quantify over universe levels, except at the point of a definition/theorem.