open import Cat.Instances.Product
open import Cat.Functor.Compose
open import Cat.Diagram.Monad
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Instances.Monads where

private variable
  o h : Level
open Precategory
open Functor

Categories of monads🔗

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

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 $\nu$ preserving the unit $\eta$ and the multiplication $\mu \text{.}$ 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) ( + n)
      H-Level-Monad-hom = basic-instance  $ Iso→is-hlevel  eqv (hlevel )
        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 
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 _ _ _