module Cat.Instances.Monads where
Categories of monadsπ
The category of monads of a category consists of monads on and natural transformations preserving the monadic structure. In terms of the bicategory of monads in , a morphism in the 1-categorical version always has the identity functor as the underlying 1-cell. That is, this 1-category of monads on is the fibre of the displayed bicategory of monads in over
module _ {C : Precategory o h} where private module C = Cat.Reasoning C Endo : Precategory (o β h) (o β h) Endo = Cat[ C , C ] module Endo = Cat.Reasoning Endo Endo-β-functor : Functor (Endo ΓαΆ Endo) Endo Endo-β-functor = Fβ-functor module Endo-β = Functor Endo-β-functor
A monad homomorphism is a natural transformation preserving the unit and the multiplication In other words, the following two diagrams commute, where is the horizontal composition:
record Monad-hom (M N : Monad C) : Type (o β h) where no-eta-equality module M = Monad M module N = Monad N field nat : M.M => N.M open _=>_ nat public field pres-unit : nat βnt M.unit β‘ N.unit pres-mult : nat βnt M.mult β‘ N.mult βnt (nat β nat)
module _ {M N : Monad C} where private module M = Monad M module N = Monad N Monad-hom-path : (Ξ½ ΞΎ : Monad-hom M N) β Ξ½ .Monad-hom.nat β‘ ΞΎ .Monad-hom.nat β Ξ½ β‘ ΞΎ Monad-hom-path Ξ½ ΞΎ p i .Monad-hom.nat = p i Monad-hom-path Ξ½ ΞΎ p i .Monad-hom.pres-unit = is-propβpathp (Ξ» i β Nat-is-set (p i βnt M.unit) N.unit) (Ξ½ .Monad-hom.pres-unit) (ΞΎ .Monad-hom.pres-unit) i Monad-hom-path Ξ½ ΞΎ p i .Monad-hom.pres-mult = is-propβpathp (Ξ» i β Nat-is-set (p i βnt M.mult) (N.mult βnt (p i β p i))) (Ξ½ .Monad-hom.pres-mult) (ΞΎ .Monad-hom.pres-mult) i abstract instance H-Level-Monad-hom : β {n} β H-Level (Monad-hom M N) (2 + n) H-Level-Monad-hom = basic-instance 2 $ Isoβis-hlevel 2 eqv (hlevel 2) where unquoteDecl eqv = declare-record-iso eqv (quote Monad-hom) instance Extensional-Monad-hom : β {β} β¦ sa : Extensional (M.M => N.M) β β¦ β Extensional (Monad-hom M N) β Extensional-Monad-hom β¦ sa β¦ = injectionβextensional! {f = Monad-hom.nat} (Monad-hom-path _ _) sa Funlike-Monad-hom : Funlike (Monad-hom M N) β C β (Ξ» x β C .Hom (M.M # x) (N.M # x)) Funlike-Monad-hom ._#_ = Monad-hom.Ξ·
We have the identity and composition as expected.
monad-hom-id : β {M : Monad C} β Monad-hom M M monad-hom-id {M = _} .Monad-hom.nat = idnt monad-hom-id {M = _} .Monad-hom.pres-unit = Endo.idl _ monad-hom-id {M = M} .Monad-hom.pres-mult = let module M = Monad M in idnt βnt M.mult β‘β¨ Endo.id-comm-sym β©β‘ M.mult βnt idnt β‘Λβ¨ ap (M.mult βnt_) Endo-β.F-id β©β‘Λ M.mult βnt (idnt β idnt) β monad-hom-β : β {M N O : Monad C} β Monad-hom N O β Monad-hom M N β Monad-hom M O monad-hom-β {M = M} {N} {O} Ξ½ ΞΎ = mh where module M = Monad M module N = Monad N module O = Monad O module Ξ½ = Monad-hom Ξ½ module ΞΎ = Monad-hom ΞΎ mh : Monad-hom M O mh .Monad-hom.nat = Ξ½.nat βnt ΞΎ.nat mh .Monad-hom.pres-unit = (Ξ½.nat βnt ΞΎ.nat) βnt M.unit β‘Λβ¨ Endo.assoc Ξ½.nat ΞΎ.nat M.unit β©β‘Λ Ξ½.nat βnt (ΞΎ.nat βnt M.unit) β‘β¨ ap (Ξ½.nat βnt_) ΞΎ.pres-unit β©β‘ Ξ½.nat βnt N.unit β‘β¨ Ξ½.pres-unit β©β‘ O.unit β mh .Monad-hom.pres-mult = (Ξ½.nat βnt ΞΎ.nat) βnt M.mult β‘Λβ¨ Endo.assoc Ξ½.nat ΞΎ.nat M.mult β©β‘Λ Ξ½.nat βnt (ΞΎ.nat βnt M.mult) β‘β¨ ap (Ξ½.nat βnt_) ΞΎ.pres-mult β©β‘ Ξ½.nat βnt (N.mult βnt (ΞΎ.nat β ΞΎ.nat)) β‘β¨ Endo.assoc Ξ½.nat N.mult (ΞΎ.nat β ΞΎ.nat) β©β‘ (Ξ½.nat βnt N.mult) βnt (ΞΎ.nat β ΞΎ.nat) β‘β¨ ap (_βnt (ΞΎ.nat β ΞΎ.nat)) Ξ½.pres-mult β©β‘ (O.mult βnt (Ξ½.nat β Ξ½.nat)) βnt (ΞΎ.nat β ΞΎ.nat) β‘Λβ¨ Endo.assoc O.mult (Ξ½.nat β Ξ½.nat) (ΞΎ.nat β ΞΎ.nat) β©β‘Λ O.mult βnt ((Ξ½.nat β Ξ½.nat) βnt (ΞΎ.nat β ΞΎ.nat)) β‘Λβ¨ ap (O.mult βnt_) $ Endo-β.F-β (Ξ½.nat , Ξ½.nat) (ΞΎ.nat , ΞΎ.nat) β©β‘Λ O.mult βnt ((Ξ½.nat βnt ΞΎ.nat) β (Ξ½.nat βnt ΞΎ.nat)) β
Putting these together, we have the category of monads.
Monads : β (C : Precategory o h) β Precategory (o β h) (o β h) Monads C .Ob = Monad C Monads C .Hom = Monad-hom Monads C .Hom-set _ _ = hlevel 2 Monads C .id = monad-hom-id Monads C ._β_ = monad-hom-β Monads C .idr _ = ext Ξ» _ β C .idr _ Monads C .idl _ = ext Ξ» _ β C .idl _ Monads C .assoc _ _ _ = ext Ξ» _ β C .assoc _ _ _