✨ Finished proving strength of delay monad

src/Category/Instance/AmbientCategory.lagda.md

@@ -83,4 +83,23 @@ module Category.Instance.AmbientCategory where
         open MR C
         open HomReasoning
         open Equiv
+  
+    iso-epi-from : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.from iso)
+    iso-epi-from iso = λ f g eq → begin 
+      f ≈⟨ introʳ (_≅_.isoʳ iso) ⟩ 
+      (f ∘ M'._≅_.from iso ∘ M'._≅_.to iso) ≈⟨ pullˡ eq ⟩
+      ((g ∘ M'._≅_.from iso) ∘ M'._≅_.to iso) ≈⟨ cancelʳ (_≅_.isoʳ iso) ⟩
+      g ∎
+      where 
+        open HomReasoning
+        open MR C
+    iso-epi-to : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.to iso)
+    iso-epi-to iso = λ f g eq → begin 
+      f ≈⟨ introʳ (_≅_.isoˡ iso) ⟩ 
+      (f ∘ M'._≅_.to iso ∘ M'._≅_.from iso) ≈⟨ pullˡ eq ⟩
+      ((g ∘ M'._≅_.to iso) ∘ M'._≅_.from iso) ≈⟨ cancelʳ (_≅_.isoˡ iso) ⟩
+      g ∎
+      where 
+        open HomReasoning
+        open MR C
 ```

src/Monad/Instance/Delay.lagda.md

@@ -22,6 +22,8 @@ module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
 ```
 
+-- TODO SERGEYS LÖSUNG: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
+
 ## Definition
 
 The delay monad is usually defined as a coinductive type with two constructors `now : X → D X` and `later : D X → D X`, e.g. in the [agda-stdlib](https://agda.github.io/agda-stdlib/Effect.Monad.Partiality.html#1523)
@@ -72,7 +74,6 @@ We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inver
 
       unitlaw : out ∘ now ≈ i₁
       unitlaw = cancelˡ (_≅_.isoʳ out-≅)
-
 ```
 
 Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the final coalgebras to get a *coiteration operator* `coit`:
@@ -100,7 +101,6 @@ At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y
 
       ι : X × N ⇒ DX
       ι = u (! {A = record { A = X × N ; α = _≅_.from nno-iso }})
-
 ```
 
 ## Delay is a monad
@@ -294,7 +294,7 @@ Next we will show that the delay monad is strong, by giving a natural transforma
       open import Categories.Category.Monoidal.Core
       open Monoidal monoidal
       open import Categories.Monad.Relative using () renaming (Monad to RMonad)
-      open RMonad kleisli using (extend) renaming (assoc to k-assoc)
+      open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
       open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
       open Monad monad using () renaming (η to η'; μ to μ')
       module η = NaturalTransformation η'
@@ -306,12 +306,12 @@ Next we will show that the delay monad is strong, by giving a natural transforma
           ; commute = commute' })
         ; identityˡ = identityˡ' -- triangle
         ; η-comm = begin -- η-τ
-          τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ 
+            τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ 
-          τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩ 
+            τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩ 
-          (out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩ 
+            (out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩ 
-          out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ 
+            out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ 
-          out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
+            out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
-          now ∎
+            now ∎
         ; μ-η-comm = μ-η-comm' -- μ-τ
         ; strength-assoc = strength-assoc' -- square
         }
@@ -346,6 +346,15 @@ Next we will show that the delay monad is strong, by giving a natural transforma
               out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimʳ (⁂∘⁂ ○ (⁂-cong₂ identity² (_≅_.isoʳ out-≅)) ○ ((⟨⟩-cong₂ identityˡ identityˡ) ○ ⁂-η)))) ⟩
               out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∎
 
+            τ-now : τ ∘ (idC ⁂ now) ≈ now
+            τ-now = begin 
+              τ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ (⁂-cong₂ identity² refl)) ⟩ 
+              τ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ τ-helper ⟩
+              (out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩
+              out⁻¹ ∘ (idC +₁ τ) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
+              out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
+              now ∎
+
             τ-unique : (t : X × D₀ Y ⇒ D₀ (X × Y)) → (out ∘ t ≈ (idC +₁ t) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) → t ≈ τ
             τ-unique t t-commutes = sym (!-unique (record { f = t ; commutes = t-commutes }))
 
@@ -388,52 +397,70 @@ Next we will show that the delay monad is strong, by giving a natural transforma
                 π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩
                 [ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
                 (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎)
+
           μ-η-comm' : ∀ {X Y} → extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈ τ (X , Y) ∘ (idC ⁂ extend idC)
           μ-η-comm' {X} {Y} = begin 
             extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y)) (record { f = extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ; commutes = begin 
-              out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw idC) ⟩ 
+              out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩
-              ([ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ pullʳ (pullˡ (extendlaw (now ∘ τ (X , Y)))) ⟩ 
+              out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ square ⟩
-              [ out ∘ idC , i₂ ∘ extend idC ] ∘ ([ out ∘ now ∘ τ _ , i₂ ∘ extend (now ∘ τ _) ] ∘ out) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullʳ (τ-law _)) ⟩ 
+              [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩
-              [ out ∘ idC , i₂ ∘ extend idC ] ∘ [ out ∘ now ∘ τ _ , i₂ ∘ extend (now ∘ τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (sym []∘+₁) ⟩∘⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩ 
+              ((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
-              ([ out , i₂ ] ∘ (idC +₁ extend idC)) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩
+              (idC +₁ (extend (τ _) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩
-              {!   !} ≈⟨ {!   !} ⟩ 
+              (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
-              -- TODO only works if (now +₁ now) ∘ out ≈ out ∘ now
+            u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y)) (record { f = τ _ ∘ (idC ⁂ extend idC) ; commutes = begin 
-              {!   !} ≈⟨ {!   !} ⟩ 
+              out ∘ τ _ ∘ (idC ⁂ extend idC) ≈⟨ pullˡ (τ-law (X , Y)) ⟩ 
-              [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (now +₁ idC) ∘ (idC +₁ now) ∘ out , (now +₁ idC) ∘ i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
+              ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
-              [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (now +₁ idC) ∘ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩
-              [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (now +₁ idC)) ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩
-              [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ ((idC ⁂ now) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
-              [ out ∘ (τ _ ∘ (idC ⁂ now)) , i₂ ] ∘ (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩
-              [ out ∘ now , i₂ ] ∘ (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
+              ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
-              (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
+              (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ 
-              (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ∎ })) ⟩ 
-            u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) }}) ≈⟨ {!   !} ⟩ 
             τ _ ∘ (idC ⁂ extend idC) ∎
             where
-              β : ∀ {A} → D₀ A + D₀ (D₀ A) ⇒ A + D₀ (D₀ A)
+              square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
-              β {A} = [ ((idC +₁ now) ∘ out) , i₂ ]
+              square = begin 
-              β⁻¹ : ∀ {A} → A + D₀ (D₀ A) ⇒ D₀ A + D₀ (D₀ A)
+                out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩ 
-              β⁻¹ {A} = [ (i₁ ∘ now) , i₂ ]
+                ([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law _) ⟩ 
-              β∘β⁻¹ : ∀ {A} → β {A} ∘ β⁻¹ ≈ idC
+                [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
-              β∘β⁻¹ = begin 
+              tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
-                [ ((idC +₁ now) ∘ out) , i₂ ] ∘ [ (i₁ ∘ now) , i₂ ] ≈⟨ ∘[] ⟩ 
+              tri = begin 
-                [ [ ((idC +₁ now) ∘ out) , i₂ ] ∘ (i₁ ∘ now) , [ ((idC +₁ now) ∘ out) , i₂ ] ∘ i₂ ] ≈⟨ []-cong₂ (pullˡ inject₁) inject₂ ⟩
+                [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩ 
-                [ ((idC +₁ now) ∘ out) ∘ now , i₂ ] ≈⟨ []-cong₂ (pullʳ unitlaw) refl ⟩
+                [ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩ 
-                [ (idC +₁ now) ∘ i₁ , i₂ ] ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) refl ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
-                [ i₁ , i₂ ] ≈⟨ +-η ⟩
+                [ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
-                idC ∎
+                [ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩ 
-              -- diag₁ : ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈ out ∘ τ _
+                [ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩ 
-              -- diag₁ = begin 
+                (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎
-              --   ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+              id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _)
-              --   (idC +₁ τ _) ∘ ((idC ⁂ now) +₁ idC) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+              id*∘Dτ = begin 
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ((idC ⁂ (now +₁ idC))) ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+                extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩ 
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ idC) ∘ (idC +₁ now) ∘ out , (now +₁ idC) ∘ i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+                extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+                extend (idC ∘ τ _) ≈⟨ extend-≈ identityˡ ⟩ 
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ out ∘ now , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+                extend (τ _) ∎
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ out) ≈⟨ sym (τ-law (X , A (Terminal.⊤ (coalgebras Y)))) ⟩ 
+              tri₂' : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ
-              --   out ∘ τ _ ∎
+              tri₂' = begin 
-              diag₂ = τ-law
+                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩ 
-              diag₃ = out-law {Y = D₀ (X × Y)} (extend idC)
+                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₁) , (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩
+                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₁) , (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⁂-cong₂ identity² inject₁) (⁂-cong₂ identity² inject₂) ⟩
+                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ idC ⁂ out , idC ⁂ i₂ ∘ extend idC ] ≈⟨ refl⟩∘⟨ ∘[] ⟩
+                (idC +₁ τ _) ∘ [ distributeˡ⁻¹ ∘ (idC ⁂ out) , distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ ∘[] ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ sym ([]-cong₂ refl (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl ((refl⟩∘⟨ dstr-law₂) ⟩∘⟨refl) ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ i₂) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym k-identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩
+                [ (idC +₁ τ _ ∘ (idC ⁂ extend idC ∘ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩
+                [ (idC +₁ τ _ ∘ (idC ⁂ extend idC) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ sym ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂) ⟩
+                [ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ i₂ ] ≈⟨ sym ∘[] ⟩
+                (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ≈⟨ sym (refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ))) ⟩
+                (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎
+              tri₂ : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
+              tri₂ = iso-epi-from 
+                (record { from = distributeˡ ; to = distributeˡ⁻¹ ; iso = IsIso.iso isIsoˡ }) 
+                ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ])) 
+                ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) 
+                (assoc ○ refl⟩∘⟨ assoc ○ tri₂' ○ sym-assoc ○ sym-assoc ○ assoc ⟩∘⟨refl)
+
           strength-assoc' : ∀ {X Y Z} → extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ ((X × Y), Z) ≈ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
           strength-assoc' {X} {Y} {Z} = begin 
             extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin 
@@ -487,11 +514,10 @@ Next we will show that the delay monad is strong, by giving a natural transforma
                 (distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
                 distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
                 distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎)
-{- ⁂ ⊤ ○ 
+-- {- ⁂ ⊤ ○ 
-Diagram for identityˡ':
+-- Diagram for identityˡ':
-https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ==
+-- https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ==
--}
+-- -}
--- ⊤
           commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) 
             → τ P₂ ∘ ((fst fg) ⁂ extend (now ∘ (snd fg))) ≈ extend (now ∘ ((fst fg) ⁂ (snd fg))) ∘ τ P₁
           commute' {(U , V)} {(W , X)} (f , g) = begin 
@@ -521,7 +547,7 @@ https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgK
               open Terminal (coalgebras (W × X))
               alg' : F-Coalgebra ((W × X) +-)
               alg' = record { A = U × D₀ V ; α = ((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }
--- ⁂ ○ ˡ ʳ 
+
       strongMonad : StrongMonad monoidal
       strongMonad = record { M = monad ; strength = strength }
 ```