module Cat.Instances.Monads where

Categories of monads🔗

The category of monads of a category $C$ consists of monads on $C$ and natural transformations preserving the monadic structure. In terms of the bicategory of monads in $Cat$ , 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 $C$ is the fibre of the displayed bicategory of monads in $Cat$ over $C .$

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