Blog. A simple Bool category in Lean4 [002u]

November 29, 2025

Definition 1. Category [002m]

November 27, 2025

There are a few ways you can define a category. In the most basic intuitive sense a category consists of a collection of things called objects and binary relationships (or transitions) between those objects called morphisms (or arrows). We can combine these relationships by composing them, and for each object there is an identity morphism that acts as a neutral element for composition. (1)

In the context of quivers a category can be defined as a quiver with a rule saying for how we can compose two edges that fit together to get a new edge. Furthermore, each vertex (object) has an edge starting and ending at that vertex (the identity morphism). The classical definition is something like this:

1.1. The data

November 27, 2025

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.

1.2. The axioms

November 27, 2025

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.

1.3. Remarks

November 27, 2025

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.

Definition 2. Isomorphism (morphisms) [002s]

November 29, 2025

A morphism \(f : X \to Y\) is called an Isomorphism if there exists a morphism \(g : Y \to X\) such that the following hold (1):

\[ g \circ f = 1_X \quad f \circ g = 1_Y \]

Sometimes an isomorphism is also denoted

\[ X \xrightarrow {\cong } Y \]

Example 3. The category

November 29, 2025

3.1. The data

November 29, 2025

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:

\[ \text {f}(x, y) = \begin {cases} 1_x &: x \to x & \texttt {if } x = y \\ \texttt {swap} &: \text {tt} \to \text {ff} & \texttt {if } x = \text {tt} \land y = \text {ff} \\ \texttt {swapInv} &: \text {ff} \to \text {tt} & \texttt {if } x = \text {ff} \land y = \text {tt} \end {cases} \]

3.2. Composition and Category instance

November 29, 2025

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

3.3. Isomorphisms in the Bool category

November 29, 2025

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

References

Reference. category [nlab-category]

November 1, 2025
nLab authors
https://ncatlab.org/nlab/show/category

Reference. 2-Dimensional Categories [johnson-yau-2d-categories-2020]

June 17, 2020
Johnson, Niles, Yau, Donald
https://arxiv.org/abs/2002.06055v3

Context

Blog posts [001a]

November 23, 2025

Blog. Understanding recursors with Lean4 [001b]

November 23, 2025

The recursor for natural numbers

November 23, 2025

Before we define recursors, let's first introduce the idea of an inductive type. We'll do this by examining how lean defines natural numbers.


    inductive Nat where
    | zero : Nat
    | succ (n : Nat) : Nat

The recursor for natural numbers

November 23, 2025

Before we define recursors, let's first introduce the idea of an inductive type. We'll do this by examining how lean defines natural numbers.


    inductive Nat where
    | zero : Nat
    | succ (n : Nat) : Nat

The idea here being that we can construct natural numbers by either using the constructor zero to get 0, or by applying the constructor succ to an existing natural number to get its successor. For example, we can construct 3 as follows:


    def three : Nat := Nat.succ (Nat.succ (Nat.succ Nat.zero))

We can equivalently express this definition using the type formation and term introduction rules:

While this explanation for inductive types usually gives most people I think enough intuition to understand the basic notions of how to use them to construct something like natural numbers, I think it kind of misses the deeper idea of what an inductive type and by extension a recursor really is. To attempt to explain this we'll take a look into some categorical semantics behind inductive types.

Definition. Natural Number Object (NNO) [001c]

November 23, 2025

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:

While at first this definition seems a bit needlessly abstract, it actually captures what the inductive type of natural numbers really is. The basic thing to recognize is that the two morphisms (just think of them as functions for now) in reality don't have anything to do with natural numbers directly. Instead, they act as a kind of blueprint for how we can use the properties or constraints of natural numbers to make anything. Here on a high level we can describe the two functions / constructors as follows:

\(0 : 1 \to \mathbb {N}\) - The represents the abstract idea of having some starting point or base case. Within natural numbers this is represented by 0, but in reality it denotes an abstract concept of having a starting point.
\(s : \mathbb {N} \to \mathbb {N}\) - This represents the abstract idea of being able to build upon existing things to create new things. Within natural numbers this is represented by the successor function.

Now this might quite fairly still seem a bit confusing and abstract. How can we use properties to make anything?. To describe this more formally lets constrain ourselves to the category of sets, \(\mathbf {Set}\). If you are unfamiliar with category theory it's sufficient to think of this as just a collection of all kinds of sets and functions between them.

Example. Natural Number Object (NNO) in Set [001e]

November 23, 2025

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:

\[ u(n) = \begin {cases} x & \text {if } n = 0 \\ f^n(x) & \text {if } n \geq 0 \end {cases} \]

So in plain English what this is saying is that given any set \(X\) where we have some starting point \(x \in X\) and some way of building upon existing elements of \(X\) (the function \(f : X \to X\)), we can use the properties of natural numbers to create a unique function \(u : \mathbb {N} \to X\) that maps natural numbers to elements of \(X\) in a way that respects our starting point and building function. A natural next question to have might be

But what does it mean to respect the starting point and building function?

Here I'd fast say intuitively you can just imagine construct which has some notion of a start and some way of building upon existing things. For example let's imagine the following graph:

\[ a \to b \to c \to d \to e \to \ldots \]

Clearly here with have:

Starting point: Our start here is the node \(a\).
Building function: Our building function i.e. successor mechanism here is just following the arrows to the next node.

So our two morphisms then are:

\(x : 1 \to X\) where \(x\) maps to \(a\).

\(f : X \to X\) where \(f\) maps each node to the next node along the arrow. That is


        f(a) = b
        f(b) = c
        f(c) = d
        f(d) = e
        ...

Creating a minimal replica of this in Lean we could do something like:


    inductive Node where
    | start : Node           -- this will play the role of “a”
    | next  : Node → Node

    def succNode (v : Node) : Node :=
      Node. next v

    def natToNode : ℕ → Node
      | 0       => Node.start
      | n + 1   => succNode (natToNode n)

So we can see our function \(u : \mathbb {N} \to X\) here is represented by natToNode. Where the function maps 0 to a and each successor natural number to the next node along the arrow.

Something you might notice here is that if our natToNode function is replaced by just an identity, i.e.:


    def natToNat : ℕ → ℕ
      | 0       => 0
      | n + 1   => n + 1

Then we get just the natural numbers themselves as defined by their properties. This is precisely what's expressed by the earlier commutative diagram we say. The two arrows:

\[ 1 \xrightarrow {0} \mathbb {N} \quad \text { and } \quad \mathbb {N} \xrightarrow {s} \mathbb {N} \]

Are just the natural numbers defined by their properties. So in a sense the natural numbers are the most basic instantiation of their own properties. So now a fair thing to wonder is:

So what does this have to do with recursers?

Well the key insight here is that our functions natToNat and natToNode both are our recursers for the natural numbers. A recursor is just a function that allows us to define functions out of an inductive type by specifying how to handle each constructor of the inductive type. So equivalently we can express our recursor for natural numbers as:


    def recNat {C : Type} (z : C) (s : C → C) : ℕ → C
      | 0       => z
      | n + 1   => s (recNat z s n)

If we examine the actual type signature generated by #check Nat.rec we have:


      «Nat».rec.{u}
      {motive : ℕ → Sort u}
      (zero : motive «Nat».zero)
      (succ : (n : ℕ)
        → motive n
        → motive n.succ)
      (t : ℕ) : motive t

In our examples above we can see that the motive is just the type we are mapping to (either \(\mathbb {N}\) or \(X\)), the zero is our starting point (either 0 or a) and the succ is our building function (either the successor function or following the arrows). So using the recursor we can rewrite our earlier natToNat and natToNode functions as:


      def natToNat : ℕ → ℕ :=
        Nat.rec
          0                 -- | 0     => 0
          (fun n => n + 1)  -- | n + 1 => n + 1

      def natToNode : ℕ → Node :=
        Nat.rec
          Node.start            -- | 0     => Node.start
          (fun n => succNode n) -- | n + 1 => succNode (natToNode n)

This for the most part covers the basic idea of recursors for the sake of brevity I won't go into more instances of recursors for other inductive types though conceptually they work the same way. You specify how to handle each constructor of the inductive type and the recursor gives you a function that maps from the inductive type to whatever type you specified.

The connection to induction

November 23, 2025

A very important property of recursors emerges when we make the motive dependent. To elaborate on what that means let's first consider the situation of simple stepwise induction.

Definition. Stepwise (Mathematical) Induction [001f]

November 23, 2025

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:

Base Case: Prove that the statement \(P(0)\) is true.
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.

\[ (P(0) \land \forall k \in \mathbb {N}.\ (P(k) \to P(k + 1))) \to \forall n \in \mathbb {N}.\ P(n) \]

Something we can notice here just by superficial observation alone is that this seems to look an awful lot like the recursor for natural numbers we defined earlier. In fact, it is an application of the recursor for natural numbers for the dependent motive \(P : \mathbb {N} \to \texttt {Prop}.\). To make this a little more concrete let's define a simple property over natural numbers:


      def P (n : ℕ) : Prop := n + 0 = n

Now its important to note that in an abstract sense this is no different from any other function from natural numbers to some type. The dependency comes into play when we try to use the recursor i.e. the properties of naturals with this motive.


      def natToProp (n : ℕ) : (P n) :=
        Nat.rec
          (motive := P)
          (by simp [P])                    -- base case: P 0
          (fun n ih => by simp [P])        -- inductive step: P n → P (n+1)
          n

A few things we can observe here:

The recursor here represents a dependent function, which is to say that the return type of the function depends on the input value. Contrasting this to the earlier case where the return type was always just \(\mathbb {N}\) or \(X\).
Base case - Importantly here as opposed to providing a function that returns some value of type \(C\) for the base case, we instead provide a proof that the property \(P(0)\) holds.
Inductive step - Similarly for the inductive step we provide a function that takes an arbitrary natural number \(n\) and a proof that \(P(n)\) holds (the inductive hypothesis) and returns a proof that \(P(n + 1)\) holds.

If we view this through the lens of the Curry-Howard correspondence it quite nicely illustrates how our proof here is just a program which constructs witnesses (valid proofs) for each natural number that the property \(P(n)\) holds. In the same way that our earlier recursor provided elements on the correct type, this dependent recursor provides proofs on the correct property. As this application of a recursor to a proposition represents said proposition being true for all natural numbers, we can equivalently use this within a theorem.


      theorem add_zero (n : ℕ) : n + 0 = n := natToProp n

Case Study: Evaluating arithmetic expressions

November 23, 2025

As a little kind of case study I want to give an example of an inductive type (and its recursor) that most people become familiar with; in a sense; as early as primary school: the operational semantics of binary operators. We'll start by defining some basic syntax for arithmetic expressions:


      inductive BinOp where
      | add : BinOp
      | sub : BinOp
      | mul : BinOp
      | div : BinOp

      inductive Expr where
      | const : ℕ → Expr
      | binop : BinOp → Expr → Expr → Expr

So here we have defined a simple language of arithmetic expressions consisting of natural number constants and binary operations. This provides us with the means to construct expressions like:


      #check Expr.binop BinOp.add (Expr.const 10) (Expr.const 20)

If we want to actually define the semantics of how to evaluate these expressions we'll need to define a set of rewrite rules that describe how we can take an expression and reduce it to a value i.e. evaluate it. To evaluate an expression we want to traverse the expression tree and whenever we encounter a binary operation with two constant operands we want to apply the operation and replace the entire sub-expression with the resulting constant. We express this as 3 rewrite rules:

Left Evaluation: If the left operand of a binary operation can be reduced, then we reduce it.
Right Evaluation: If the left operand is a constant and the right operand can be reduced, then we reduce the right operand.
Operation Evaluation: If both operands are constants, we apply the binary operation and replace the entire sub-expression with the resulting constant.


      def eval_op : BinOp → (Nat → Nat → Nat)
      | .add => Nat.add
      | .sub => Nat.sub
      | .mul => Nat.mul
      | .div => Nat.div

      inductive Step : Expr -> Expr -> Prop
      | ST_BinOp1 (op : BinOp)
          (e₁ e₁' e₂ : Expr)
          (h : Step e₁ e₁') :
          Step (Expr.binop op e₁ e₂)
               (Expr.binop op e₁' e₂)
      | ST_BinOp2 (op : BinOp)
          (v₁ : Nat)
          (e₂ e₂' : Expr)
          (h : Step e₂ e₂') :
          Step (Expr.binop op (Expr.const v₁) e₂)
               (Expr.binop op (Expr.const v₁) e₂')
      | ST_BinOpConst (op : BinOp) (v₁ v₂ : Nat) :
          Step (Expr.binop op (Expr.const v₁) (Expr.const v₂))
               (Expr.const (eval_op op v₁ v₂))

Since expressions can naturally require multiple evaluations steps it makes sense to define a multistep evaluation relation as the reflexive transitive closure of the single step evaluation relation defined above. This we can define as:


      abbrev MultiStep := Relation.ReflTransGen Step

      -- helper notation to express multi-step evaluation
      notation:50 e " ->ⁿ " e' =>  MultiStep e e'

Let's also define a small helper syntax and macro to make it easier to write arithmetic expressions:

A small arithmetic expression grammar

November 23, 2025


          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₂}))

Describing arithmetic evaluation

November 23, 2025

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.

Recursors describe usage

November 23, 2025

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.

Proving correct evaluation

November 23, 2025

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.

Blog. Type universes in Lean4 [002r]

November 28, 2025

A brief overview

November 28, 2025

Universe hierarchy

November 28, 2025

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

\[ \begin {align*} \texttt {Prop} : \texttt {Type 0} : \texttt {Type 1} : \texttt {Type 2} : \cdots \\ \texttt {Sort 0} : \texttt {Sort 1} : \texttt {Sort 2} : \texttt {Sort 3} : \cdots \end {align*} \]

\(\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:

\[ \texttt {Type u} \equiv \texttt {Sort (u + 1)} \]\[ \texttt {Prop} \equiv \texttt {Sort 0} \]

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

Predicative universes

November 28, 2025

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.

Impredicative universes

November 28, 2025

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:

\[ (\forall a : \texttt {Prop},\ a \to a) : \texttt {Prop} \]

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

The general rule

November 28, 2025

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:

\[ \texttt {imax}(u, v) = \begin {cases} 0 & \text {if } v = 0 \\ \texttt {max}(u, v) & \text {otherwise} \end {cases} \]

The level grammar

November 28, 2025

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

Universe Binding

November 28, 2025

Explicit

November 28, 2025

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 β := ...

Implicit

November 28, 2025

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)

Implicit + fresh

November 28, 2025

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 β := ...

Universe Lifting

November 28, 2025

Sometimes we may want to explicitly lift a type from one universe to a higher universe. Lean4 provides lifting operators which are wrappers around terms of a type that reside in a higher universe. There are two main lifting operators:

\(\texttt {PLift}\): Lifts a proposition from \(\texttt {Prop}\) to \(\texttt {Type 0}\) (i.e. \(\texttt {Sort 1}\)).
\(\texttt {ULift}\): Lifts a type from \(\texttt {Type u}\) to any number of levels.

PLift

November 28, 2025

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

ULift

November 28, 2025

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]

Example: Preorder Category

November 28, 2025

A preorder relation is a binary relation that is reflexive and transitive. In Lean this is expressed as follows:


    class Preorder (α : Type*) extends LE α, LT α where
      le_refl   : ∀ a : α, a ≤ a
      le_trans  : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
      lt := fun a b => a ≤ b ∧ ¬b ≤ a
      lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl

We can already see here that the preorder relation uses implicit universe polymorphism via the \(\texttt {Type*}\) annotation. We can now construct a small category from a preorder relation as follows:


    open CategoryTheory

    instance {α : Type u} [Preorder α] : SmallCategory α where
      Hom a b          := ULift <| PLift (a ≤ b)
      id a             := .up <| .up <| le_refl a
      comp {a b c} f g := .up <| .up <| (le_trans f.down.down g.down.down)

Let's break this down part by part starting with the homomorphism:

Arrows

November 28, 2025

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

Identity morphism

November 28, 2025

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

Composition

November 28, 2025

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

Blog. A simple Bool category in Lean4 [002u]

November 29, 2025

Definition. Category [002m]

November 27, 2025

The data

November 27, 2025

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 axioms

November 27, 2025