How are type universes handled in Lean 4 compared to MLTT?

Stream: lean4

[Junseong O]

In Martin-Löf type theory, if we have A : Type u, then we also have A : Type (u+1) (by cumulativity).
However, in Lean 4, for example, Nat : Type (i.e. Nat : Type 0) does not seem to coerce naturally to Type 1, Type 2, or higher universes.
Could someone explain the formal aspects of Lean 4’s type universe system and how it differs from the usual presentation in classical type theory?

[Lawrence Wu (llllvvuu)]

in practice you can do docs#ULift

[Junseong O]

Oh I see!! Thank you so much :+1:

[Junseong O]

But isn’t this just introducing a new type inductively, rather than a judgment that the same type also belongs to a higher universe?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yeah, Lean does not have cumulative universes. We can use ULift, but that is not the same as having cumulativity. Consider A : Type 0 and B : A -> Type 1 so that (a : A) -> B a : Type 1. Then ULift.{2} A : Type 2 and ULift.{2} B : Type 2 and ULift.{2} ((a : A) -> B a) : Type 2. Now we can ask, is ULift.{2} ((a : A) -> B a) = (a : ULift.{2} A) -> ULift.{2} (B a.down), i.e., are the two types provably equal? The answer is no. In a type theory with cumulativity there is no question to be asked because ULifts are silent/not recorded in the terms.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Note also that inductive and Pi type formation in Lean is implicitly cumulative. In the example above we get (a : A) -> B a : Type 1 even though A : Type 0. This is basically what lets Lean get away without having general cumulativity, and is the reason why we don't have to use ULift all the time. It would be unusable without this feature.

[Junseong O]

I see, thank you for the explanation. From which book (or resource) can I learn all the rules of Lean 4 as a formal language?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

#leantt is the most precise afaik.

[Junseong O]

Thank you!