✨ Finished proof that delay is commutative

index.lagda.md

@@ -15,6 +15,8 @@ We start out by formalizing Caprettas Delay Monad in category theory by existenc
 
 ```agda
 open import Monad.Instance.Delay
+open import Monad.Instance.Delay.Strong
+open import Monad.Instance.Delay.Commutative
 ```
 
 The next step is to quotient the delay monad by weak bisimilarity, in category theory this corresponds to existence of fitting coequalizers.

src/Category/Instance/AmbientCategory.lagda.md

@@ -114,6 +114,30 @@ module Category.Instance.AmbientCategory where
       (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)) ∎
+    -- TODO extract distribution proofs of the non inverses
+    distribute₁' : ∀ {X Y Z U V W} (f : X ⇒ U) (g : Y ⇒ V) (h : Z ⇒ W) → ((g ⁂ f) +₁ (h ⁂ f)) ∘ distributeʳ⁻¹ ≈ distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f)
+    distribute₁' f g h = 
+      Iso⇒Mono C (IsIso.iso isIsoʳ) ((g ⁂ f +₁ h ⁂ f) ∘ distributeʳ⁻¹) (distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f)) 
+      (Iso⇒Epi C (IsIso.iso isIsoʳ) (distributeʳ ∘ (g ⁂ f +₁ h ⁂ f) ∘ distributeʳ⁻¹) (distributeʳ ∘ distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f)) (begin 
+        (distributeʳ ∘ (g ⁂ f +₁ h ⁂ f) ∘ distributeʳ⁻¹) ∘ distributeʳ ≈⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoʳ)) ⟩ 
+        distributeʳ ∘ (g ⁂ f +₁ h ⁂ f) ≈⟨ []∘+₁ ⟩ 
+        [ (i₁ ⁂ idC) ∘ (g ⁂ f) , (i₂ ⁂ idC) ∘ (h ⁂ f) ] ≈⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩ 
+        [ (i₁ ∘ g ⁂ idC ∘ f) , (i₂ ∘ h ⁂ idC ∘ f) ] ≈˘⟨ []-cong₂ (⁂-cong₂ +₁∘i₁ id-comm) (⁂-cong₂ +₁∘i₂ id-comm) ⟩ 
+        [ (g +₁ h) ∘ i₁ ⁂ f ∘ idC , (g +₁ h) ∘ i₂ ⁂ f ∘ idC ] ≈˘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩ 
+        [ ((g +₁ h) ⁂ f) ∘ (i₁ ⁂ idC) , ((g +₁ h) ⁂ f) ∘ (i₂ ⁂ idC) ] ≈˘⟨ ∘[] ⟩ 
+        (((g +₁ h) ⁂ f) ∘ distributeʳ) ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoʳ) ⟩∘⟨refl ⟩ 
+        (distributeʳ ∘ distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f)) ∘ distributeʳ ∎))
+    dstldstr : ∀ {X Y U V} → (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ (distributeˡ⁻¹ {X + Y} {U} {V})
+    dstldstr = Iso⇒Epi C (IsIso.iso isIsoˡ) ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) (sym (begin 
+      (([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeˡ) ≈⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoˡ)) ⟩ 
+      ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹)) ≈⟨ []∘+₁ ⟩ 
+      [ (i₁ +₁ i₁) ∘ distributeʳ⁻¹ , (i₂ +₁ i₂) ∘ distributeʳ⁻¹ ] ≈⟨ {!   !} ⟩ 
+      {!   !} ≈˘⟨ {!   !} ⟩ 
+      {!   !} ≈˘⟨ {!   !} ⟩ 
+      {!   !} ≈˘⟨ {!   !} ⟩ 
+      {!   !} ≈˘⟨ {!   !} ⟩ 
+      [ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (idC ⁂ i₁) , ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (idC ⁂ i₂) ] ≈˘⟨ ∘[] ⟩ 
+      (((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ distributeˡ) ∎))
   
     iso-epi-from : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.from iso)
     iso-epi-from iso = λ f g eq → begin 

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

@@ -76,6 +76,18 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D
         (out⁻¹ ∘ out) ∘ σ ∘ (out⁻¹ ⁂ idC) ≈⟨ pullʳ (pullˡ (u-commutes (σ-coalg X Y))) ⟩ 
         out⁻¹ ∘ ((idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC)) ∘ (out⁻¹ ⁂ idC) ≈⟨ refl⟩∘⟨ (pullʳ (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ (_≅_.isoʳ out-≅) identity² ○ ⟨⟩-unique id-comm id-comm))) ⟩ 
         out⁻¹ ∘ (idC +₁ σ) ∘ distributeʳ⁻¹ ∎
+
+      -- TODO this should be in commutative, it expresses that σ is natural
+      σ-commute : ∀ {U V W X : Obj} (f : U ⇒ V) (g : W ⇒ X) → σ ∘ (extend (now ∘ f) ⁂ g) ≈ extend (now ∘ (f ⁂ g)) ∘ σ
+      σ-commute {U} {V} {W} {X} f g = begin 
+        σ ∘ (D₁ f ⁂ g) ≈⟨ pullʳ (pullʳ swap∘⁂) ⟩ 
+        D₁ swap ∘ τ ∘ (g ⁂ extend (now ∘ f)) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (τ-commute (g , f))) ⟩ 
+        D₁ swap ∘ (D₁ (g ⁂ f) ∘ τ) ∘ swap ≈⟨ pullˡ (pullˡ (sym D-homomorphism)) ⟩ 
+        (D₁ (swap ∘ (g ⁂ f)) ∘ τ) ∘ swap ≈⟨ ((D-resp-≈ swap∘⁂) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
+        (D₁ ((f ⁂ g) ∘ swap) ∘ τ) ∘ swap ≈⟨ pushˡ D-homomorphism ⟩∘⟨refl ⟩ 
+        (D₁ (f ⁂ g) ∘ D₁ swap ∘ τ) ∘ swap ≈⟨ assoc²' ⟩ 
+        D₁ (f ⁂ g) ∘ σ ∎
+
       commutes' : ∀ {X Y} → extend σ ∘ τ {D₀ X} {Y} ≈ extend τ ∘ σ 
       commutes' {X} {Y} = guarded-unique g (extend σ ∘ τ) (extend τ ∘ σ) guarded (fixpoint-eq fixpoint₁) (fixpoint-eq fixpoint₂)
         where
@@ -97,30 +109,83 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D
             [ D₁ (distributeʳ⁻¹ ∘ (i₁ ⁂ idC)) ∘ τ , D₁ (distributeʳ⁻¹ ∘ (i₂ ⁂ idC)) ∘ τ ] ≈⟨ []-cong₂ (D-resp-≈ dstr-law₃ ⟩∘⟨refl) ((D-resp-≈ dstr-law₄) ⟩∘⟨refl) ⟩ 
             [ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩ 
             ([ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)
-          fixpoint₁ = {!   !}
+
-          -- fixpoint₁ = Iso⇒Mono (_≅_.iso out-≅) (extend σ ∘ τ) (out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w) (begin 
+          fixpoint₁ = Iso⇒Mono (_≅_.iso out-≅) (extend σ ∘ τ) (out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w) (begin 
-          --   out ∘ extend σ ∘ τ ≈⟨ pullˡ (extendlaw σ) ⟩ 
+            out ∘ extend σ ∘ τ ≈⟨ pullˡ (extendlaw σ) ⟩ 
-          --   ([ out ∘ σ , i₂ ∘ extend' σ ] ∘ out) ∘ τ  ≈⟨ pullʳ (τ-law (D₀ X , Y)) ⟩
+            ([ out ∘ σ , i₂ ∘ extend' σ ] ∘ out) ∘ τ  ≈⟨ pullʳ (τ-law (D₀ X , Y)) ⟩
-          --   [ out ∘ σ , i₂ ∘ extend' σ ] ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)  ≈⟨ pullˡ []∘+₁ ⟩
+            [ out ∘ σ , i₂ ∘ extend' σ ] ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)  ≈⟨ pullˡ []∘+₁ ⟩
-          --   [ (out ∘ σ) ∘ idC , (i₂ ∘ extend' σ) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)  ≈⟨ ([]-cong₂ (identityʳ ○ u-commutes (σ-coalg X Y)) assoc) ⟩∘⟨refl ⟩
+            [ (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 ⟩
+            [ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend' σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (sym (_≅_.isoˡ out-≅)) refl ⟩
-          --   [ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend' σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out⁻¹ ∘ out ⁂ out)  ≈⟨ sym (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩
+            [ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend' σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out⁻¹ ∘ out ⁂ out)  ≈⟨ sym (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩
-          --   [ (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' σ ∘ τ ] ∘ 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) , i₂ ∘ extend' σ ∘ τ ] ∘ (((out⁻¹ ⁂ idC) +₁ (out⁻¹ ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (out ⁂ out)  ≈⟨ pullˡ (pullˡ []∘+₁) ⟩
-          --   ([ ((idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC)) ∘ (out⁻¹ ⁂ idC) , (i₂ ∘ extend' σ ∘ τ) ∘ (out⁻¹ ⁂ idC) ] ∘ distributeˡ⁻¹) ∘ (out ⁂ out)  ≈⟨ assoc ○ ([]-cong₂ (pullʳ (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ (_≅_.isoʳ out-≅) identity² ○ ⟨⟩-unique id-comm id-comm))) (refl⟩∘⟨ (⁂-cong₂ refl (sym D-identity)) ○ (pullʳ (pullʳ (τ-commute (out⁻¹ , idC)))))) ⟩∘⟨refl ⟩
+            ([ ((idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC)) ∘ (out⁻¹ ⁂ idC) , (i₂ ∘ extend' σ ∘ τ) ∘ (out⁻¹ ⁂ idC) ] ∘ distributeˡ⁻¹) ∘ (out ⁂ out)  ≈⟨ assoc ○ ([]-cong₂ (pullʳ (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ (_≅_.isoʳ out-≅) identity² ○ ⟨⟩-unique id-comm id-comm))) (refl⟩∘⟨ (⁂-cong₂ refl (sym D-identity)) ○ (pullʳ (pullʳ (τ-commute (out⁻¹ , idC)))))) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend' σ ∘ D₁ (out⁻¹ ⁂ idC) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ (pullˡ (sym k-assoc)) ○ refl⟩∘⟨ ((extend-≈ (pullˡ k-identityʳ)) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend' σ ∘ D₁ (out⁻¹ ⁂ idC) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ (pullˡ (sym k-assoc)) ○ refl⟩∘⟨ ((extend-≈ (pullˡ k-identityʳ)) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend' (σ ∘ (out⁻¹ ⁂ idC)) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ((extend-≈ σ-helper) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend' (σ ∘ (out⁻¹ ⁂ idC)) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ((extend-≈ σ-helper) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend' (out⁻¹ ∘ (idC +₁ σ) ∘ distributeʳ⁻¹) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈˘⟨ ([]-cong₂ refl (refl⟩∘⟨ ((sym k-assoc ○ extend-≈ (pullˡ k-identityʳ) ○ extend-≈ assoc) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend' (out⁻¹ ∘ (idC +₁ σ) ∘ distributeʳ⁻¹) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈˘⟨ ([]-cong₂ refl (refl⟩∘⟨ ((sym k-assoc ○ extend-≈ (pullˡ k-identityʳ) ○ extend-≈ assoc) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ (extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ D₁ distributeʳ⁻¹) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ pullʳ helper₁)) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ (extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ D₁ distributeʳ⁻¹) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ pullʳ helper₁)) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ [ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ refl assoc²') ⟩
+            [ (idC +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ [ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ refl assoc²') ⟩
-          --   [ (idC +₁ σ) , i₂ ∘ extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ [ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ∘[])) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) , i₂ ∘ extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ [ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ∘[])) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) , i₂ ∘ [ extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ D₁ i₁ ∘ τ , extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ D₁ i₂ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ))) (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ)))))) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) , i₂ ∘ [ extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ D₁ i₁ ∘ τ , extend' (out⁻¹ ∘ (idC +₁ σ)) ∘ D₁ i₂ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ))) (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ)))))) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) , i₂ ∘ [ extend' ((out⁻¹ ∘ (idC +₁ σ)) ∘ i₁) ∘ τ , extend' ((out⁻¹ ∘ (idC +₁ σ)) ∘ i₂) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ ((extend-≈ (pullʳ +₁∘i₁)) ⟩∘⟨refl) ((extend-≈ (pullʳ +₁∘i₂)) ⟩∘⟨refl)))) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) , i₂ ∘ [ extend' ((out⁻¹ ∘ (idC +₁ σ)) ∘ i₁) ∘ τ , extend' ((out⁻¹ ∘ (idC +₁ σ)) ∘ i₂) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ ((extend-≈ (pullʳ +₁∘i₁)) ⟩∘⟨refl) ((extend-≈ (pullʳ +₁∘i₂)) ⟩∘⟨refl)))) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) , i₂ ∘ [ extend' (out⁻¹ ∘ i₁ ∘ idC) ∘ τ , extend' (out⁻¹ ∘ i₂ ∘ σ) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ (elimˡ ((extend-≈ (refl⟩∘⟨ identityʳ)) ○ k-identityˡ)) ((extend-≈ sym-assoc) ⟩∘⟨refl)))) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) , i₂ ∘ [ extend' (out⁻¹ ∘ i₁ ∘ idC) ∘ τ , extend' (out⁻¹ ∘ i₂ ∘ σ) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ (elimˡ ((extend-≈ (refl⟩∘⟨ identityʳ)) ○ k-identityˡ)) ((extend-≈ sym-assoc) ⟩∘⟨refl)))) ⟩∘⟨refl ⟩
-          --   [ (idC +₁ σ) , i₂ ∘ [ τ , extend' (▷ ∘ σ) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ refl ((sym (▷∘extendˡ σ)) ⟩∘⟨refl ○ assoc)))) ⟩∘⟨refl ⟩
+            [ (idC +₁ σ) , i₂ ∘ [ τ , extend' (▷ ∘ σ) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ refl ((sym (▷∘extendˡ σ)) ⟩∘⟨refl ○ assoc)))) ⟩∘⟨refl ⟩
-          --   [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w  ≈˘⟨ cancelˡ (_≅_.isoʳ out-≅) ⟩
+            [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w  ≈˘⟨ cancelˡ (_≅_.isoʳ out-≅) ⟩
-          --   out ∘ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w ∎)
+            out ∘ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w ∎)
-          fixpoint₂ = {!   !}
+
+          helper₂ : (D₁ distributeˡ⁻¹) ∘ σ ≈ [ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ∘ distributeˡ⁻¹
+          helper₂ = Iso⇒Epi (IsIso.iso isIsoˡ) ((D₁ distributeˡ⁻¹) ∘ σ) ([ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ∘ distributeˡ⁻¹) (begin 
+            ((D₁ distributeˡ⁻¹) ∘ σ) ∘ distributeˡ ≈⟨ ∘[] ⟩ 
+            [ ((D₁ distributeˡ⁻¹) ∘ σ) ∘ (idC ⁂ i₁) , ((D₁ distributeˡ⁻¹) ∘ σ) ∘ (idC ⁂ i₂) ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⁂-cong₂ (sym D-identity) refl) (refl⟩∘⟨ ⁂-cong₂ (sym D-identity) refl) ⟩ 
+            [ ((D₁ distributeˡ⁻¹) ∘ σ) ∘ (D₁ idC ⁂ i₁) , ((D₁ distributeˡ⁻¹) ∘ σ) ∘ (D₁ idC ⁂ i₂) ] ≈⟨ []-cong₂ (pullʳ (σ-commute idC i₁)) (pullʳ (σ-commute idC i₂)) ⟩ 
+            [ (D₁ distributeˡ⁻¹) ∘ D₁ (idC ⁂ i₁) ∘ σ , (D₁ distributeˡ⁻¹) ∘ D₁ (idC ⁂ i₂) ∘ σ ] ≈⟨ []-cong₂ (pullˡ (sym D-homomorphism)) (pullˡ (sym D-homomorphism)) ⟩ 
+            [ D₁ (distributeˡ⁻¹ ∘ (idC ⁂ i₁)) ∘ σ , D₁ (distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ σ ] ≈⟨ []-cong₂ (D-resp-≈ dstr-law₁ ⟩∘⟨refl) (D-resp-≈ dstr-law₂ ⟩∘⟨refl) ⟩ 
+            [ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩ 
+            ([ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
+          helper₃ = begin 
+            [ idC +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out {X} ⁂ out {Y}) ≈⟨ refl⟩∘⟨ helper ⟩ 
+            [ idC +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ] ∘ [ [ i₁ ∘ i₁ , i₂ ∘ i₁ ] , [ (i₁ ∘ i₂) , (i₂ ∘ i₂) ] ] ∘ w ≈⟨ pullˡ ∘[] ⟩
+            [ [ idC +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ] ∘ [ i₁ ∘ i₁ , i₂ ∘ i₁ ] , [ idC +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ] ∘ [ (i₁ ∘ i₂) , (i₂ ∘ i₂) ] ] ∘ w ≈⟨ ([]-cong₂ ∘[] ∘[]) ⟩∘⟨refl ⟩
+            [ [ [ idC +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ] ∘ i₁ ∘ i₁ , [ idC +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ] ∘ i₂ ∘ i₁ ] , [ [ idC +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ] ∘ (i₁ ∘ i₂) , [ idC +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ] ∘ (i₂ ∘ i₂) ] ] ∘ w ≈⟨ ([]-cong₂ ([]-cong₂ (pullˡ inject₁) (pullˡ inject₂ ○ assoc)) ([]-cong₂ (pullˡ inject₁) (pullˡ inject₂ ○ assoc))) ⟩∘⟨refl ⟩
+            [ [ (idC +₁ τ) ∘ i₁ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ∘ i₁ ] , [ (idC +₁ τ) ∘ i₂ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , ▷ ∘ extend τ ∘ σ ] ∘ i₂ ] ] ∘ w ≈⟨ ([]-cong₂ ([]-cong₂ (+₁∘i₁ ○ identityʳ) (refl⟩∘⟨ inject₁)) ([]-cong₂ +₁∘i₂ (refl⟩∘⟨ inject₂))) ⟩∘⟨refl ⟩
+            [ [ i₁ , i₂ ∘ σ ] , [ i₂ ∘ τ , i₂ ∘ ▷ ∘ extend τ ∘ σ ] ] ∘ w ≈˘⟨ ([]-cong₂ ([]-cong₂ identityʳ refl) ∘[]) ⟩∘⟨refl ⟩
+            [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend τ ∘ σ ] ] ∘ w ∎
+            where
+              helper : (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out {X} ⁂ out {Y}) ≈ [ [ i₁ ∘ i₁ , i₂ ∘ i₁ ] , [ (i₁ ∘ i₂) , (i₂ ∘ i₂) ] ] ∘ w
+              helper = sym (begin 
+                [ [ i₁ ∘ i₁ , i₂ ∘ i₁ ] , [ (i₁ ∘ i₂) , (i₂ ∘ i₂) ] ] ∘ w ≈⟨ pullˡ []∘+₁ ⟩ 
+                [ (i₁ +₁ i₁) ∘ distributeʳ⁻¹ , (i₂ +₁ i₂) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ ((+₁-cong₂ (sym dstr-law₁) (sym dstr-law₁)) ⟩∘⟨refl) ((+₁-cong₂ (sym dstr-law₂) (sym dstr-law₂)) ⟩∘⟨refl)) ⟩∘⟨refl ⟩ 
+                [ (distributeˡ⁻¹ ∘ (idC ⁂ i₁) +₁ distributeˡ⁻¹ ∘ (idC ⁂ i₁)) ∘ distributeʳ⁻¹ , (distributeˡ⁻¹ ∘ (idC ⁂ i₂) +₁ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘+₁)) ⟩∘⟨refl) ⟩ 
+                [ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ ((idC ⁂ i₁) +₁ (idC ⁂ i₁)) ∘ distributeʳ⁻¹ , (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ ((idC ⁂ i₂) +₁ (idC ⁂ i₂)) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ sym (pullˡ ∘[]) ⟩
+                (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ [ ((idC ⁂ i₁) +₁ (idC ⁂ i₁)) ∘ distributeʳ⁻¹ , ((idC ⁂ i₂) +₁ (idC ⁂ i₂)) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ []-cong₂ (distribute₁' i₁ idC idC) (distribute₁' i₂ idC idC) ⟩∘⟨refl ⟩ 
+                (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ [ distributeʳ⁻¹ ∘ ((idC +₁ idC) ⁂ i₁) , distributeʳ⁻¹ ∘ ((idC +₁ idC) ⁂ i₂) ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ (sym (pullˡ ∘[])) ⟩ 
+                (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ [ ((idC +₁ idC) ⁂ i₁) , ((idC +₁ idC) ⁂ i₂) ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ([]-cong₂ (⁂-cong₂ ([]-unique id-comm-sym id-comm-sym) refl) (⁂-cong₂ ([]-unique id-comm-sym id-comm-sym) refl)) ⟩∘⟨refl ⟩ 
+                (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩ 
+                (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ∎)
+
+          fixpoint₂ = Iso⇒Mono ((_≅_.iso out-≅)) (extend τ ∘ σ) (out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend τ ∘ σ ] ] ∘ w) (begin 
+            out ∘ extend τ ∘ σ ≈⟨ pullˡ (extendlaw τ) ⟩ 
+            ([ out ∘ τ , i₂ ∘ extend τ ] ∘ out) ∘ σ ≈⟨ pullʳ (u-commutes (σ-coalg X (D₀ Y))) ⟩ 
+            [ out ∘ τ , i₂ ∘ extend τ ] ∘ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) ≈⟨ pullˡ []∘+₁ ⟩ 
+            [ (out ∘ τ) ∘ idC , (i₂ ∘ extend τ) ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend τ ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) (_≅_.isoˡ out-≅)) ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend τ ∘ σ ] ∘ distributeʳ⁻¹ ∘ ((idC +₁ idC) ⁂ out⁻¹) ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ (pullˡ (sym (distribute₁' out⁻¹ idC idC))) ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend τ ∘ σ ] ∘ (((idC ⁂ out⁻¹) +₁ (idC ⁂ out⁻¹)) ∘ distributeʳ⁻¹) ∘ (out ⁂ out) ≈⟨ pullˡ (pullˡ []∘+₁) ⟩ 
+            ([ ((idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ out⁻¹) , (i₂ ∘ extend τ ∘ σ) ∘ (idC ⁂ out⁻¹) ] ∘ distributeʳ⁻¹) ∘ (out ⁂ out) ≈⟨ assoc ○ ([]-cong₂ (pullʳ (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² (_≅_.isoʳ out-≅) ○ ⟨⟩-unique id-comm id-comm))) (refl⟩∘⟨ (⁂-cong₂ (sym D-identity) refl))) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ , (i₂ ∘ extend τ ∘ σ) ∘ (D₁ idC ⁂ out⁻¹) ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (pullʳ (pullʳ (σ-commute idC out⁻¹)))) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ , i₂ ∘ extend τ ∘ D₁ (idC ⁂ out⁻¹) ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ))))) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ , i₂ ∘ extend (τ ∘ (idC ⁂ out⁻¹)) ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ((extend-≈ (τ-helper (X , Y))) ⟩∘⟨refl))) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ , i₂ ∘ extend (out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈˘⟨ ([]-cong₂ refl (refl⟩∘⟨ pullˡ ((sym k-assoc) ○ (extend-≈ (pullˡ k-identityʳ) ○ extend-≈ assoc)))) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ , i₂ ∘ extend (out⁻¹ ∘ (idC +₁ τ)) ∘ D₁ distributeˡ⁻¹ ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl ((refl⟩∘⟨ (refl⟩∘⟨ helper₂)) ○ sym assoc²')) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) ∘ distributeˡ⁻¹ , (i₂ ∘ extend (out⁻¹ ∘ (idC +₁ τ)) ∘ [ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ]) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ 
+            ([ (idC +₁ τ) , i₂ ∘ extend (out⁻¹ ∘ (idC +₁ τ)) ∘ [ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹)) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ assoc ○ ([]-cong₂ refl (refl⟩∘⟨ ∘[])) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) , i₂ ∘ [ extend (out⁻¹ ∘ (idC +₁ τ)) ∘ D₁ i₁ ∘ σ , extend (out⁻¹ ∘ (idC +₁ τ)) ∘ D₁ i₂ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ (pullˡ (sym k-assoc ○ extend-≈ (pullˡ k-identityʳ))) (pullˡ (sym k-assoc ○ extend-≈ (pullˡ k-identityʳ)))))) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) , i₂ ∘ [ extend ((out⁻¹ ∘ (idC +₁ τ)) ∘ i₁) ∘ σ , extend ((out⁻¹ ∘ (idC +₁ τ)) ∘ i₂) ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ []-cong₂ refl (refl⟩∘⟨ []-cong₂ (extend-≈ (pullʳ inject₁) ⟩∘⟨refl) (extend-≈ (pullʳ inject₂) ⟩∘⟨refl)) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) , i₂ ∘ [ extend (out⁻¹ ∘ i₁ ∘ idC) ∘ σ , extend (out⁻¹ ∘ i₂ ∘ τ) ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ []-cong₂ refl (refl⟩∘⟨ []-cong₂ (elimˡ (extend-≈ (refl⟩∘⟨ identityʳ) ○ k-identityˡ)) (extend-≈ sym-assoc ⟩∘⟨refl ○ sym (pullˡ (▷∘extendˡ τ)))) ⟩∘⟨refl ⟩ 
+            [ (idC +₁ τ) , i₂ ∘ [ σ , ▷ ∘ extend τ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ helper₃ ⟩ 
+            [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend τ ∘ σ ] ] ∘ w ≈˘⟨ cancelˡ (_≅_.isoʳ out-≅) ⟩ 
+            out ∘ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend τ ∘ σ ] ] ∘ w ∎)
+
           fixpoint-eq : ∀ {f : D₀ X × D₀ Y ⇒ D₀ (X × Y)} → f ≈ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ f ] ] ∘ w → f ≈ extend [ now , f ] ∘ g
           fixpoint-eq {f} fix = begin 
             f ≈⟨ fix ⟩