Can you explain the .{u} notation?

Stream: new members

[Mr Proof]

I understand that rfl.{u} {Sort u} means you don't have to specify the universe. But I can't really find an explanation of the funny notation "dot brackets u". Also u is a natural number but actually isn't because we haven't defined natural numbers.

Can anyone explain this strange notation in terms of why the notation is written like this?

By understanding (correct me if I'm wrong) but it means there is one RFL for each type level

rfl0 : (a:Type 0)->(x:a)->(x=x)
rfl1 : (a:Type 1)->(x:a)->(x=x)
rfl2: (a:Type 2)->(x:a)->(x=x)

But if that is the case how would I reference, say, rfl2. Is there some way to do this in Lean?

As an aside. Numbering the Type universes with natural numbers seems a bit chicken-and-egg. :hatching:I hope there's a better way in Lean 5

[Yakov Pechersky]

Universe levels aren't natural numbers

[Yakov Pechersky]

You can say rfl.{3} for rfl over Type 2. Because Type 2 is Sort 3.

[Mr Proof]

I don't know what you mean when you say 3 is not a number :sob:

[Yakov Pechersky]

Universe levels have 0, succ, max, and imax. They do not have recursors. They have different unification rules than naturals. 3 is a literal that stands for succ succ succ 0. "3 is not a number", correct, it is notation for something else.

[Jason Rute]

First, there are the sorts you can name: Sort 0 (aka Prop), Sort (succ 0) (aka Sort 1, Type 0), Sort (succ (succ 0)) (aka Sort 2, Type 1), etc. This 0 and succ are totally different from the natural numbers in Lean. They use the same notation, but then again 0 is used for lots of things in Lean like the unit of an additive group. But unlike 0 (used in any other context in Lean), universe levels are not elements of a type. There is no type of universe levels. You can't put a universe level where a type (or element of a type) would go, and you can't put a type (or element of a type) where a universe level would go. Lean is just nice to you and lets you write Type 2 instead of Type (succ (succ zero)), and Type (u + 3) instead of Type (succ (succ (succ u))), but internally it is stored more like the later.

Now, to avoid having a separate refl for each universe level, there is universe polymorphism where we can use Type u or Type (max u v), etc to specify a universe. You normally don't need to worry about what universe level you are using since Lean figures it out for you, but you can specify it with foo.{3} or foo.{u} or if there are multiple universe levels used in a theorem, foo.{1, 2}.

You also can't really prove formally in Lean anything about universe levels (except for proving a theorem with a universe level in it). Now, it is true that the only explicit universe levels you can construct with the four constructors are 0, 1, 2, 3, ... But there is really nothing saying that the universe levels are isomorphic to the natural numbers or that there isn't a universe level in between say 2 and 3. We just know that for a universe level u there is some higher universe level succ u. For u and v there is some upper bound universe level max u v satisfying say max (succ u) u is the same as succ u and max (max u v) w is the same as max u (max v w). (imax u v is the maximum of u and v if v is not 0, and 0 otherwise). These are just rules built into Lean which Lean uses to check if two universes are compatible.

[Jason Rute]

An interesting fact is that since we don't know if there are "in-between" universes, we can't say much about the relative cardinalities of the universes Type u and Type (u + 1). It is consistent that Type (u + 1) is just a bit larger than Type u. (I think formally that is saying the cardinality of Type (u + 1) is the next largest inaccessible cardinal.) It is also consistent that Type (u + 1) is much larger (there are many, even uncountably many, inaccessible cardinals in between). (https://proofassistants.stackexchange.com/questions/1605/cardinality-of-type-in-a-given-universe)

[Yaël Dillies]

docs#Lean.Level does exist, though

[Mark Fischer]

Mr Proof said:

I don't know what you mean when you say 3 is not a number :sob:

This is a bit of a tangent...

I'm not completely sure, but I believe the type-theory perspective is that the only way to have an element of ℕ is for something to be given to you as such. You can't have a thing and wonder "Is this thing a ℕ"? You can have a subtype like {x : ℕ // Even x} after which if you have an ℕ, you can ask something akin to if this is also a {x : ℕ // Even x}.

Thinking of programming languages like C, without the types everything looks just like a binary number. For the non-ML based programming languages, types were invented to deal with the "everything looks the same" problem - as it's dangerous to mistake a pointer for a struct or some such..

I think that's at least one sense in which the universes aren't numbers.

Of course that's not very convincing because if the definition of ℕ where somehow tied up in the Universe Levels, you may well still wonder if there's some logical fallacy at play - maybe.

[Riccardo Brasca]

I usually think as the 3 in Sort 3 as a completely separate object as 3 : Nat. Indeed, if you have i : Nat, you cannot write Sort i. The hierarchy of universes is present before giving the definition of natural numbers.