diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib
index 91c6c57d7..186e350b1 100644
--- 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-1.7.1
 include: src/
diff --git a/src/Categories/Adjoint/Construction/Adjunctions.agda b/src/Categories/Adjoint/Construction/Adjunctions.agda
new file mode 100644
index 000000000..8ba082a2d
--- /dev/null
+++ b/src/Categories/Adjoint/Construction/Adjunctions.agda
@@ -0,0 +1,176 @@
+{-# 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 : Category _ _ _
+Split = 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⟩∘⟨ (refl⟩∘⟨ ((X.G.homomorphism ⟩∘⟨refl) ⟩∘⟨refl))) ⟩
+                         {!   !} ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ assoc)) ⟩
+                         {!   !} ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ X.adj.unit.commute _) ⟩
+                         {!   !} ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ extendʳ C (Equiv.sym X.G.homomorphism ○ X.G.F-resp-≈ (Γᵤ.⇐.commute _) ○ X.G.homomorphism))) ⟩
+                         {!   !} ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (extendʳ C (Equiv.sym (Functor.homomorphism (X.G ∘F Hᵤ)) ○ Functor.F-resp-≈ ((X.G ∘F Hᵤ)) (Γᵥ.⇐.commute _) ○ Functor.homomorphism ((X.G ∘F Hᵤ))))) ⟩
+                         {!   !} ≈⟨ {!   !} ⟩
+                         {!   !} ≈⟨ {!   !} ⟩
+                         {!   !} ≈⟨ {!   !} ⟩
+
+                         {!   !} ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ Equiv.sym Bμ-comp) ⟩
+                         {!   !} ≈⟨ Equiv.sym Aμ-comp ⟩
+                         {!   !} ∎) }
+{-
+Equiv.sym X.G.homomorphism ○ X.G.F-resp-≈ (Γᵤ.⇐.commute _) ○ X.G.homomorphism
+-}
+
+
+{-
+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
new file mode 100644
index 000000000..38e514049
--- /dev/null
+++ b/src/Categories/Adjoint/Construction/Adjunctions/Properties.agda
@@ -0,0 +1,211 @@
+{-# 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; _∘F_) renaming (id to idF)
+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
+open import Categories.Object.Initial Split
+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.μ.η _                          ≈⟨ id-comm-sym C ⟩
+             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.μ.η _                                               ≈⟨ id-comm-sym C ⟩
+             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
+        G.F₁ D.id ∘ (G.F₁ (adj.counit.η (F.₀ x) D.∘ F.₁ (GF≃M.⇐.η x ∘ M.F.F₁ id)) ∘ G.F₁ D.id ∘ adj.unit.η (M.F.F₀ x)) ∘ M.F.F₁ id
+          ≈⟨ elimˡ C G.identity ⟩
+        (G.F₁ (adj.counit.η (F.₀ x) D.∘ F.₁ (GF≃M.⇐.η x ∘ M.F.F₁ id)) ∘ G.F₁ D.id ∘ adj.unit.η (M.F.F₀ x)) ∘ M.F.F₁ id
+          ≈⟨ elimʳ C M.F.identity ⟩
+        G.F₁ (adj.counit.η (F.₀ x) D.∘ F.₁ (GF≃M.⇐.η x ∘ M.F.F₁ id)) ∘ G.F₁ D.id ∘ adj.unit.η (M.F.F₀ x)
+          ≈⟨ refl⟩∘⟨ elimˡ C G.identity ⟩
+        (G.F₁ ( adj.counit.η (F.₀ x) D.∘  F.₁ (GF≃M.⇐.η x ∘ M.F.F₁ id)) ∘ adj.unit.η (M.F.F₀ x))
+          ≈⟨ (G.homomorphism ⟩∘⟨refl) ⟩
+        ((G.F₁ (adj.counit.η (F.₀ x)) ∘ Functor.F₁ (G ∘F F) (GF≃M.⇐.η x ∘ M.F.F₁ id)) ∘ adj.unit.η (M.F.F₀ x))
+          ≈⟨ pullʳ C (adj.unit.sym-commute _) ⟩
+        (G.F₁ (adj.counit.η (F.₀ x)) ∘ adj.unit.η (G.F₀ (F.₀ x)) ∘ GF≃M.⇐.η x ∘ M.F.F₁ id)
+          ≈⟨ sym-assoc ⟩
+        (G.F₁ (adj.counit.η (F.₀ x)) ∘ adj.unit.η (G.F₀ (F.₀ x))) ∘ GF≃M.⇐.η x ∘ M.F.F₁ id
+          ≈⟨ elimˡ C adj.zag ⟩
+        (GF≃M.⇐.η x ∘ M.F.F₁ id)
+          ≈⟨ elimʳ C M.F.identity ⟩
+        GF≃M.⇐.η x ∎) }
+  } 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
+            Γ.⇐.η _ ∘ A.adj.counit.η (A.F.F₀ _) ∘ A.F.F₁ (A.GF≃M.⇐.η _ C.∘ f)
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ A.F.F-resp-≈ ((H.μ-comp CH.⟩∘⟨refl) CH.○ (C.assoc CH.○ (CH.refl⟩∘⟨ C.assoc))) ⟩
+            Γ.⇐.η _ ∘ A.adj.counit.η (A.F.F₀ _) ∘ A.F.F₁ (A.G.₁ (Γ.⇒.η _) C.∘ (A.G.₁ (H.H.F₁ (M.F.F₁ C.id)) C.∘ (A.G.₁ (Γ.⇐.η (M.F.F₀ _)) C.∘ A.adj.unit.η (M.F.F₀ _))) C.∘ M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ A.F.homomorphism ⟩
+            Γ.⇐.η _ ∘ A.adj.counit.η (A.F.F₀ _) ∘ Functor.F₁ (A.F Categories.Functor.∘F A.G) (Γ.⇒.η _) ∘ A.F.F₁ ((A.G.₁ (H.H.F₁ (M.F.F₁ C.id)) C.∘ A.G.₁ (Γ.⇐.η (M.F.F₀ _)) C.∘ A.adj.unit.η (M.F.F₀ _)) C.∘ M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ pullˡ A.D (A.adj.counit.commute _) ⟩
+            Γ.⇐.η _ ∘ (Γ.⇒.η _ ∘ A.adj.counit.η (H.H.F₀ (Functor.₀ K.F _))) ∘ A.F.F₁ ((A.G.₁ (H.H.F₁ (M.F.F₁ C.id)) C.∘ (A.G.₁ (Γ.⇐.η (M.F.F₀ _)) C.∘ A.adj.unit.η (M.F.F₀ _))) C.∘ M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ assoc ⟩
+            Γ.⇐.η _ ∘ Γ.⇒.η _ ∘ A.adj.counit.η (H.H.F₀ (Functor.₀ K.F _)) ∘ A.F.F₁ ((A.G.₁ (H.H.F₁ (M.F.F₁ C.id)) C.∘ A.G.₁ (Γ.⇐.η (M.F.F₀ _)) C.∘ A.adj.unit.η (M.F.F₀ _)) C.∘ M.F.F₁ C.id C.∘ f)
+              ≈⟨ cancelˡ A.D (Γ.iso.isoˡ _) ⟩
+            A.adj.counit.η (H.H.F₀ (Functor.₀ K.F _)) ∘ A.F.F₁ ((A.G.₁ (H.H.F₁ (M.F.F₁ C.id)) C.∘ (A.G.₁ (Γ.⇐.η (M.F.F₀ _)) C.∘ A.adj.unit.η (M.F.F₀ _))) C.∘ M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ A.F.homomorphism ⟩
+            A.adj.counit.η (H.H.F₀ (Functor.₀ K.F _)) ∘ A.F.F₁ (A.G.₁ (H.H.F₁ (M.F.F₁ C.id)) C.∘ A.G.₁ (Γ.⇐.η (M.F.F₀ _)) C.∘ A.adj.unit.η (M.F.F₀ _)) ∘ A.F.F₁ (M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ pushˡ A.D A.F.homomorphism ⟩
+            A.adj.counit.η (H.H.F₀ (Functor.₀ K.F _)) ∘ Functor.F₁ (A.F Categories.Functor.∘F A.G) (H.H.F₁ (M.F.F₁ C.id)) ∘ A.F.F₁ (A.G.₁ (Γ.⇐.η (M.F.F₀ _)) C.∘ A.adj.unit.η (M.F.F₀ _)) ∘ A.F.F₁ (M.F.F₁ C.id C.∘ f)
+              ≈⟨ extendʳ A.D (A.adj.counit.commute _) ⟩
+            H.H.F₁ (M.F.F₁ C.id) ∘ A.adj.counit.η (H.H.F₀ (Functor.₀ K.F (M.F.F₀ _))) ∘ A.F.F₁ (A.G.₁ (Γ.⇐.η (M.F.F₀ _)) C.∘ A.adj.unit.η (M.F.F₀ _)) ∘ A.F.F₁ (M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ A.D A.F.homomorphism ⟩
+            H.H.F₁ (M.F.F₁ C.id) ∘ A.adj.counit.η (H.H.F₀ (Functor.₀ K.F (M.F.F₀ _))) ∘ Functor.F₁ (A.F Categories.Functor.∘F A.G) (Γ.⇐.η (M.F.F₀ _)) ∘ A.F.F₁ (A.adj.unit.η (M.F.F₀ _)) ∘ A.F.F₁ (M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ extendʳ A.D (A.adj.counit.commute _) ⟩
+            H.H.F₁ (M.F.F₁ C.id) ∘ Γ.⇐.η (M.F.F₀ _) ∘ A.adj.counit.η (A.F.F₀ (M.F.F₀ _)) ∘ A.F.F₁ (A.adj.unit.η (M.F.F₀ _)) ∘ A.F.F₁ (M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ A.D A.adj.zig ⟩
+            H.H.F₁ (M.F.F₁ C.id) ∘ Γ.⇐.η (M.F.F₀ _) ∘ id ∘ A.F.F₁ (M.F.F₁ C.id C.∘ f)
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (identityˡ ○ A.F.F-resp-≈ (elimˡ C M.F.identity)) ⟩
+            H.H.F₁ (M.F.F₁ C.id) ∘ Γ.⇐.η (M.F.F₀ _) ∘ A.F.F₁ f
+              ≈⟨ refl⟩∘⟨ Γ.⇐.commute f ⟩
+            H.H.F₁ (M.F.F₁ C.id) ∘ H.H.F₁ (M.η.η (M.F.F₀ (Functor.₀ K.F _)) C.∘ f) ∘ Γ.⇐.η _
+              ≈⟨ pullˡ A.D (Equiv.sym H.H.homomorphism) ⟩
+            H.H.F₁ ((M.μ.η (Functor.₀ K.F _) C.∘ M.F.F₁ (M.F.F₁ C.id)) C.∘  M.η.η (M.F.F₀ (Functor.₀ K.F _)) C.∘ f) ∘ Γ.⇐.η _
+              ≈⟨ H.H.F-resp-≈ (elimʳ C (M.F.F-resp-≈ M.F.identity CH.○ M.F.identity) CH.⟩∘⟨refl) ⟩∘⟨refl ⟩
+            H.H.F₁ (M.μ.η (Functor.₀ K.F _) C.∘  M.η.η (M.F.F₀ (Functor.₀ K.F _)) C.∘ f) ∘ Γ.⇐.η _
+              ≈⟨ H.H.F-resp-≈ (pullˡ C M.identityʳ CH.○ C.identityˡ) ⟩∘⟨refl ⟩
+            H.H.F₁ f ∘ Γ.⇐.η _ ∎
+      ; iso = NaturalIsomorphism.iso (sym H.Γ)
+      })
+    }
+  }
diff --git a/src/Categories/NaturalTransformation/Core.agda b/src/Categories/NaturalTransformation/Core.agda
index db06af31e..77a842aa6 100644
--- 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)
diff --git a/src/Categories/Tactic/Category.agda b/src/Categories/Tactic/Category.agda
index 1ab24c52b..5f791c268 100644
--- a/src/Categories/Tactic/Category.agda
+++ b/src/Categories/Tactic/Category.agda
@@ -35,21 +35,21 @@ module _ {o ℓ e} (𝒞 : Category o ℓ e) where
       f g   : A ⇒ B
 
   --------------------------------------------------------------------------------
-  -- An 'Expr' reifies the parentheses/identity morphisms of some series of 
+  -- An 'Expr' reifies the parentheses/identity morphisms of some series of
   -- compositions of morphisms into a data structure. In fact, this is also
   -- a category!
   --------------------------------------------------------------------------------
   data Expr : Obj → Obj → Set (o ⊔ ℓ) where
-    _∘′_ : ∀ {A B C} → Expr B C → Expr A B → Expr A C 
+    _∘′_ : ∀ {A B C} → Expr B C → Expr A B → Expr A C
     id′  : ∀ {A} → Expr A A
     [_↑] : ∀ {A B} → A ⇒ B → Expr A B
-  
+
   -- Embed a morphism in 'Expr' back into '𝒞' without normalizing.
-  [_↓] : Expr A B → A ⇒ B 
+  [_↓] : Expr A B → A ⇒ B
   [ f ∘′ g ↓] = [ f ↓] ∘ [ g ↓]
   [ id′ ↓]    = id
   [ [ f ↑] ↓] = f
-  
+
   -- Convert an 'Expr' back into a morphism, while normalizing
   --
   -- This actually embeds the morphism into the category of copresheaves
@@ -60,7 +60,7 @@ module _ {o ℓ e} (𝒞 : Category o ℓ e) where
   embed id′ h       = h
   embed [ f ↑] h    = f ∘ h
 
-  
+
   preserves-≈′ : ∀ (f : Expr B C) → (h : A ⇒ B) → embed f id ∘ h ≈ embed f h
   preserves-≈′ id′ f      = identityˡ
   preserves-≈′ [ x ↑] f   = ∘-resp-≈ˡ identityʳ
@@ -71,7 +71,7 @@ module _ {o ℓ e} (𝒞 : Category o ℓ e) where
     embed f id ∘ embed g id ∘ h   ≈⟨ refl⟩∘⟨ preserves-≈′ g h ⟩
     embed f id ∘ embed g h        ≈⟨ preserves-≈′ f (embed g h) ⟩
     embed (f ∘′ g) h              ∎
-  
+
   preserves-≈ : ∀ (f : Expr A B) → embed f id ≈ [ f ↓]
   preserves-≈ id′      = refl
   preserves-≈ [ x ↑]   = identityʳ
@@ -181,4 +181,3 @@ solve-macro mon hole = do
 macro
   solve : Term → Term → TC _
   solve = solve-macro
-