Monads · The Lumenary

Lens

MotivationH

Formal expressions and how to evaluate them

Take a set $X$ and form the set $TX$ of finite lists of elements of $X$ — formal products $x_1 x_2 \cdots x_n$ with no rule for multiplying yet. Three pieces of structure are already there, before any algebra is chosen:

every element is a one-letter word: $x \mapsto [x]$ ;
a list of lists can be flattened: $[[x_1, x_2], [\,], [x_3]] \mapsto [x_1, x_2, x_3]$ ;
a monoid $M$ is exactly a set with a way to evaluate words, $TM \to M$ , compatible with the first two.

The same pattern appears far from monoids. Subsets of subsets can be flattened by union, and a complete lattice is a set where every subset can be evaluated to its supremum. Probability distributions over probability distributions can be flattened by averaging, and expectation evaluates a distribution of numbers to a number. On a topological space, Godement's "standard construction" sends a sheaf to its sheaf of discontinuous sections and builds sheaf cohomology by iterating. In a programming language, a computation that may fail, branch or print returns a value wrapped in that effect, and running two such computations in sequence requires flattening.

A monad is the common shape: a functor $T$ with a unit $\eta : X \to TX$ and a flattening $\mu : TTX \to TX$ obeying associativity and unit laws. Its algebras are the structures that $T$ describes. This lesson develops the theory — algebras, the Kleisli and Eilenberg–Moore categories, the correspondence with adjunctions, and Beck's monadicity theorem — and then looks at the same idea through the eyes of topologists, algebraists, probabilists and computer scientists.

IntuitionH

Wrap, flatten, evaluate

Read $TX$ as " $X$ -shaped things wrapped in a $T$ -structure": words in $X$ , subsets of $X$ , distributions on $X$ , terms built from variables in $X$ , computations returning an $X$ .

$\eta_X : X \to TX$ wraps a plain element as a trivial structure: the one-letter word, the singleton, the point mass, the variable, the computation that does nothing and returns $x$ .
$\mu_X : TTX \to TX$ flattens two layers of structure into one: concatenation of words, union of subsets, averaging of distributions, substitution of terms into terms, running a computation that returns a computation.

The laws say that flattening three layers does not depend on which two layers you flatten first, and that wrapping then flattening (on the inside or the outside) does nothing. They are the laws of a monoid — written one dimension up, with composition of functors in place of multiplication. That analogy is precise: monads on $\mathcal{C}$ are the monoid objects in the monoidal category of endofunctors of $\mathcal{C}$ (see monoidal categories).

An algebra is a place where wrapped things can be evaluated: $a : TA \to A$ . The unit law says that evaluating a trivially wrapped element returns it; the associativity law says that evaluating the inner layers first and then the outer layer is the same as flattening first and then evaluating. For lists this is the generalised associative law of a monoid, and that is the whole story: the algebras of the list monad are exactly the monoids.

DefinitionsH

Monads, algebras and Kleisli arrows

Throughout, $\mathcal{C}$ is a category and composition is written $g \circ f$ (" $g$ after $f$ "). Recall from natural transformations how to whisker: for $\alpha : S \Rightarrow S'$ and a functor $T$ , $(T\alpha)_X = T(\alpha_X)$ and $(\alpha T)_X = \alpha_{TX}$ .

Definition— monad

A monad on $\mathcal{C}$ is a triple $(T, \eta, \mu)$ consisting of a functor $T : \mathcal{C} \to \mathcal{C}$ and natural transformations $\eta : \mathrm{id}_{\mathcal{C}} \Rightarrow T$ (the unit) and $\mu : T^2 \Rightarrow T$ (the multiplication) such that for every object $X$

\mu_X \circ T\mu_X = \mu_X \circ \mu_{TX} \qquad\text{and}\qquad \mu_X \circ \eta_{TX} = \mathrm{id}_{TX} = \mu_X \circ T\eta_X .

The laws are the commutativity of the following diagrams (associativity on the left, the two unit laws on the right).

The monad laws: associativity of

\mu

(left) and the unit laws (right).

Definition— algebra for a monad (Eilenberg–Moore algebra)

A $T$ -algebra is a pair $(A, a)$ of an object $A$ and a morphism $a : TA \to A$ (the structure map) such that

a \circ \eta_A = \mathrm{id}_A \qquad\text{and}\qquad a \circ Ta = a \circ \mu_A .

A morphism of algebras $f : (A, a) \to (B, b)$ is a morphism $f : A \to B$ with $f \circ a = b \circ Tf$ . Algebras and their morphisms form the Eilenberg–Moore category $\mathcal{C}^T$ , with a forgetful functor $U^T : \mathcal{C}^T \to \mathcal{C}$ . For every $X$ , the pair $(TX, \mu_X)$ is an algebra — the free algebra on $X$ — and $F^T X = (TX, \mu_X)$ , $F^T f = Tf$ defines a functor $F^T : \mathcal{C} \to \mathcal{C}^T$ .

The algebra laws: the unit law (left) and the associativity law (right).

Definition— Kleisli category

The Kleisli category $\mathcal{C}_T$ has the same objects as $\mathcal{C}$ , and a morphism $A \rightsquigarrow B$ in $\mathcal{C}_T$ is a morphism $f : A \to TB$ in $\mathcal{C}$ (a Kleisli arrow). The Kleisli composite of $f : A \to TB$ and $g : B \to TC$ and the Kleisli identity are

g \circ_T f = \mu_C \circ Tg \circ f : A \to TC, \qquad \mathrm{id}^T_A = \eta_A : A \to TA .

There are functors $F_T : \mathcal{C} \to \mathcal{C}_T$ , $F_T A = A$ , $F_T(h) = \eta_B \circ h$ for $h : A \to B$ , and $U_T : \mathcal{C}_T \to \mathcal{C}$ , $U_T A = TA$ , $U_T(f) = \mu_B \circ Tf$ for $f : A \to TB$ .

Think of a Kleisli arrow as a "generalised function" from $A$ to $B$ : many-valued (list or power-set monad), partial (maybe monad), random (distribution monad), or effectful (in programming).

Definition— monadic functor

A functor $G : \mathcal{D} \to \mathcal{C}$ is monadic if it has a left adjoint $F$ and the comparison functor $K : \mathcal{D} \to \mathcal{C}^{GF}$ (constructed below) is an equivalence of categories. Informally: the objects of $\mathcal{D}$ are exactly "objects of $\mathcal{C}$ with $T$ -algebra structure".

Worked examplesH

Examples and non-examples

Example— The list (free monoid) monad on Set

$TX = \mathrm{List}(X)$ , the set of finite sequences; $Tf$ applies $f$ to each entry; $\eta_X(x) = [x]$ ; $\mu_X$ concatenates a list of lists. Associativity says that flattening a list of lists of lists inside-first or outside-first gives the same list; the unit laws say $\mu[w] = w$ and $\mu[[x_1], \dots, [x_n]] = [x_1, \dots, x_n]$ . All three are proved by induction on the outer list (and in Lean below). This monad comes from the adjunction between the free-monoid functor and the forgetful functor $\cat{Mon} \to \cat{Set}$ .

Example— The power-set monad on Set

$TX = \mathcal{P}X$ ; $Tf(S) = f[S]$ (direct image); $\eta_X(x) = \{x\}$ ; $\mu_X(\mathcal{S}) = \bigcup \mathcal{S}$ . Associativity is $\bigcup_{\mathcal{S} \in \mathfrak{S}} \bigcup \mathcal{S} = \bigcup \bigcup \mathfrak{S}$ for $\mathfrak{S} \in \mathcal{P}\mathcal{P}\mathcal{P}X$ ; the unit laws are $\bigcup\{S\} = S$ and $\bigcup_{x \in S} \{x\} = S$ .

An algebra $a : \mathcal{P}A \to A$ is a complete join-semilattice: define $x \le y \iff a\{x, y\} = y$ . Conversely, a poset with all joins gives $a(S) = \bigvee S$ . (Sketch: the associativity law gives $a(S) = a\{a(S_1), a(S_2)\}$ whenever $S = S_1 \cup S_2$ , from which $\le$ is a partial order and $a(S)$ is the least upper bound of $S$ ; the unit law gives $a\{x\} = x$ .) Algebra morphisms are maps preserving all joins. A Kleisli arrow $A \to \mathcal{P}B$ is a relation from $A$ to $B$ , and Kleisli composition is composition of relations: $\cat{Set}_{\mathcal{P}} \cong \cat{Rel}$ .

Example— The maybe (exception) monad on Set

$TX = X \sqcup \{\bot\}$ ; $\eta_X(x) = x$ ; $\mu_X$ collapses the two copies of $\bot$ in $X \sqcup \{\bot\} \sqcup \{\bot\}$ . An algebra $a : A \sqcup \{\bot\} \to A$ must be the identity on $A$ (unit law), and the associativity law then holds automatically, so an algebra is just a base point $a(\bot) \in A$ : $\cat{Set}^T$ is the category of pointed sets. (The empty set has no algebra structure.) A Kleisli arrow $A \to B \sqcup \{\bot\}$ is a partial function, and $\cat{Set}_T$ is the category of sets and partial functions.

Example— Closure operators: monads on a poset

Regard a poset $(P, \le)$ as a category with a unique arrow $x \to y$ when $x \le y$ . A functor $c : P \to P$ is a monotone map; $\eta$ says $x \le c(x)$ ; $\mu$ says $c(c(x)) \le c(x)$ ; all diagrams commute automatically. So a monad on a poset is exactly a closure operator (and then $c \circ c = c$ ). Its algebras are the elements with $c(x) \le x$ , i.e. the closed elements. Topological closure on $\mathcal{P}X$ , the subgroup generated by a subset, the convex hull and the radical of an ideal are all examples; so is $S \mapsto S^{\perp\perp}$ for any Galois connection.

Example— The distribution monad

$DX$ is the set of finitely supported probability distributions on $X$ ; $Df$ pushes distributions forward; $\eta_X(x) = \delta_x$ (point mass); $\mu_X(\Phi)(x) = \sum_{\varphi} \Phi(\varphi)\, \varphi(x)$ averages a distribution of distributions. A Kleisli arrow $X \to DY$ is a Markov kernel — for finite $X, Y$ , a stochastic matrix — and Kleisli composition is the Chapman–Kolmogorov formula: the product of stochastic matrices (see Markov chains). Expectation $\mathbb{E} : D\R \to \R$ is an algebra; its associativity law is the tower property $\mathbb{E}[\mathbb{E}[Z \mid W]] = \mathbb{E}[Z]$ for finitely supported random variables. More generally every convex subset of a real vector space is a $D$ -algebra via barycentres — but so is every join-semilattice (send a distribution to the join of its support), so " $D$ -algebra" (also called a convex space) is broader than "convex set".

Example— Monads from adjunctions

Every adjunction gives a monad (proved below). The free group functor $F \dashv U : \cat{Grp} \to \cat{Set}$ gives the monad $UF$ sending $X$ to the set of reduced words in $X^{\pm 1}$ . For a ring $R$ , extension of scalars $R \otimes_{\Z} - \dashv U : R\text{-}\cat{Mod} \to \cat{Ab}$ gives the monad $R \otimes_{\Z} -$ on $\cat{Ab}$ , whose algebras are $R$ -modules. The discrete-space functor $\mathrm{Disc} \dashv U : \cat{Top} \to \cat{Set}$ gives the identity monad, since $U \circ \mathrm{Disc} = \mathrm{id}$ ; this will show that $\cat{Top}$ is not monadic over $\cat{Set}$ .

Example— A non-example: the wrong multiplication

Keep $\mathcal{P}$ and $\eta_X(x) = \{x\}$ but flatten by intersection, $\mu_X(\mathcal{S}) = \bigcap \mathcal{S}$ . The associativity law and the left unit law $\bigcap\{S\} = S$ hold (with the convention $\bigcap \varnothing = X$ ), but the right unit law fails: $\mu(\mathcal{P}\eta(\{0, 1\})) = \{0\} \cap \{1\} = \varnothing \neq \{0, 1\}$ . Nor is this $\mu$ natural: for a non-injective $f$ , $f[S_1 \cap S_2]$ can be smaller than $f[S_1] \cap f[S_2]$ . (The experiment below finds the unit-law counterexample by search.)

ProofH

Adjunctions, Kleisli and Eilenberg–Moore

Let $F : \mathcal{C} \to \mathcal{D}$ be left adjoint to $G : \mathcal{D} \to \mathcal{C}$ , with unit $\eta : \mathrm{id}_{\mathcal{C}} \Rightarrow GF$ and counit $\varepsilon : FG \Rightarrow \mathrm{id}_{\mathcal{D}}$ satisfying the triangle identities $\varepsilon_{FX} \circ F\eta_X = \mathrm{id}_{FX}$ and $G\varepsilon_B \circ \eta_{GB} = \mathrm{id}_{GB}$ .

Theorem— Theorem 1 (every adjunction induces a monad; Huber)

$(GF, \eta, G\varepsilon F)$ is a monad on $\mathcal{C}$ : its multiplication has components $\mu_X = G(\varepsilon_{FX}) : GFGFX \to GFX$ .

Proof

$\mu$ is natural because $\varepsilon$ is. Associativity. Naturality of $\varepsilon$ applied to the morphism $\varepsilon_{FX} : FGFX \to FX$ gives $\varepsilon_{FX} \circ FG(\varepsilon_{FX}) = \varepsilon_{FX} \circ \varepsilon_{FGFX}$ . Applying $G$ :

\mu_X \circ T\mu_X = G\varepsilon_{FX} \circ GFG\varepsilon_{FX} = G(\varepsilon_{FX} \circ FG\varepsilon_{FX}) = G(\varepsilon_{FX} \circ \varepsilon_{FGFX}) = \mu_X \circ \mu_{TX}.

Left unit. $\mu_X \circ \eta_{TX} = G\varepsilon_{FX} \circ \eta_{GFX} = \mathrm{id}$ by the second triangle identity at $B = FX$ . Right unit. $\mu_X \circ T\eta_X = G\varepsilon_{FX} \circ GF\eta_X = G(\varepsilon_{FX} \circ F\eta_X) = G(\mathrm{id}_{FX}) = \mathrm{id}$ by the first triangle identity.

∎

Now go the other way: start with a monad $(T, \eta, \mu)$ and look for adjunctions that induce it.

Theorem— Theorem 2 (the Kleisli adjunction; Kleisli 1965)

$\mathcal{C}_T$ is a category, $F_T$ and $U_T$ are functors, $F_T \dashv U_T$ , and the monad induced by this adjunction is $(T, \eta, \mu)$ .

Proof

Identities. For $f : A \to TB$ : $\eta_B \circ_T f = \mu_B \circ T\eta_B \circ f = f$ by the right unit law; and $f \circ_T \eta_A = \mu_B \circ Tf \circ \eta_A = \mu_B \circ \eta_{TB} \circ f = f$ by naturality of $\eta$ and the left unit law.

Associativity. For $f : A \to TB$ , $g : B \to TC$ , $h : C \to TD$ :

(h \circ_T g) \circ_T f = \mu_D \circ T\mu_D \circ T^2 h \circ Tg \circ f = \mu_D \circ \mu_{TD} \circ T^2 h \circ Tg \circ f = \mu_D \circ Th \circ \mu_C \circ Tg \circ f = h \circ_T (g \circ_T f),

using associativity of $\mu$ and then naturality of $\mu$ at $h$ ( $\mu_{TD} \circ T^2 h = Th \circ \mu_C$ ).

Functors. $F_T(k \circ h) = \eta \circ k \circ h = (\eta \circ k) \circ_T (\eta \circ h)$ by naturality of $\eta$ and the unit law; $U_T(g \circ_T f) = \mu \circ T\mu \circ T^2 g \circ Tf = \mu \circ \mu \circ T^2 g \circ Tf = \mu \circ Tg \circ \mu \circ Tf = U_T g \circ U_T f$ by the same two laws; identities are preserved by the unit laws.

Adjunction. $\mathcal{C}_T(F_T A, B) = \mathcal{C}(A, TB) = \mathcal{C}(A, U_T B)$ , and this identity bijection is natural in $A$ and $B$ (a direct check with the formulas above). Its unit is $\eta_A$ (the arrow corresponding to $\mathrm{id}^T_A$ ) and its counit at $B$ is the Kleisli arrow $\mathrm{id}_{TB} : TB \rightsquigarrow B$ .

The induced monad. $U_T F_T A = TA$ and $U_T F_T h = \mu_B \circ T\eta_B \circ Th = Th$ , so $U_T F_T = T$ ; the unit is $\eta$ ; and $U_T(\varepsilon_{F_T A}) = U_T(\mathrm{id}_{TA}) = \mu_A \circ T(\mathrm{id}_{TA}) = \mu_A$ .

∎

Theorem— Theorem 3 (the Eilenberg–Moore adjunction; Eilenberg and Moore 1965)

$F^T \dashv U^T : \mathcal{C}^T \to \mathcal{C}$ , and the monad induced by this adjunction is $(T, \eta, \mu)$ .

Proof

First, $(TX, \mu_X)$ is an algebra: the unit and associativity laws for it are the left unit law and the associativity law of the monad; and $Tf$ is an algebra map $(TX, \mu_X) \to (TY, \mu_Y)$ by naturality of $\mu$ . For an algebra $(A, a)$ define

\Phi : \mathcal{C}^T\big((TX, \mu_X), (A, a)\big) \to \mathcal{C}(X, A),\quad \Phi(f) = f \circ \eta_X; \qquad \Psi(g) = a \circ Tg .

$\Psi(g)$ is an algebra map: $a \circ Tg \circ \mu_X = a \circ \mu_A \circ T^2 g = a \circ Ta \circ T^2 g = a \circ T(a \circ Tg)$ (naturality of $\mu$ , then the associativity law of $a$ ). The maps are inverse: $\Phi\Psi(g) = a \circ Tg \circ \eta_X = a \circ \eta_A \circ g = g$ (naturality of $\eta$ , unit law of $a$ ), and for an algebra map $f$ , $\Psi\Phi(f) = a \circ Tf \circ T\eta_X = f \circ \mu_X \circ T\eta_X = f$ (algebra map, right unit law). Naturality in $X$ and $(A, a)$ is immediate. The unit of the adjunction is $\Phi(\mathrm{id}) = \eta_X$ , and the counit at $(A, a)$ is $\Psi(\mathrm{id}_A) = a$ , an algebra map $(TA, \mu_A) \to (A, a)$ . Finally $U^T F^T = T$ and $U^T \varepsilon_{F^T X} = \mu_X$ .

∎

So every monad arises from an adjunction, generally from many. The two constructions are the extreme ones.

Theorem— Theorem 4 (comparison functors)

Let $F \dashv G$ induce $T = GF$ . Then $K : \mathcal{D} \to \mathcal{C}^T$ , $K(B) = (GB, G\varepsilon_B)$ , $K(h) = Gh$ , is a functor with $U^T K = G$ and $K F = F^T$ . Likewise $L : \mathcal{C}_T \to \mathcal{D}$ , $L(A) = FA$ , $L(f) = \varepsilon_{FB} \circ Ff$ for $f : A \to GFB$ , is a functor with $L F_T = F$ and $G L = U_T$ . Each is the unique functor with these properties; hence the Kleisli adjunction is initial and the Eilenberg–Moore adjunction terminal among adjunctions inducing $T$ .

Proof

We check that $K$ is well defined. Unit law: $G\varepsilon_B \circ \eta_{GB} = \mathrm{id}$ (triangle identity). Associativity law: $G\varepsilon_B \circ T(G\varepsilon_B) = G(\varepsilon_B \circ FG\varepsilon_B) = G(\varepsilon_B \circ \varepsilon_{FGB}) = G\varepsilon_B \circ \mu_{GB}$ (naturality of $\varepsilon$ at $\varepsilon_B$ ). For $h : B \to B'$ , $Gh \circ G\varepsilon_B = G(\varepsilon_{B'} \circ FGh) = G\varepsilon_{B'} \circ T(Gh)$ , so $Gh$ is an algebra map. Clearly $U^T K = G$ , and $KFX = (GFX, G\varepsilon_{FX}) = (TX, \mu_X) = F^T X$ , with $KFf = Tf = F^T f$ . The checks for $L$ are similar (functoriality uses the triangle identity $\varepsilon_{FA} \circ F\eta_A = \mathrm{id}$ and naturality of $\varepsilon$ ). For uniqueness, see Mac Lane, Categories for the Working Mathematician, VI.3 Theorem 1 and VI.5 Theorem 3.

∎

Applied to the Eilenberg–Moore adjunction, the functor $L : \mathcal{C}_T \to \mathcal{C}^T$ sends $A$ to the free algebra $F^T A$ and $f : A \to TB$ to $\mu_B \circ Tf$ . It is fully faithful: on morphisms it is the bijection $\Psi : \mathcal{C}(A, TB) \cong \mathcal{C}^T(F^T A, F^T B)$ of Theorem 3. So the Kleisli category is (equivalent to) the full subcategory of free algebras. Whether it is all of $\mathcal{C}^T$ depends on the monad.

Theorem— Proposition 5 (Kleisli and Eilenberg–Moore can differ)

For the maybe monad, $\mathcal{C}_T \to \mathcal{C}^T$ is an equivalence. For the list monad, $\mathcal{C}_T$ and $\mathcal{C}^T \simeq \cat{Mon}$ are not equivalent by any functor.

Proof

Maybe. Every pointed set $(X, x_0)$ is isomorphic to the free algebra on $X \setminus \{x_0\}$ , so the fully faithful functor $\mathcal{C}_T \to \mathcal{C}^T$ is essentially surjective, hence an equivalence: sets and partial functions are equivalent to pointed sets.

List. An equivalence of categories preserves endomorphism monoids up to isomorphism (it is fully faithful). In $\cat{Mon}$ , the monoid $\Z/2$ has exactly two endomorphisms ( $1 \mapsto 0$ and $1 \mapsto 1$ ). In $\mathcal{C}_T$ , the endomorphisms of $A$ are the functions $A \to \mathrm{List}(A)$ : one if $A = \varnothing$ , infinitely many otherwise. So no object of $\mathcal{C}_T$ can correspond to $\Z/2$ .

∎

ExplanationH

Beck's monadicity theorem

Which adjunctions are "the Eilenberg–Moore one" up to equivalence? A parallel pair $f, g : A \rightrightarrows B$ in $\mathcal{D}$ is $G$ -split if $Gf, Gg$ has a split coequaliser in $\mathcal{C}$ : a morphism $e : GB \to Z$ with $e \circ Gf = e \circ Gg$ , together with $s : Z \to GB$ and $t : GB \to GA$ such that $e \circ s = \mathrm{id}_Z$ , $Gf \circ t = \mathrm{id}_{GB}$ and $Gg \circ t = s \circ e$ . (Split coequalisers are coequalisers, and are preserved by every functor.)

Theorem— Beck's monadicity theorem (Beck 1967)

A functor $G : \mathcal{D} \to \mathcal{C}$ is monadic if and only if

$G$ has a left adjoint,
$G$ reflects isomorphisms, and
$\mathcal{D}$ has coequalisers of $G$ -split pairs, and $G$ preserves them.

The proof constructs a left adjoint to the comparison functor $K$ by sending an algebra $(A, a)$ to the coequaliser in $\mathcal{D}$ of the $G$ -split pair $F a, \varepsilon_{FA} : FGFA \rightrightarrows FA$ (every algebra is canonically a coequaliser of free algebras), and then shows that unit and counit are isomorphisms. Full proofs: Mac Lane, CWM VI.7; Riehl, Category Theory in Context, Theorem 5.5.1. Mathlib proves it (cited in the formal section).

Example— Groups are monadic over Set

$U : \cat{Grp} \to \cat{Set}$ has the free-group left adjoint, and a bijective homomorphism is an isomorphism, so $U$ reflects isomorphisms. Sketch of condition 3. Let $f, g : H \rightrightarrows K$ be homomorphisms with a split coequaliser $e : K \to Z$ of sets, with $s, t$ as above. If $e(x) = e(y)$ , then with $h = t(x)$ and $h' = t(y)$ we get $x = f(h)$ , $g(h) = s(e(x)) = s(e(y)) = g(h')$ and $y = f(h')$ . So the relation $e(x) = e(y)$ is the composite of the relation $R = \{(f(h), g(h))\}$ with its converse. $R$ is the image of the homomorphism $(f, g) : H \to K \times K$ , hence a subgroup of $K \times K$ , and composites and converses of subgroups of $K \times K$ are again subgroups. So $\ker e$ is a congruence on $K$ , $Z$ carries a unique group structure making $e$ a homomorphism, and one checks that $e$ is then a coequaliser of $f, g$ in $\cat{Grp}$ , preserved by $U$ . By Beck, $\cat{Grp} \simeq \cat{Set}^{UF}$ .

The same argument (or Linton's theorem that every variety of universal algebras is monadic) applies to $\cat{Ab}$ , $\cat{Ring}$ , $R\text{-}\cat{Mod}$ and $\cat{Mon}$ . The category of compact Hausdorff spaces is monadic over $\cat{Set}$ too, via the ultrafilter monad (Manes 1969) — although it is not a variety of finitary algebras.

Example— Topological spaces are not monadic over Set

The left adjoint of $U : \cat{Top} \to \cat{Set}$ is the discrete-space functor, so the induced monad is the identity monad, whose algebras are just sets (the unit law forces $a = \mathrm{id}$ ). The comparison functor $\cat{Top} \to \cat{Set}$ is $U$ itself, and it is not an equivalence: the identity map from a two-point discrete space to a two-point indiscrete space is continuous and bijective but not a homeomorphism, so $U$ does not reflect isomorphisms (condition 2 fails). The same argument shows that posets are not monadic over $\cat{Set}$ .

Example— Monads in programming (Moggi)

Model a programming language whose programs may have effects by a monad $T$ on a category of types: a program from $A$ to $B$ is a Kleisli arrow $A \to TB$ , and running programs in sequence is Kleisli composition. Exceptions: $TB = B + E$ . Nondeterminism: $TB = \mathcal{P}_{\mathrm{fin}}B$ or $\mathrm{List}(B)$ . Global state: $TB = (B \times S)^S$ . Output to a log: $TB = M \times B$ for a monoid $M$ . Probabilistic choice: $TB = DB$ . Moggi (1989, 1991) made this precise; Wadler brought it into functional programming, and in Haskell return is $\eta$ and >>= (bind) is Kleisli extension: $f : A \to TB$ extends to $f^* = \mu_B \circ Tf : TA \to TB$ . A monad can equivalently be given as a Kleisli triple $(T, \eta, (-)^*)$ satisfying $\eta^* = \mathrm{id}$ , $f^* \circ \eta = f$ and $g^* \circ f^* = (g^* \circ f)^*$ — which are exactly the three Kleisli category laws, i.e. Haskell's "monad laws". The monads came from algebra and topology; programming found them afterwards.

Formal mathematicsF

Monads in Lean

The Lean module works at two levels. First, with plain functions on types, it checks the monad and Kleisli laws for lists by induction, and proves in full that list-algebras are monoids:

list_monad_lawsLean 4Proved here from basic factsFormally verified

/-- **The list monad satisfies the monad laws.** Here `T X = List X`, the unit `η` sends `x` to
the one-element list `[x]`, and the multiplication `μ` flattens a list of lists.
1. associativity `μ ∘ Tμ = μ ∘ μT`: flattening the inner lists first, or the outer list first,
   gives the same list;
2. left unit `μ ∘ ηT = id`: flattening `[xs]` gives `xs`;
3. right unit `μ ∘ Tη = id`: flattening `[[x₁], …, [xₙ]]` gives `[x₁, …, xₙ]`.
Each law is proved by induction on the outer list. -/
theorem list_monad_laws {α : Type u} :
    (∀ xsss : List (List (List α)), (xsss.map List.flatten).flatten = xsss.flatten.flatten) ∧
    (∀ xs : List α, [xs].flatten = xs) ∧
    (∀ xs : List α, (xs.map fun x => [x]).flatten = xs) := by
  refine ⟨fun xsss => ?_, fun xs => by simp, fun xs => ?_⟩
  · induction xsss with
    | nil => rfl
    | cons xss rest ih =>
      simp only [List.map_cons, List.flatten_cons, List.flatten_append, ih]
  · induction xs with
    | nil => rfl
    | cons x rest ih => simp only [List.map_cons, List.flatten_cons, ih, List.singleton_append]

Axioms used: propextformal/Lumenary/Monads.leanTry it in the Lean web editor

listKleisliLean 4Formally verified

/-- **Kleisli composition for the list monad.** A Kleisli arrow `α → List β` is a
"many-valued function". To compose `f : α → List β` with `g : β → List γ`, apply `g` to every
output of `f` and flatten: in categorical notation `μ ∘ T g ∘ f`. -/
def listKleisli {α : Type u} {β : Type v} {γ : Type w} (f : α → List β) (g : β → List γ) :
    α → List γ :=
  fun a => (f a).flatMap g

Axioms used: No axiomsformal/Lumenary/Monads.leanTry it in the Lean web editor

list_kleisli_lawsLean 4Proved here from basic factsFormally verified

/-- **The Kleisli category of the list monad is a category.** Kleisli composition is associative,
and `η = fun a => [a]` is a two-sided identity. Associativity is core Lean's `List.flatMap_assoc`;
the identity laws are short computations. -/
theorem list_kleisli_laws {α β γ δ : Type u} (f : α → List β) (g : β → List γ)
    (h : γ → List δ) :
    listKleisli (listKleisli f g) h = listKleisli f (listKleisli g h) ∧
    listKleisli (fun a => [a]) f = f ∧
    listKleisli f (fun b => [b]) = f := by
  refine ⟨?_, ?_, ?_⟩
  · funext a
    exact List.flatMap_assoc
  · funext a
    simp [listKleisli]
  · funext a
    simp [listKleisli]

Axioms used: propext, Quot.soundformal/Lumenary/Monads.leanTry it in the Lean web editor

A list algebra is an evaluation map with the two laws. The key lemma is the human proof's first step: an algebra is determined by evaluating two-element lists.

ListAlgebraLean 4Formally verified

/-- An **algebra for the list monad** on a type `X`: an evaluation map `act : List X → X` such
that evaluating a one-element list returns its element (`act ∘ η = id`), and evaluating a list of
lists "inside first" or "flatten first" agrees (`act ∘ T act = act ∘ μ`). -/
structure ListAlgebra (X : Type u) where
  /-- Evaluate a list of elements to a single element. -/
  act : List X → X
  /-- The unit law `act [x] = x`. -/
  unit : ∀ x : X, act [x] = x
  /-- The associativity law: evaluate the inner lists first, or flatten first. -/
  assoc : ∀ xss : List (List X), act (xss.map act) = act xss.flatten

Axioms used: No axiomsformal/Lumenary/Monads.leanTry it in the Lean web editor

act_consLean 4Proved here from basic factsFormally verified

/-- In a list algebra, evaluating `x :: xs` is the same as evaluating the two-element list
`[x, act xs]`:
`act [x, act xs] = act [act [x], act xs] = act (flatten [[x], xs]) = act (x :: xs)`,
using the unit law and then the associativity law. -/
theorem act_cons (A : ListAlgebra X) (x : X) (xs : List X) :
    A.act (x :: xs) = A.act [x, A.act xs] := by
  calc A.act (x :: xs) = A.act ([[x], xs].flatten) := by simp
    _ = A.act ([[x], xs].map A.act) := (A.assoc [[x], xs]).symm
    _ = A.act [x, A.act xs] := by simp [A.unit]

Axioms used: propextformal/Lumenary/Monads.leanTry it in the Lean web editor

toMonoidLean 4Formally verified

/-- **Every list algebra is a monoid.** Multiply by evaluating two-element lists,
`x * y = act [x, y]`, and take `1 = act []`. The monoid laws follow from the algebra laws:
for example `(x * y) * z = act [act [x, y], act [z]] = act [x, y, z]`, and likewise
`x * (y * z) = act [x, y, z]`. -/
@[instance_reducible]
def toMonoid (A : ListAlgebra X) : Monoid X where
  mul x y := A.act [x, y]
  one := A.act []
  mul_assoc x y z := by
    show A.act [A.act [x, y], z] = A.act [x, A.act [y, z]]
    have h₁ : A.act [A.act [x, y], z] = A.act [x, y, z] := by
      calc A.act [A.act [x, y], z] = A.act ([[x, y], [z]].map A.act) := by simp [A.unit]
        _ = A.act [x, y, z] := by rw [A.assoc]; simp
    have h₂ : A.act [x, A.act [y, z]] = A.act [x, y, z] := by
      calc A.act [x, A.act [y, z]] = A.act ([[x], [y, z]].map A.act) := by simp [A.unit]
        _ = A.act [x, y, z] := by rw [A.assoc]; simp
    rw [h₁, h₂]
  one_mul x := by
    show A.act [A.act [], x] = x
    calc A.act [A.act [], x] = A.act ([[], [x]].map A.act) := by simp [A.unit]
      _ = x := by rw [A.assoc]; simp [A.unit]
  mul_one x := by
    show A.act [x, A.act []] = x
    calc A.act [x, A.act []] = A.act ([[x], []].map A.act) := by simp [A.unit]
      _ = x := by rw [A.assoc]; simp [A.unit]

Axioms used: propextformal/Lumenary/Monads.leanTry it in the Lean web editor

ofMonoidLean 4Formally verified

/-- **Every monoid is a list algebra**: evaluate a list by multiplying it out, `act = List.prod`.
The unit law is `List.prod_singleton` and the associativity law is core Lean's
`List.prod_flatten` (multiplying blockwise, then multiplying the results, is multiplying
everything). -/
def ofMonoid (M : Type u) [Monoid M] : ListAlgebra M where
  act := List.prod
  unit _ := List.prod_singleton
  assoc _ := List.prod_flatten.symm

Axioms used: propextformal/Lumenary/Monads.leanTry it in the Lean web editor

act_eq_prodLean 4Proved here from basic factsFormally verified

/-- **A list algebra is determined by its binary multiplication and unit.** Evaluating any list
is multiplying it out in the monoid `A.toMonoid`. Proof by induction on the list, using
`act_cons` at each step. -/
theorem act_eq_prod (A : ListAlgebra X) (xs : List X) :
    A.act xs = @List.prod X A.toMonoid.toMul A.toMonoid.toOne xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    rw [act_cons, ih]
    rfl

Axioms used: propextformal/Lumenary/Monads.leanTry it in the Lean web editor

The theorem "algebras for the list monad are exactly monoids" is then an explicit bijection between the two kinds of structure on a type:

listAlgebraEquivMonoidLean 4Proved here from basic factsFormally verified

/-- **Algebras for the list monad are exactly monoids.** On any type `X`, list-algebra structures
correspond bijectively to monoid structures: send an algebra to its binary multiplication, and a
monoid to `List.prod`. Going around one way uses `act_eq_prod`; going around the other way only
has to check that the multiplications agree (`Monoid.ext`), and `List.prod [x, y] = x * (y * 1)`. -/
def listAlgebraEquivMonoid (X : Type u) : ListAlgebra X ≃ Monoid X where
  toFun A := A.toMonoid
  invFun m := @ListAlgebra.ofMonoid X m
  left_inv A := by
    ext xs
    exact (A.act_eq_prod xs).symm
  right_inv m := by
    let _ := m
    apply Monoid.ext
    funext x y
    show List.prod [x, y] = x * y
    simp

Axioms used: propext, Quot.soundformal/Lumenary/Monads.leanTry it in the Lean web editor

optionAlgebraEquivLean 4Proved here from basic factsFormally verified

/-- **Algebras for the maybe monad are exactly pointed sets.** An `Option`-algebra on `X` is
determined by where it sends `none`, and every choice of base point gives an algebra (with
`act = fun o => o.getD a`; the associativity law then holds automatically, by checking the three
shapes `none`, `some none`, `some (some x)`). -/
def optionAlgebraEquiv (X : Type u) : OptionAlgebra X ≃ X where
  toFun A := A.act none
  invFun a :=
    { act := fun o => o.getD a
      unit := fun _ => rfl
      assoc := by
        intro oo
        rcases oo with _ | _ | x <;> rfl }
  left_inv A := by
    rcases A with ⟨act, unit, assoc⟩
    have h : (fun o => o.getD (act none)) = act := by
      funext o
      cases o with
      | none => rfl
      | some x => exact (unit x).symm
    simp only [OptionAlgebra.mk.injEq]
    exact h
  right_inv _ := rfl

Axioms used: propext, Quot.soundformal/Lumenary/Monads.leanTry it in the Lean web editor

Second, Mathlib has the general theory: CategoryTheory.Monad, the Eilenberg–Moore category Monad.Algebra, Kleisli, Adjunction.toMonad, the comparison functor and Beck's theorem. The following are one-line applications of Mathlib, recording Theorems 1–4 and Beck's theorem in Mathlib's language (note that Mathlib writes composition in diagrammatic order: F ⋙ G is $G \circ F$ ):

adjunction_monadLean 4Applies a library theoremFormally verified

/-- **Every adjunction induces a monad.** For `F ⊣ G` with unit `η` and counit `ε`, the monad
`h.toMonad` (Mathlib's `Adjunction.toMonad`) has underlying functor `G ∘ F` (written `F ⋙ G` in
diagrammatic order), unit `η`, and multiplication `μ_X = G(ε_{F X})`. -/
theorem adjunction_monad {F : C ⥤ D} {G : D ⥤ C} (h : F ⊣ G) (X : C) :
    (h.toMonad : C ⥤ C) = F ⋙ G ∧ h.toMonad.η = h.unit ∧
      h.toMonad.μ.app X = G.map (h.counit.app (F.obj X)) :=
  ⟨rfl, rfl, rfl⟩