We assume that \(\mathcal L\) is a category with a terminal object \(1\). This category has a natural number object (NNO) if there exists an object \(\mathbb {N}\) together with two morphisms:

• \(0 : 1 \to \mathbb {N}\)
• \(s : \mathbb {N} \to \mathbb {N}\)

such that, given any global element \(z : 1 \to X\) and any morphism \(f : X \to X\), there exists a unique morphism \(u : \mathbb {N} \to X\) such that the following diagram commutes:

In the category Set, the natural number object (NNO) can be represented by the set of natural numbers \(\mathbb {N} = \{0, 1, 2, 3, \ldots \}\). If we take some arbitrary other set \(X\) with some point \(x : 1 \to X\) (which can be identified with an element of \(X\)) and some function \(f : X \to X\), we can define a unique function \(u : \mathbb {N} \to X\) as follows:

Stepwise (mathematical/natural/ordinary) induction is a proof technique used to establish the truth of a statement \(P(n)\) for all natural numbers \(n \in \mathbb {N}\). The process involves two main steps:

1. Base Case: Prove that the statement \(P(0)\) is true.
2. Inductive Step: Assume that the statement \(P(k)\) is true for some arbitrary natural number \(k \in \mathbb {N}\) (this assumption is called the inductive hypothesis). Then, using this assumption, prove that the statement \(P(k + 1)\) is also true.

If both the base case and the inductive step are successfully proven, we can conclude that the statement \(P(n)\) holds for all natural numbers \(n \in \mathbb {N}\). The concise formulation of this can be given by the induction principle.

          declare_syntax_cat arithTm

          -- atoms
          syntax num                      : arithTm
          syntax "(" arithTm ")"          : arithTm

          -- multiplicative level (higher precedence)
          syntax:70 arithTm:70 "*" arithTm:71 : arithTm
          syntax:70 arithTm:70 "/" arithTm:71 : arithTm

          -- additive level (lower precedence)
          syntax:60 arithTm:60 "+" arithTm:61 : arithTm
          syntax:60 arithTm:60 "-" arithTm:61 : arithTm

          syntax "ex{" arithTm "}" : term

          macro_rules
            -- numerals
            | `(ex{ $n:num }) =>
                `(Expr.const $n)

            -- parentheses
            | `(ex{ ($t:arithTm) }) =>
                `(ex{$t})

            -- addition
            | `(ex{ $e₁:arithTm + $e₂:arithTm }) =>
                `(Expr.binop BinOp.add (ex{$e₁}) (ex{$e₂}))

            -- subtraction
            | `(ex{ $e₁:arithTm - $e₂:arithTm }) =>
                `(Expr.binop BinOp.sub (ex{$e₁}) (ex{$e₂}))

            -- multiplication
            | `(ex{ $e₁:arithTm * $e₂:arithTm }) =>
                `(Expr.binop BinOp.mul (ex{$e₁}) (ex{$e₂}))

            -- division
            | `(ex{ $e₁:arithTm / $e₂:arithTm }) =>
                `(Expr.binop BinOp.div (ex{$e₁}) (ex{$e₂}))
        

Now say that we wanted to evaluate the expression \(((2 * 3) + 4)\) on a high level what we would do is rewrite the multiplication to \(6 + 4\) and then rewrite that to \(10\). Expressing this in lean we have:

        example : -- ((2 * 3) + 4) ->ⁿ 10
        ex{ ((2 * 3) + 4) } ->ⁿ ex{ 10 } :=
          .trans (rw_lhs (rw_const .mul 2 3)) (rw_const .add 6 4)
      

Here we say that the expression \(((2 * 3) + 4)\) after multiple steps evaluates to \(10\) by first rewriting the left-hand side multiplication to \(6 + 4\) and then rewriting that to \(10\). And we chain these operations together using the .trans constructor of the multistep evaluation relation. Now the question becomes, how do we define these rewrite steps? Intuitively we can imagine evaluation as being described by the following sort of graph

        +(lhs [op] rhs)
        |
        +-+(rw_lhs) ->ⁿ lhs' [op] rhs    (1) reduce lhs some number of steps
          |
          +-+(rw_rhs) ->ⁿ lhs [op] rhs'  (2) reduce rhs some number of steps
            |
            +- (rw_const) -> value       (3) reduce both to a constant value
      

The idea of each rule being that:

• rw_lhs: If the left-hand side can be reduced some number of steps we can reduce it while keeping the right-hand side the same. This corresponds to the ST_BinOp1 rule defined earlier.
• rw_rhs: If the left-hand side is a constant we can reduce the right-hand side some number of steps while keeping the left-hand side the same. This corresponds to the ST_BinOp2 rule defined earlier.
• rw_const: If both sides are constants we can apply the binary operation and reduce the entire expression to a single constant value. This corresponds to the ST_BinOpConst rule defined earlier.

As these rules are defined over the structure of multistep evaluation our implementation of them will naturally be in terms of the inductive structure of a multistep relationship:

        lemma rw_lhs (lhs_rw : lhs ->ⁿ lhs') :
          (lhs [op] rhs) ->ⁿ (lhs' [op] rhs) :=
        match lhs_rw with
        | .refl       => .refl
        | .tail S₁ S₂ => (rw_lhs S₁).tail (.ST_BinOp1 S₂)

        lemma rw_rhs (rhs_rw : rhs ->ⁿ rhs') :
          ((.const lhs) [op] rhs) ->ⁿ ((.const lhs) [op] rhs') :=
        match rhs_rw with
        | .refl       => .refl
        | .tail S₁ S₂ => (rw_rhs S₁).tail (.ST_BinOp2 S₂)

        lemma rw_const (op : BinOp) (lhs rhs : Nat) :
          ((.const lhs) [op] (.const rhs)) ->ⁿ .const (eval_op op lhs rhs) :=
        .single (.ST_BinOpConst op lhs rhs)
      

Alternatively we can specify the left and right rewrite rules using the recursor or or head induction principle for multistep evaluation:

        lemma rw_rhs' (rhs_rw : rhs ->ⁿ rhs') :
          ((.const lhs) [op] rhs) ->ⁿ ((.const lhs) [op] rhs') :=
        .rec
          (refl := .refl)
          (tail := by
            intro _ _ _ hcb ih
            exact ih.tail (.ST_BinOp2 hcb)
          ) rhs_rw

        lemma rw_rhs'' (rhs_rw : rhs ->ⁿ rhs') :
          ((.const lhs) [op] rhs) ->ⁿ ((.const lhs) [op] rhs') :=
        .head_induction_on
          (refl := .refl)
          (head := by
            intro _ _ hac _ ih
            exact ih.head (.ST_BinOp2 hac)
          ) rhs_rw
      

The motive function here is inferred by Lean via the Lemma, which allos us to avoid having to explicitly specify it. Other than this we can see that the recursors again simply correspond to providing methods to describe what to do for each of the constructors.

So at this point you might, I think fairly ask yourself:

Wait why are you spending so much time on this random example for recursors?

The main reason is that to me it provides one of the most grounded direct examples of what it means for a recursor function to eliminate a term of an inductive type. In general in type theory we say that term elimination represents the natural deduction rules for how to use terms of a given type. Applied to our example we can see that these recursors precisely correspond to the rules of how we evaluate i.e. use arithmetic expressions.

Each rewrite rule describes how we can take an expression and reduce it step by step until we reach a final value. So in a sense the recursor here eliminates the expression by providing a systematic way to break it down into its constituent parts and evaluate it. This is precisely the essence of what recursors do in type theory; they provide a way to systematically deconstruct and utilize terms of inductive types according to their defined structure and properties.

One of the wonderful things we then naturally get from these recursors is that we can use them to describe how a correct evaluation works. So given our evaluation function:

        @[simp]
        def eval : Expr -> Nat
          | Expr.const n => n
          | Expr.binop op e₁ e₂ =>
              let v₁ := eval e₁
              let v₂ := eval e₂
              eval_op op v₁ v₂
      

We can use the recursors describing the rewrite rules to show that this evaluation function for our expressions both yields a constant and that we have some sequence of reduction steps (application of rewrite rules) to get to said constant. Or expressed formally:

        (e : Expr) : -- for any expression e
          (∃ v : Nat), -- there exists a value v
            (eval e = v) ∧ (e ->ⁿ (.const v))
            -- such that eval e = v and e reduces to the constant v
      

The proof of this statement works by induction on the structure of the expression e if our expression represents a constant then the proof is trivial as we can just take the value of the constant itself. If our expression represents a binary operation then same as we showed for the concrete example we just apply our recursors to first rewrite the lhs, then the rhs and finally apply the operation to get the final constant value. In full the proof looks like:

        theorem eval_correct (e : Expr) :
        ∃ v : Nat, (eval e = v) ∧ (e ->ⁿ (.const v)) := by
        induction e with
        | const n => exists n
        | binop op lhs rhs eval_lhs eval_rhs =>
          rcases eval_lhs with ⟨lhs_v, ⟨rhs_is_v, lhs_rw⟩⟩
          rcases eval_rhs with ⟨rhs_v, ⟨lhs_is_v, rhs_rw⟩⟩
          simp [rhs_is_v, lhs_is_v]

          exact
            (rw_lhs lhs_rw).trans (
              (rw_rhs rhs_rw).trans (
                rw_const op lhs_v rhs_v
              )
            )
      

In other words our proof for describing that our evaluation function is correct amounts to essentially simulating or describing quite literally how the evaluation works step by step using the recursors we defined earlier. To see precisely how rcases works here I'd recommend to paste the code into a Lean environment and examine the types of each of the intermediate values.

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).

A category \(C\) consists of:

• A collection (or class (2)) of objects, denoted as \(\text {Ob}(C)\) or \(C_0\).
• A collection (or set (2)) of morphisms (or arrows), denoted \(C_1\) or \(C(x, y)\) for \(x, y \in \text {Ob}(C)\).
  • For every morphism \(f \in C(x, y)\), there are two associated objects: the source (or domain) \(x\) and the target (or co-domain) \(y\). In standard function notation, we write \(f: x \to y\) where \(x = \text {dom}(f)\) and \(y = \text {cod}(f)\). NLab has a nice convention where it denotes the source \(s\) of a morphism as \(s(f)\) and the target \(t\) as \(t(f)\).
  • For every pair of morphisms \(f \in C(x, y)\) and \(g \in C(y, z)\) (s.t. \(t(f) = s(g)\) i.e. the morphisms type check), there is a composition morphism \(g \circ f \in C(x, z)\). Written out we can denote this as: \[ C(x, y) \times C(y, z) \to C(x, z) \] in diagrammatic order this is often written as \(f; g\) we can equivalently use a more graphical notation:

  • For every object \(x \in \text {Ob}\) there is an identity morphism: \[ (\text {id}_x : x \to x) \in C(x, x) \]
  Note: Some additional notations for morphisms include \(\text {hom}(x, y)\), \(\text {hom}_C(x, y)\) or \(C_1(x, y)\). Additionally, people use the notation \(\text {Mor(C)}\) to denote the following disjoint union \[ \text {Mor}(C) = \bigsqcup _{x, y \in \text {Ob}(C)} C(x, y) \] Which just expresses the idea that the collection of all morphisms in a category is made up of the morphisms between each pair of objects.

The above are often called data of a category. In addition to this data, a category must satisfy the following axioms or (conditions):

• Morphisms need to be associative which means that for every triple of morphisms \(f \in C(w, x)\), \(g \in C(x, y)\), and \(h \in C(y, z)\) the following holds: \[ h \circ (g \circ f) = (h \circ g) \circ f \]
• For each morphism \(f \in C(x, y)\) the identity morphisms act as neutral elements for composition: \[ \text {id}_y \circ f = f = f \circ \text {id}_x \] This is also known as the left and right unit laws or just unity in general.

• A category such as the one described above is often also called a 1-category to distinguish it from higher categories such as 2-categories, n-categories.

We want to start off by defining the data of our category. On a high level we want to define a category with two objects, \(\texttt {true}\) and \(\texttt {false}\). Starting with the object representation we have:

      /-- A wrapper type to make a custom category on Bool -/
      structure BoolCat : Type where
        val : Bool
      deriving DecidableEq, Repr

      /-- The two objects -/
      def BoolCat.tt : BoolCat := ⟨true⟩
      def BoolCat.ff : BoolCat := ⟨false⟩
    

Next we want to define the morphisms between these objects. For each pair of objects we express 3 kinds of morphisms: the identity morphism, a morphism from \(\texttt {false}\) to \(\texttt {true}\), \(\texttt {false}\)from \(\texttt {true}\) to \(\texttt {false}\). We can express this in Lean as follows:

      /-- Morphisms: we allow identity on each, plus iso between them -/
      inductive BCHom : BoolCat → BoolCat → Type
        | id (b : BoolCat) : BCHom b b
        | swap : BCHom BoolCat.tt BoolCat.ff
        | swapInv : BCHom BoolCat.ff BoolCat.tt
    

Formally what this describes is a kind of piecewise function:

Now we have some notion of objects and morphisms between them, we can move on to defining composition of morphisms.

      def comp : {X Y Z : BoolCat} → BCHom Y Z → BCHom X Y → BCHom X Z
        | _, _, _, id _, f => f
        | _, _, _, f, id _ => f
        | _, _, _, swapInv, swap => id _
        | _, _, _, swap, swapInv => id _
    

This defines composition by pattern matching on the possible morphism combinations. Note that we have to explicitly handle the cases where we compose \(\texttt {swap}\) and \(\texttt {swapInv}\) to get the identity morphism on the respective objects. To construct our category we have to provide proofs for the category axioms, namely associativity and identity.

      @[simp] theorem id_comp' {X Y : BoolCat} (f : BCHom X Y) 
          : comp (id Y) f = f := by
        cases f <;> rfl

      @[simp] theorem comp_id' {X Y : BoolCat} (f : BCHom X Y) 
          : comp f (id X) = f := by
        cases f <;> rfl

      theorem assoc'  (f : BCHom W X) (g : BCHom X Y) (h : BCHom Y Z) :
          comp h (comp g f) = comp (comp h g) f := by
        cases f <;> cases g <;> cases h <;> rfl
    

With all this in place we can finally define our category instance:

      instance : Category BoolCat where
        -- The data
        Hom     := BCHom
        id      := BCHom. id
        comp    := fun f g => BCHom. comp g f

        -- Category laws
        id_comp := fun f     => BCHom.comp_id' f
        comp_id := fun f     => BCHom.id_comp' f
        assoc   := fun f g h => BCHom.assoc' f g h
    

Since we clearly see that the morphisms \(\texttt {swap}\) and \(\texttt {swapInv}\) are inverses of each other, we can construct an isomorphism between the two objects \(\texttt {tt}\) and \(\texttt {ff}\) as follows:

      def ttFfIso : BoolCat.tt ≅ BoolCat.ff where
        hom := BCHom.swap
        inv := BCHom.swapInv
        hom_inv_id := rfl
        inv_hom_id := rfl
    

We can see that lean uses a similar notation for isomorphism as we do in our notes, namely the \(\texttt {≅}\) symbol between the two objects. We can see that an isomorphism consists of a \(\texttt {hom}\) and an \(\texttt {inv}\) morphism along with proofs that composing them in either order yields the respective identity morphism. In Lean4 its defined as follows:

      structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
        /-- The forward direction of an isomorphism. -/
        hom : X ⟶ Y
        /-- The backwards direction of an isomorphism. -/
        inv : Y ⟶ X
        /-- Composition is the identity on the source. -/
        hom_inv_id : hom ≫ inv = 𝟙 X := by cat_disch
        /-- Composition, in reverse, is the identity on the target. -/
        inv_hom_id : inv ≫ hom = 𝟙 Y := by cat_disch

      ...

      /-- Notation for an isomorphism in a category. -/
      infixr:10 " ≅ " => Iso 
    

We can check out some properties of our isomorphism like so:

      -- Verify it's an isomorphism
      #check ttFfIso           -- BoolCat.tt ≅ BoolCat.ff
      #check ttFfIso.hom       -- BoolCat.tt ⟶ BoolCat.ff
      #check ttFfIso.inv       -- BoolCat.ff ⟶ BoolCat.tt
    

Furthermore we can also show the identity isomorphism \(tt \cong tt\):

      -- Every object is isomorphic to itself (trivially)
      def ttSelfIso : BoolCat.tt ≅ BoolCat.tt := Iso.refl _

      #check ttSelfIso -- BoolCat.tt ≅ BoolCat.tt
    

Finally for the sake of completeness we can also demonstrate the isomorphism laws in examples as so:

      -- The isomorphism laws
      example : ttFfIso.hom ≫ ttFfIso.inv = 𝟙 BoolCat.tt 
        := ttFfIso.hom_inv_id

      example : ttFfIso.inv ≫ ttFfIso.hom = 𝟙 BoolCat.ff 
        := ttFfIso.inv_hom_id