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

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)

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 _ _ _