In Lean4, types are organized into a hierarchy of universes (also referred to as sorts). Each universe is associated with a level, which is a natural number. The \(\texttt {Sort}\) operator constructs a universe from a given level. To avoid things like Girard's paradox, Lean4 employs a stratified type system where each universe can only contain types from lower universes, we have the following hierarchy (1):

\(\texttt {Sort}\) has two main aliases used in Lean4: \(\texttt {Prop}\) and \(\texttt {Type u}\). Here, \(\texttt {Prop}\) (which is equivalent to \(\texttt {Sort 0}\)) is the universe of logical propositions, while \(\texttt {Type u}\) (which is equivalent to \(\texttt {Sort (u + 1)}\)) represents a universe of types at level \(u\). So we can say:

In general we can express the hierarchy for any universe level \(u\) as follows:

Except propositions, a type in a universe at level \(u\) cannot quantify over types from strictly larger universes unless the whole result is lifted to a larger universe. In the case of types we have:

To demonstrate some valid instance of this inference rule lets consider the following lean examples:

      example (α : Type 1) (β : Type 2) : Type 2 := α → β
      example (α : Type 2) (β : Type 1) : Type 2 := α → β
    

Both of the above examples are valid because the resulting type is lifted to the maximum universe level of the input types. In general, we say that the behavior of the \(\texttt {Type}\) universes is called predicative meaning that objects may not be defined in terms of quantifiers ranging over that same object.

We can observe that a function type's universe is determined by the universes of its argument and return types. However, in the case of propositions we have a different behavior:

Predicates, which are functions that return propositions, may have argument types in any universe, but the function itself remains in the \(\texttt {Prop}\) universe. This behavior is called impredicative meaning that objects may be defined in terms of quantifiers ranging over that same object. The rule \(\textsc {ArrowProp}\) means that expressions such \(\forall a : \texttt {Prop}, a \to a\), which quantify over all propositions (including themselves), yield a proposition, that is:

We can see some more examples of quantifying both over propositions and types as follows:

      /-- Quantifying over propositions yields a proposition -/
      example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2

      /-- Proposition quantifying over all type stays in Prop -/
      example : Prop := ∀ (α : Type), ∀ (x : α), x = x
      example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x
    

We can combine these two rules to get a more general rule for function types that return types in any universe:

Here the function type's universe is determined by the (impredicative max) imax of the universes of its argument and return types, where \(\texttt {imax}\) is defined as follows:

We can describe the level grammar via the following inductive type:

      inductive Level
      | zero : Level
      | succ : Level → Level
      | max  : Level → Level → Level
      | imax : Level → Level → Level
    

We can define functions and types that are universe polymorphic by introducing universe levels either explicitly or implicitly. An explicit universe level is specified directly in the definition, while an implicit universe level is inferred by Lean4. For example:

        /-- Explicit universe level -/
        def map.{u v} {α : Type u} {β : Type v} 
            (f : α → β) : List α → List β :=
          | []       ⇒ []
          | x :: xs  => f x :: map f xs
      

Here the map is declared with explicit universe levels \(u\) and \(v\) and instantiates the polymorphic \(\texttt {List}\). We can also define the same function with implicit universe levels as follows:

        universe u v
        def map {α : Type u} {β : Type v} 
            (f : α → β) : List α → List β := ...
      

By default in Lean4 the option \(\texttt {autoImplicit}\) is set to true, meaning that our universe levels will be inferred automatically meaning that we can simply write:

        def map {α : Type u} {β : Type v} 
            (f : α → β) : List α → List β := ...
      

Importantly automatic implicit parameter inference only works if the universe is mentioned in the header preceding the assignment, i.e:

        /-- Bad: unknown universe u -/
        def L := List (Type u)
        /-- Good: universe u mentioned in header -/
        def L.{u} := List (Type u)
      

We can also go even further with implicit universes by allowing Lean4 to generate fresh universe levels for us. This is done by omitting the universe annotation and replacing it with a * suffix:

      /-- Fresh implicit universe levels -/
      def map {α : Type*} {β : Type*} 
          (f : α → β) : List α → List β := ...
    

The \(\texttt {PLift}\) operator is used to lift propositions into the first type universe. It is defined as follows:

      structure PLift (α : Sort u) : Type u where
        /-- Wraps a proof/value to increase its type's universe lvl -/
        up ::
        /-- Extracts a wrapped proof/value from a lifted prop/type. -/
        down : α
    

Some simple examples:

      #check False       -- False : Prop
      #check PLift False -- PLift False : Type
      #check Nat         -- Nat : Type
      #check PLift Nat   -- PLift Nat : Type 1

      example : PLift Prop        := PLift.up True
      example : Prop              := (PLift.down (PLift.up False))
      example : List (PLift True) := [.up (by trivial), .up (by decide)]
    

The \(\texttt {ULift}\) operator is used to lift types to higher universes. It is defined as follows:

      structure ULift.{r, s} (α : Type s) : Type (max s r) where
        /-- Wraps a value to increase its type's universe level. -/
        up ::
        /-- Extracts a wrapped value from a universe-lifted type. -/
        down : α
    

Some simple examples:

      #check Nat               -- Nat : Type
      #check ULift Nat         -- ULift Nat : Type 1
      #check ULift (ULift Nat) -- ULift (ULift Nat) : Type 2

      example : ULift Nat        := ULift.up 42
      example : List (ULift Nat) := [.up 1, .up 2, .up 3]
    

For the case of the category definition, Lean fundamentally uses quivers to represent the homs between objects. Now before showing how lean defines them lets I think try and do it ourselves. So in this instance in an abstract sense we want the relationship \(\leq \) to represent our morphism or arrow between two objects, so in a sense the following two are equivalent:

So in the most straightforward sense what we can do is define any kind of "container" to represent our source and target objects under some label, we can define this naively as follows:

      class Graph (Obj : Type) where
        arrow (source : Obj) (target : Obj) : Type
    

Now let's try to define an instance of such a graph on a preorder relation in which our objects simply live in \(\texttt {Type 0}\):

      instance {α : Type} [Preorder α] : Graph α where
        arrow a b := a ≤ b -- arrow from a to b is the relation a ≤ b
    

Here we are declaring an instance, this instance takes

• An implicit type parameter \(\alpha \) which is the type of our objects at the universe level 0.
• A type class constraint \(\texttt {[Preorder α]}\) which ensures that the type \(\alpha \) has a preorder relation defined on it. In other words it guarantees that the relation \(\leq \) is reflexive and transitive for all elements of type \(\alpha \).

A first thought might be to just set the arrow type to be \(\texttt {Prop}\) directly, in our definition of the class \(\texttt {Graph}\) though this is rather restrictive as it means that any graph we wish to define can only ever have arrows representing propositions, what if we want to have arrows represent other types such as functions or numbers?

One way to approach this is to use the \(\texttt {PLift}\) operator to lift our preorder relation from \(\texttt {Prop}\) to \(\texttt {Type 0}\) as follows:

      instance {α : Type} [Preorder α] : Graph α where
        arrow a b := PLift (a ≤ b) -- lift relation to Type 0
    

While this does work, and often is probably a reasonable way to go about things, much of Lean's mathlib employs universe polymorphic types to define various kinds of structures. Thus parameterizing over some universe level \(u\) we define our polymorphic instance as:

      instance {α : Type u} [Preorder α] : Graph α where
        arrow a b := PLift (a ≤ b) 
    

But now we naturally run into another issue, namely that the class for our graph is now no longer universe polymorphic which leads to a universe level mismatch. The most straightforward fix here is to simply make the objects in the graph universe polymorphic as well:

      class Graph (Obj : Type u) where -- now polymorphic over u
        arrow (source : Obj) (target : Obj) : Type
    

But this leads to another question, what level should the arrows live in? We've already seen that arrows can represent various different kinds of things different from the types of objects themselves, (e.g. \(2 \leq 3\) is a proposition but clearly 2 and 3 are numbers). Now one approach is to simply leave the arrows in \(\texttt {Type 0}\) but this already is mildly annoying as it forces us to lift any arrows that don't naturally live in \(\texttt {Type 0}\). Furthermore, we've already seen that having the type stuck at Prop is also not nice, so what we can do is make the arrows' universe polymorphic as well, though over a different universe level \(v\) motivated by the aforementioned situation of different levels of arrows and objects:

      class Graph (Obj : Type u) where
        arrow (source : Obj) (target : Obj) : Sort v

      instance {α : Type u} [Preorder α] : Graph α where
        arrow a b := a ≤ b -- now lives in Sort 0 (i.e. Prop)
    

But hold up, why are we lifting in the definition of the instance for the SmallCategory? Let's take a look at all the relevant type signatures:

      -- Quiver 
      -- (V : Type u) where

      -- CategoryStruct
      -- (obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj

      -- Category 
      -- (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj 

      -- SmallCategory
      -- (obj : Type u) : Type (u + 1) extends Category.{u} obj 
    

Let's break this down step by step starting first with the relationship between CategoryStruct and Quiver, for the sake of simplicity i'll abstract away some exact names and make all universes explicit:

      variable {α : Type m} [Preorder α] (a b c : α)

      class Box.{u, v} (obj : Type u) where
        pair : obj → obj → Sort v

      class A.{u, v} (obj : Type u) 
        : Type max u (v + 1) extends (Box.{u, v + 1} obj) where
    

I think an interesting question I first had here is with the extension of \(\texttt {Box}\) in \(\texttt {A}\) why might you want to increase the universe level of the arrows by one? The main reason this is done in general is to essentially constrain the \(v\) to never be zero. The implication of this being that our extended class \(\texttt {A}\) can never have any pairs which live in \(\texttt {Prop}\).

A good follow up to this might be, why would you not want things to live in \(\texttt {Prop}\)? In the most general sense some reasons are:

• \(\texttt {Prop}\) is proof irrelevant: In Lean, propositions are considered proof irrelevant, meaning that all proofs of a given proposition are treated as equal. This can lead to loss of information when you want to be able to distinguish between different morphisms or in our simplified example pairs.
• \(\texttt {Prop}\) is not computational: Propositions in Lean are not computationally relevant, meaning that they do not have computational content. If you want to perform computations or extract algorithms from your morphisms or pairs, having them in \(\texttt {Prop}\) would prevent that.
• \(\texttt {Prop}\) has limited structure: Propositions in Lean do not have the same rich structure as types in higher universes. If you need to work with morphisms or pairs that have additional structure (like being functions, sets, etc.), you would want them to live in a higher universe.

As an example we can consider the following:

      -- @classname disables universe inference for that class
      variable (a₁ : @A.{m, v} α)
      #check (a₁.pair a b : Sort (v + 1)) -- Box.pair a b : Type v
    

We can see here that the pair now lives in \(\texttt {Sort (v + 1)}\), meaning that if we had \(v = 0\) then our pairs would now live in \(\texttt {Type 0}\). A natural byproduct of this choice - having arrows live in \(\texttt {Sort (v + 1)}\) - is that the type of the structure itself must now live in the largest universe such that it can contain both the objects and the arrows. This is why we have the type signature \(\texttt {Type max u (v + 1)}\) for \(\texttt {A}\). Equivalently we can expand this as:

      -- since Type u = Sort (u + 1) and Type (v + 1) = Sort (v + 2)
      Sort (max (u + 1) (v + 2)) 
    

If we then create similarly abstract versions for the Category class (B) and SmallCategory class (C) we have:

      class B.{u, v} (obj : Type u) 
        : Type max u (v + 1) extends A.{u, v} obj where

      class C.{u} (obj : Type u) 
        : Type (u + 1) extends B.{u, u} obj where 
      --                        ^ can also type B.{u} (inferres v = u)
    

We can see here that our SmallCategory (C) now constrains the arrows to live in the same universe as the objects by setting \(v = u\) in the extension of \(\texttt {B}\). Thus, if we construct our pair, we have:

      variable (c : @C.{m} α)
      #check (c.pair a b : Sort (m + 1)) -- Box.pair a b : Type m
    

Next up let's look at the identity morphism:

      id a := .up <| .up <| le_refl a
    

The identity is defined as a function that quantifies over all objects \(a\) in our category and returns an arrow from \(a\) to \(a\). Naturally we then first want to construct our arrow, the identity arrow from \(a\) to \(a\) is simply the reflexivity property of the preorder relation \(\leq \), that is \(a \leq a\) which we can get via \(\texttt {le\_refl a}\). However since our arrows live in \(\texttt {Type m}\), we need to lift our relation twice, first using \(\texttt {PLift.up}\) to lift it from \(\texttt {Prop}\) to \(\texttt {Type 0}\), and then again using \(\texttt {ULift.up}\) to lift it from \(\texttt {Type 0}\) to \(\texttt {Type m}\). A note to make for people unfamiliar with the syntax here, the following pieces of code are equivalent:

      -- .up <| .up <| le_refl a == ULift.up (PLift.up (le_refl a))
    

Finally let's look at the composition of arrows:

      comp {a b c} f g := .up <| .up <| (le_trans f.down.down g.down.down)
    

The lifting portion here follows the same reasoning as the identity morphism, we need to lift the resulting relation from \(\texttt {Prop}\) to \(\texttt {Type m}\). The actual composition is done via the transitivity property of the preorder relation \(\leq \). The thing is here that our input arrows \(f\) and \(g\) are both lifted types corresponding to:

      f : ULift (PLift (a ≤ b))
      g : ULift (PLift (b ≤ c))
    

Thus to extract the actual preorder relations we need to use the \(\texttt {down}\) method twice, first to go from \(\texttt {ULift}\) to \(\texttt {PLift}\), and then again to go from \(\texttt {PLift}\) to the actual relation in \(\texttt {Prop}\). Once we have the two relations extracted we can then apply the transitivity property \(\texttt {le\_trans}\) to get the composed relation \(a \leq c\) (which we then lift back up).