agda · tetrapharmakon · Nov 30, 2021 · Nov 30, 2021 · Nov 30, 2021 · Nov 30, 2021
diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib
@@ -1,3 +1,3 @@
 name: agda-categories
-depend: standard-library-1.7
+depend: standard-library-2.0
 include: src/
diff --git a/src/Categories/Adjoint/Construction/Adjunctions.agda b/src/Categories/Adjoint/Construction/Adjunctions.agda
@@ -0,0 +1,163 @@
+{-# OPTIONS --without-K  --allow-unsolved-metas #-}
+
+open import Level
+open import Categories.Category.Core using (Category)
+open import Categories.Category
+open import Categories.Monad
+
+module Categories.Adjoint.Construction.Adjunctions {o ℓ e} {C : Category o ℓ e} (M : Monad C) where
+
+private
+  module C = Category C
+  module M = Monad M
+  open C
+
+open import Categories.Adjoint
+open import Categories.Functor
+open import Categories.Morphism hiding (_≅_)
+open import Categories.Functor.Properties
+open import Categories.NaturalTransformation.Core
+open import Categories.NaturalTransformation.NaturalIsomorphism
+open import Categories.NaturalTransformation.Equivalence renaming (_≃_ to _≅_)
+open import Categories.Morphism.Reasoning as MR
+open import Categories.Tactic.Category
+
+-- the category of adjunctions splitting a given monad
+record SplitObj : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+  constructor splitobj
+  field
+    D : Category o ℓ e
+    F : Functor C D
+    G : Functor D C
+    adj : F ⊣ G
+    GF≃M : G ∘F F ≃ M.F
+
+  module D = Category D
+  module F = Functor F
+  module G = Functor G
+  module adj = Adjoint adj
+  module GF≃M = NaturalIsomorphism GF≃M
+
+  field
+    η-eq : ∀ {A} → GF≃M.⇐.η _ ∘ M.η.η A ≈ adj.unit.η _
+    μ-eq : ∀ {A} → GF≃M.⇐.η _ ∘ M.μ.η A ≈ G.₁ (adj.counit.η (F.₀ A)) ∘ GF≃M.⇐.η _ ∘ M.F.F₁ (GF≃M.⇐.η A)
+
+  {-
+  η-eq:
+                 adj.unit.η A
+            A ------------------+
+    M.η.η A |                   |
+            v                   v
+            MA --------------> GFA
+                  GF≃M.⇐.η A
+
+  μ-eq:
+             GF≃M.⇐.η              G.F₁ (F.F₁ (GF≃M.⇐.η))
+        ---------------------> GFMA -------------------->
+    MMA ---------------------> MGFA --------------------> GFGFA
+     |   M.F.F₁ (GF≃M.⇐.η A)              GF≃M.⇐.η         |
+     |                                                      |
+     | M.μ A                                                | G.₁ (adj.counit.η (F.₀ A))
+     v                                                      v
+     MA -------------------------------------------------> GFA
+                     GF≃M.⇐.η A
+  -}
+
+record Split⇒ (X Y : SplitObj) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+  constructor split⇒
+  private
+    module X = SplitObj X
+    module Y = SplitObj Y
+
+  field
+    H : Functor X.D Y.D
+    Γ : H ∘F X.F ≃ Y.F
+
+  module Γ = NaturalIsomorphism Γ
+  module H = Functor H
+
+  field
+    μ-comp : ∀ {x : Obj} → Y.GF≃M.⇐.η x ≈ Y.G.F₁ (Γ.⇒.η x) ∘ ((Y.G.F₁ (Functor.F₁ H (X.adj.counit.η (X.F.F₀ x)))) ∘ Y.G.F₁ (Γ.⇐.η (X.G.F₀ (X.F.F₀ x))) ∘ (Y.adj.unit.η (X.G.F₀ (X.F.F₀ x)))) ∘ X.GF≃M.⇐.η x
+
+Split : Monad C → Category _ _ _
+Split M = record
+  { Obj = SplitObj
+  ; _⇒_ = Split⇒
+  ; _≈_ = λ U V → Split⇒.H U ≃ Split⇒.H V
+  ; id = split-id
+  ; _∘_ = comp
+  ; assoc = λ { {f = f} {g = g} {h = h} → associator (Split⇒.H f) (Split⇒.H g) (Split⇒.H h) }
+  ; sym-assoc = λ { {f = f} {g = g} {h = h} → sym-associator (Split⇒.H f) (Split⇒.H g) (Split⇒.H h) }
+  ; identityˡ = unitorˡ
+  ; identityʳ = unitorʳ
+  ; identity² = unitor²
+  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
+  ; ∘-resp-≈ = _ⓘₕ_
+  }
+  where
+  open NaturalTransformation
+  split-id : {A : SplitObj} → Split⇒ A A
+  split-id {A} = record
+    { H = Categories.Functor.id
+    ; Γ = unitorˡ
+    ; μ-comp = λ { {x} →
+      Equiv.sym(begin _ ≈⟨ elimˡ C (Functor.identity A.G) ⟩
+                      _ ≈⟨ (refl⟩∘⟨ elimˡ C (Functor.identity A.G)) ⟩∘⟨refl ⟩
+                      _ ≈⟨ elimˡ C A.adj.zag ⟩
+                      _ ∎)}
+    } where module A = SplitObj A
+            open C
+            open C.HomReasoning
+  comp : {A B X : SplitObj} → Split⇒ B X → Split⇒ A B → Split⇒ A X
+  comp {A = A} {B = B} {X = X} (split⇒ Hᵤ Γᵤ Aμ-comp) (split⇒ Hᵥ Γᵥ Bμ-comp) = record
+    { H = Hᵤ ∘F Hᵥ
+    ; Γ = Γᵤ ⓘᵥ (Hᵤ ⓘˡ Γᵥ) ⓘᵥ associator (SplitObj.F A) Hᵥ Hᵤ
+    ; μ-comp = λ { {x} →
+        Equiv.sym (begin {!   !} ≈⟨ (X.G.F-resp-≈ (X.D.HomReasoning.refl⟩∘⟨ X.D.identityʳ) ⟩∘⟨refl) ⟩
+                         {!   !} ≈⟨ (refl⟩∘⟨ ((refl⟩∘⟨ (X.G.F-resp-≈ (X.D.identityˡ X.D.HomReasoning.⟩∘⟨refl) ⟩∘⟨refl)) ⟩∘⟨refl)) ⟩
+                         {!   !} ≈⟨ pushˡ C X.G.homomorphism ⟩
+                         {!   !} ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ assoc) ⟩
+                         {!   !} ≈⟨ {!  !} ⟩
+                         {!   !} ≈⟨ {!   !} ⟩
+                         {!   !} ≈⟨ {!   !} ⟩
+                         {!   !} ≈⟨ {!  !} ⟩
+                         {!   !} ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ Equiv.sym Bμ-comp) ⟩
+                         {!   !} ≈⟨ Equiv.sym Aμ-comp ⟩
+                         {!   !} ∎) }
+
+
+{-
+Have
+
+X.G.F₁ (Γᵤ.⇒.η x) ∘
+      X.G.F₁ (Hᵤ.F₁ (Γᵥ.⇒.η x)) ∘
+      X.G.F₁ (Hᵤ.F₁ (Hᵥ.F₁ (A.adj.counit.η (A.F.F₀ x)))) ∘
+      (X.G.F₁
+       (Hᵤ.F₁ (Γᵥ.⇐.η (A.G.F₀ (A.F.F₀ x))) X.D.∘
+        Γᵤ.⇐.η (A.G.F₀ (A.F.F₀ x)))
+       ∘ X.adj.unit.η (A.G.F₀ (A.F.F₀ x)))
+      ∘ A.GF≃M.⇐.η x
+
+Goal
+
+      X.G.F₁ (Γᵤ.⇒.η x) ∘
+      (X.G.F₁ (Hᵤ.F₁ (B.adj.counit.η (B.F.F₀ x))) ∘
+       X.G.F₁ (Γᵤ.⇐.η (B.G.F₀ (B.F.F₀ x))) ∘
+       X.adj.unit.η (B.G.F₀ (B.F.F₀ x)))
+      ∘
+      B.G.F₁ (Γᵥ.⇒.η x) ∘
+      (B.G.F₁ (Hᵥ.F₁ (A.adj.counit.η (A.F.F₀ x))) ∘
+       B.G.F₁ (Γᵥ.⇐.η (A.G.F₀ (A.F.F₀ x))) ∘
+       B.adj.unit.η (A.G.F₀ (A.F.F₀ x)))
+      ∘ A.GF≃M.⇐.η x
+-}
+    } where
+       module A = SplitObj A
+       module B = SplitObj B
+       module X = SplitObj X
+       open C
+       open C.HomReasoning
+       module Hᵤ = Functor Hᵤ
+       module Hᵥ = Functor Hᵥ
+       module Γᵤ = NaturalIsomorphism Γᵤ
+       module Γᵥ = NaturalIsomorphism Γᵥ
diff --git a/src/Categories/Adjoint/Construction/Adjunctions/Properties.agda b/src/Categories/Adjoint/Construction/Adjunctions/Properties.agda
@@ -0,0 +1,186 @@
+{-# OPTIONS --without-K  --allow-unsolved-metas #-}
+
+open import Level
+open import Categories.Category.Core using (Category)
+open import Categories.Category
+open import Categories.Monad
+
+module Categories.Adjoint.Construction.Adjunctions.Properties {o ℓ e} {C : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e} (M : Monad C) where
+
+private
+  module C = Category C
+  module M = Monad M
+
+open import Categories.Adjoint using (Adjoint)
+open import Categories.Functor using (Functor)
+open import Categories.Morphism.Reasoning
+open import Categories.NaturalTransformation hiding (id)
+open NaturalTransformation using (η)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper; sym; associator)
+
+open import Categories.Adjoint.Construction.Adjunctions M
+
+open import Categories.Object.Terminal (Split M)
+open import Categories.Object.Initial (Split M)
+open import Categories.Category.Construction.EilenbergMoore
+open import Categories.Category.Construction.Kleisli
+open import Categories.Adjoint.Construction.Kleisli M as KL
+open import Categories.Adjoint.Construction.EilenbergMoore M as EM
+
+open import Categories.Tactic.Category
+
+-- EM-object : SplitObj
+-- EM-object = record
+--   { D = EilenbergMoore M
+--   ; F = EM.Free
+--   ; G = EM.Forgetful
+--   ; adj = EM.Free⊣Forgetful
+--   ; GF≃M = EM.FF≃F
+--   ; η-eq = begin
+--              M.F.₁ id ∘ M.η.η _ ≈⟨ M.F.identity ⟩∘⟨refl ⟩
+--              id ∘ M.η.η _       ≈⟨ identityˡ ⟩
+--              M.η.η _            ∎
+--   ; μ-eq = begin
+--              M.F.₁ id ∘ M.μ.η _                    ≈⟨ M.F.identity ⟩∘⟨refl ⟩
+--              id ∘ M.μ.η _                          ≈⟨ identityˡ ⟩
+--              M.μ.η _                               ≈⟨ Equiv.sym identityʳ ⟩
+--              M.μ.η _  ∘ id                         ≈⟨ refl⟩∘⟨ Equiv.sym M.F.identity ⟩
+--              M.μ.η _ ∘ M.F.₁ id                    ≈⟨ Equiv.sym identityʳ ⟩
+--              (M.μ.η _ ∘ M.F.₁ id) ∘ id             ≈⟨ assoc ⟩
+--              M.μ.η _ ∘ M.F.₁ id ∘ id               ≈⟨ refl⟩∘⟨  refl⟩∘⟨ Equiv.sym M.F.identity ⟩
+--              M.μ.η _ ∘ M.F.₁ id ∘ M.F.₁ id         ≈⟨ refl⟩∘⟨  refl⟩∘⟨ M.F.F-resp-≈ (Equiv.sym M.F.identity) ⟩
+--              M.μ.η _ ∘ M.F.₁ id ∘ M.F.₁ (M.F.₁ id) ∎
+--   } where open Category C
+--           open HomReasoning
+
+Kl-object : SplitObj
+Kl-object = record
+  { D = Kleisli M
+  ; F = KL.Free
+  ; G = KL.Forgetful
+  ; adj = KL.Free⊣Forgetful
+  ; GF≃M = KL.FF≃F
+  ; η-eq = begin
+             M.F.₁ id ∘ M.η.η _ ≈⟨ M.F.identity ⟩∘⟨refl ⟩
+             id ∘ M.η.η _       ≈⟨ identityˡ ⟩
+             M.η.η _            ∎
+  ; μ-eq = begin M.F.₁ id ∘ M.μ.η _                                     ≈⟨ M.F.identity ⟩∘⟨refl ⟩
+             id ∘ M.μ.η _                                               ≈⟨ identityˡ ⟩
+             M.μ.η _                                                    ≈⟨ Equiv.sym identityʳ ⟩
+             M.μ.η _ ∘ id                                               ≈⟨ refl⟩∘⟨ Equiv.sym M.F.identity ⟩
+             M.μ.η _ ∘ M.F.₁ id                                         ≈⟨ refl⟩∘⟨ M.F.F-resp-≈ (Equiv.sym M.F.identity) ⟩
+             M.μ.η _ ∘ M.F.₁ (M.F.₁ id)                                 ≈⟨ Equiv.sym identityʳ ⟩
+             (M.μ.η _ ∘ M.F.₁ (M.F.₁ id)) ∘ id                          ≈⟨ refl⟩∘⟨ Equiv.sym M.F.identity ⟩
+             (M.μ.η _ ∘ M.F.₁ (M.F.₁ id)) ∘ M.F.₁ id                    ≈⟨ Equiv.sym identityʳ  ⟩
+             ((M.μ.η _ ∘ M.F.₁ (M.F.₁ id)) ∘ M.F.₁ id) ∘ id             ≈⟨ assoc ⟩
+             (M.μ.η _ ∘ M.F.₁ (M.F.₁ id)) ∘ M.F.₁ id ∘ id               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Equiv.sym M.F.identity ⟩
+             (M.μ.η _ ∘ M.F.₁ (M.F.₁ id)) ∘ M.F.₁ id ∘ M.F.₁ id         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ M.F.F-resp-≈ (Equiv.sym M.F.identity) ⟩
+             (M.μ.η _ ∘ M.F.₁ (M.F.₁ id)) ∘ M.F.₁ id ∘ M.F.₁ (M.F.₁ id) ∎
+  } where open Category C
+          open HomReasoning
+
+
+! : {A : SplitObj} → Split⇒ Kl-object A
+! {splitobj D F G adj GF≃M η-eq μ-eq} = record
+  { H =
+    let open D
+        open D.HomReasoning in
+    record
+      { F₀ = F.₀
+      ; F₁ = λ f → adj.counit.η _ ∘ F.₁ (GF≃M.⇐.η _ C.∘ f)
+      ; identity = λ {A} →
+        begin
+          adj.counit.η (F.₀ A) ∘ F.₁ (GF≃M.⇐.η A C.∘ M.η.η A) ≈⟨ refl⟩∘⟨ F.F-resp-≈ η-eq ⟩
+          adj.counit.η (F.₀ A) ∘ F.₁ (adj.unit.η A)           ≈⟨ adj.zig ⟩
+          D.id                                                ∎
+      ; homomorphism = λ {X} {Y} {Z} {f} {g} →
+        let ε x = adj.counit.η x in 
+        begin
+          ε _ ∘ F.₁ (GF≃M.⇐.η _ C.∘ (M.μ.η _ C.∘ M.F.₁ g) C.∘ f)                                ≈⟨ refl⟩∘⟨ F.F-resp-≈ (assoc²'' C) ⟩
+          ε _ ∘ F.₁ ((GF≃M.⇐.η _ C.∘ M.μ.η _) C.∘ M.F.₁ g C.∘ f)                                ≈⟨ refl⟩∘⟨ F.F-resp-≈ (μ-eq CHR.⟩∘⟨refl) ⟩
+          ε _ ∘ F.₁ ((G.₁ (ε (F.₀ _)) C.∘ GF≃M.⇐.η _ C.∘ M.F.₁ (GF≃M.⇐.η _)) C.∘ M.F.₁ g C.∘ f) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (assoc²' C) ⟩
+          ε _ ∘ F.₁ (G.₁ (ε (F.₀ _)) C.∘ GF≃M.⇐.η _ C.∘ M.F.₁ (GF≃M.⇐.η _) C.∘ M.F.₁ g C.∘ f)   ≈⟨ refl⟩∘⟨ F.F-resp-≈ (CHR.refl⟩∘⟨ CHR.refl⟩∘⟨ pullˡ C (C.Equiv.sym M.F.homomorphism)) ⟩
+          ε _ ∘ F.₁ (G.₁ (ε (F.₀ _)) C.∘ GF≃M.⇐.η _ C.∘ M.F.₁ (GF≃M.⇐.η _ C.∘ g) C.∘ f)         ≈⟨ refl⟩∘⟨ F.F-resp-≈ (CHR.refl⟩∘⟨ extendʳ C (GF≃M.⇐.commute _)) ⟩
+          ε _ ∘ F.₁ (G.₁ (ε (F.₀ _)) C.∘ G.₁ (F.₁ (GF≃M.⇐.η _ C.∘ g)) C.∘ GF≃M.⇐.η _ C.∘ f)     ≈⟨ refl⟩∘⟨ F.homomorphism ⟩
+          ε _ ∘ F.₁ (G.₁ (ε (F.₀ _))) ∘ F.₁ (G.₁ (F.₁ (GF≃M.⇐.η _ C.∘ g)) C.∘ GF≃M.⇐.η _ C.∘ f) ≈⟨ DMR.extendʳ (adj.counit.commute _) ⟩
+          ε _ ∘ ε _ ∘ F.₁ (G.₁ (F.₁ (GF≃M.⇐.η _ C.∘ g)) C.∘ GF≃M.⇐.η _ C.∘ f)                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.homomorphism ⟩
+          ε _ ∘ ε _ ∘ F.₁ (G.₁ (F.₁ (GF≃M.⇐.η _ C.∘ g))) ∘ F.₁ (GF≃M.⇐.η _ C.∘ f)               ≈⟨ refl⟩∘⟨ DMR.extendʳ (adj.counit.commute _) ⟩
+          ε _ ∘ F.₁ (GF≃M.⇐.η _ C.∘ g) ∘ ε _ ∘ F.₁ (GF≃M.⇐.η _ C.∘ f)                           ≈⟨ sym-assoc ⟩
+          (ε _ ∘ F.₁ (GF≃M.⇐.η _ C.∘ g)) ∘ ε _ ∘ F.₁ (GF≃M.⇐.η _ C.∘ f)                         ∎
+      ; F-resp-≈ = λ x → D.∘-resp-≈ʳ (F.F-resp-≈ (C.∘-resp-≈ʳ x))
+      }
+  ; Γ =
+    let open D
+        open D.HomReasoning in
+    niHelper (record
+      { η = λ _ → D.id
+      ; η⁻¹ = λ _ → D.id
+      ; commute = λ f → 
+        begin
+          D.id ∘ adj.counit.η _ ∘ F.₁ (GF≃M.⇐.η _ C.∘ M.η.η _ C.∘ f) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ (pullˡ C η-eq) ⟩
+          D.id ∘ adj.counit.η _ ∘ F.₁ (adj.unit.η _ C.∘ f)           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.homomorphism ⟩
+          D.id ∘ adj.counit.η _ ∘ F.₁ (adj.unit.η _) ∘ F.₁ f         ≈⟨ refl⟩∘⟨ pullˡ D adj.zig ⟩
+          D.id ∘ D.id ∘ F.₁ f                                        ≈⟨ identityˡ ⟩
+          D.id ∘ F.₁ f                                               ≈⟨ identityˡ ⟩
+          F.₁ f                                                      ≈⟨ D.Equiv.sym identityʳ ⟩
+          (F.₁ f ∘ D.id)                                             ∎
+      ; iso = λ X → record { isoˡ = identityˡ ; isoʳ = identityˡ }
+      })
+  ; μ-comp = λ { {x} → let open C
+                           open C.HomReasoning in 
+                            Equiv.sym 
+                              (begin _ ≈⟨ elimˡ C G.identity ⟩ 
+                                    _ ≈⟨ elimʳ C M.F.identity ⟩ 
+                                    _ ≈⟨ (refl⟩∘⟨ elimˡ C G.identity) ⟩ 
+                                    _ ≈⟨ (G.homomorphism ⟩∘⟨refl) ⟩ 
+                                    _ ≈⟨ pullʳ C (adj.unit.sym-commute _) ⟩ 
+                                    _ ≈⟨ sym-assoc ⟩
+                                    _ ≈⟨ elimˡ C adj.zag ⟩
+                                    _ ≈⟨ elimʳ C M.F.identity ⟩ 
+                                    _ ∎) }
+  } where
+    module adj  = Adjoint adj
+    module F    = Functor F
+    module G    = Functor G
+    module GF≃M = NaturalIsomorphism GF≃M
+    module D    = Category D
+    module CHR = C.HomReasoning
+    module DHR = D.HomReasoning
+    module DMR = Categories.Morphism.Reasoning D
+    module CMR = Categories.Morphism.Reasoning C
+
+Kl-initial : IsInitial Kl-object
+Kl-initial = record
+  { ! = !
+  ; !-unique = λ { {A} H → niHelper (
+    let module A = SplitObj A
+        module K = SplitObj Kl-object
+        module H = Split⇒ H
+        module Γ = NaturalIsomorphism H.Γ
+        module CH = C.HomReasoning
+        open Category A.D in
+    record
+      { η   = Γ.⇐.η
+      ; η⁻¹ = Γ.⇒.η
+      ; commute = λ f → let open A.D.HomReasoning in 
+          begin _ ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ A.F.F-resp-≈ ((H.μ-comp   CH.⟩∘⟨refl) CH.○ (C.assoc CH.○ (CH.refl⟩∘⟨ C.assoc))))) ⟩ 
+                _ ≈⟨ ((refl⟩∘⟨ refl⟩∘⟨ A.F.homomorphism)) ⟩
+                _ ≈⟨ (refl⟩∘⟨ pullˡ A.D (A.adj.counit.commute _)) ⟩
+                _ ≈⟨ (refl⟩∘⟨ assoc) ⟩
+                _ ≈⟨ cancelˡ A.D (Γ.iso.isoˡ _) ⟩
+                _ ≈⟨ (refl⟩∘⟨ A.F.homomorphism) ⟩ 
+                _ ≈⟨ (refl⟩∘⟨ pushˡ A.D A.F.homomorphism) ⟩ 
+                _ ≈⟨ extendʳ A.D (A.adj.counit.commute _) ⟩ 
+                _ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pushˡ A.D A.F.homomorphism) ⟩ -- (refl⟩∘⟨ (refl⟩∘⟨ A.F.homomorphism)) ⟩ 
+                _ ≈⟨ (refl⟩∘⟨ extendʳ A.D (A.adj.counit.commute _)) ⟩ -- (extendʳ A.D (A.adj.counit.commute _)) ⟩ 
+                _ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullˡ A.D A.adj.zig) ⟩ -- (refl⟩∘⟨ refl⟩∘⟨ elimˡ A.D A.adj.zig) ⟩ 
+                _ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ (identityˡ ○ A.F.F-resp-≈ (elimˡ C M.F.identity))) ⟩ -- (refl⟩∘⟨ refl⟩∘⟨ A.F.F-resp-≈ {! (elimˡ C M.F.identity) !}) ⟩ 
+                _ ≈⟨ (refl⟩∘⟨ Γ.⇐.commute f) ⟩ 
+                _ ≈⟨ pullˡ A.D (Equiv.sym H.H.homomorphism) ⟩ 
+                _ ≈⟨ (H.H.F-resp-≈ (elimʳ C (M.F.F-resp-≈ M.F.identity CH.○ M.F.identity) CH.⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
+                _ ≈⟨ (H.H.F-resp-≈ (pullˡ C M.identityʳ CH.○ C.identityˡ) ⟩∘⟨refl) ⟩ 
+                _ ∎
+      ; iso = NaturalIsomorphism.iso (sym H.Γ)
+      })
+    }
+  }
diff --git a/src/Categories/NaturalTransformation/Core.agda b/src/Categories/NaturalTransformation/Core.agda
@@ -102,6 +102,7 @@ _∘ₕ_ {E = E} {F} {I = I} Y X = ntHelper record
         open Functor I renaming (F₀ to I₀; F₁ to I₁)
         open MR E
 
+-- F * α
 _∘ˡ_ : ∀ {G H : Functor C D} (F : Functor D E) → NaturalTransformation G H → NaturalTransformation (F ∘F G) (F ∘F H)
 _∘ˡ_ F α = record
   { η           = λ X → F₁ (η X)
@@ -111,6 +112,7 @@ _∘ˡ_ F α = record
   where open Functor F
         open NaturalTransformation α
 
+-- α * F
 _∘ʳ_ : ∀ {G H : Functor D E} → NaturalTransformation G H → (F : Functor C D) → NaturalTransformation (G ∘F F) (H ∘F F)
 _∘ʳ_ {D = D} {E = E} {G = G} {H = H} α F = record
   { η           = λ X → η (F₀ X)