diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md
index c458582..38f151e 100644
--- a/src/Monad/Instance/K/Commutative.lagda.md
+++ b/src/Monad/Instance/K/Commutative.lagda.md
@@ -210,37 +210,48 @@ KCommutative = record { commutes = commutes' }
                   (idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎
             comm₈ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#
             comm₈ {U} g = begin
-              ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩ 
-              ((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
-              (((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #  ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
-              (((extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ((η (U × K.₀ Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩
-              extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym (τ-η _)) refl) ⟩∘⟨refl)) ⟩
-              extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ refl⟩∘⟨ (τ-comm ((η (K.₀ Y) +₁ idC) ∘ h) ○ #-resp-≈ (algebras _) comm) ⟩
-              extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h)#) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
-              extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ ((η (K.₀ X × K.₀ Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)))) ⟩∘⟨refl ⟩
-              extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
-              extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁' idC (η (K.₀ X)) idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ σ-η (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
-              extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ⁂ idC) ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))))) ⟩∘⟨refl ⟩
-              extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ∘ g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (σ-comm ((η (K.₀ X) +₁ idC) ∘ g))) ⟩∘⟨refl) ⟩
-              extend ψ ∘ extend (σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ idC)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) (((η _ +₁ idC) ∘ g) # ⁂ idC))) ⟩
-              extend ψ ∘ extend (σ _) ∘ K.₁ (((η _ +₁ idC) ∘ g) # ⁂ idC) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
-              {! extend ψ ∘ extend (σ _) ∘ τ _ ∘ K.₁ (((η _ +₁ idC) ∘ g) # ⁂ idC) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #)  !} ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
+              ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ στ ⟩
+              extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ {!   !} ⟩ -- lemma 42
+              extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ sym τσ ⟩
               ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
               where
-                by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈ (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
-                by-uni = begin 
-                  ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩ 
-                  (ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((g #) ⁂ idC) ∘ (idC ⁂ h) ≈⟨ {!   !} ⟩ 
-                  (ψ +₁ idC) ∘ ((((g #) ⁂ idC) +₁ ((g #) ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym ○ sym +₁∘+₁)) ⟩ 
-                  (((idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc² ⟩ 
-                  (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
-                comm : (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ≈ (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
-                comm = sym (begin 
-                  (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩ 
-                  (τ _ +₁ idC) ∘ ((idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η (K.₀ Y)) idC)) ⟩ 
-                  (τ _ +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ 
-                  (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ∎)
+                τσ : ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ≈ extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
+                τσ = begin 
+                  (((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ≈⟨ {!   !} ⟩ 
+                  {!   !} ≈⟨ {!   !} ⟩ 
+                  {!   !} ≈⟨ {!   !} ⟩ 
+                  {!   !} ≈⟨ {!   !} ⟩ 
+                  extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
+                στ : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈ extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
+                στ = begin
+                  ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩ 
+                  ((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
+                  (((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #  ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
+                  (((extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ((η (U × K.₀ Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩
+                  extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym (τ-η _)) refl) ⟩∘⟨refl)) ⟩
+                  extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ refl⟩∘⟨ (τ-comm ((η (K.₀ Y) +₁ idC) ∘ h) ○ #-resp-≈ (algebras _) comm) ⟩
+                  extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h)#) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
+                  extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ ((η (K.₀ X × K.₀ Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)))) ⟩∘⟨refl ⟩
+                  extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
+                  extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁' idC (η (K.₀ X)) idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ σ-η (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
+                  extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ⁂ idC) ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))))) ⟩∘⟨refl ⟩
+                  extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ∘ g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (σ-comm ((η (K.₀ X) +₁ idC) ∘ g))) ⟩∘⟨refl) ⟩
+                  extend ψ ∘ extend (σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ idC)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) (((η _ +₁ idC) ∘ g) # ⁂ idC))) ⟩
+                  extend ψ ∘ extend (σ _) ∘ K.₁ (((η _ +₁ idC) ∘ g) # ⁂ idC) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (strengthen.commute (((η (K.₀ X) +₁ idC) ∘ g) # , idC))) ⟩
+                  extend ψ ∘ extend (σ _) ∘ (τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ K.₁ idC)) ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ monadK.F.identity))) ⟩
+                  extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
+                  where
+                    by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈ (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
+                    by-uni = begin 
+                      ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩ 
+                      (ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((g #) ⁂ idC) ∘ (idC ⁂ h) ≈⟨ {!   !} ⟩ 
+                      (ψ +₁ idC) ∘ ((((g #) ⁂ idC) +₁ ((g #) ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym ○ sym +₁∘+₁)) ⟩ 
+                      (((idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc² ⟩ 
+                      (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
+                    comm : (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ≈ (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
+                    comm = sym (begin 
+                      (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩ 
+                      (τ _ +₁ idC) ∘ ((idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η (K.₀ Y)) idC)) ⟩ 
+                      (τ _ +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ 
+                      (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ∎)
 ```