Still working on delay strength, finished strength-assoc

src/Category/Instance/AmbientCategory.lagda.md

@@ -66,8 +66,21 @@ module Category.Instance.AmbientCategory where
     distributeʳ⁻¹ : ∀ {A B C : Obj} → (B + C) × A ⇒ B × A + C × A
     distributeʳ⁻¹ = IsIso.inv isIsoʳ
 
-    
-
     module M = M'
     module MR = MR'
+
+    distribute₁ : ∀ {X Y Z U V W} (f : X ⇒ U) (g : Y ⇒ V) (h : Z ⇒ W) → ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))
+    distribute₁ f g h = begin 
+      ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩ 
+      (distributeˡ⁻¹ ∘ distributeˡ) ∘ ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (pullʳ []∘+₁) ⟩
+      (distributeˡ⁻¹ ∘ [(idC ⁂ i₁) ∘ (f ⁂ g) , (idC ⁂ i₂) ∘ (f ⁂ h)]) ∘ distributeˡ⁻¹ ≈⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩
+      (distributeˡ⁻¹ ∘ [ idC ∘ f ⁂ i₁ ∘ g , idC ∘ f ⁂ i₂ ∘ h ]) ∘ distributeˡ⁻¹ ≈⟨ sym ((refl⟩∘⟨ ([]-cong₂ (⁂-cong₂ id-comm +₁∘i₁) (⁂-cong₂ id-comm +₁∘i₂))) ⟩∘⟨refl) ⟩
+      (distributeˡ⁻¹ ∘ [ f ∘ idC ⁂ (g +₁ h) ∘ i₁ , f ∘ idC ⁂ (g +₁ h) ∘ i₂ ]) ∘ distributeˡ⁻¹ ≈˘⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩
+      (distributeˡ⁻¹ ∘ [ ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₁)) , ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₂)) ]) ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ (pullʳ ∘[])) ⟩
+      (distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
+      distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h)) ∎
+      where 
+        open MR C
+        open HomReasoning
+        open Equiv
 ```

src/Monad/Instance/Delay.lagda.md

@@ -305,23 +305,15 @@ Next we will show that the delay monad is strong, by giving a natural transforma
           { η = τ
           ; commute = commute' })
         ; identityˡ = identityˡ' -- triangle
-        ; η-comm = begin -- η
+        ; η-comm = begin -- η-τ
           τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ 
           τ _ ∘ (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⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
           now ∎
-        ; μ-η-comm = μ-η-comm' -- μ-η
+        ; μ-η-comm = μ-η-comm' -- μ-τ
-        ; strength-assoc = λ {X} {Y} {Z} → begin 
+        ; strength-assoc = strength-assoc' -- square
-          extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin 
-            out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ pullˡ (extendlaw (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩ 
-            {!   !} ≈⟨ {!   !} ⟩ 
-            {!   !} ≈⟨ {!   !} ⟩ 
-            {!   !} ≈⟨ {!   !} ⟩ 
-            (idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ {!   !} ∎ })) ⟩ 
-          u (Terminal.! (coalgebras (X × Y × Z)) {A = record { A = (X × Y) × D₀ Z ; α = {!   !} }}) ≈⟨ {!   !} ⟩
-          τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎ -- square
         }
         where
           open import Agda.Builtin.Sigma
@@ -330,8 +322,10 @@ Next we will show that the delay monad is strong, by giving a natural transforma
             out ∘ extend (now ∘ f) ≈⟨ extendlaw (now ∘ f) ⟩ 
             [ out ∘ now ∘ f , i₂ ∘ extend (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
             (f +₁ extend (now ∘ f)) ∘ out ∎
-          dstr-law : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁
+          dstr-law₁ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁
-          dstr-law = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
+          dstr-law₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
+          dstr-law₂ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₂) ≈ i₂
+          dstr-law₂ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
 
           module _ (P : Category.Obj (CProduct C C)) where
             X = fst P
@@ -428,18 +422,71 @@ Next we will show that the delay monad is strong, by giving a natural transforma
                 [ (idC +₁ now) ∘ i₁ , i₂ ] ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) refl ⟩
                 [ i₁ , i₂ ] ≈⟨ +-η ⟩
                 idC ∎
-              diag₁ : ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈ out ∘ τ _
+              -- diag₁ : ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈ out ∘ τ _
-              diag₁ = begin 
+              -- diag₁ = begin 
-                ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+              --   ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-                (idC +₁ τ _) ∘ ((idC ⁂ now) +₁ idC) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+              --   (idC +₁ τ _) ∘ ((idC ⁂ now) +₁ idC) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-                (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ((idC ⁂ (now +₁ idC))) ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ((idC ⁂ (now +₁ idC))) ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-                (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ idC) ∘ (idC +₁ now) ∘ out , (now +₁ idC) ∘ i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ idC) ∘ (idC +₁ now) ∘ out , (now +₁ idC) ∘ i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-                (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-                (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ out ∘ now , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
+              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ out ∘ now , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-                (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ out) ≈⟨ sym (τ-law (X , A (Terminal.⊤ (coalgebras Y)))) ⟩ 
+              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ out) ≈⟨ sym (τ-law (X , A (Terminal.⊤ (coalgebras Y)))) ⟩ 
-                out ∘ τ _ ∎
+              --   out ∘ τ _ ∎
               diag₂ = τ-law
               diag₃ = out-law {Y = D₀ (X × Y)} (extend idC)
+          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 
+              out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ pullˡ (extendlaw (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩ 
+              ([ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law (X × Y , Z)) ⟩ 
+              [ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩ 
+              (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ 
+              (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl ⟩ 
+              (idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩ 
+              (idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩ 
+            u (Terminal.! (coalgebras (X × Y × Z)) {A = record { A = (X × Y) × D₀ Z ; α = (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ; commutes = begin 
+              out ∘ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-law (X , Y × Z)) ⟩ 
+              ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullʳ (pullˡ (pullʳ ⁂∘⁂)) ⟩ 
+              (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ assoc ⟩ 
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityʳ (assoc ○ sym (τ-law (Y , Z)))) ⟩∘⟨refl) ⟩ 
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ ((idC ∘ idC) ∘ idC ⁂ ((idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ ⁂∘⁂ ○ pullˡ ⁂∘⁂))) ⟩ 
+              (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ helper₁)) ⟩ 
+              (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₂ ⟩∘⟨refl) ⟩ 
+              (idC +₁ τ _) ∘ ((idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym assoc²') ⟩
+              (idC +₁ τ _) ∘ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩ 
+              (idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₃ ⟩∘⟨refl) ⟩ 
+              (idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc²'' ⟩
+              ((idC +₁ τ _ ∘ (idC ⁂ τ _)) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym ((+₁-cong₂ refl (identityʳ ○ sym-assoc) ○ sym +₁∘+₁) ⟩∘⟨refl) ⟩ 
+              (idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩ 
+              (idC +₁ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
+            τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
+            where
+              helper₁ : (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC {X × Y} ⁂ out {Z})
+              helper₁ = begin 
+                (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩ 
+                ⟨ idC ∘ π₁ ∘ π₁ , (idC ⁂ out) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ identityˡ ⁂∘⟨⟩ ⟩ 
+                ⟨ π₁ ∘ π₁ , ⟨ idC ∘ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ identityˡ refl) ⟩ 
+                ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl)) ⟩ 
+                ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩ 
+                ⟨ π₁ ∘ idC ∘ π₁ , ⟨ (π₂ ∘ π₁) ∘ (idC {X × Y} ⁂ out {Z}) , π₂ ∘ (idC {X × Y} ⁂ out {Z}) ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ (pullʳ project₁) ⟨⟩∘) ⟩ 
+                ⟨ (π₁ ∘ π₁) ∘ (idC {X × Y} ⁂ out {Z}) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC {X × Y} ⁂ out {Z}) ⟩ ≈⟨ sym ⟨⟩∘ ⟩ 
+                ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC {X × Y} ⁂ out {Z}) ∎
+              helper₂ : distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _)) ≈ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹
+              helper₂ = sym (distribute₁ idC idC (τ _)) ○ (+₁-cong₂ (⟨⟩-unique id-comm id-comm) refl) ⟩∘⟨refl
+              helper₃ : distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹
+              helper₃ = sym (begin 
+                (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩ 
+                (distributeˡ⁻¹ ∘ distributeˡ) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ≈⟨ pullʳ (pullˡ []∘+₁) ⟩
+                distributeˡ⁻¹ ∘ [ (idC ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , (idC ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (([]-cong₂ ⁂∘⟨⟩ ⁂∘⟨⟩) ⟩∘⟨refl) ⟩
+                distributeˡ⁻¹ ∘ [ ⟨ idC ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ idC ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ identityˡ (pushˡ (sym dstr-law₁))) (⟨⟩-cong₂ identityˡ ((pushˡ (sym dstr-law₂)))) ⟩∘⟨refl ⟩
+                distributeˡ⁻¹ ∘ [ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ ○ sym identityˡ) refl ○ sym ⁂∘⟨⟩))) (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ ○ sym identityˡ) refl ○ sym ⁂∘⟨⟩))) ⟩∘⟨refl) ⟩
+                distributeˡ⁻¹ ∘ [ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ (identityˡ ○ refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) (⟨⟩-cong₂ (identityˡ ○ refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩∘⟨refl) ⟩
+                distributeˡ⁻¹ ∘ [ ⟨ idC ∘ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩ ⟩ , ⟨ idC ∘ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘⁂)) (pullʳ ⟨⟩∘)) (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘⁂)) (pullʳ ⟨⟩∘)) ⟩∘⟨refl) ⟩
+                distributeˡ⁻¹ ∘ [ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ i₁) , (distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ i₁) ⟩ , ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ i₂) , (distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ i₂) ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ ⟨⟩∘ ⟨⟩∘ ⟩∘⟨refl) ⟩
+                distributeˡ⁻¹ ∘ [ (⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ i₁)) , (⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC  ⁂ i₂)) ] ∘ distributeˡ⁻¹ ≈˘⟨ pullʳ (pullˡ ∘[]) ⟩
+                (distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
+                distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
+                distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎)
 {- ⁂ ⊤ ○ 
 Diagram for identityˡ':
 https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ==
@@ -474,16 +521,6 @@ 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) }
-              distribute₁ : ∀ {X Y Z U V W} (f : X ⇒ U) (g : Y ⇒ V) (h : Z ⇒ W) → ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))
-              distribute₁ f g h = begin 
-                ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩ 
-                (distributeˡ⁻¹ ∘ distributeˡ) ∘ ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (pullʳ []∘+₁) ⟩
-                (distributeˡ⁻¹ ∘ [(idC ⁂ i₁) ∘ (f ⁂ g) , (idC ⁂ i₂) ∘ (f ⁂ h)]) ∘ distributeˡ⁻¹ ≈⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩
-                (distributeˡ⁻¹ ∘ [ idC ∘ f ⁂ i₁ ∘ g , idC ∘ f ⁂ i₂ ∘ h ]) ∘ distributeˡ⁻¹ ≈⟨ sym ((refl⟩∘⟨ ([]-cong₂ (⁂-cong₂ id-comm +₁∘i₁) (⁂-cong₂ id-comm +₁∘i₂))) ⟩∘⟨refl) ⟩
-                (distributeˡ⁻¹ ∘ [ f ∘ idC ⁂ (g +₁ h) ∘ i₁ , f ∘ idC ⁂ (g +₁ h) ∘ i₂ ]) ∘ distributeˡ⁻¹ ≈˘⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩
-                (distributeˡ⁻¹ ∘ [ ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₁)) , ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₂)) ]) ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ (pullʳ ∘[])) ⟩
-                (distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
-                distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h)) ∎
 -- ⁂ ○ ˡ ʳ 
       strongMonad : StrongMonad monoidal
       strongMonad = record { M = monad ; strength = strength }