module Cat.Bi.Diagram.Monad  where

Monads in a bicategoryπŸ”—

Recall that a monad on a category consists of a functor and natural transformations While the words β€œfunctor” and β€œnatural transformation” are specific to the setup where 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
      M : a B.↦ a
      ΞΌ : (M B.βŠ— M) B.β‡’ M
      Ξ· : 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 we abstract all of that away into the setup of the bicategory 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 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
  open Monad
  private module C = Cr C

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

    monad' : Cat.Monad C
    monad' .M = M.M
    monad' .unit = M.Ξ·
    monad' .mult = M.ΞΌ
    monad' .left-ident {x} =
        ap (M.μ .η x C.∘_) (C.intror refl)
      βˆ™ M.ΞΌ-unitr Ξ·β‚š x
    monad' .right-ident {x} =
        ap (M.μ .η x C.∘_) (C.introl (M.M .Functor.F-id))
      βˆ™ M.ΞΌ-unitl Ξ·β‚š x
    monad' .mult-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 monad = monad' where
    private module M = Cat.Monad monad

    monad' : Monad (Cat _ _) C
    monad' .M = M.M
    monad' .ΞΌ = M.mult
    monad' .Ξ· = M.unit
    monad' .ΞΌ-assoc = ext Ξ» _ β†’
        ap (M.μ _ C.∘_) (C.elimr refl)
     Β·Β· M.mult-assoc
     Β·Β· ap (M.ΞΌ _ C.∘_) (C.introl (M.M-id) βˆ™ C.intror refl)
    monad' .ΞΌ-unitr = ext Ξ» _ β†’
        ap (M.μ _ C.∘_) (C.elimr refl)
      βˆ™ M.left-ident
    monad' .ΞΌ-unitl = ext Ξ» _ β†’
        ap (M.μ _ C.∘_) (C.eliml M.M-id)
      βˆ™ M.right-ident