🚧 Work on commutativity

src/Algebra/Search.lagda.md

@@ -43,4 +43,8 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where
     IsSearchAlgebra⇒Search-Algebra : ∀ {A} (α : F-Algebra-on functor A) → IsSearchAlgebra α → Search-Algebra
     IsSearchAlgebra⇒Search-Algebra {A} α is = record { A = A ; search-algebra-on = record { α = α ; identity₁ = identity₁ ; identity₂ = identity₂ } }
       where open IsSearchAlgebra is
+
+    Search-Algebra-on⇒IsSearchAlgebra : ∀ {A} → (search : Search-Algebra-on A) → IsSearchAlgebra (Search-Algebra-on.α search)
+    Search-Algebra-on⇒IsSearchAlgebra {A} search = record { identity₁ = identity₁ ; identity₂ = identity₂ }
+      where open Search-Algebra-on search
 ```

src/Category/Instance/AmbientCategory.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Category.Core
 
@@ -10,11 +11,14 @@ open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
 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.Category.Cocartesian using (Cocartesian)
 open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
 open import Categories.Object.Exponential using (Exponential)
 open import Categories.Object.Terminal
+open import Categories.Morphism.Properties
 import Categories.Morphism as M'
 import Categories.Morphism.Reasoning as MR'
 ```
@@ -47,8 +51,10 @@ module Category.Instance.AmbientCategory where
     open Cartesian cartesian public
     monoidal : Monoidal C
     monoidal = CartesianMonoidal.monoidal cartesian
-    -- open Terminal terminal public
+
-    -- Don't open the terminal object, because we are interested in many different terminal objects stemming from multiple categories
+    symmetric : Symmetric monoidal
+    symmetric = symm C cartesian
+
     open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
     open ParametrizedNNO ℕ public renaming (η to pnno-η)
 
@@ -66,6 +72,20 @@ module Category.Instance.AmbientCategory where
     distributeʳ⁻¹ : ∀ {A B C : Obj} → (B + C) × A ⇒ B × A + C × A
     distributeʳ⁻¹ = IsIso.inv isIsoʳ
 
+    -- TODO add to agda-categories
+    distributeˡ⁻¹∘swap : ∀ {A B C : Obj} → distributeˡ⁻¹ ∘ swap ≈ (swap +₁ swap) ∘ distributeʳ⁻¹ {A} {B} {C}
+    distributeˡ⁻¹∘swap = Iso⇒Mono C (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ swap) ((swap +₁ swap) ∘ distributeʳ⁻¹) (begin 
+      (distributeˡ ∘ distributeˡ⁻¹ ∘ swap) ≈⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩
+      swap ≈⟨ sym (cancelʳ (IsIso.isoʳ isIsoʳ)) ⟩ 
+      ((swap ∘ distributeʳ) ∘ distributeʳ⁻¹) ≈⟨ ∘[] ⟩∘⟨refl ⟩ 
+      [ swap ∘ (i₁ ⁂ idC) , swap ∘ (i₂ ⁂ idC) ] ∘ distributeʳ⁻¹ ≈⟨ sym ([]-cong₂ (sym swap∘⁂) (sym swap∘⁂) ⟩∘⟨refl) ⟩ 
+      [ (idC ⁂ i₁) ∘ swap , (idC ⁂ i₂) ∘ swap ] ∘ distributeʳ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩ 
+      distributeˡ ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ∎)
+      where
+        open HomReasoning
+        open MR' C
+        open Equiv
+
     module M = M'
     module MR = MR'
 

src/Monad/Commutative.agda

@@ -0,0 +1,35 @@
+{-# OPTIONS --without-K --safe #-}
+
+-- Commutative Monad on a symmetric monoidal category
+-- https://ncatlab.org/nlab/show/commutative+monad
+
+module Monad.Commutative where
+
+open import Level
+open import Data.Product using (_,_)
+
+open import Categories.Category.Core
+open import Categories.Category.Monoidal
+open import Categories.Category.Monoidal.Symmetric
+open import Categories.Monad
+open import Categories.Monad.Strong
+
+private
+  variable
+    o ℓ e : Level
+
+record CommutativeMonad {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) (T : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where
+  open Category C
+  open Symmetric S
+  open StrongMonad T
+
+
+  private
+    σ : ∀ {X Y} → X ⊗₀ M.F.₀ Y ⇒ M.F.₀ (X ⊗₀ Y)
+    σ {X} {Y} = strengthen.η (X , Y)
+
+  τ : ∀ {X Y} → M.F.₀ X ⊗₀ Y ⇒ M.F.₀ (X ⊗₀ Y)
+  τ {X} {Y} = M.F.₁ (braiding.⇐.η (X , Y)) ∘ σ ∘ braiding.⇒.η (M.F.₀ X , Y)
+
+  field
+    commutes : ∀ {X Y} → M.μ.η (X ⊗₀ Y) ∘ M.F.₁ τ ∘ σ ≈ M.μ.η (X ⊗₀ Y) ∘ M.F.₁ σ ∘ τ

src/Monad/Instance/Delay.lagda.md

@@ -10,7 +10,6 @@ open import Categories.Functor.Coalgebra
 open import Categories.Functor renaming (id to idF)
 open import Categories.Functor.Algebra
 open import Categories.Monad.Construction.Kleisli
-open import Categories.Monad.Strong
 open import Categories.Category.Construction.F-Coalgebras
 open import Categories.NaturalTransformation
 open import Category.Instance.AmbientCategory using (Ambient)
@@ -204,6 +203,41 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
         [ g , idC ] ∘ i₁                                               ≈⟨ inject₁ ⟩
         g ∎
 
+    -- Lemma 39: ▷ ∘ f* ≈ (▷ ∘ f)* ≈ f* ∘ ▷
+
+    module _ {X Y} (f : X ⇒ D₀ Y) where
+      private
+          helper : out ∘ [ f , extend' (▷ ∘ f) ] ∘ out ≈ [ out ∘ f , i₂ ∘ [ f , extend' (▷ ∘ f) ] ∘ out ] ∘ out
+          helper = pullˡ ∘[] ○ (([]-cong₂ refl (extendlaw (▷ ∘ f) ○ ((([]-cong₂ (pullˡ laterlaw) refl) ⟩∘⟨refl) ○ sym (pullˡ ∘[])))) ⟩∘⟨refl)
+          helper₁ : [ f , extend' (▷ ∘ f) ] ∘ out ≈ extend' f
+          helper₁ = sym (extend'-unique f ([ f , extend' (▷ ∘ f) ] ∘ out) helper)
+
+      ▷∘extendˡ : ▷ ∘ extend' f ≈ extend' (▷ ∘ f)
+      ▷∘extendˡ = sym (begin 
+        extend' (▷ ∘ f)                                      ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+        (out⁻¹ ∘ out) ∘ extend' (▷ ∘ f)                      ≈⟨ pullʳ (extendlaw (▷ ∘ f)) ⟩
+        out⁻¹ ∘ [ out ∘ ▷ ∘ f , i₂ ∘ extend' (▷ ∘ f) ] ∘ out ≈⟨ (refl⟩∘⟨ (([]-cong₂ (pullˡ laterlaw) refl) ○ (sym ∘[])) ⟩∘⟨refl) ⟩
+        out⁻¹ ∘ (i₂ ∘ [ f , extend' (▷ ∘ f) ]) ∘ out         ≈⟨ (refl⟩∘⟨ (pullʳ helper₁)) ⟩
+        out⁻¹ ∘ i₂ ∘ extend' f                               ≈⟨ sym-assoc ⟩
+        ▷ ∘ extend' f                                        ∎)
+
+      ▷∘extend-comm : ▷ ∘ extend' f ≈ extend' f ∘ ▷
+      ▷∘extend-comm = sym (begin 
+        extend' f ∘ ▷                                    ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+        (out⁻¹ ∘ out) ∘ extend' f ∘ ▷                    ≈⟨ pullʳ (pullˡ (extendlaw f)) ⟩ 
+        out⁻¹ ∘ ([ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ ▷ ≈⟨ (refl⟩∘⟨ pullʳ laterlaw) ⟩ 
+        out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₂        ≈⟨ (refl⟩∘⟨ inject₂) ○ sym-assoc ⟩ 
+        ▷ ∘ extend' f                                    ∎)
+
+      ▷∘extendʳ : extend' f ∘ ▷ ≈ extend' (▷ ∘ f)
+      ▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ
+
+    out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend' (now ∘ f) ≈ (f +₁ extend' (now ∘ f)) ∘ out {X}
+    out-law {X} {Y} f = begin 
+      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                   ∎
+
     kleisli : KleisliTriple C
     kleisli = record
       { F₀ = D₀ 
@@ -242,47 +276,47 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
 
         identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → extend' f ∘ now {X} ≈ f
         identityʳ' {X} {Y} {f} = begin 
-          extend' f ∘ now                                          ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩ 
+          extend' f ∘ now                                       ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩ 
-          (out⁻¹ ∘ out ∘ extend' f) ∘ now                      ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
+          (out⁻¹ ∘ out ∘ extend' f) ∘ now                       ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
-          (out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩
+          (out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ now    ≈⟨ pullʳ (pullʳ unitlaw) ⟩
-          out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₁              ≈⟨ refl⟩∘⟨ inject₁ ⟩
+          out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₁             ≈⟨ refl⟩∘⟨ inject₁ ⟩
           out⁻¹ ∘ out ∘ f                                       ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩
-          f                                                         ∎
+          f                                                     ∎
 
         identityˡ' : ∀ {X} → extend' now ≈ idC
         identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend' now ; commutes = begin 
           out ∘ extend' now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩ 
-          ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁   ≈⟨ pullʳ inject₁ ⟩
+          ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁     ≈⟨ pullʳ inject₁ ⟩
           (idC +₁ (u (! (coalgebras X) {A = alg now}))) 
-          ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out               ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
+          ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out                   ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
           (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
           [ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ 
           , (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out      ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
           [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out  ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
-          [ i₁ ∘ idC , i₂ ∘ (extend' now) ] ∘ out                               ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
+          [ i₁ ∘ idC , i₂ ∘ (extend' now) ] ∘ out                                ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
-          ([ i₁ , i₂ ] ∘ (idC +₁ extend' now)) ∘ out                            ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
+          ([ i₁ , i₂ ] ∘ (idC +₁ extend' now)) ∘ out                             ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
-          (idC +₁ extend' now) ∘ out                                            ∎ })
+          (idC +₁ extend' now) ∘ out                                             ∎ })
 
         assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → extend' (extend' h ∘ g) ≈ extend' h ∘ extend' g
         assoc' {X} {Y} {Z} {g} {h} = extend'-unique (extend' h ∘ g) (extend' h ∘ extend' g) (begin 
-          out ∘ extend' h ∘ extend' g                                           ≈⟨ pullˡ (extendlaw h) ⟩
+          out ∘ extend' h ∘ extend' g                                       ≈⟨ pullˡ (extendlaw h) ⟩
-          ([ out ∘ h , i₂ ∘ extend' h ] ∘ out) ∘ extend' g                    ≈⟨ pullʳ (extendlaw g) ⟩
+          ([ out ∘ h , i₂ ∘ extend' h ] ∘ out) ∘ extend' g                  ≈⟨ pullʳ (extendlaw g) ⟩
           [ out ∘ h , i₂ ∘ extend' h ] ∘ [ out ∘ g , i₂ ∘ extend' g ] ∘ out ≈⟨ pullˡ ∘[] ⟩
           [ [ out ∘ h , i₂ ∘ extend' h ] ∘ out ∘ g 
-          , [ out ∘ h , i₂ ∘ extend' h ] ∘ i₂ ∘ extend' g ] ∘ out             ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
+          , [ out ∘ h , i₂ ∘ extend' h ] ∘ i₂ ∘ extend' g ] ∘ out           ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
-          [ (out ∘ extend' h) ∘ g , (i₂ ∘ extend' h) ∘ extend' g ] ∘ out       ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
+          [ (out ∘ extend' h) ∘ g , (i₂ ∘ extend' h) ∘ extend' g ] ∘ out    ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
-          [ out ∘ extend' h ∘ g , i₂ ∘ extend' h ∘ extend' g ] ∘ out           ∎)
+          [ out ∘ extend' h ∘ g , i₂ ∘ extend' h ∘ extend' g ] ∘ out        ∎)
         
         extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend' f ≈ extend' g
         extend-≈' {X} {Y} {f} {g} eq = begin
           u (! (coalgebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y}         ≈⟨ (!-unique (coalgebras Y) (record { f = (u (! (coalgebras Y) {A = alg g }) ∘ idC) ; commutes = begin 
             α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ 
             α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y))       ≈⟨ commutes (! (coalgebras Y)) ⟩ 
-            (idC +₁ u (! (coalgebras Y))) ∘ α (alg g)       ≈˘⟨ Functor.F-resp-≈ (Y +-) identityʳ ⟩∘⟨ αf≈αg eq ⟩ 
+            (idC +₁ u (! (coalgebras Y))) ∘ α (alg g)         ≈˘⟨ Functor.F-resp-≈ (Y +-) identityʳ ⟩∘⟨ αf≈αg eq ⟩ 
-            (idC +₁ u (! (coalgebras Y)) ∘ idC) ∘ α (alg f) ∎ }))
+            (idC +₁ u (! (coalgebras Y)) ∘ idC) ∘ α (alg f)   ∎ }))
             ⟩∘⟨refl ⟩ 
           (u (! (coalgebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩
-          extend' g                                                ∎
+          extend' g                                                 ∎
 
     monad : Monad C
     monad = Kleisli⇒Monad C kleisli
@@ -291,270 +325,3 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
     functor : Endofunctor C
     functor = Monad.F monad
 ```
-
-Next we will show that the delay monad is strong, by giving a natural transformation `strengthen : X × DY ⇒ D (X × Y)
-
-```agda
-    module _ where
-      open Functor
-      open import Categories.Category.Monoidal.Core
-      open Monoidal monoidal
-      open import Categories.Monad.Relative using () renaming (Monad to RMonad)
-      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 η'
-      module μ = NaturalTransformation μ'
-      strength : Strength monoidal monad
-      strength = record
-        { strengthen = ntHelper (record 
-          { η = τ
-          ; commute = commute' })
-        ; identityˡ = identityˡ' -- triangle
-        ; η-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 +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ 
-            out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
-            now ∎
-        ; μ-η-comm = μ-η-comm' -- μ-τ
-        ; strength-assoc = strength-assoc' -- square
-        }
-        where
-          open import Agda.Builtin.Sigma
-          out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend (now ∘ f) ≈ (f +₁ extend (now ∘ f)) ∘ out {X}
-          out-law {X} {Y} f = begin 
-            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₁ = (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
-            Y = snd P
-            open Terminal (coalgebras (X × Y))
-
-            τ : X × D₀ Y ⇒ D₀ (X × Y)
-            τ = u (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
-
-            τ-law : out ∘ τ ≈ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
-            τ-law = commutes (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
-
-            τ-helper : τ ∘ (idC ⁂ out⁻¹) ≈ out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹
-            τ-helper = begin 
-              τ ∘ (idC ⁂ out⁻¹) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
-              (out⁻¹ ∘ out) ∘ τ ∘ (idC ⁂ out⁻¹) ≈⟨ pullʳ (pullˡ τ-law) ⟩
-              out⁻¹ ∘ ((idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ assoc) ⟩
-              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 }))
-
-          identityˡ' : ∀ {X : Obj} → extend (now ∘ π₂) ∘ τ (Terminal.⊤ terminal , X) ≈ π₂
-          identityˡ' {X} = begin
-            extend (now ∘ π₂) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = extend (now ∘ π₂) ∘ τ _ ; commutes = begin 
-              out ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym identityʳ)) ⟩ 
-              out ∘ extend (now ∘ π₂) ∘ τ _ ∘ idC ≈⟨ pullˡ diag₃ ⟩ 
-              ((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ _ ∘ idC ≈⟨ pullʳ (pullˡ (diag₂ (Terminal.⊤ terminal , X))) ⟩ 
-              (π₂ +₁ extend (now ∘ π₂)) ∘ ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ idC ≈⟨ refl⟩∘⟨ (pullʳ (assoc ○ sym diag₁)) ⟩ 
-              (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ CC.+-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩ 
-              (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ 
-              (π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm refl) ⟩∘⟨refl ⟩ 
-              (idC ∘ π₂ +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
-              (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimˡ identity²)) ⟩ 
-              (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ 
-              (idC +₁ extend (now ∘ π₂)) ∘ (idC ∘ π₂ +₁ τ _ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullʳ (pullˡ +₁∘+₁) ⟩ 
-              ((idC +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (homomorphism (X +-)) ⟩∘⟨refl ⟩ 
-              (idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
-            u (Terminal.! (coalgebras X)) ≈⟨ Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = π₂ ; commutes = begin 
-              out ∘ π₂ ≈˘⟨ π₂∘⁂ ⟩ 
-              π₂ ∘ (idC ⁂ out) ≈˘⟨ pullˡ distribute₂ ⟩ -- TODO this might be wrong if distribute₂ is unprovable
-              (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ 
-              (idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
-              (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
-            π₂ ∎ 
-            where
-              diag₁ : (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈ distributeˡ⁻¹ {Terminal.⊤ terminal} {X} {D₀ X} ∘ (idC ⁂ out) ∘ idC
-              diag₁ = begin 
-                (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ 
-                (⟨ Terminal.! terminal , idC ⟩ ∘ π₂ +₁ idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ⟩∘⟨ (refl⟩∘⟨ sym identityʳ) ⟩ 
-                (idC +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ≈⟨ elimˡ (CC.+-unique id-comm-sym id-comm-sym) ⟩ 
-                distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ∎
-              diag₂ = τ-law
-              diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out
-              diag₃ = out-law π₂
-              distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
-              distribute₂ = sym (begin 
-                π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ 
-                π₂ ∘ 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)) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩
-              out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ square ⟩
-              [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩
-              ((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
-              (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) ∎ })) ⟩
-            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)) ⟩ 
-              ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
-              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩
-              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩
-              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
-              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩
-              ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
-              (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ 
-            τ _ ∘ (idC ⁂ extend idC) ∎
-            where
-              -- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
-              square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
-              square = begin 
-                out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩ 
-                ([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law _) ⟩ 
-                [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
-              tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
-              tri = begin 
-                [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩ 
-                [ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩ 
-                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
-                [ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
-                [ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩ 
-                [ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩ 
-                (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎
-              id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _)
-              id*∘Dτ = begin 
-                extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩ 
-                extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
-                extend (idC ∘ τ _) ≈⟨ extend-≈ identityˡ ⟩ 
-                extend (τ _) ∎
-              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ˡ
-              tri₂' = begin 
-                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩ 
-                (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 
-              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==
--- -}
-          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 
-            τ _ ∘ (f ⁂ extend (now ∘ g)) ≈⟨ sym (!-unique (record { f = τ _ ∘ (f ⁂ extend (now ∘ g)) ; commutes = begin 
-              out ∘ τ (W , X) ∘ (f ⁂ extend (now ∘ g)) ≈⟨ pullˡ (τ-law (W , X)) ⟩ 
-              ((idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (f ⁂ extend (now ∘ g)) ≈⟨ pullʳ (pullʳ ⁂∘⁂) ⟩ 
-              (idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (idC ∘ f ⁂ out ∘ extend (now ∘ g)) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityˡ (extendlaw (now ∘ g)))) ⟩ 
-              (idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ refl (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl))) ⟩ 
-              (idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ [ i₁ ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identityʳ) refl)) ⟩ 
-              (idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ∘ idC ⁂ (g +₁ extend (now ∘ g)) ∘ out) ≈⟨ sym (pullʳ (pullʳ ⁂∘⁂)) ⟩ 
-              ((idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ extend (now ∘ g)))) ∘ (idC ⁂ out) ≈⟨ (refl⟩∘⟨ (sym (distribute₁ f g (extend (now ∘ g))))) ⟩∘⟨refl ⟩ 
-              ((idC +₁ τ (W , X)) ∘ ((f ⁂ g) +₁ (f ⁂ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ (pullˡ +₁∘+₁) ⟩∘⟨refl ⟩ 
-              ((idC ∘ (f ⁂ g) +₁ τ (W , X) ∘ (f ⁂ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (((+₁-cong₂ refl identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
-              ((idC ∘ (f ⁂ g) +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g))) ∘ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩ 
-              (idC +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g)))) ∘ ((f ⁂ g +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ∎ })) ⟩ 
-            u ! ≈⟨ !-unique (record { f = extend (now ∘ (f ⁂ g)) ∘ τ _ ; commutes = begin 
-              out ∘ extend (now ∘ (f ⁂ g)) ∘ τ _                                                                ≈⟨ pullˡ (extendlaw (now ∘ (f ⁂ g))) ⟩ 
-              ([ out ∘ now ∘ (f ⁂ g) , i₂ ∘ extend (now ∘ (f ⁂ g)) ] ∘ out) ∘ τ (U , V)                         ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩∘⟨refl ⟩
-              ([ i₁ ∘ (f ⁂ g) , i₂ ∘ extend (now ∘ (f ⁂ g)) ] ∘ out) ∘ τ (U , V)                                ≈⟨ pullʳ (τ-law (U , V)) ⟩
-              ((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                ≈⟨ sym-assoc ○ sym-assoc ⟩
-              ((((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ _)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)            ≈⟨ (+₁∘+₁ ⟩∘⟨refl) ⟩∘⟨refl ⟩
-              ((((f ⁂ g) ∘ idC) +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)         ≈⟨ sym (((+₁-cong₂ id-comm-sym identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
-              (((idC ∘ (f ⁂ g)) +₁ ((extend (now ∘ (f ⁂ g)) ∘ τ (U , V)) ∘ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩
-              (idC +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ (((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ∎ }) ⟩
-            extend (now ∘ (f ⁂ g)) ∘ τ _ ∎
-            where
-              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 }
-```

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

@@ -0,0 +1,115 @@
+<!--
+```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+open import Level
+
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Categories.Category.Core
+open import Categories.Functor
+open import Categories.Functor.Coalgebra
+open import Category.Instance.AmbientCategory
+open import Monad.Commutative
+open import Monad.Instance.Delay
+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 Categories.Object.Terminal
+```
+-->
+
+```agda
+module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where
+  open Ambient ambient
+  open HomReasoning
+  open Equiv
+  open MR C
+  open M C
+  open F-Coalgebra-Morphism using () renaming (f to u; commutes to u-commutes)
+  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₁)
+  open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
+  open Monad monad using (η; μ)
+  open StrongMonad strongMonad using ()
+```
+
+# The Delay Monad is commutative
+
+```agda
+  commutativeMonad : CommutativeMonad symmetric strongMonad
+  commutativeMonad = record { commutes = λ {X} {Y} → pullˡ (Kleisli⇒Monad⇒Kleisli kleisli _) ○ commutes' ○ pushˡ (sym (Kleisli⇒Monad⇒Kleisli kleisli _)) }
+    where
+      open τ-mod hiding (τ)
+      τ : ∀ {X Y} → X × D₀ Y ⇒ D₀ (X × Y)
+      τ {X} {Y} = τ-mod.τ (X , Y)
+      σ : ∀ {X Y} → D₀ X × Y ⇒ D₀ (X × Y)
+      σ {X} {Y} = D₁ swap ∘ τ ∘ swap
+      σ-coalg : ∀ (X Y : Obj) → F-Coalgebra-Morphism {F = (X × Y) +- } (record { A = D₀ X × Y ; α = distributeʳ⁻¹ {Y} {X} {D₀ X} ∘ (out {X} ⁂ idC) }) (record { A = D₀ (X × Y) ; α = out {X × Y} })
+      σ-coalg X Y = record { f = σ ; commutes = begin 
+        out ∘ σ ≈⟨ pullˡ (out-law swap) ⟩ 
+        ((swap +₁ D₁ swap) ∘ out) ∘ τ ∘ swap ≈⟨ pullˡ (pullʳ (τ-law (Y , X))) ⟩ 
+        ((swap +₁ D₁ swap) ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ swap ≈⟨ pullʳ (pullʳ (pullʳ (sym swap∘⁂))) ⟩ 
+        (swap +₁ D₁ swap) ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ swap ∘ (out ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹∘swap ⟩ 
+        (swap +₁ D₁ swap) ∘ (idC +₁ τ) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (out ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩ 
+        (swap ∘ idC +₁ D₁ swap ∘ τ) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (out ⁂ idC) ≈⟨ pullˡ (pullˡ +₁∘+₁) ⟩ 
+        (((swap ∘ idC) ∘ swap +₁ (D₁ swap ∘ τ) ∘ swap) ∘ distributeʳ⁻¹) ∘ (out ⁂ idC) ≈⟨ ((+₁-cong₂ (identityʳ ⟩∘⟨refl ○ swap∘swap) assoc) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
+        ((idC +₁ D₁ swap ∘ τ ∘ swap) ∘ distributeʳ⁻¹) ∘ (out ⁂ idC) ≈⟨ assoc ⟩ 
+        (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) ∎ }
+      commutes' : ∀ {X Y} → extend σ ∘ τ {D₀ X} {Y} ≈ extend τ ∘ σ 
+      commutes' {X} {Y} = begin 
+        extend σ ∘ τ ≈⟨ sym (!-unique (coalgebras (X × Y)) (record { f = extend σ ∘ τ ; commutes = begin 
+          out ∘ extend σ ∘ τ ≈⟨ pullˡ (extendlaw σ) ⟩ 
+          ([ out ∘ σ , i₂ ∘ extend σ ] ∘ out) ∘ τ ≈⟨ pullʳ (τ-law (D₀ X , Y)) ⟩
+          [ out ∘ σ , i₂ ∘ extend σ ] ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ []∘+₁ ⟩
+          [ (out ∘ σ) ∘ idC , (i₂ ∘ extend σ) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ ([]-cong₂ (identityʳ ○ u-commutes (σ-coalg X Y)) assoc) ⟩∘⟨refl ⟩
+          [ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ((⁂-cong₂ (sym (_≅_.isoˡ out-≅)) refl) ○ sym (⁂-cong₂ refl identityˡ) ○ sym ⁂∘⁂) ⟩
+          [ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out⁻¹ ⁂ idC) ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym))) ⟩∘⟨refl ⟩
+          [ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out⁻¹ ⁂ (idC +₁ idC)) ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ pullˡ (sym (distribute₁ out⁻¹ idC idC)) ⟩
+          [ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend σ ∘ τ ] ∘ (((out⁻¹ ⁂ idC) +₁ (out⁻¹ ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (out ⁂ out) ≈⟨ pullˡ (pullˡ []∘+₁) ⟩
+          ([ ((idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC)) ∘ (out⁻¹ ⁂ idC) , (i₂ ∘ extend σ ∘ τ) ∘ (out⁻¹ ⁂ idC) ] ∘ distributeˡ⁻¹) ∘ (out ⁂ out) ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          [ idC +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          (idC +₁ extend σ ∘ τ) ∘ {!   !} ∎ })) ⟩ 
+        u (! (coalgebras (X × Y))) ≈⟨ {!   !} ⟩ 
+        extend τ ∘ σ ∎
+      {-
+      out⁻¹ ∘ out ∘ extend σ ∘ τ
+    ≈ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)
+    ≈ extend [ now , extend σ ∘ τ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)
+    ≈ extend [ now , extend σ ∘ τ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
+
+      out⁻¹ ∘ out ∘ extend τ ∘ σ
+    ≈ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , later ∘ extend τ ∘ σ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)
+    ≈ extend [ now , extend τ ∘ σ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)
+    ≈ extend [ now , extend τ ∘ σ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
+
+
+
+    out ∘ extend [ now , extend σ ∘ τ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
+    [ out ∘ [ now , extend σ ∘ τ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ] ∘ out ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
+    [ [ i₁ , out ∘ extend σ ∘ τ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ] ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
+    [ [ [ i₁ , out ∘ extend σ ∘ τ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ] ∘ (i₁ +₁ (D₁ i₁) ∘ σ) , [ [ i₁ , out ∘ extend σ ∘ τ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ] ∘ i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
+    [ [ [ i₁ , out ∘ extend σ ∘ τ ] ∘ i₁ , i₂ ∘ extend [ now , extend σ ∘ τ ] ∘ (D₁ i₁) ∘ σ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
+    [ [ i₁ , i₂ ∘ σ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
+    [ [ i₁ , i₂ ∘ σ ] , i₂ ∘ [extend [ now , extend σ ∘ τ ] ∘ D₁ i₁ ∘ τ , extend [ now , extend σ ∘ τ ] ∘ now ∘ i₂ ] ] ∘ w
+    [ [ i₁ , i₂ ∘ σ ] , i₂ ∘ [ τ , extend σ ∘ τ ] ] ∘ w
+      -}
+      
+```

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

@@ -36,7 +36,7 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe
 
     open Functor D-Functor using () renaming (F₁ to D₁; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈; identity to D-identity)
     open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ)
-    open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ)
+    open Monad D-Monad using (μ; η) renaming (assoc to M-assoc; identityʳ to M-identityʳ)
     open HomReasoning
     open M C
     open MR C
@@ -80,15 +80,42 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe
 
       2⇒3 : cond-2 → cond-3
       2⇒3 c-2 X = record
-        { elgot = {!   !} 
+        { elgot = Elgot-Algebra.algebra (D-Algebra+Search⇒Elgot D (record 
+          { A = Ď₀ X 
+          ; action = α
+          ; commute = epi-DDρ (α ∘ D₁ α) (α ∘ extend (idC)) (sym (begin 
+            (α ∘ μ.η (Ď₀ X)) ∘ D₁ (D₁ ρ) ≈⟨ pullʳ (μ.commute ρ) ⟩
+            α ∘ D₁ ρ ∘ μ.η (D₀ X)        ≈⟨ pullˡ (sym ρ-algebra-morphism) ⟩
+            (ρ ∘ μ.η X) ∘ μ.η (D₀ X)     ≈⟨ pullʳ μ∘Dμ ⟩
+            ρ ∘ μ.η X ∘ D₁ (μ.η X)       ≈⟨ pullˡ ρ-algebra-morphism ⟩
+            (α ∘ D₁ ρ) ∘ D₁ (μ.η X)      ≈⟨ pullʳ (sym D-homomorphism) ⟩
+            α ∘ D₁ (ρ ∘ μ.η X)           ≈⟨ (refl⟩∘⟨ (D-resp-≈ ρ-algebra-morphism)) ⟩
+            α ∘ D₁ (α ∘ D₁ ρ)            ≈⟨ (refl⟩∘⟨ D-homomorphism) ⟩
+            α ∘ D₁ α ∘ D₁ (D₁ ρ)         ≈⟨ sym-assoc ⟩
+            (α ∘ D₁ α) ∘ D₁ (D₁ ρ)       ∎))
+          ; identity = identity₁ 
+          }) (Search-Algebra-on⇒IsSearchAlgebra D s-alg-on))
         ; isFO = {!   !}
         ; isStable = {!   !}
         ; ρ-algebra-morphism = {!   !}
         ; ρ-law = {!   !}
         }
+        where
+          open cond-2' (c-2 X)
+          open Search-Algebra-on s-alg-on
+          epi-DDρ : Epi (D₁ (D₁ ρ))
+          epi-DDρ = {!   !}
+          μ∘Dμ : ∀ {X} → μ.η X ∘ μ.η (D₀ X) ≈ μ.η X ∘ D₁ (μ.η X)
+          μ∘Dμ {X} = begin 
+            μ.η X ∘ μ.η (D₀ X)                       ≈⟨ sym k-assoc ⟩ 
+            extend (extend idC ∘ idC)                ≈⟨ extend-≈ identityʳ ⟩ 
+            extend (extend idC)                      ≈⟨ extend-≈ (introˡ k-identityʳ) ⟩ 
+            extend ((extend idC ∘ now) ∘ extend idC) ≈⟨ extend-≈ assoc ⟩ 
+            extend (extend idC ∘ now ∘ extend idC)   ≈⟨ k-assoc ⟩ 
+            μ.η X ∘ D₁ (μ.η X)                       ∎
 
       1⇒2 : cond-1 → cond-2
-      1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎ }
+      1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = D-universal }
         where
           open Coequalizer (coeqs X) renaming (universal to coeq-universal)
           open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique)
@@ -96,18 +123,18 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe
           s-alg-on = record 
             { α = α'
             ; identity₁ = ρ-epi (α' ∘ now) idC (begin 
-              (α' ∘ now) ∘ ρ ≈⟨ pullʳ (η.commute ρ) ⟩ 
+              (α' ∘ now) ∘ ρ    ≈⟨ pullʳ (η.commute ρ) ⟩ 
-              α' ∘ D₁ ρ ∘ now ≈⟨ pullˡ (sym D-universal) ⟩
+              α' ∘ D₁ ρ ∘ now   ≈⟨ pullˡ (sym D-universal) ⟩
               (ρ ∘ μ.η X) ∘ now ≈⟨ cancelʳ M-identityʳ ⟩
-              ρ ≈⟨ sym identityˡ ⟩
+              ρ                 ≈⟨ sym identityˡ ⟩
-              idC ∘ ρ ∎) 
+              idC ∘ ρ           ∎) 
             ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin 
-              (α' ∘ ▷) ∘ D₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ 
+              (α' ∘ ▷) ∘ D₁ ρ    ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ 
-              α' ∘ D₁ ρ ∘ ▷ ≈⟨ pullˡ (sym D-universal) ⟩
+              α' ∘ D₁ ρ ∘ ▷      ≈⟨ pullˡ (sym D-universal) ⟩
-              (ρ ∘ μ.η X) ∘ ▷ ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩
+              (ρ ∘ μ.η X) ∘ ▷    ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩
               ρ ∘ ▷ ∘ extend idC ≈⟨ pullˡ ρ▷ ⟩
-              ρ ∘ extend idC ≈⟨ D-universal ⟩
+              ρ ∘ extend idC     ≈⟨ D-universal ⟩
-              α' ∘ D₁ ρ ∎) 
+              α' ∘ D₁ ρ          ∎) 
             }
             where
               μ∘Dι : μ.η X ∘ D₁ ι ≈ extend ι
@@ -115,14 +142,14 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe
               eq₁ : D₁ (extend ι) ≈ D₁ (μ.η X) ∘ D₁ (D₁ ι)
               eq₁ = sym (begin 
                 D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ sym D-homomorphism ⟩ 
-                D₁ (μ.η X ∘ D₁ ι) ≈⟨ D-resp-≈ μ∘Dι ⟩
+                D₁ (μ.η X ∘ D₁ ι)      ≈⟨ D-resp-≈ μ∘Dι ⟩
-                D₁ (extend ι) ∎)
+                D₁ (extend ι)          ∎)
               α' = D-coequalize {h = ρ {X} ∘ μ.η X} (begin 
-                (ρ ∘ μ.η X) ∘ D₁ (extend ι) ≈⟨ (refl⟩∘⟨ eq₁) ⟩ 
+                (ρ ∘ μ.η X) ∘ D₁ (extend ι)          ≈⟨ (refl⟩∘⟨ eq₁) ⟩ 
                 (ρ ∘ μ.η X) ∘ D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ pullʳ (pullˡ M-assoc) ⟩
                 ρ ∘ (μ.η X ∘ μ.η (D₀ X)) ∘ D₁ (D₁ ι) ≈⟨ (refl⟩∘⟨ pullʳ (μ.commute ι)) ⟩
-                ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N) ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩
+                ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N)     ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩
-                ρ ∘ extend ι ∘ μ.η (X × N) ≈⟨ pullˡ equality ⟩
+                ρ ∘ extend ι ∘ μ.η (X × N)           ≈⟨ pullˡ equality ⟩
-                (ρ ∘ D₁ π₁) ∘ μ.η (X × N) ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩
+                (ρ ∘ D₁ π₁) ∘ μ.η (X × N)            ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩
-                (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁) ∎)
+                (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁)             ∎)
 ```

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

@@ -78,36 +78,6 @@ We will now show that the following conditions are equivalent:
       ρ-epi : ∀ {X} → Epi (ρ {X})
       ρ-epi {X} = Coequalizer⇒Epi (coeqs X)
 
-      -- TODO this belongs in a different module
-      module _ {X Y} (f : X ⇒ D₀ Y) where
-        private
-            helper : out ∘ [ f , extend (▷ ∘ f) ] ∘ out ≈ [ out ∘ f , i₂ ∘ [ f , extend (▷ ∘ f) ] ∘ out ] ∘ out
-            helper = pullˡ ∘[] ○ (([]-cong₂ refl (extendlaw (▷ ∘ f) ○ ((([]-cong₂ (pullˡ laterlaw) refl) ⟩∘⟨refl) ○ sym (pullˡ ∘[])))) ⟩∘⟨refl)
-            helper₁ : [ f , extend (▷ ∘ f) ] ∘ out ≈ extend f
-            helper₁ = sym (extend'-unique f ([ f , extend (▷ ∘ f) ] ∘ out) helper)
-
-        ▷∘extendˡ : ▷ ∘ extend f ≈ extend (▷ ∘ f)
-        ▷∘extendˡ = sym (begin 
-          extend (▷ ∘ f) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
-          (out⁻¹ ∘ out) ∘ extend (▷ ∘ f) ≈⟨ pullʳ (extendlaw (▷ ∘ f)) ⟩
-          out⁻¹ ∘ [ out ∘ ▷ ∘ f , i₂ ∘ extend (▷ ∘ f) ] ∘ out ≈⟨ (refl⟩∘⟨ (([]-cong₂ (pullˡ laterlaw) refl) ○ (sym ∘[])) ⟩∘⟨refl) ⟩
-          out⁻¹ ∘ (i₂ ∘ [ f , extend (▷ ∘ f) ]) ∘ out ≈⟨ (refl⟩∘⟨ (pullʳ helper₁)) ⟩
-          out⁻¹ ∘ i₂ ∘ extend f ≈⟨ sym-assoc ⟩
-          ▷ ∘ extend f ∎)
-
-        ▷∘extend-comm : ▷ ∘ extend f ≈ extend f ∘ ▷
-        ▷∘extend-comm = sym (begin 
-          extend f ∘ ▷ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
-          (out⁻¹ ∘ out) ∘ extend f ∘ ▷ ≈⟨ pullʳ (pullˡ (extendlaw f)) ⟩ 
-          out⁻¹ ∘ ([ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ ▷ ≈⟨ (refl⟩∘⟨ pullʳ laterlaw) ⟩ 
-          out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₂ ≈⟨ (refl⟩∘⟨ inject₂) ○ sym-assoc ⟩ 
-          ▷ ∘ extend f ∎)
-
-        ▷∘extendʳ : extend f ∘ ▷ ≈ extend (▷ ∘ f)
-        ▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ
-
-
-
       ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
       ρ▷ {X} = sym (begin 
         ρ ≈⟨ introʳ intro-helper ⟩ 

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

@@ -0,0 +1,299 @@
+<!--
+```agda
+open import Level
+
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Categories.Category
+open import Category.Instance.AmbientCategory
+open import Categories.Functor
+open import Categories.Functor.Coalgebra
+open import Monad.Instance.Delay
+open import Categories.Monad
+open import Categories.Monad.Strong
+open import Categories.Monad.Relative using () renaming (Monad to RMonad)
+open import Categories.NaturalTransformation
+open import Categories.Object.Terminal
+open import Categories.Monad.Relative using () renaming (Monad to RMonad)
+open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
+```
+-->
+
+```agda
+module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where
+  open Ambient ambient
+  open HomReasoning
+  open Equiv
+  open MR C
+  open M C
+  open F-Coalgebra-Morphism renaming (f to u)
+```
+
+# The Delay Monad is strong
+
+```agda
+  module _ where
+    open DelayM D
+    open Functor
+    open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
+    open Monad monad using (η; μ)
+
+    -- TODO change 'coinduction' proofs, move the two proofs i.e. f ≈ ! and ! ≈ g to the where clause
+    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₂
+    dstr-law₂ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
+    distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
+    distribute₂ = sym (begin 
+      π₂                                                      ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ 
+      π₂ ∘ distributeˡ ∘ distributeˡ⁻¹                        ≈⟨ pullˡ ∘[] ⟩
+      [ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
+      (π₂ +₁ π₂) ∘ distributeˡ⁻¹                              ∎)
+
+    module τ-mod (P : Category.Obj (CProduct C C)) where
+      private
+        X = proj₁ P
+        Y = proj₂ P
+      open Terminal (coalgebras (X × Y))
+
+      τ : X × D₀ Y ⇒ D₀ (X × Y)
+      τ = u (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
+
+      τ-law : out ∘ τ ≈ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
+      τ-law = commutes (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
+
+      τ-helper : τ ∘ (idC ⁂ out⁻¹) ≈ out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹
+      τ-helper = begin 
+        τ ∘ (idC ⁂ out⁻¹)                                                  ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+        (out⁻¹ ∘ out) ∘ τ ∘ (idC ⁂ out⁻¹)                                  ≈⟨ pullʳ (pullˡ τ-law) ⟩
+        out⁻¹ ∘ ((idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ assoc) ⟩
+        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                                               ∎
+      
+      ▷∘τ : τ ∘ (idC ⁂ ▷) ≈ ▷ ∘ τ
+      ▷∘τ = begin 
+        τ ∘ (idC ⁂ ▷)                                     ≈⟨ 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₂ ∘ τ                                    ≈⟨ sym-assoc ⟩ 
+        ▷ ∘ τ                                             ∎
+
+      τ-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 }))      
+
+    open τ-mod
+
+    strength : Strength monoidal monad
+    strength = record
+      { strengthen = ntHelper (record 
+        { η = τ
+        ; commute = commute' })
+      ; identityˡ = identityˡ' -- triangle
+      ; η-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 +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ 
+          out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
+          now ∎
+      ; μ-η-comm = μ-η-comm' -- μ-τ
+      ; strength-assoc = strength-assoc' -- square
+      }
+      where
+        identityˡ' : ∀ {X : Obj} → extend (now ∘ π₂) ∘ τ (Terminal.⊤ terminal , X) ≈ π₂
+        identityˡ' {X} = begin
+          extend (now ∘ π₂) ∘ τ _       ≈⟨ sym (Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = extend (now ∘ π₂) ∘ τ _ ; commutes = begin 
+            out ∘ extend (now ∘ π₂) ∘ τ _                                                                                                 ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym identityʳ)) ⟩ 
+            out ∘ extend (now ∘ π₂) ∘ τ _ ∘ idC                                                                                           ≈⟨ pullˡ diag₃ ⟩ 
+            ((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ _ ∘ idC                                                                                 ≈⟨ pullʳ (pullˡ (diag₂ (Terminal.⊤ terminal , X))) ⟩ 
+            (π₂ +₁ extend (now ∘ π₂)) ∘ ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ idC                                                ≈⟨ refl⟩∘⟨ (pullʳ (assoc ○ sym diag₁)) ⟩ 
+            (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ CC.+-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩ 
+            (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                          ≈⟨ pullˡ +₁∘+₁ ⟩ 
+            (π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                             ≈⟨ (+₁-cong₂ id-comm refl) ⟩∘⟨refl ⟩ 
+            (idC ∘ π₂ +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                             ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
+            (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                          ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimˡ identity²)) ⟩ 
+            (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                                        ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ 
+            (idC +₁ extend (now ∘ π₂)) ∘ (idC ∘ π₂ +₁ τ _ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                            ≈˘⟨ pullʳ (pullˡ +₁∘+₁) ⟩ 
+            ((idC +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                       ≈˘⟨ (homomorphism (X +-)) ⟩∘⟨refl ⟩ 
+            (idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                                  ∎ })) ⟩
+          u (Terminal.! (coalgebras X)) ≈⟨ Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = π₂ ; commutes = begin 
+            out ∘ π₂                                                ≈˘⟨ π₂∘⁂ ⟩ 
+            π₂ ∘ (idC ⁂ out)                                        ≈˘⟨ pullˡ distribute₂ ⟩
+            (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ 
+            (idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)    ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
+            (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
+          π₂                            ∎ 
+          where
+            diag₁ : (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈ distributeˡ⁻¹ {Terminal.⊤ terminal} {X} {D₀ X} ∘ (idC ⁂ out) ∘ idC
+            diag₁ = begin 
+              (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ 
+              (⟨ Terminal.! terminal , idC ⟩ ∘ π₂ +₁ idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)    ≈⟨ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ⟩∘⟨ (refl⟩∘⟨ sym identityʳ) ⟩ 
+              (idC +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC                                   ≈⟨ elimˡ (CC.+-unique id-comm-sym id-comm-sym) ⟩ 
+              distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC                                                  ∎
+            diag₂ = τ-law
+            diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out
+            diag₃ = out-law π₂
+
+        μ-η-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)) ∘ τ _                                                                                                  ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩
+            out ∘ extend (τ (X , Y)) ∘ τ _                                                                                                                     ≈⟨ square ⟩
+            [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                                                     ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩
+            ((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)                          ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
+            (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) ∎ })) ⟩
+          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)) ⟩ 
+            ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC)                                                               ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
+            (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC)                                                                         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩
+            (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out)                                                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩
+            (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out)                                                          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
+            (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out)                                                  ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩
+            ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
+            (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)   ∎ }) ⟩ 
+          τ _ ∘ (idC ⁂ extend idC)                                                                                                                                               ∎
+          where
+            -- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
+            square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
+            square = begin 
+              out ∘ extend (τ (X , Y)) ∘ τ _                                                 ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩ 
+              ([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _                    ≈⟨ pullʳ (τ-law _) ⟩ 
+              [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
+            tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
+            tri = begin 
+              [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹                                                                  ≈⟨ pullˡ []∘+₁ ⟩ 
+              [ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹                                                                 ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩ 
+              [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹                                          ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
+              [ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹                                 ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
+              [ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹           ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩ 
+              [ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩ 
+              (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹                               ∎
+            id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _)
+            id*∘Dτ = begin 
+              extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩ 
+              extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
+              extend (idC ∘ τ _)              ≈⟨ extend-≈ identityˡ ⟩ 
+              extend (τ _)                    ∎
+            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ˡ
+            tri₂' = begin 
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ]                                      ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩ 
+              (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 
+            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==
+-- -}
+        commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) 
+          → τ P₂ ∘ ((proj₁ fg) ⁂ extend (now ∘ (proj₂ fg))) ≈ extend (now ∘ ((proj₁ fg) ⁂ (proj₂ fg))) ∘ τ P₁
+        commute' {(U , V)} {(W , X)} (f , g) = begin 
+          τ _ ∘ (f ⁂ extend (now ∘ g)) ≈⟨ sym (!-unique (record { f = τ _ ∘ (f ⁂ extend (now ∘ g)) ; commutes = begin 
+            out ∘ τ (W , X) ∘ (f ⁂ extend (now ∘ g))                                                       ≈⟨ pullˡ (τ-law (W , X)) ⟩ 
+            ((idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (f ⁂ extend (now ∘ g))                    ≈⟨ pullʳ (pullʳ ⁂∘⁂) ⟩ 
+            (idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (idC ∘ f ⁂ out ∘ extend (now ∘ g))                        ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityˡ (extendlaw (now ∘ g)))) ⟩ 
+            (idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out)     ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ refl (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl))) ⟩ 
+            (idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ [ i₁ ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out)            ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identityʳ) refl)) ⟩ 
+            (idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ∘ idC ⁂ (g +₁ extend (now ∘ g)) ∘ out)                 ≈⟨ sym (pullʳ (pullʳ ⁂∘⁂)) ⟩ 
+            ((idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ extend (now ∘ g)))) ∘ (idC ⁂ out)             ≈⟨ (refl⟩∘⟨ (sym (distribute₁ f g (extend (now ∘ g))))) ⟩∘⟨refl ⟩ 
+            ((idC +₁ τ (W , X)) ∘ ((f ⁂ g) +₁ (f ⁂ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)       ≈⟨ (pullˡ +₁∘+₁) ⟩∘⟨refl ⟩ 
+            ((idC ∘ (f ⁂ g) +₁ τ (W , X) ∘ (f ⁂ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)          ≈⟨ sym (((+₁-cong₂ refl identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
+            ((idC ∘ (f ⁂ g) +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g))) ∘ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)  ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩ 
+            (idC +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g)))) ∘ ((f ⁂ g +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ∎ })) ⟩ 
+          u !                          ≈⟨ !-unique (record { f = extend (now ∘ (f ⁂ g)) ∘ τ _ ; commutes = begin 
+            out ∘ extend (now ∘ (f ⁂ g)) ∘ τ _                                                                ≈⟨ pullˡ (extendlaw (now ∘ (f ⁂ g))) ⟩ 
+            ([ out ∘ now ∘ (f ⁂ g) , i₂ ∘ extend (now ∘ (f ⁂ g)) ] ∘ out) ∘ τ (U , V)                         ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩∘⟨refl ⟩
+            ([ i₁ ∘ (f ⁂ g) , i₂ ∘ extend (now ∘ (f ⁂ g)) ] ∘ out) ∘ τ (U , V)                                ≈⟨ pullʳ (τ-law (U , V)) ⟩
+            ((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                ≈⟨ sym-assoc ○ sym-assoc ⟩
+            ((((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ _)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)            ≈⟨ (+₁∘+₁ ⟩∘⟨refl) ⟩∘⟨refl ⟩
+            ((((f ⁂ g) ∘ idC) +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)         ≈⟨ sym (((+₁-cong₂ id-comm-sym identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
+            (((idC ∘ (f ⁂ g)) +₁ ((extend (now ∘ (f ⁂ g)) ∘ τ (U , V)) ∘ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩
+            (idC +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ (((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)  ∎ }) ⟩
+          extend (now ∘ (f ⁂ g)) ∘ τ _ ∎
+          where
+            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 }
+```