open import Cat.Functor.Adjoint open import Cat.Functor.Base open import Cat.Prelude open Functor open _=>_ module Cat.Diagram.Monad {o h : _} (C : Precategory o h) where import Cat.Reasoning C as C

# Monadsπ

A **monad on a category**
$\ca{C}$
is one way of categorifying the concept of monoid. Specifically, rather than living
in a monoidal category, a monad lives in a bicategory. Here, we concern
ourselves with the case of monads in the bicategory of categories, so
that we may say: A monad is an endofunctor
$M$,
equipped with a unit natural transformation
$\id{Id} \To M$,
and a multiplication
$(M \circ M) \To M$.

record Monad : Type (o β h) where no-eta-equality field M : Functor C C unit : Id => M mult : (M Fβ M) => M module unit = _=>_ unit module mult = _=>_ mult Mβ = Fβ M Mβ = Fβ M M-id = F-id M M-β = F-β M

Furthermore, these natural transformations must satisfy identity and associativity laws exactly analogous to those of a monoid.

field left-ident : β {x} β mult.Ξ· x C.β Mβ (unit.Ξ· x) β‘ C.id right-ident : β {x} β mult.Ξ· x C.β unit.Ξ· (Mβ x) β‘ C.id field mult-assoc : β {x} β mult.Ξ· x C.β Mβ (mult.Ξ· x) β‘ mult.Ξ· x C.β mult.Ξ· (Mβ x)

# Algebras over a monadπ

One way of interpreting a monad
$M$
is as giving a *signature* for an algebraic theory. For instance,
the free monoid monad describes the signature for the theory of monoids,
and the free group monad describes
the theory of groups.

Under this light, an **algebra over a monad** is a way
of *evaluating* the abstract operations given by a monadic
expression to a concrete value. Formally, an algebra for
$M$
is given by a choice of object
$A$
and a morphism
$\nu : M(A) \to A$.

record Algebra-on (M : Monad) (ob : C.Ob) : Type (o β h) where no-eta-equality open Monad M field Ξ½ : C.Hom (Mβ ob) ob

This morphism must satisfy equations categorifying those which define
a monoid action. If we think of
$M$
as specifying a signature of *effects*, then `v-unit`

says that the unit has no effects, and `v-mult`

says that, given two layers
$M(M(A))$,
it doesnβt matter whether you first join then evaluate, or evaluate
twice.

Ξ½-unit : Ξ½ C.β unit.Ξ· ob β‘ C.id Ξ½-mult : Ξ½ C.β Mβ Ξ½ β‘ Ξ½ C.β mult.Ξ· ob Algebra : Monad β Type (o β h) Algebra M = Ξ£ _ (Algebra-on M)

# Eilenberg-Moore Categoryπ

If we take a monad
$M$
as the signature of an (algebraic) theory, and
$M$-algebras
as giving *models* of that theory, then we can ask (like with
everything in category theory): Are there maps between interpretations?
The answer (as always!) is yes: An algebra
homomorphism is a map of the underlying objects which
βcommutes with the algebrasβ.

record Algebra-hom (M : Monad) (X Y : Algebra M) : Type (o β h) where no-eta-equality private module X = Algebra-on (X .snd) module Y = Algebra-on (Y .snd) open Monad M field morphism : C.Hom (X .fst) (Y .fst) commutes : morphism C.β X.Ξ½ β‘ Y.Ξ½ C.β Mβ morphism open Algebra-hom

We can be more specific about βcommuting with the algebrasβ by drawing a square: A map $m : X \to Y$ in the ambient category is a homomorphism of $M$-algebras when the square below commutes.

Since commutes is an identification between morphisms, it inhabits a proposition (because Hom-sets are sets), equality of algebra homomorphisms only depends on an equality of their underlying morphisms.

Algebra-hom-path : {M : Monad} {X Y : Algebra M} {F G : Algebra-hom M X Y} β morphism F β‘ morphism G β F β‘ G Algebra-hom-path x i .morphism = x i Algebra-hom-path {M = M} {X} {Y} {F} {G} x i .commutes = is-propβpathp (Ξ» i β C.Hom-set _ _ (x i C.β X .snd .Algebra-on.Ξ½) (Y .snd .Algebra-on.Ξ½ C.β Monad.Mβ M (x i))) (F .commutes) (G .commutes) i

Since the square we drew above commutes for the identity morphism,
and we can show that the composite of two algebra homomorphisms is an
algebra homomorphism, they assemble into a category: The
**Eilenberg-Moore** category of
$M$.

module _ (M : Monad) where private module M = Monad M open M hiding (M) open Precategory open Algebra-on Eilenberg-Moore : Precategory _ _ Eilenberg-Moore .Ob = Algebra M Eilenberg-Moore .Hom X Y = Algebra-hom M X Y

Defining the identity and composition maps is mostly an exercise in categorical yoga:

Eilenberg-Moore .id {o , x} .morphism = C.id Eilenberg-Moore .id {o , x} .commutes = C.id C.β Ξ½ x β‘β¨ C.id-comm-sym β©β‘ Ξ½ x C.β C.id β‘β¨ ap (C._β_ _) (sym M-id) β©β‘ Ξ½ x C.β Mβ C.id β Eilenberg-Moore ._β_ {_ , x} {_ , y} {_ , z} F G .morphism = morphism F C.β morphism G Eilenberg-Moore ._β_ {_ , x} {_ , y} {_ , z} F G .commutes = (morphism F C.β morphism G) C.β Ξ½ x β‘β¨ C.extendr (commutes G) β©β‘ β morphism F C.β Ξ½ y β C.β Mβ (morphism G) β‘β¨ ap! (commutes F) β©β‘ (Ξ½ z C.β Mβ (morphism F)) C.β Mβ (morphism G) β‘β¨ C.pullr (sym (M-β _ _)) β©β‘ Ξ½ z C.β Mβ (morphism F C.β morphism G) β

## Because we have characterised equality of algebra homomorphisms as equality of their underlying maps, the Eilenberg-Moore category inherits the identity and associativity laws from its underlying category.

Eilenberg-Moore .idr f = Algebra-hom-path (C.idr (morphism f)) Eilenberg-Moore .idl f = Algebra-hom-path (C.idl (morphism f)) Eilenberg-Moore .assoc f g h = Algebra-hom-path (C.assoc _ _ _) Eilenberg-Moore .Hom-set X Y = is-hlevelβ 2 (IsoβEquiv eqv eβ»ΒΉ) (hlevel 2) where open C.HLevel-instance

By projecting the underlying object of the algebras, and the underlying morphisms of the homomorphisms between them, we can define a functor from Eilenberg-Moore back to the underlying category:

Forget : Functor Eilenberg-Moore C Forget .Fβ = fst Forget .Fβ = Algebra-hom.morphism Forget .F-id = refl Forget .F-β f g = refl

The lemma Algebra-hom-path says exactly that this functor is faithful.

Forget-is-faithful : is-faithful Forget Forget-is-faithful = Algebra-hom-path

## Free Algebrasπ

In exactly the same way that we may construct a *free group* by taking the
inhabitants of some set
$X$
as generating the βwordsβ of a group, we can, given an object
$A$
of the underlying category, build a **free
$M$-algebra**
on
$A$.
Keeping with our interpretation of monads as logical signatures, this is
the *syntactic model* of
$M$,
with a set of βneutralsβ chosen from the object
$A$.

This construction is a lot simpler to do in generality than in any
specific case: We can always turn
$A$
into an
$M$-algebra
by taking the underlying object to be
$M(A)$,
and the algebra map to be the monadic multiplication; The associativity
and unit laws of the monad *itself* become those of the
$M$-action.

Free : Functor C Eilenberg-Moore Free .Fβ A .fst = Mβ A Free .Fβ A .snd .Ξ½ = mult .Ξ· A Free .Fβ A .snd .Ξ½-mult = mult-assoc Free .Fβ A .snd .Ξ½-unit = right-ident

The construction of free $M$-algebras is furthermore functorial on the underlying objects; Since the monadic multiplication is a natural transformation $M\circ M \To M$, the naturality condition (drawn below) doubles as showing that the functorial action of $M$ can be taken as an algebraic action:

Free .Fβ f .morphism = Mβ f Free .Fβ f .commutes = sym $ mult.is-natural _ _ _ Free .F-id = Algebra-hom-path M-id Free .F-β f g = Algebra-hom-path (M-β f g)

This is a free construction in the precise sense of the word: itβs the left adjoint to the functor Forget, so in particular it provides a systematic, universal way of mapping from $\ca{C}$ to $\ca{C}^M$.

open _β£_ Freeβ£Forget : Free β£ Forget Freeβ£Forget .unit = NT M.unit.Ξ· M.unit.is-natural Freeβ£Forget .counit .Ξ· x = record { morphism = x .snd .Ξ½ ; commutes = sym (x .snd .Ξ½-mult) } Freeβ£Forget .counit .is-natural x y f = Algebra-hom-path (sym (commutes f)) Freeβ£Forget .zig = Algebra-hom-path left-ident Freeβ£Forget .zag {x} = x .snd .Ξ½-unit