open import Cat.Instances.Shape.Terminal
open import Cat.Bi.Instances.Terminal
open import Cat.Bi.Base
open import Cat.Prelude

import Cat.Diagram.Monad as Cat
import Cat.Reasoning as Cr

module Cat.Bi.Diagram.Monad  where

open _=>_ hiding (η)
open Functor

module _ {o ℓ ℓ'} (B : Prebicategory o ℓ ℓ') where
  private module B = Prebicategory B

Monads in a bicategory🔗

Recall that a monad on a category $C$ consists of a functor $M : C \to C$ and natural transformations $μ : MM \Rightarrow M,$ $η : Id \Rightarrow M .$ While the words “functor” and “natural transformation” are specific to the setup where $C$ is a category, if we replace those with “1-cell” and “2-cell”, then the definition works in any bicategory!

  record Monad (a : B.Ob) : Type (ℓ ⊔ ℓ') where
    field
      M : a B.↦ a
      μ : (M B.⊗ M) B.⇒ M
      η : B.id B.⇒ M

The setup is, in a sense, a lot more organic when phrased in an arbitrary bicategory: Rather than dealing with the specificities of natural transformations and the category $C,$ we abstract all of that away into the setup of the bicategory $B .$ All we need is that the multiplication $μ$ be compatible with the associator $α,$ and the unit $η$ must be appropriately compatible with the left and right unitors $λ, ρ .$

      μ-assoc : μ B.∘ (M B.▶ μ) ≡ μ B.∘ (μ B.◀ M) B.∘ B.α← M M M
      μ-unitr : μ B.∘ (M B.▶ η) ≡ B.ρ← M
      μ-unitl : μ B.∘ (η B.◀ M) ≡ B.λ← M

We can draw these compatibility conditions as pretty commutative diagrams. The commutative altar (on top) indicates associativity of multiplication, or more abstractly, compatibility of the multiplication with the associator. The commutative upside-down triangle indicates mutual compatibility of the multiplication and unit with the unitors.

In Cat🔗

To prove that this is an actual generalisation of the 1-categorical notion, we push some symbols around and prove that a monad in the bicategory $Cat$ is the same thing as a monad on some category. Things are set up so that this is almost definitional, but the compatibility paths have to be adjusted slightly. Check it out below:

module _ {o ℓ} {C : Precategory o ℓ} where
  open Cat.Monad-on
  open Monad
  private module C = Cr C

  Bicat-monad→monad : Monad (Cat _ _) C → Cat.Monad C
  Bicat-monad→monad monad = _ , monad' where
    module M = Monad monad

    monad' : Cat.Monad-on M.M
    monad' .unit = M.η
    monad' .mult = M.μ
    monad' .μ-unitr {x} =
        ap (M.μ ._=>_.η x C.∘_) (C.intror refl)
      ∙ M.μ-unitr ηₚ x
    monad' .μ-unitl {x} =
        ap (M.μ ._=>_.η x C.∘_) (C.introl (M.M .Functor.F-id))
      ∙ M.μ-unitl ηₚ x
    monad' .μ-assoc {x} =
        ap (M.μ ._=>_.η x C.∘_) (C.intror refl)
     ∙∙ M.μ-assoc ηₚ x
     ∙∙ ap (M.μ ._=>_.η x C.∘_) (C.elimr refl ∙ C.eliml (M.M .Functor.F-id))

  Monad→bicat-monad : Cat.Monad C → Monad (Cat _ _) C
  Monad→bicat-monad (M , monad) = monad' where
    module M = Cat.Monad-on (monad)

    monad' : Monad (Cat _ _) C
    monad' .Monad.M = M
    monad' .μ = M.mult
    monad' .η = M.unit
    monad' .μ-assoc = ext λ _ →
        ap (M.μ _ C.∘_) (C.elimr refl)
     ∙∙ M.μ-assoc
     ∙∙ ap (M.μ _ C.∘_) (C.introl (M.M-id) ∙ C.intror refl)
    monad' .μ-unitr = ext λ _ →
        ap (M.μ _ C.∘_) (C.elimr refl)
      ∙ M.μ-unitr
    monad' .μ-unitl = ext λ _ →
        ap (M.μ _ C.∘_) (C.eliml M.M-id)
      ∙ M.μ-unitl

module _ {o ℓ ℓ'} (B : Prebicategory o ℓ ℓ') where
  private
    open module B = Prebicategory B

Monads as lax functors🔗

Suppose that we have a lax functor $P$ from the terminal bicategory to $B .$ Then $P$ identifies a single object $a = P_{0} (*)$ as well as a morphism $M : a \to a$ given by $P_{1} (id_{*}) .$ The composition operation is a natural transformation $P_{1} (id_{*}) P_{1} (id_{*}) \Rightarrow P_{1} (id_{*})$ i.e. a natural transformation $μ : MM \Rightarrow M .$ Finally, the unitor gives $η : id \Rightarrow M .$ Altogether, this is exactly the same data as an object $a \in B$ and a monad in $B$ on $a .$

  monad→lax-functor : Σ[ a ∈ B.Ob ] Monad B a → Lax-functor ⊤Bicat B
  monad→lax-functor (a , monad) = P where
    open Monad monad
    open Lax-functor
    P : Lax-functor ⊤Bicat B
    P .P₀ _ = a
    P .P₁ = !Const M
    P .compositor ._=>_.η _ = μ
    P .compositor .is-natural _ _ _ = B.Hom.elimr (B.compose .F-id) ∙ sym (B.Hom.idl _)
    P .unitor = η
    P .hexagon _ _ _ =
      Hom.id ∘ μ ∘ (μ ◀ M)                ≡⟨ Hom.pulll (Hom.idl _) ⟩
      μ ∘ (μ ◀ M)                         ≡⟨ Hom.intror $ ap (λ nt → nt ._=>_.η (M , M , M)) associator.invr ⟩
      (μ ∘ μ ◀ M) ∘ (α← M M M ∘ α→ M M M) ≡⟨ cat! (Hom a a) ⟩
      (μ ∘ μ ◀ M ∘ α← M M M) ∘ α→ M M M   ≡˘⟨ Hom.pulll μ-assoc ⟩
      μ ∘ (M ▶ μ) ∘ (α→ M  M  M)          ∎
    P .right-unit _ = Hom.id ∘ μ ∘ M ▶ η  ≡⟨ Hom.idl _ ∙ μ-unitr ⟩ ρ← M ∎
    P .left-unit _ = Hom.id ∘ μ ∘ (η ◀ M) ≡⟨ Hom.idl _ ∙ μ-unitl ⟩ λ← M ∎

  lax-functor→monad : Lax-functor ⊤Bicat B → Σ[ a ∈ B.Ob ] Monad B a
  lax-functor→monad P = (a , record { monad }) where
    open Lax-functor P

    a : B.Ob
    a = P₀ tt

    module monad where
      M = P₁.F₀ _
      μ = γ→ _ _
      η = unitor
      μ-assoc =
        μ ∘ M ▶ μ                           ≡⟨ (Hom.intror $ ap (λ nt → nt ._=>_.η (M , M , M)) associator.invl) ⟩
        (μ ∘ M ▶ μ) ∘ (α→ M M M ∘ α← M M M) ≡⟨ cat! (Hom a a) ⟩
        (μ ∘ M ▶ μ ∘ α→ M M M) ∘ α← M M M   ≡˘⟨ hexagon _ _ _ Hom.⟩∘⟨refl ⟩
        (P₁.F₁ _ ∘ μ ∘ μ ◀ M) ∘ α← M M M    ≡⟨ ( P₁.F-id Hom.⟩∘⟨refl) Hom.⟩∘⟨refl  ⟩
        (Hom.id ∘ μ ∘ μ ◀ M) ∘ α← M M M     ≡⟨ cat! (Hom a a) ⟩
        μ ∘ μ ◀ M ∘ α← M M M ∎
      μ-unitr = P₁.introl refl ∙ right-unit _
      μ-unitl = P₁.introl refl ∙ left-unit _