Working on small lemma

src/Algebra/Elgot/Properties.lagda.md

@@ -5,6 +5,11 @@ open import Level
 open import Category.Instance.AmbientCategory
 open import Categories.Functor
 open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Categories.Object.Initial
+open import Categories.Object.Terminal
+open import Categories.Object.NaturalNumbers.Properties.F-Algebras
+open import Categories.Functor.Algebra
+open import Categories.Functor.Coalgebra
 ```
 -->
 
@@ -24,12 +29,65 @@ module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
   module _ {D : DelayM} (algebra : Guarded-Elgot-Algebra (DelayM.functor D)) where
     open DelayM D
     open Functor functor renaming (F₁ to D₁)
-    open RMonad kleisli
+    open RMonad kleisli using (extend)
     open Guarded-Elgot-Algebra algebra
+    open MR C
+    open M C
 
     commutes : α ∘ extend ι ≈ α ∘ (D₁ π₁)
     commutes = {!   !}
       where
         α∘ι : α ∘ ι ≈ π₁
-        α∘ι = {!   !}    
+        α∘ι = begin 
+          α ∘ ι ≈⟨ sym (IsInitial.!-unique isInitial (record { f = α ∘ ι ; commutes = begin 
+            (α ∘ ι) ∘ [ ⟨ idC , z ∘ _ ⟩ , idC ⁂ s ] ≈⟨ ∘[] ⟩ 
+            [ (α ∘ ι) ∘ ⟨ idC , z ∘ _ ⟩ , (α ∘ ι) ∘ (idC ⁂ s) ] ≈⟨ []-cong₂ helper₁ (pullʳ helper₂) ⟩ 
+            [ idC , α ∘ ι ] ≈˘⟨ {!   !} ⟩ 
+            {!   !} ≈˘⟨ {!   !} ⟩ 
+            [ idC , idC ] ∘ [ i₁ , i₂ ∘ α ∘ ι ] ∎ })) ⟩ 
+          F-Algebra-Morphism.f (IsInitial.! isInitial) ≈⟨ IsInitial.!-unique isInitial (record { f = π₁ ; commutes = begin 
+            π₁ ∘ [ ⟨ idC , z ∘ _ ⟩ , idC ⁂ s ] ≈⟨ ∘[] ⟩ 
+            [ π₁ ∘ ⟨ idC , z ∘ _ ⟩ , π₁ ∘ (idC ⁂ s) ] ≈⟨ []-cong₂ project₁ π₁∘⁂ ⟩ 
+            [ idC , idC ∘ π₁ ] ≈˘⟨ []-cong₂ inject₁ (pullˡ inject₂) ⟩ 
+            [ [ idC , idC ] ∘ i₁ , [ idC , idC ] ∘ i₂ ∘ π₁ ] ≈˘⟨ ∘[] ⟩ 
+            [ idC , idC ] ∘ [ i₁ , i₂ ∘ π₁ ] ∎ }) ⟩ 
+          π₁ ∎    
+          where
+            isInitial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ A
+            helper₁ = begin 
+              (α ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (sym (Terminal.!-unique (coalgebras A) (record { f = ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ; commutes = begin 
+                out ∘ ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ pullˡ ι-commutes ⟩ 
+                ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈˘⟨ refl⟩∘⟨ inject₁ ⟩ 
+                ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ pullʳ (cancelˡ (_≅_.isoʳ nno-iso)) ⟩ 
+                (idC +₁ ι) ∘ i₁ ≈⟨ +₁∘i₁ ○ identityʳ ⟩ 
+                i₁ ≈˘⟨ +₁∘i₁ ○ identityʳ ⟩ 
+                (idC +₁ ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩) ∘ i₁ ∎ }))) ⟩ 
+              α ∘ F-Coalgebra-Morphism.f (Terminal.! (coalgebras A)) ≈⟨ refl⟩∘⟨ (Terminal.!-unique (coalgebras A) (record { f = now ; commutes = begin 
+                out ∘ now ≈⟨ unitlaw ⟩ 
+                i₁ ≈˘⟨ +₁∘i₁ ○ identityʳ ⟩ 
+                (idC +₁ now) ∘ i₁ ∎ })) ⟩
+              α ∘ now ≈⟨ {!   !} ⟩ -- TODO elgot⇒search
+              idC ∎
+            helper₂ = begin 
+              ι ∘ (idC ⁂ s) ≈⟨ sym (Terminal.!-unique (coalgebras A) (record { f = ι ∘ (idC ⁂ s) ; commutes = begin 
+                out ∘ ι ∘ (idC ⁂ s) ≈⟨ pullˡ ι-commutes ⟩ 
+                ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ≈⟨ {!   !} ⟩ 
+                ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₂ ≈⟨ {!   !} ⟩ 
+                (idC +₁ ι) ∘ i₂ ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                ((idC +₁ ι) ∘ (idC +₁ (idC ⁂ s))) ∘ _≅_.from nno-iso ≈⟨ {!   !} ⟩ 
+                (idC +₁ ι ∘ (idC ⁂ s)) ∘ _≅_.from nno-iso ∎ })) ⟩ 
+              -- TODO remove last part, iota is the final morphism...
+              F-Coalgebra-Morphism.f (Terminal.! (coalgebras A)) ≈⟨ Terminal.!-unique (coalgebras A) (record { f = ι ; commutes = begin 
+                out ∘ ι ≈⟨ ι-commutes ⟩ 
+                (idC +₁ ι) ∘ _≅_.from nno-iso ∎ }) ⟩ 
+              ι ∎
+```
+
+- For every X, a final coalgebra Y → X + H Y is a free H-guarded algebra over X.
+
+```agda
+  -- final-to-guarded : ∀ {A} → ?η
 ```

src/Category/Instance/AmbientCategory.lagda.md

@@ -14,6 +14,9 @@ open import Categories.Category.Cartesian.Monoidal
 open import Categories.Category.Cartesian.SymmetricMonoidal using () renaming (symmetric to symm)
 open import Categories.Category.Monoidal
 open import Categories.Category.Monoidal.Symmetric
+open import Categories.Monad
+open import Categories.Monad.Construction.Kleisli
+open import Categories.Monad.Relative renaming (Monad to RMonad)
 open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
 open import Categories.Object.Exponential using (Exponential)
@@ -85,7 +88,6 @@ module Category.Instance.AmbientCategory where
       [ (idC ⁂ i₁) ∘ swap , (idC ⁂ i₂) ∘ swap ] ∘ distributeʳ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩ 
       distributeˡ ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ∎)
 
-
     dstr-law₁ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁
     dstr-law₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
     dstr-law₂ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₂) ≈ i₂
@@ -94,6 +96,12 @@ module Category.Instance.AmbientCategory where
     dstr-law₃ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ))
     dstr-law₄ : ∀ {A B C} → distributeʳ⁻¹ {A} {B} {C} ∘ (i₂ ⁂ idC) ≈ i₂
     dstr-law₄ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ))
+    dstr-law₅ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
+    dstr-law₅ = Iso⇒Epi C (IsIso.iso isIsoˡ) ((π₂ +₁ π₂) ∘ distributeˡ⁻¹) π₂ (begin 
+      (((π₂ +₁ π₂) ∘ distributeˡ⁻¹) ∘ distributeˡ) ≈⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩ 
+      (π₂ +₁ π₂) ≈˘⟨ []-cong₂ project₂ project₂ ⟩
+      [ π₂ ∘ _ , π₂ ∘ _ ] ≈˘⟨ ∘[] ⟩
+      π₂ ∘ distributeˡ ∎)
     distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
     distribute₂ = sym (begin 
       π₂                                                      ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ 
@@ -101,6 +109,22 @@ module Category.Instance.AmbientCategory where
       [ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
       (π₂ +₁ π₂) ∘ distributeˡ⁻¹                              ∎)
 
+    distributeˡ⁻¹-assoc : ∀ {A B C D : Obj} → distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc ≈ (_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹ {A × B} {C} {D}
+    distributeˡ⁻¹-assoc {A} {B} {U} {D} = Iso⇒Epi C (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) (begin 
+      (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ [ idC ⁂ i₁ , idC ⁂ i₂ ] ≈⟨ ∘[] ⟩ 
+      [ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (idC ⁂ i₁) , (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (idC ⁂ i₂) ] ≈⟨ []-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (pullʳ (pullʳ ⟨⟩∘)) ⟩ 
+      [ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩ 
+      [ distributeˡ⁻¹ ∘ ⟨ idC ∘ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ idC ∘ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩ 
+      [ distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘))) (refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘)) ⟩ 
+      [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) ⟩ 
+      [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) ⟩ 
+      [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) ⟩  
+      [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ dstr-law₁))) (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ dstr-law₂))) ⟩ 
+      [ distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩ 
+      [ distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (pullˡ dstr-law₁) (pullˡ dstr-law₂) ⟩ 
+      (_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩ 
+      ((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
+
     module M = M'
     module MR = MR'
 
@@ -127,18 +151,8 @@ module Category.Instance.AmbientCategory where
         [ ((g +₁ h) ⁂ f) ∘ (i₁ ⁂ idC) , ((g +₁ h) ⁂ f) ∘ (i₂ ⁂ idC) ] ≈˘⟨ ∘[] ⟩ 
         (((g +₁ h) ⁂ f) ∘ distributeʳ) ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoʳ) ⟩∘⟨refl ⟩ 
         (distributeʳ ∘ distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f)) ∘ distributeʳ ∎))
-    dstldstr : ∀ {X Y U V} → (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ (distributeˡ⁻¹ {X + Y} {U} {V})
-    dstldstr = Iso⇒Epi C (IsIso.iso isIsoˡ) ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) (sym (begin 
-      (([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeˡ) ≈⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoˡ)) ⟩ 
-      ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹)) ≈⟨ []∘+₁ ⟩ 
-      [ (i₁ +₁ i₁) ∘ distributeʳ⁻¹ , (i₂ +₁ i₂) ∘ distributeʳ⁻¹ ] ≈⟨ {!   !} ⟩ 
-      {!   !} ≈˘⟨ {!   !} ⟩ 
-      {!   !} ≈˘⟨ {!   !} ⟩ 
-      {!   !} ≈˘⟨ {!   !} ⟩ 
-      {!   !} ≈˘⟨ {!   !} ⟩ 
-      [ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (idC ⁂ i₁) , ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (idC ⁂ i₂) ] ≈˘⟨ ∘[] ⟩ 
-      (((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ distributeˡ) ∎))
   
+    -- TODO replace with use of Iso⇒Epi etc.
     iso-epi-from : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.from iso)
     iso-epi-from iso = λ f g eq → begin 
       f ≈⟨ introʳ (_≅_.isoʳ iso) ⟩ 
@@ -151,4 +165,29 @@ module Category.Instance.AmbientCategory where
       (f ∘ M'._≅_.to iso ∘ M'._≅_.from iso) ≈⟨ pullˡ eq ⟩
       ((g ∘ M'._≅_.to iso) ∘ M'._≅_.from iso) ≈⟨ cancelʳ (_≅_.isoˡ iso) ⟩
       g ∎
+
+    -- TODO should be in agda-categories
+    Kleisli⇒Monad⇒Kleisli : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend (Monad⇒Kleisli C (Kleisli⇒Monad C K)) f ≈ RMonad.extend K f
+    Kleisli⇒Monad⇒Kleisli K f = begin 
+      extend idC ∘ extend (unit ∘ f) ≈⟨ sym kleisli.assoc ⟩ 
+      extend (extend idC ∘ unit ∘ f) ≈⟨ extend-≈ (pullˡ kleisli.identityʳ) ⟩
+      extend (idC ∘ f)               ≈⟨ extend-≈ (identityˡ) ⟩
+      extend f                       ∎
+      where 
+        module kleisli = RMonad K 
+        open kleisli using (unit; extend; extend-≈)
+    Monad⇒Kleisli⇒Monad : ∀ (M : Monad C) {X Y} (f : X ⇒ Monad.F.₀ M Y) → Monad.F.₁ (Kleisli⇒Monad C (Monad⇒Kleisli C M)) f ≈ Monad.F.₁ M f
+    Monad⇒Kleisli⇒Monad M f = begin 
+      μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩ 
+      μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ monad.identityˡ ⟩ 
+      F.₁ f ∎
+      where
+        module monad = Monad M
+        open monad using (F; η; μ)
+    F₁⇒extend : ∀ (M : Monad C) {X Y} (f : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) (RMonad.unit (Monad⇒Kleisli C M) ∘ f) ≈ Monad.F.₁ M f
+    F₁⇒extend M f = begin 
+      μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩ 
+      μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ m-identityˡ ⟩ 
+      F.₁ f ∎
+      where open Monad M using (F; η; μ) renaming (identityˡ to m-identityˡ)
 ```

src/Monad/Instance/Delay.lagda.md

@@ -105,8 +105,14 @@ At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y
       nno-iso : X × N ≅ X + X × N
       nno-iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X })
 
+      ι-coalg : F-Coalgebra-Morphism (record { A = X × N ; α = _≅_.from nno-iso }) (record { A = DX ; α = out })
+      ι-coalg = ! {A = record { A = X × N ; α = _≅_.from nno-iso }}
+
       ι : X × N ⇒ DX
-      ι = u (! {A = record { A = X × N ; α = _≅_.from nno-iso }})
+      ι = u ι-coalg
+
+      ι-commutes : out ∘ ι ≈ (idC +₁ ι) ∘ _≅_.from nno-iso
+      ι-commutes = commutes ι-coalg
 ```
 
 ## Delay is a monad

src/Monad/Instance/Delay/Commutative.lagda.md

@@ -30,15 +30,6 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D
   open import Categories.Morphism.Properties C
   open Terminal using (!; !-unique; ⊤)
 
-  -- TODO should be in agda-categories
-  Kleisli⇒Monad⇒Kleisli : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend (Monad⇒Kleisli C (Kleisli⇒Monad C K)) f ≈ RMonad.extend K f
-  Kleisli⇒Monad⇒Kleisli K {X} {Y} f = begin 
-    extend idC ∘ extend (unit ∘ f) ≈⟨ sym k-assoc ⟩ 
-    extend (extend idC ∘ unit ∘ f) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
-    extend (idC ∘ f)               ≈⟨ extend-≈ (identityˡ) ⟩
-    extend f                       ∎
-    where open RMonad K using (unit; extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
-
   open DelayM D
   open import Monad.Instance.Delay.Strong ambient D
   open Functor functor using () renaming (F₁ to D₁; identity to D-identity; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈)

src/Monad/Instance/Delay/Lemmas.lagda.md

@@ -0,0 +1,30 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory
+open import Categories.Functor
+open import Categories.Monad.Relative using () renaming (Monad to RMonad)
+```
+-->
+
+```agda
+module Monad.Instance.Delay.Lemmas {o ℓ e} (ambient : Ambient o ℓ e) where 
+open Ambient ambient
+open import Monad.Instance.Delay ambient
+open import Monad.Instance.Delay.Strong ambient
+open import Monad.Instance.Delay.Commutative ambient
+open M C
+```
+
+# Helper Lemmas concerning the Delay Monad
+
+```agda
+module _ (D : DelayM) where
+  open DelayM D
+  module D = Functor functor
+  open RMonad kleisli using (extend)
+  
+  
+  Lemma47 : ⟨ D.₁ π₁ , D.₁ π₂ ⟩ SectionOf {!   !}
+  Lemma47 = {!   !}
+```

src/Monad/Instance/K.lagda.md

@@ -10,6 +10,8 @@ open import Categories.Adjoint
 open import Categories.Adjoint.Properties
 open import Categories.Monad
 open import Categories.Monad.Strong
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Categories.Monad.Construction.Kleisli
 open import Category.Instance.AmbientCategory using (Ambient)
 open import Categories.NaturalTransformation
 open import Categories.Object.Terminal
@@ -35,10 +37,12 @@ In this file I explore the monad ***K*** and its properties:
 module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
   open import Category.Construction.UniformIterationAlgebras ambient
-  open import Algebra.UniformIterationAlgebra
+  open import Algebra.UniformIterationAlgebra ambient
   open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
 
   open Equiv
+  open MR C
+  open M C
   open HomReasoning
 
 ```
@@ -48,13 +52,13 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
 ```agda
   record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where
     field
-      algebras : ∀ X → FreeUniformIterationAlgebra X
+      freealgebras : ∀ X → FreeUniformIterationAlgebra X
 
     freeF : Functor C Uniform-Iteration-Algebras
-    freeF = FO⇒Functor uniformForgetfulF algebras
+    freeF = FO⇒Functor uniformForgetfulF freealgebras
     
     adjoint : freeF ⊣ uniformForgetfulF
-    adjoint = FO⇒LAdj uniformForgetfulF algebras
+    adjoint = FO⇒LAdj uniformForgetfulF freealgebras
 
     K : Monad C
     K = adjoint⇒monad adjoint
@@ -65,13 +69,18 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
 ```agda
   record MonadKStrong : Set (suc o ⊔ suc ℓ ⊔ suc e) where
     field
-      algebras : ∀ X → FreeUniformIterationAlgebra X
+      freealgebras : ∀ X → FreeUniformIterationAlgebra X
-      stable : ∀ X → IsStableFreeUniformIterationAlgebra (algebras X)
+      stable : ∀ X → IsStableFreeUniformIterationAlgebra (freealgebras X)
+    
+    algebras : ∀ (X : Obj) → Uniform-Iteration-Algebra
+    algebras X = FreeObject.FX (freealgebras X)
 
     K : Monad C
-    K = MonadK.K (record { algebras = algebras })
+    K = MonadK.K (record { freealgebras = freealgebras })
 
-    open Monad K using (F)
+    open Monad K using (F; μ) renaming (identityʳ to m-identityʳ)
+    module kleisli = RMonad (Monad⇒Kleisli C K)
+    open kleisli using (extend)
     open Functor F using () renaming (F₀ to K₀; F₁ to K₁)
 
     KStrong : StrongMonad {C = C} monoidal
@@ -79,47 +88,195 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
       { M = K
       ; strength = record
         { strengthen = ntHelper (record { η = τ ; commute = commute' })
-        ; identityˡ = λ {X} → begin 
+        ; identityˡ = identityˡ'
-          K₁ π₂ ∘ τ _ ≈⟨ refl ⟩
+        ; η-comm = λ {A} {B} → τ-η (A , B)
-          Uniform-Iteration-Algebra-Morphism.h ((algebras (Terminal.⊤ terminal × X) FreeObject.*) (FreeObject.η (algebras X) ∘ π₂)) ∘ τ _ ≈⟨ {!   !} ⟩
+        ; μ-η-comm = μ-η-comm'
-          {!   !} ≈⟨ {!   !} ⟩
+        ; strength-assoc = strength-assoc'
-          {!   !} ≈⟨ {!   !} ⟩
-          π₂ ∎
-        ; η-comm = λ {A} {B} → begin τ _ ∘ (idC ⁂ η (A , B) B) ≈⟨ τ-η (A , B) ⟩ η (A , B) (A × B) ∎
-        ; μ-η-comm = λ {A} {B} → {!   !}
-        ; strength-assoc = λ {A} {B} {D} → begin 
-          K₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ τ _ ≈⟨ {!   !} ⟩ 
-          τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
         }
       }
       where
         open import Agda.Builtin.Sigma
-        open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving)
+        open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
+        open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
+        η = λ Z → FreeObject.η (freealgebras Z)
+        _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
+        _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
 
         module _ (P : Category.Obj (CProduct C C)) where
-          η = λ Z → FreeObject.η (algebras Z)
+          private
-          [_,_,_]♯ = λ {A} X Y f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} Y f
-
-
             X = fst P
             Y = snd P
           τ : X × K₀ Y ⇒ K₀ (X × Y)
-          τ = [ Y , FreeObject.FX (algebras (X × Y)) , η (X × Y) ]♯
+          τ = η (X × Y) ♯
 
           τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
           τ-η = sym (♯-law (stable Y) (η (X × Y)))
 
-        [_,_]# : ∀ (A : Uniform-Iteration-Algebra ambient) {X} → (X ⇒ ((Uniform-Iteration-Algebra.A A) + X)) → (X ⇒ Uniform-Iteration-Algebra.A A)
+        τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ h #) ≈ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
-        [ A , f ]# = Uniform-Iteration-Algebra._# A f
+        τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X × Y)) h
 
-        τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ [ FreeObject.FX (algebras Y) , h ]#) ≈ [ FreeObject.FX (algebras (X × Y)) , (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ]#
+        K₁η : ∀ {X Y} (f : X ⇒ Y) → K₁ f ∘ η X ≈ η Y ∘ f
-        τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X , Y) (X × Y)) h
+        K₁η {X} {Y} f = begin 
+          K₁ f ∘ η X ≈⟨ (sym (F₁⇒extend K f)) ⟩∘⟨refl ⟩ 
+          extend (η Y ∘ f) ∘ η X ≈⟨ kleisli.identityʳ ⟩ 
+          η Y ∘ f ∎
+
+        μ-η-comm' : ∀ {A B} → μ.η _ ∘ K₁ (τ _) ∘ τ (A , K₀ B) ≈ τ _ ∘ (idC ⁂ μ.η _)
+        μ-η-comm' {A} {B} = begin 
+          μ.η _ ∘ K₁ (τ _) ∘ τ _ ≈⟨ ♯-unique (stable (K₀ B)) (τ (A , B)) (μ.η _ ∘ K₁ (τ _) ∘ τ _) comm₁ comm₂ ⟩ 
+          (τ _ ♯) ≈⟨ sym (♯-unique (stable (K₀ B)) (τ (A , B)) (τ _ ∘ (idC ⁂ μ.η _)) (sym (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² m-identityʳ ○ ⟨⟩-unique id-comm id-comm))) comm₃) ⟩ 
+          τ _ ∘ (idC ⁂ μ.η _) ∎
+          where
+            comm₁ : τ (A , B) ≈ (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _)
+            comm₁ = sym (begin 
+              (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ 
+              μ.η _ ∘ K₁ (τ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η (τ (A , B))) ⟩ 
+              μ.η _ ∘ η _ ∘ τ _ ≈⟨ cancelˡ m-identityʳ ⟩ 
+              τ _ ∎)
+            comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ (K₀ B) + Z) → (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+            comm₂ {Z} h = begin 
+              (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (τ-comm h)) ⟩ 
+              μ.η _ ∘ K₁ (τ _) ∘ (((τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ τ _))) ⟩ 
+              μ.η _ ∘ ((K₁ (τ _) +₁ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩ 
+              ((μ.η _ +₁ idC) ∘ (K₁ (τ _) +₁ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ 
+              ((μ.η _ ∘ K₁ (τ _) +₁ idC ∘ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
+              (((μ.η _ ∘ K₁ (τ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (cancelʳ identity²)) ⟩∘⟨refl) ⟩
+              ((μ.η _ ∘ K₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
+            comm₃ : ∀ {Z : Obj} (h : Z ⇒ K₀ (K₀ B) + Z) → (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+            comm₃ {Z} h = begin 
+              (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
+              τ _ ∘ (idC ∘ idC ⁂ μ.η _ ∘ h #) ≈⟨ refl⟩∘⟨ (⁂-cong₂ identity² (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC))) ⟩ 
+              τ _ ∘ (idC ⁂ ((μ.η _ +₁ idC) ∘ h) #) ≈⟨ τ-comm ((μ.η B +₁ idC) ∘ h) ⟩ 
+              ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (μ.η B +₁ idC) ∘ h)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂))) ⟩ 
+              ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (μ.η B +₁ idC)) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁ idC (μ.η B) idC)))) ⟩
+              ((τ _ +₁ idC) ∘ ((idC ⁂ μ.η B +₁ idC ⁂ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩ 
+              (((τ _ ∘ (idC ⁂ μ.η B) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) assoc ⟩
+              ((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
+
+        module assoc {A} {B} {C} = _≅_ (×-assoc {A} {B} {C})
+
+        strength-assoc' : ∀ {X Y Z} → K₁ assoc.to ∘ τ (X × Y , Z) ≈ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to
+        strength-assoc' {X} {Y} {Z} = begin
+          K₁ assoc.to ∘ τ _ ≈⟨ ♯-unique (stable _) (η (X × Y × Z) ∘ assoc.to) (K₁ assoc.to ∘ τ _) (sym (pullʳ (τ-η _) ○ K₁η _)) comm₁ ⟩ 
+          ((η (X × Y × Z) ∘ assoc.to) ♯) ≈⟨ sym (♯-unique (stable _) (η (X × Y × Z) ∘ assoc.to) (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) comm₂ comm₃) ⟩
+          τ _ ∘ (idC ⁂ τ _) ∘ assoc.to ∎
+          where
+            comm₁ : ∀ {A : Obj} (h : A ⇒ K₀ Z + A) → (K₁ assoc.to ∘ τ _) ∘ (idC ⁂ h #) ≈ ((K₁ assoc.to ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+            comm₁ {A} h = begin 
+              (K₁ assoc.to ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (τ-comm h) ⟩ 
+              K₁ assoc.to ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _) ⟩ 
+              ((K₁ assoc.to +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
+              ((K₁ assoc.to ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
+            comm₂ : η (X × Y × Z) ∘ assoc.to ≈ (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ η _)
+            comm₂ = sym (begin 
+              (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ η _) ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩ 
+              (τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ η _) ≈⟨ pullʳ ⟨⟩∘ ⟩ 
+              τ _ ∘ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ η _) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ η _) ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩ 
+              τ _ ∘ ⟨ π₁ ∘ idC ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ η _) , π₂ ∘ (idC ⁂ η _) ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩ 
+              τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , η _ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) refl) ○ sym ⁂∘⟨⟩))) ⟩ 
+              τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ (idC ⁂ η _) ∘ ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (τ-η (Y , Z)))) ⟩ 
+              τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , η _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩ 
+              τ _ ∘ (idC ⁂ η _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-η _) ⟩ 
+              η _ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl) ⟩ 
+              η (X × Y × Z) ∘ assoc.to ∎)
+            comm₃ : ∀ {A : Obj} (h : A ⇒ K₀ Z + A) → (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ τ _) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+            comm₃ {A} h = begin 
+              (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ h #) ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩ 
+              (τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⟨⟩∘ ⟩ 
+              τ _ ∘ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ h #) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ h #) ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩ 
+              τ _ ∘ ⟨ π₁ ∘ idC ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ h #) , π₂ ∘ (idC ⁂ h #) ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩ 
+              τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , h # ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl))) ⟩ 
+              τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ idC ∘ π₂ ∘ π₁ , h # ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ (sym ⁂∘⟨⟩)) ⟩ 
+              τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ (idC ⁂ h #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ (τ-comm h))) ⟩ 
+              τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , (((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩ 
+              τ _ ∘ (idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ assoc.to ≈⟨ pullˡ (τ-comm _) ⟩ 
+              ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) # ∘ assoc.to ≈⟨ sym (#-Uniformity (algebras _) (begin 
+                (idC +₁ assoc.to) ∘ (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
+                (idC ∘ τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ assoc.to ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
+                (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ idC ∘ assoc.to) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ (+₁∘+₁ ○ +₁-cong₂ assoc refl) ⟩∘⟨refl ⟩ 
+                ((τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (assoc.to +₁ assoc.to)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹-assoc)) ⟩ 
+                (τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ assoc²' ⟩ 
+                (τ _ ∘ (idC ⁂ τ _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈˘⟨ (+₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ⟩ 
+                (τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈˘⟨ assoc ○ assoc ⟩
+                (((τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ _≅_.to ×-assoc ∘ (idC ⁂ h) ≈˘⟨ pullˡ (pullˡ (pullˡ +₁∘+₁)) ⟩
+                (τ _ +₁ idC) ∘ ((((idC ⁂ τ _) +₁ (idC ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ ((distribute₁ idC (τ (Y , Z)) idC) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
+                (τ _ +₁ idC) ∘ ((distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC))) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (assoc ○ assoc ○ refl⟩∘⟨ sym-assoc) ⟩
+                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC)) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩∘⟨refl ⟩ 
+                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl ⟩ 
+                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assoc.to ∘ ((idC ⁂ idC) ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⁂ ⟩ 
+                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h)) ∘ assoc.to ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
+                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h))) ∘ assoc.to ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂∘⁂ ⟩∘⟨refl ⟩ 
+                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) ∘ assoc.to ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ((⁂-cong₂ identity² assoc) ⟩∘⟨refl) ○ sym-assoc) ○ sym-assoc ⟩
+                ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ∘ assoc.to ∎)) ⟩
+              ((τ _ ∘ (idC ⁂ τ _) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
         
         commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) 
           → τ P₂ ∘ ((fst fg) ⁂ K₁ (snd fg)) ≈ K₁ ((fst fg) ⁂ (snd fg)) ∘ τ P₁
         commute' {(U , V)} {(W , X)} (f , g) = begin 
-          τ _ ∘ (f ⁂ Uniform-Iteration-Algebra-Morphism.h ((algebras V FreeObject.*) (FreeObject.η (algebras X) ∘ g))) ≈⟨ {!   !} ⟩ 
+          τ _ ∘ (f ⁂ K₁ g) ≈⟨ ♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (τ _ ∘ (f ⁂ K₁ g)) comm₁ comm₂ ⟩ 
-          {!   !} ≈⟨ {!   !} ⟩
+          (η _ ∘ (f ⁂ g)) ♯ ≈⟨ sym (♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (K₁ (f ⁂ g) ∘ τ _) comm₃ comm₄) ⟩
-          {!   !} ≈⟨ {!   !} ⟩
+          K₁ (f ⁂ g) ∘ τ _ ∎
-          Uniform-Iteration-Algebra-Morphism.h ((algebras (U × V) FreeObject.*) (FreeObject.η (algebras (W × X)) ∘ (f ⁂ g))) ∘ τ _ ∎
+          where
+            comm₁ : η (W × X) ∘ (f ⁂ g) ≈ (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ η V)
+            comm₁ = sym (begin 
+              (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ η V) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
+              τ (W , X) ∘ (f ∘ idC ⁂ K₁ g ∘ η V) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm (K₁η g)) ⟩ 
+              τ (W , X) ∘ (idC ∘ f ⁂ η X ∘ g) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩ 
+              τ (W , X) ∘ (idC ⁂ η X) ∘ (f ⁂ g) ≈⟨ pullˡ (τ-η (W , X)) ⟩ 
+              η (W × X) ∘ (f ⁂ g) ∎)
+            comm₃ : η (W × X) ∘ (f ⁂ g) ≈ (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V)
+            comm₃ = sym (begin
+              (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V) ≈⟨ pullʳ (τ-η (U , V)) ⟩ 
+              K₁ (f ⁂ g) ∘ η (U × V) ≈⟨ K₁η (f ⁂ g) ⟩ 
+              η (W × X) ∘ (f ⁂ g) ∎)
+            comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ V + Z) → (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ h #) ≈ ((τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
+            comm₂ {Z} h = begin 
+              (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
+              τ (W , X) ∘ (f ∘ idC ⁂ K₁ g ∘ (h #)) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm ((Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η X ∘ g))) ○ sym identityʳ)) ⟩ 
+              τ (W , X) ∘ (idC ∘ f ⁂ ((K₁ g +₁ idC) ∘ h) # ∘ idC) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩ 
+              τ (W , X) ∘ (idC ⁂ ((K₁ g +₁ idC) ∘ h) #) ∘ (f ⁂ idC) ≈⟨ pullˡ (♯-preserving (stable _) (η _) ((K₁ g +₁ idC) ∘ h)) ⟩ 
+              ((τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (K₁ g +₁ idC) ∘ h)) # ∘ (f ⁂ idC) ≈⟨ sym (#-Uniformity (algebras _) (begin 
+                (idC +₁ f ⁂ idC) ∘ (τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
+                (idC ∘ τ (W , X) ∘ (f ⁂ K₁ g) +₁ (f ⁂ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
+                (τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC ∘ (f ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ 
+                ((τ (W , X) +₁ idC) ∘ ((f ⁂ K₁ g) +₁ (f ⁂ idC))) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullʳ (pullˡ (distribute₁ f (K₁ g) idC)) ⟩ 
+                (τ (W , X) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (f ⁂ (K₁ g +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ refl)) ⟩ 
+                (τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (f ⁂ (K₁ g +₁ idC) ∘ h) ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ)) ⟩ 
+                ((τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (K₁ g +₁ idC) ∘ h)) ∘ (f ⁂ idC) ∎)) ⟩ 
+              ((τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎ 
+            comm₄ : ∀ {Z : Obj} (h : Z ⇒ K₀ V + Z) → (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ h #) ≈ ((K₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+            comm₄ {Z} h = begin 
+              (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ (h #)) ≈⟨ pullʳ (τ-comm h) ⟩ 
+              K₁ (f ⁂ g) ∘ ((τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η (W × X) ∘ (f ⁂ g))) ⟩ 
+              ((K₁ (f ⁂ g) +₁ idC) ∘ (τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras (W × X)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
+              ((K₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
+
+        identityˡ' : ∀ {X : Obj} → K₁ π₂ ∘ τ _ ≈ π₂
+        identityˡ' {X} = begin 
+          K₁ π₂ ∘ τ _ ≈⟨ ♯-unique (stable X) (η X ∘ π₂) (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) comm₁ comm₂ ⟩
+          (η X ∘ π₂) ♯ ≈⟨ sym (♯-unique (stable X) (η X ∘ π₂) π₂ (sym π₂∘⁂) comm₃) ⟩
+          π₂ ∎
+          where
+            comm₁ : η X ∘ π₂ ≈ (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X)
+            comm₁ = sym (begin 
+              (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X) ≈⟨ pullʳ (τ-η (Terminal.⊤ terminal , X)) ⟩ 
+              K₁ π₂ ∘ η (Terminal.⊤ terminal × X) ≈⟨ (sym (F₁⇒extend K π₂)) ⟩∘⟨refl ⟩
+              extend (η _ ∘ π₂) ∘ η _ ≈⟨ kleisli.identityʳ ⟩
+              η X ∘ π₂ ∎)
+            comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ X + Z) → (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ h # ) ≈ ((K₁ π₂ ∘ τ (Terminal.⊤ terminal , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
+            comm₂ {Z} h = begin
+              (K₁ π₂ ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (♯-preserving (stable X) (η _) h) ⟩ 
+              K₁ π₂ ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras (Terminal.⊤ terminal × X) FreeObject.*) (η X ∘ π₂)) ⟩
+              ((K₁ π₂ +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras X) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
+              ((K₁ π₂ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
+            comm₃ : ∀ {Z : Obj} (h : Z ⇒ K₀ X + Z) → π₂ ∘ (idC ⁂ h #) ≈ ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+            comm₃ {Z} h = begin 
+              π₂ ∘ (idC ⁂ h #) ≈⟨ π₂∘⁂ ⟩ 
+              h # ∘ π₂ ≈⟨ sym (#-Uniformity (algebras X) (begin 
+                (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
+                (idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ 
+                (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ dstr-law₅ ⟩ 
+                π₂ ∘ (idC ⁂ h) ≈⟨ project₂ ⟩ 
+                h ∘ π₂ ∎)) ⟩ 
+              ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
 ```