Universe levels in Lean 4

One technical aspect of the Type theory used in the implementation of Lean (and more generally a side -effect for dependently typed languages) is the need for multiple universe levels.

The need for this separation of universe levels is vaguely reminiscent of Russell's paradox, and the need to distinguish between sets and collections in ZFC set theory. The implementation in Lean is that there is some base type Sort 0 (or Prop as a synonym). The type of Sort 0 is Sort 1, denoted as Type or Type 0. Similarly Type 0 : Type 1 and so on for Type n : Type (n + 1).

It is sufficient to understand Lean universes as the inductive data type

  inductive Univ where
    | Zero                         -- Prop
    | Succ  : Univ → Univ          -- Sort 1 = Succ(Zero), ...
    | Max   : Univ → Univ → Univ  
    | IMax  : Univ → Univ → Univ 
    | Param : Name → Nat → Univ    -- Universe "variables" that are (implicitly) bound in elaboration

Here the difference between Max u v and IMax u v differs only when v = 0 (in which case IMax u v is always zero).