defn: monads are lax functors (#460)

I noticed this on the
[nlab](https://ncatlab.org/nlab/show/monad#Etymology) and it sounded fun
to write down.
Really it'd be nice to do this using displayed bicategories with a
displayed bicategory of monads over a base bicategory $$\mathsf{S}$$.

# Description

* A few facts about the terminal category
* The terminal bicategory
* Monads are equivalent to lax functors from said bicategory

src/Cat/Bi/Base.lagda.md

@@ -180,6 +180,8 @@ naturally isomorphic to the identity functor.
       → Cr._≅_ Cat[ Hom C D ×ᶜ Hom B C ×ᶜ Hom A B , Hom A D ]
         (compose-assocˡ {H = Hom} compose)
         (compose-assocʳ {H = Hom} compose)
+
+  module associator {a} {b} {c} {d} = Cr._≅_ _ (associator {a} {b} {c} {d})
 ```
 
 It's traditional to refer to the left unitor as $\lambda$, to the right
@@ -217,26 +219,26 @@ abbreviations here too:
 
   α→ : ∀ {A B C D} (f : C ↦ D) (g : B ↦ C) (h : A ↦ B)
      → (f ⊗ g) ⊗ h ⇒ f ⊗ (g ⊗ h)
-  α→ f g h = associator .Cr._≅_.to .η (f , g , h)
+  α→ f g h = associator.to .η (f , g , h)
 
   α← : ∀ {A B C D} (f : C ↦ D) (g : B ↦ C) (h : A ↦ B)
      → f ⊗ (g ⊗ h) ⇒ (f ⊗ g) ⊗ h
-  α← f g h = associator .Cr._≅_.from .η (f , g , h)
+  α← f g h = associator.from .η (f , g , h)
 
   α←nat : ∀ {A B C D} {f f' : C ↦ D} {g g' : B ↦ C} {h h' : A ↦ B}
         → (β : f ⇒ f') (γ : g ⇒ g') (δ : h ⇒ h')
         → Path (f ⊗ g ⊗ h ⇒ ((f' ⊗ g') ⊗ h'))
           (α← _ _ _ ∘ (β ◆ (γ ◆ δ))) (((β ◆ γ) ◆ δ) ∘ α← _ _ _)
   α←nat {A} {B} {C} {D} {f} {f'} {g} {g'} {h} {h'} β γ δ =
-    associator .Cr._≅_.from .is-natural (f , g , h) (f' , g' , h') (β , γ , δ)
+    associator.from .is-natural (f , g , h) (f' , g' , h') (β , γ , δ)
 
   α→nat : ∀ {A B C D} {f f' : C ↦ D} {g g' : B ↦ C} {h h' : A ↦ B}
         → (β : f ⇒ f') (γ : g ⇒ g') (δ : h ⇒ h')
         → Path ((f ⊗ g) ⊗ h ⇒ (f' ⊗ g' ⊗ h'))
            (α→ _ _ _ ∘ ((β ◆ γ) ◆ δ))
            ((β ◆ (γ ◆ δ)) ∘ α→ _ _ _)
   α→nat {A} {B} {C} {D} {f} {f'} {g} {g'} {h} {h'} β γ δ =
-    associator .Cr._≅_.to .is-natural (f , g , h) (f' , g' , h') (β , γ , δ)
+    associator.to .is-natural (f , g , h) (f' , g' , h') (β , γ , δ)
 ```
 
 The final data we need are coherences relating the left and right
@@ -425,7 +427,7 @@ have components $F_1(f)F_1(g) \To F_1(fg)$ and $\id \To F_1(\id)$.
 
 <!--
 ```agda
-  module P₁ {A} {B} = Functor (P₁ {A} {B})
+  module P₁ {A} {B} = Fr (P₁ {A} {B})
 
   ₀ : B.Ob → C.Ob
   ₀ = P₀

src/Cat/Bi/Diagram/Monad.lagda.md

@@ -1,5 +1,7 @@
 <!--
 ```agda
+open import Cat.Instances.Shape.Terminal
+open import Cat.Bi.Instances.Terminal
 open import Cat.Bi.Base
 open import Cat.Prelude
 
@@ -14,7 +16,8 @@ module Cat.Bi.Diagram.Monad  where
 
 <!--
 ```agda
-open _=>_
+open _=>_ hiding (η)
+open Functor
 
 module _ {o ℓ ℓ'} (B : Prebicategory o ℓ ℓ') where
   private module B = Prebicategory B
@@ -113,15 +116,15 @@ module _ {o ℓ} {C : Precategory o ℓ} where
     monad' .unit = M.η
     monad' .mult = M.μ
     monad' .left-ident {x} =
-        ap (M.μ .η x C.∘_) (C.intror refl)
+        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))
+        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)
+        ap (M.μ ._=>_.η x C.∘_) (C.intror refl)
      ·· M.μ-assoc ηₚ x
-     ·· ap (M.μ .η x C.∘_) (C.elimr refl ∙ C.eliml (M.M .Functor.F-id))
+     ·· 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
@@ -142,3 +145,63 @@ module _ {o ℓ} {C : Precategory o ℓ} where
         ap (M.μ _ C.∘_) (C.eliml M.M-id)
       ∙ M.right-ident
 ```
+
+<!--
+```agda
+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 $\cB$.
+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_*)\To P_1(\id_*) $$
+i.e. a natural transformation $\mu :M M\To M$. Finally, the unitor gives
+$\eta:\id\To M$.
+Altogether, this is exactly the same data as an object $a\in\cB$ and a [[monad in]]
+$\cB$ on $a$.
+
+```agda
+  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 _
+```

src/Cat/Bi/Instances/Terminal.lagda.md

@@ -0,0 +1,35 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Cat.Instances.Shape.Terminal
+open import Cat.Univalent
+open import Cat.Bi.Base
+
+import Cat.Reasoning
+```
+-->
+
+```agda
+module Cat.Bi.Instances.Terminal where
+```
+
+# The terminal bicategory {defines="terminal-bicategory"}
+
+The **terminal bicategory** is the [[bicategory]] with a single object, and a trivial
+category of morphisms.
+
+```agda
+open Prebicategory
+
+⊤Bicat : Prebicategory lzero lzero lzero
+⊤Bicat .Ob = ⊤
+⊤Bicat .Hom _ _ = ⊤Cat
+⊤Bicat .Prebicategory.id = tt
+⊤Bicat .compose = !F
+⊤Bicat .unitor-l = path→iso !F-unique₂
+⊤Bicat .unitor-r = path→iso !F-unique₂
+⊤Bicat .associator = path→iso !F-unique₂
+⊤Bicat .triangle _ _ = refl
+⊤Bicat .pentagon _ _ _ _ = refl
+```

src/Cat/Functor/Naturality.lagda.md

@@ -23,7 +23,6 @@ module collects some notation that will help us with that task.
 ```agda
 module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} where
   private
-    module DD = Cat.Reasoning Cat[ D , D ]
     module CD = Cat.Reasoning Cat[ C , D ]
     module D = Cat.Reasoning D
     module C = Cat.Reasoning C

src/Cat/Instances/Shape/Terminal.lagda.md

@@ -69,6 +69,9 @@ category.
 
   !F-unique : ∀ {F : Functor C ⊤Cat} → F ≡ !F
   !F-unique = Functor-path (λ _ → refl) (λ _ → refl)
+
+  !F-unique₂ : ∀ {F G : Functor C ⊤Cat} → F ≡ G
+  !F-unique₂ = Functor-path (λ _ → refl) (λ _ → refl)
 ```
 
 Conversely, functors $\top \to \cC$ are determined by their behaviour

src/Cat/Instances/Shape/Terminal/Properties.lagda.md

@@ -0,0 +1,29 @@
+<!--
+```agda
+open import Cat.Functor.Equivalence.Path
+open import Cat.Instances.Shape.Terminal
+open import Cat.Functor.Equivalence
+open import Cat.Instances.Product
+open import Cat.Prelude
+```
+-->
+
+```agda
+module Cat.Instances.Shape.Terminal.Properties where
+```
+
+# Properties
+
+We note that the [[terminal category]] is a unit to the categorical product.
+
+```agda
+⊤Cat-unit : ∀ {o h} {C : Precategory o h} → ⊤Cat ×ᶜ C ≡ C
+⊤Cat-unit = sym $ Precategory-path Cat⟨ !F , Id ⟩ Cat⟨!F,Id⟩-is-iso where
+  open is-precat-iso
+  open is-iso
+  Cat⟨!F,Id⟩-is-iso : is-precat-iso Cat⟨ !F , Id ⟩
+  Cat⟨!F,Id⟩-is-iso .has-is-ff  .is-eqv (tt , f) .centre = f , refl
+  Cat⟨!F,Id⟩-is-iso .has-is-iso .is-eqv (tt , a) .centre = a , refl
+  Cat⟨!F,Id⟩-is-iso .has-is-ff  .is-eqv (tt , f) .paths (g , p) i = p (~ i) .snd , λ j → p (~ i ∨ j)
+  Cat⟨!F,Id⟩-is-iso .has-is-iso .is-eqv (tt , a) .paths (b , p) i = p (~ i) .snd , λ j → p (~ i ∨ j)
+```