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:
\[
a \leq b \equiv a \xrightarrow {\leq } b
\]
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 \).
And we provide the necessary implementation for the \(\texttt {arrow}\) function by setting it to be the preorder relation \(\leq \). But what you will notice is that we have a problem here, namely that our preorder relation lives in the universe \(\texttt {Prop}\) as it's obviously a logical relation, but our graph arrows need to live in \(\texttt {Type}\) (i.e. \(\texttt {Type 0}\)).
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