open import Cat.Functor.FullSubcategory
open import Cat.Displayed.Univalence
open import Cat.Functor.Conservative
open import Cat.Functor.Properties
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Displayed.Morphism
import Cat.Functor.Reasoning
import Cat.Reasoning

open _=>_ using (is-natural)
open Displayed
open Total-hom
open Functor

module Cat.Diagram.Monad where

module _ {o h : _} (C : Precategory o h) where
private module C = Cat.Reasoning C


A monad on a category 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 equipped with a unit natural transformation and a multiplication

  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β   = M .Fβ
Mβ   = M .Fβ
M-id = M .F-id
M-β  = M .F-β
open unit using (Ξ·) public
open mult renaming (Ξ· to ΞΌ) using () public


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

    field
left-ident  : β {x} β ΞΌ x C.β Mβ (Ξ· x) β‘ C.id
right-ident : β {x} β ΞΌ x C.β Ξ· (Mβ x) β‘ C.id
mult-assoc  : β {x} β ΞΌ x C.β Mβ (ΞΌ x) β‘ ΞΌ x C.β ΞΌ (Mβ x)


One way of interpreting a monad 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 is given by a choice of object and a morphism

  record Algebra-on (M : Monad) (ob : C.Ob) : Type (o β h) where
no-eta-equality

field
Ξ½ : C.Hom (Mβ ob) ob


This morphism must satisfy equations categorifying those which define a monoid action. If we think of as specifying a signature of effects, then v-unit says that the unit has no effects, and v-mult says that, given two layers it doesnβt matter whether you first join then evaluate, or evaluate twice.

      Ξ½-unit : Ξ½ C.β Ξ· ob β‘ C.id
Ξ½-mult : Ξ½ C.β Mβ Ξ½ β‘ Ξ½ C.β ΞΌ ob

  Algebra-on-pathp
: β {M} {X Y} (p : X β‘ Y) {A : Algebra-on M X} {B : Algebra-on M Y}
β PathP (Ξ» i β C.Hom (Monad.Mβ M (p i)) (p i)) (A .Algebra-on.Ξ½) (B .Algebra-on.Ξ½)
β PathP (Ξ» i β Algebra-on M (p i)) A B
Algebra-on-pathp over mults i .Algebra-on.Ξ½ = mults i
Algebra-on-pathp {M} over {A} {B} mults i .Algebra-on.Ξ½-unit =
is-propβpathp (Ξ» i β C.Hom-set _ _ (mults i C.β M.Ξ· _) (C.id {x = over i}))
(A .Algebra-on.Ξ½-unit) (B .Algebra-on.Ξ½-unit) i
where module M = Monad M
Algebra-on-pathp {M} over {A} {B} mults i .Algebra-on.Ξ½-mult =
is-propβpathp (Ξ» i β C.Hom-set _ _ (mults i C.β M.Mβ (mults i)) (mults i C.β M.ΞΌ _))
(A .Algebra-on.Ξ½-mult) (B .Algebra-on.Ξ½-mult) i
where module M = Monad M

instance
Extensional-Algebra-on
: β {o β βr} {C : Precategory o β} {M : Monad C}
β (let open Precategory C)
β β {X}
β β¦ sa : Extensional (Hom (Monad.Mβ M X) X) βr β¦
β Extensional (Algebra-on C M X) βr
Extensional-Algebra-on {C = C} β¦ sa β¦ =
injectionβextensional! (Algebra-on-pathp C refl) sa


# Eilenberg-Moore categoryπ

If we take a monad as the signature of an (algebraic) theory, and 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β.

We can be more specific about βcommuting with the algebrasβ by drawing a square: A map in the ambient category is a homomorphism of when the square below commutes.

We can assemble and their homomorphisms into a displayed category over the type of objects over some consists of all possible algebra structures on and the type of morphisms over are proofs that is an homomorphism.

module _ {o β} {C : Precategory o β} (M : Monad C) where
private
module C = Cat.Reasoning C
module MR = Cat.Functor.Reasoning M.M
open M hiding (M)
open Algebra-on


  Monad-algebras : Displayed C (o β β) β
Monad-algebras .Ob[_] X = Algebra-on C M X
Monad-algebras .Hom[_] f Ξ± Ξ² = f C.β Ξ± .Ξ½ β‘ Ξ² .Ξ½ C.β Mβ f
Monad-algebras .Hom[_]-set _ _ _ = hlevel 2


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

  Monad-algebras .id' {X} {Ξ±} =
C.id C.β Ξ± .Ξ½    β‘β¨ C.idl _ β C.intror M-id β©β‘
Ξ± .Ξ½ C.β Mβ C.id β
Monad-algebras ._β'_ {_} {_} {_} {Ξ±} {Ξ²} {Ξ³} {f = f} {g = g} p q =
(f C.β g) C.β Ξ± .Ξ½       β‘β¨ C.pullr q β©β‘
f C.β Ξ² .Ξ½ C.β Mβ g      β‘β¨ C.pulll p β©β‘
(Ξ³ .Ξ½ C.β Mβ f) C.β Mβ g β‘β¨ C.pullr (sym (M-β _ _)) β©β‘
Ξ³ .Ξ½ C.β Mβ (f C.β g)    β

The equations all hold trivially, as the type of displayed morphisms over is a proposition.
  Monad-algebras .idr' _ = prop!
Monad-algebras .assoc' _ _ _ = prop!


The total category of this displayed category is referred to as the Eilenberg Moore category of

  Eilenberg-Moore : Precategory (o β β) β

private
module EM = Cat.Reasoning Eilenberg-Moore

Algebra : Type _
Algebra = EM.Ob

Algebra-hom : (X Y : Algebra) β Type _
Algebra-hom X Y = EM.Hom X Y

module _ {o β} {C : Precategory o β} {M : Monad C} where
private
module C = Cat.Reasoning C
module MR = Cat.Functor.Reasoning M.M
module EM = Cat.Reasoning (Eilenberg-Moore M)
open M hiding (M)
open Algebra-on

instance
Extensional-Algebra-Hom
: β {βr} {a b} {A : Algebra-on C M a} {B : Algebra-on C M b}
β β¦ sa : Extensional (C.Hom a b) βr β¦
β Extensional (Algebra-hom M (a , A) (b , B)) βr
Extensional-Algebra-Hom β¦ sa β¦ = injectionβextensional!
(Ξ» p β total-hom-path (Monad-algebras M) p prop!) sa


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-EM : Functor (Eilenberg-Moore M) C


This functor is faithful as the maps in the Eilenberg-Moore category are structured maps of

  Forget-EM-is-faithful : is-faithful Forget-EM
Forget-EM-is-faithful = ext


Moreover, this functor is conservative. This follows from a bit of routine algebra.

  Forget-EM-is-conservative : is-conservative Forget-EM
Forget-EM-is-conservative {X , Ξ±} {Y , Ξ²} {f = f} f-inv =
EM.make-invertible f-alg-inv (ext invl) (ext invr)
where
open C.is-invertible f-inv

f-alg-inv : Algebra-hom M (Y , Ξ²) (X , Ξ±)
f-alg-inv .hom = inv
f-alg-inv .preserves =
inv C.β Ξ² .Ξ½                                 β‘β¨ apβ C._β_ refl (C.intror (MR.annihilate invl)) β©β‘
inv C.β Ξ² .Ξ½ C.β Mβ (f .hom) C.β M.Mβ inv    β‘β¨ apβ C._β_ refl (C.extendl (sym (f .preserves))) β©β‘
inv C.β f .hom C.β Ξ± .Ξ½ C.β M.Mβ inv         β‘β¨ C.cancell invr β©β‘
Ξ± .Ξ½ C.β Mβ inv                              β


### Univalenceπ

The displayed category of monad algebras is a displayed univalent category. This is relatively straightforward to show: first, note that the type of displayed isomorphisms must be a proposition. Next, we can perform a bit of simple algebra to show that the actions of two isomorphic are, in fact, equal.

  Monad-algebras-is-category : is-category-displayed (Monad-algebras M)
Monad-algebras-is-category f Ξ± (Ξ² , p) (Ξ³ , q) =
Ξ£-prop-path (Ξ» _ _ _ β ext prop!) $ext$
Ξ² .Ξ½                         β‘β¨ C.introl invl β©β‘
(to C.β from) C.β Ξ² .Ξ½       β‘β¨ C.pullr (p .from') β©β‘
to C.β Ξ± .Ξ½ C.β Mβ from      β‘β¨ C.pulll (q .to') β©β‘
(Ξ³ .Ξ½ C.β Mβ to) C.β Mβ from β‘β¨ MR.cancelr invl β©β‘
Ξ³ .Ξ½                         β
where
open C._β_ f


By univalence of total categories, we can immediately deduce that the Eilenberg-Moore category inherits univalence from the base category.

  EM-is-category : is-category C β is-category (Eilenberg-Moore M)
EM-is-category cat =


## Free algebrasπ

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

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

  Free-EM : Functor C (Eilenberg-Moore M)
Free-EM .Fβ A .fst = Mβ A
Free-EM .Fβ A .snd .Ξ½ = ΞΌ A
Free-EM .Fβ A .snd .Ξ½-mult = mult-assoc
Free-EM .Fβ A .snd .Ξ½-unit = right-ident


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

  Free-EM .Fβ f .hom = Mβ f
Free-EM .Fβ f .preserves = sym $mult.is-natural _ _ _ Free-EM .F-id = ext M-id Free-EM .F-β f g = ext (M-β f g)  This is a free construction in the precise sense of the word: itβs the left adjoint to the functor Forget-EM, so in particular it provides a systematic, universal way of mapping from to  open _β£_ Free-EMβ£Forget-EM : Free-EM β£ Forget-EM Free-EMβ£Forget-EM .unit = NT M.Ξ· M.unit.is-natural Free-EMβ£Forget-EM .counit = NT (Ξ» x β total-hom (x .snd .Ξ½) (sym (x .snd .Ξ½-mult))) (Ξ» x y f β ext (sym (f .preserves))) Free-EMβ£Forget-EM .zig = ext left-ident Free-EMβ£Forget-EM .zag {x} = x .snd .Ξ½-unit  The full subcategory of free is often referred to as the Kleisli category of module _ {o β} {C : Precategory o β} (M : Monad C) where private module C = Cat.Reasoning C module M = Monad M module MR = Cat.Functor.Reasoning M.M open M hiding (M) open Algebra-on   Kleisli : Precategory (o β β) β Kleisli = Essential-image (Free-EM {M = M})  If is univalent then so is the Kleisli category as it is a full subcategory of a univalent category. module _ {o β} {C : Precategory o β} {M : Monad C} where private module C = Cat.Reasoning C module M = Monad M module MR = Cat.Functor.Reasoning M.M open M hiding (M) open Algebra-on   Kleisli-is-category : is-category C β is-category (Kleisli M) Kleisli-is-category cat = Essential-image-is-category Free-EM (EM-is-category cat)  As the Kleisli category is a full subcategory, there is a canonical full inclusion into the Eilenberg-Moore category.  KleisliβEM : Functor (Kleisli M) (Eilenberg-Moore M) KleisliβEM = Forget-full-subcat KleisliβEM-is-ff : is-fully-faithful KleisliβEM KleisliβEM-is-ff = id-equiv  Additionally, the free/forgetful adjunction between and the Eilenberg-Moore category can be restricted to the Kleisli category.  Forget-Kleisli : Functor (Kleisli M) C Forget-Kleisli = Forget-EM Fβ KleisliβEM Free-Kleisli : Functor C (Kleisli M) Free-Kleisli = Essential-inc Free-EM Free-Kleisliβ£Forget-Kleisli : Free-Kleisli β£ Forget-Kleisli Free-Kleisliβ£Forget-Kleisli ._β£_.unit ._=>_.Ξ· = Ξ· Free-Kleisliβ£Forget-Kleisli ._β£_.unit .is-natural = unit.is-natural Free-Kleisliβ£Forget-Kleisli ._β£_.counit ._=>_.Ξ· ((X , Ξ±) , free) = total-hom (Ξ± .Ξ½) (sym (Ξ± .Ξ½-mult)) Free-Kleisliβ£Forget-Kleisli ._β£_.counit .is-natural _ _ f = ext (sym (f .preserves)) Free-Kleisliβ£Forget-Kleisli ._β£_.zig = ext left-ident Free-Kleisliβ£Forget-Kleisli ._β£_.zag {(X , Ξ±) , free} = Ξ± . Ξ½-unit  Note that the forgetful functor from the Kleisli category of to is also faithful and conservative.  Forget-Kleisli-is-faithful : is-faithful Forget-Kleisli Forget-Kleisli-is-faithful = Forget-EM-is-faithful Forget-Kleisli-is-conservative : is-conservative Forget-Kleisli Forget-Kleisli-is-conservative f-inv = super-invβsub-inv _$
Forget-EM-is-conservative f-inv

module _ {o h : _} {C : Precategory o h} {M N : Monad C} where
private
module C = Cat.Reasoning C

: (p0 : β x β M.Mβ x β‘ N.Mβ x)
β (p1 : β {x y} (f : C.Hom x y) β PathP (Ξ» i β C.Hom (p0 x i) (p0 y i)) (M.Mβ f) (N.Mβ f))
β (β x β PathP (Ξ» i β C.Hom x (p0 x i)) (M.Ξ· x) (N.Ξ· x))
β (β x β PathP (Ξ» i β C.Hom (p0 (p0 x i) i) (p0 x i)) (M.ΞΌ x) (N.ΞΌ x))
β M β‘ N
Monad-path p0 p1 punit pmult = path where
M=N : M.M β‘ N.M
M=N = Functor-path p0 p1

path : M β‘ N
path i .Monad.M = M=N i
Nat-pathp refl M=N {a = M.unit} {b = N.unit} punit i
Nat-pathp (apβ _Fβ_ M=N M=N) M=N {a = M.mult} {b = N.mult} pmult i
path i .Monad.left-ident {x = x} =
is-propβpathp (Ξ» i β C.Hom-set (p0 x i) (p0 x i) (pmult x i C.β p1 (punit x i) i) C.id)
M.left-ident
N.left-ident i
path i .Monad.right-ident {x = x} =
is-propβpathp (Ξ» i β C.Hom-set (p0 x i) (p0 x i) (pmult x i C.β punit (p0 x i) i) C.id)
M.right-ident
N.right-ident i