reorganize file

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

@@ -17,11 +17,10 @@ module Cat.Bi.Diagram.Monad  where
 <!--
 ```agda
 open _=>_ hiding (η)
+open Functor
 
 module _ {o ℓ ℓ'} (B : Prebicategory o ℓ ℓ') where
-  private
-    open module B = Prebicategory B
-    open Functor
+  private module B = Prebicategory B
 ```
 -->
 
@@ -94,60 +93,6 @@ mutual compatibility of the multiplication and unit with the unitors.
 
 </div>
 
-# 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(*)$. The composition operation is a natural transformation
-\[
-P\_1(*)\otimes P\_1(*)\To P\_1(*\otimes *)
-\]
-i.e. a natural transformation $\mu :M\otimes 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 on $a$.
-
-```agda
-  lax-functor→monad : Σ[ a ∈ B.Ob ] Monad a → Lax-functor ⊤Bicat B
-  lax-functor→monad (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 ∎
-
-  monad→lax-functor : Lax-functor ⊤Bicat B → Σ[ a ∈ B.Ob ] Monad a
-  monad→lax-functor 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 _
-```
-
 ## In Cat
 
 To prove that this is an actual generalisation of the 1-categorical
@@ -200,3 +145,65 @@ 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(*)$. The composition operation is a natural transformation
+\[
+P\_1(*)\otimes P\_1(*)\To P\_1(*\otimes *)
+\]
+i.e. a natural transformation $\mu :M\otimes 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
+  lax-functor→monad : Σ[ a ∈ B.Ob ] Monad B a → Lax-functor ⊤Bicat B
+  lax-functor→monad (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 ∎
+
+  monad→lax-functor : Lax-functor ⊤Bicat B → Σ[ a ∈ B.Ob ] Monad B a
+  monad→lax-functor 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 _
+```