From c3fc7678b9df19ebaf1f0838778bdf1f50c2eb30 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 15 Jul 2023 10:05:27 +0200
Subject: [PATCH 1/2] Add variant of glue

---
 src/Categories/Morphism/Reasoning/Core.agda | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/Categories/Morphism/Reasoning/Core.agda b/src/Categories/Morphism/Reasoning/Core.agda
index 44325de2f..5caef190f 100644
--- a/src/Categories/Morphism/Reasoning/Core.agda
+++ b/src/Categories/Morphism/Reasoning/Core.agda
@@ -157,6 +157,16 @@ glue {c′ = c′} {a′ = a′} {a = a} {c″ = c″} {c = c} {b′ = b′} {b
   (c″ ∘ a′) ∘ b′ ≈⟨ assoc ⟩
   c″ ∘ (a′ ∘ b′) ∎
 
+-- A "rotated" version of glue′. Equivalent to 'Equiv.sym (glue (Equiv.sym sq-a) (Equiv.sym sq-b))'
+glue′ : CommutativeSquare a′ c′ c″ a →
+        CommutativeSquare b′ c c′ b →
+        CommutativeSquare (a′ ∘ b′) c c″ (a ∘ b)
+glue′ {a′ = a′} {c′ = c′} {c″ = c″} {a = a} {b′ = b′} {c = c} {b = b} sq-a sq-b = begin
+  c″ ∘ (a′ ∘ b′) ≈⟨ pullˡ sq-a ⟩
+  (a ∘ c′) ∘ b′  ≈⟨ pullʳ sq-b ⟩
+  a ∘ (b ∘ c)    ≈⟨ sym-assoc ⟩
+  (a ∘ b) ∘ c    ∎
+
 glue◃◽ : a ∘ c′ ≈ c″ → CommutativeSquare c b′ b c′ → CommutativeSquare c b′ (a ∘ b) c″
 glue◃◽ {a = a} {c′ = c′} {c″ = c″} {c = c} {b′ = b′} {b = b} tri-a sq-b = begin
   (a ∘ b) ∘ c   ≈⟨ pullʳ sq-b ⟩

From 781d16bd8639457d7e066114092005b2c7afd419 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 15 Jul 2023 10:05:54 +0200
Subject: [PATCH 2/2] Clean up proofs in Kleisli category construction

---
 .../Category/Construction/Kleisli.agda        | 33 +++++++------------
 1 file changed, 11 insertions(+), 22 deletions(-)

diff --git a/src/Categories/Category/Construction/Kleisli.agda b/src/Categories/Category/Construction/Kleisli.agda
index b2284b434..6e8e68d27 100644
--- a/src/Categories/Category/Construction/Kleisli.agda
+++ b/src/Categories/Category/Construction/Kleisli.agda
@@ -7,7 +7,7 @@ open import Categories.Category
 open import Categories.Functor using (Functor; module Functor)
 open import Categories.NaturalTransformation hiding (id)
 open import Categories.Monad
-import Categories.Morphism.Reasoning as MR
+import Categories.Morphism.Reasoning.Core as MR
 
 private
   variable
@@ -36,34 +36,23 @@ Kleisli {𝒞 = 𝒞} M = record
   open HomReasoning
   open MR 𝒞
 
-  -- shorthands to make the proofs nicer
-  F≈ = F-resp-≈
-
   assoc′ : ∀ {A B C D} {f : A ⇒ F₀ B} {g : B ⇒ F₀ C} {h : C ⇒ F₀ D}
           → (μ.η D ∘ (F₁ ((μ.η D ∘ F₁ h) ∘ g))) ∘ f ≈ (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)
-  assoc′ {A} {B} {C} {D} {f} {g} {h} =
-      begin
-        (μ.η D ∘ F₁ ((μ.η D ∘ F₁ h) ∘ g)) ∘ f       ≈⟨ pullʳ (F≈ assoc ⟩∘⟨refl) ⟩
-        μ.η D ∘ (F₁ (μ.η D ∘ (F₁ h ∘ g)) ∘ f)       ≈⟨ refl⟩∘⟨ (homomorphism ⟩∘⟨refl) ⟩
-        μ.η D ∘ ((F₁ (μ.η D) ∘ F₁ (F₁ h ∘ g)) ∘ f)  ≈⟨ pushʳ assoc ⟩
-        (μ.η D ∘ F₁ (μ.η D)) ∘ (F₁ (F₁ h ∘ g) ∘ f)  ≈⟨ pushˡ M.assoc ⟩
-        μ.η D ∘ (μ.η (F₀ D) ∘ F₁ (F₁ h ∘ g) ∘ f)    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ homomorphism ⟩∘⟨refl ⟩
-        μ.η D ∘ μ.η (F₀ D) ∘ (F₁ (F₁ h) ∘ F₁ g) ∘ f ≈⟨ refl⟩∘⟨ center⁻¹ (μ.commute h) Equiv.refl ⟩
-        μ.η D ∘ ((F₁ h ∘ μ.η C) ∘ F₁ g ∘ f)         ≈⟨ pushʳ (center Equiv.refl) ⟩
-        (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)       ∎
+  assoc′ {A} {B} {C} {D} {f} {g} {h} = begin
+    (μ.η D ∘ F₁ ((μ.η D ∘ F₁ h) ∘ g)) ∘ f           ≈⟨ pushʳ homomorphism ⟩∘⟨refl ⟩
+    ((μ.η D ∘ F₁ (μ.η D ∘ F₁ h)) ∘ F₁ g) ∘ f        ≈⟨ pushˡ (∘-resp-≈ˡ (∘-resp-≈ʳ homomorphism)) ⟩
+    (μ.η D ∘ (F₁ (μ.η D) ∘ F₁ (F₁ h))) ∘ (F₁ g ∘ f) ≈⟨ pushˡ (glue′ M.assoc (μ.commute h)) ⟩
+    (μ.η D ∘ F₁ h) ∘ (μ.η C ∘ (F₁ g ∘ f))           ≈⟨ refl⟩∘⟨ sym-assoc ⟩
+    (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)           ∎
 
   identityˡ′ : ∀ {A B} {f : A ⇒ F₀ B} → (μ.η B ∘ F₁ (η.η B)) ∘ f ≈ f
   identityˡ′ {A} {B} {f} = elimˡ M.identityˡ
 
   identityʳ′ : ∀ {A B} {f : A ⇒ F₀ B} → (μ.η B ∘ F₁ f) ∘ η.η A ≈ f
-  identityʳ′ {A} {B} {f} =
-      begin
-        (μ.η B ∘ F₁ f) ∘ η.η A      ≈⟨ assoc ⟩
-        μ.η B ∘ (F₁ f ∘ η.η A)      ≈˘⟨ refl⟩∘⟨ η.commute f ⟩
-        μ.η B ∘ (η.η (F₀ B) ∘ f)    ≈⟨ sym-assoc ⟩
-        (μ.η B ∘ η.η (F₀ B)) ∘ f    ≈⟨ elimˡ M.identityʳ ⟩
-        f
-      ∎
+  identityʳ′ {A} {B} {f} = begin
+        (μ.η B ∘ F₁ f) ∘ η.η A    ≈˘⟨ extendˡ (η.commute f) ⟩
+        (μ.η B ∘ η.η (F₀ B)) ∘ f  ≈⟨ elimˡ M.identityʳ ⟩
+        f                         ∎
 
   identity²′ : {A : Obj} → (μ.η A ∘ F₁ (η.η A)) ∘ η.η A ≈ η.η A
   identity²′ = elimˡ M.identityˡ