Categories, Monoids, and Preorders (in Lean 4)

This session is an impromptu lecture, live-coded in Lean 4, working toward one slogan: a category is a proof-relevant preorder that had the monoid laws shoved back in. Or, said the other way: a monoid that learned to go places. Each structure is defined from scratch, so the slogan ends up as a precise mathematical statement rather than a vibe.

Monoids#

A monoid is a type $M$ with a binary operation, an identity element, and two laws: associativity, so it doesn't matter which way you nest the multiplication, and the identity law, so multiplying by the identity on either side does nothing. As a Lean structure, in the Bourbaki style:

structure Monoid (M : Type) where
  mul : M → M → M
  one : M
  assoc : ∀ a b c, mul a (mul b c) = mul (mul a b) c
  identity : ∀ a, mul a one = a ∧ mul one a = a

The session is deliberately Mathlib-free (this Monoid shadows Mathlib's), so nothing is imported and every structure is our own.

The first example is the endofunction monoid: functions from $A$ to $A$, where mul is function composition (written backwards, for reasons that pay off later) and one is the identity function. Both laws fall to rfl: beta plus Lean's definitional eta. From any monoid we build two more: the opposite monoid flips the multiplication, each law proved by flipping the original proof, and the product monoid on $M_1\times M_2$ runs two monoids side by side, componentwise.

Preorders#

Now something that looks very different. A preorder is a relation le : P → P → Prop with transitivity, from $a\le b$ and $b\le c$ conclude $a\le c$, and reflexivity, $a\le a$ for every $a$. The natural numbers with the usual ordering are the first example (Lean's omega tactic discharges both laws). And the same two constructions go through: an opposite preorder that flips the relation, and a product preorder that compares componentwise.

One Lean detail matters here: Prop is proof irrelevant, meaning any two proofs of the same proposition are equal.

The resemblance#

In what sense are these similar? Look at transitivity with monoid eyes: it combines a proof of $a\le b$ with a proof of $b\le c$ into a proof of $a\le c$. That is a composition operation, except the endpoints must match; you cannot compose two proofs of $a\le b$ with each other. Reflexivity acts as an identity for transitivity. And transitivity is associative, automatically: by proof irrelevance any two proofs of $a\le c$ are equal, so any two ways of composing your way there agree. The preorder satisfies a moral equivalent of the monoid laws for free.

So the preorder is secretly monoidal, and the monoid is like a preorder with only one endpoint. There is a structure that combines them: the category.

structure Category (Obj : Type u) where
  Hom : Obj → Obj → Type v
  compose : ∀ {A B C}, Hom A B → Hom B C → Hom A C
  id : ∀ {A}, Hom A A
  assoc : ∀ {A B C D} (f : Hom A B) (g : Hom B C) (h : Hom C D),
    compose f (compose g h) = compose (compose f g) h
  identity : ∀ {A B} (f : Hom A B), compose f id = f ∧ compose id f = f

Hom is a Type, not a Prop: this is a proof-relevant preorder, with possibly many genuinely different morphisms from $A$ to $B$. compose is transitivity, id is reflexivity. But we lost proof irrelevance, so the laws the preorder inherited silently must now be demanded explicitly, and since we already had monoids to inspire us, we know exactly how to write them: the monoid laws, with endpoints.

Pause and try: every monoid is a category with one object. Write down what Obj, Hom, compose, and id must be.

Take Obj := Unit, the type with a single element. There is only one choice of endpoints, so set Hom _ _ := M. Then compose := mul and id := one, and the category's associativity and identity laws are the monoid's laws, verbatim. The morphisms are the elements of the monoid; the single object is just a peg to hang them on.

Everything coincides#

Every preorder is also a category: take the elements as objects and a proof of $a\le b$ as the morphism from $a$ to $b$ (wrapped in a small structure to lift it from Prop to Type, which takes a little persuading of Lean). Composition is transitivity, identity is reflexivity, and both category laws are trivial, by proof irrelevance again.

The constructions transfer too: the opposite and product categories mirror the opposite and product monoids almost line for line. And the payoff for composing backwards earlier: the endofunction monoid generalizes to the category of types, where Hom A B is the function type A → B, composition is function composition, and both laws are proved by rfl. A genuine generalization of both the monoid and the preorder, landing in the same place.

If you remember three things#

1. A monoid is an associative operation with identity on one type; a preorder is transitivity plus reflexivity across endpoints, and proof irrelevance of Prop makes it satisfy the monoid laws automatically.
2. A category is a proof-relevant preorder: once Hom lands in Type, the silently inherited laws must be demanded explicitly, and they are exactly the monoid laws with endpoints.
3. Both parents embed: a monoid is a one-object category, a preorder is a category whose morphisms are proofs of $a\le b$, and the opposite, product, and function constructions generalize uniformly.