diff --git a/index.lagda.md b/index.lagda.md index 05d0606..dd43efc 100644 --- a/index.lagda.md +++ b/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. diff --git a/src/Monad/Instance/Delay/Commutative.lagda.md b/src/Monad/Instance/Delay/Commutative.lagda.md index 04a737c..12f1a49 100644 --- a/src/Monad/Instance/Delay/Commutative.lagda.md +++ b/src/Monad/Instance/Delay/Commutative.lagda.md @@ -93,50 +93,46 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D where w = (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) g = out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w - guarded = {! !} - -- guarded : is-guarded g - -- guarded = [ idC +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w , (begin - -- (i₁ +₁ idC) ∘ [ idC +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ pullˡ ∘[] ⟩ - -- [ (i₁ +₁ idC) ∘ (idC +₁ D₁ i₁ ∘ σ) , (i₁ +₁ idC) ∘ i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ ([]-cong₂ +₁∘+₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ - -- [ (i₁ ∘ idC +₁ idC ∘ D₁ i₁ ∘ σ) , (i₂ ∘ idC) ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ ([]-cong₂ (+₁-cong₂ identityʳ identityˡ) (identityʳ ⟩∘⟨refl)) ⟩∘⟨refl ⟩ - -- [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ sym (cancelˡ (_≅_.isoʳ out-≅)) ⟩ - -- out ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ∎) - -- 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ʳ⁻¹) ∘ τ) ∘ (i₁ ⁂ idC) , ((D₁ distributeʳ⁻¹) ∘ τ) ∘ (i₂ ⁂ idC) ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⁂-cong₂ refl (sym D-identity))) (refl⟩∘⟨ (⁂-cong₂ refl (sym D-identity))) ⟩ - -- [ ((D₁ distributeʳ⁻¹) ∘ τ) ∘ (i₁ ⁂ D₁ idC) , ((D₁ distributeʳ⁻¹) ∘ τ) ∘ (i₂ ⁂ D₁ idC) ] ≈⟨ []-cong₂ (pullʳ (τ-commute (i₁ , idC))) (pullʳ (τ-commute (i₂ , idC))) ⟩ - -- [ (D₁ distributeʳ⁻¹) ∘ D₁ (i₁ ⁂ idC) ∘ τ , (D₁ distributeʳ⁻¹) ∘ D₁ (i₂ ⁂ idC) ∘ τ ] ≈⟨ []-cong₂ (pullˡ (sym D-homomorphism)) (pullˡ (sym D-homomorphism)) ⟩ - -- [ 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 - -- 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 ⟩ + guarded : is-guarded g + guarded = [ idC +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w , (begin + (i₁ +₁ idC) ∘ [ idC +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ pullˡ ∘[] ⟩ + [ (i₁ +₁ idC) ∘ (idC +₁ D₁ i₁ ∘ σ) , (i₁ +₁ idC) ∘ i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ ([]-cong₂ +₁∘+₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ + [ (i₁ ∘ idC +₁ idC ∘ D₁ i₁ ∘ σ) , (i₂ ∘ idC) ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ ([]-cong₂ (+₁-cong₂ identityʳ identityˡ) (identityʳ ⟩∘⟨refl)) ⟩∘⟨refl ⟩ + [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ sym (cancelˡ (_≅_.isoʳ out-≅)) ⟩ + out ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ∎) + 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ʳ⁻¹) ∘ τ) ∘ (i₁ ⁂ idC) , ((D₁ distributeʳ⁻¹) ∘ τ) ∘ (i₂ ⁂ idC) ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⁂-cong₂ refl (sym D-identity))) (refl⟩∘⟨ (⁂-cong₂ refl (sym D-identity))) ⟩ + [ ((D₁ distributeʳ⁻¹) ∘ τ) ∘ (i₁ ⁂ D₁ idC) , ((D₁ distributeʳ⁻¹) ∘ τ) ∘ (i₂ ⁂ D₁ idC) ] ≈⟨ []-cong₂ (pullʳ (τ-commute (i₁ , idC))) (pullʳ (τ-commute (i₂ , idC))) ⟩ + [ (D₁ distributeʳ⁻¹) ∘ D₁ (i₁ ⁂ idC) ∘ τ , (D₁ distributeʳ⁻¹) ∘ D₁ (i₂ ⁂ idC) ∘ τ ] ≈⟨ []-cong₂ (pullˡ (sym D-homomorphism)) (pullˡ (sym D-homomorphism)) ⟩ + [ 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ʳ ∎) - -- [ (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⁻¹ ⁂ (idC +₁ idC)) ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ pullˡ (sym (distribute₁ out⁻¹ idC idC)) ⟩ + fixpoint₁ = Iso⇒Mono (_≅_.iso out-≅) (extend σ ∘ τ) (out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w) (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 ⟩ + [ (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' σ ∘ τ ] ∘ (((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ʳ⁻¹ , 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ʳ⁻¹) ∘ τ ] ∘ 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₁ 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₁ ∘ τ , 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⁻¹ ∘ 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 σ ∘ τ ] ] ∘ w ≈˘⟨ cancelˡ (_≅_.isoʳ out-≅) ⟩ + out ∘ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w ∎) - -- [ (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ʳ⁻¹ , 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ʳ⁻¹) ∘ τ ] ∘ 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₁ 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₁ ∘ τ , 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⁻¹ ∘ 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 σ ∘ τ ] ] ∘ w ≈˘⟨ cancelˡ (_≅_.isoʳ out-≅) ⟩ - -- out ∘ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend σ ∘ τ ] ] ∘ w ∎) 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ˡ ≈⟨ ∘[] ⟩ @@ -146,6 +142,27 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D [ 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))) ⟩ @@ -165,41 +182,28 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D [ (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) ≈⟨ {! !} ⟩ - [ (idC +₁ τ) , i₂ ∘ [ D₁ swap ∘ τ , ▷ ∘ extend τ ∘ σ ] ] ∘ (idC +₁ (swap +₁ idC)) ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - -- TODO proof D₁ swap ∘ τ ≈ σ ∘ swap , follows by definition!! - -- ... wrong lead, brings σ back.. - {- - extend τ ∘ σ - ≈ extend τ ∘ D₁ swap ∘ τ ∘ swap - ≈ extend (τ ∘ swap) ∘ τ ∘ swap - -} - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - [ idC +₁ D₁ swap ∘ τ , i₂ ∘ [ τ , ▷ ∘ extend τ ∘ σ ] ] ∘ ((idC +₁ swap) +₁ idC) ∘ w ≈⟨ {! !} ⟩ + [ (idC +₁ τ) , i₂ ∘ [ σ , ▷ ∘ extend τ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) ≈⟨ helper₃ ⟩ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend τ ∘ σ ] ] ∘ w ≈˘⟨ cancelˡ (_≅_.isoʳ out-≅) ⟩ out ∘ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ extend τ ∘ σ ] ] ∘ w ∎) - fixpoint-eq = {! !} - -- 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 ⟩ - -- out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ f ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (refl⟩∘⟨ ([]-cong₂ refl (pullʳ inject₂))) ⟩∘⟨refl ⟩ - -- out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , (▷ ∘ [ now , f ]) ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (sym ∘[] ○ refl⟩∘⟨ []-cong₂ (elimˡ (extend-≈ inject₁ ○ k-identityˡ)) (pullˡ k-identityʳ)) ⟩∘⟨refl ⟩ - -- out⁻¹ ∘ [ idC +₁ σ , [ i₂ ∘ extend ([ now , f ] ∘ i₁) ∘ τ , i₂ ∘ extend (▷ ∘ [ now , f ]) ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ ([]-cong₂ (sym identityʳ) (refl⟩∘⟨ (elimˡ ((extend-≈ inject₁) ○ k-identityˡ)))) ([]-cong₂ (pullʳ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ)))) (pullʳ (pullˡ (▷∘extendʳ [ now , f ])))) ⟩∘⟨refl ⟩ - -- out⁻¹ ∘ [ [ i₁ , i₂ ∘ extend ([ now , f ] ∘ i₁) ∘ σ ] , [ (i₂ ∘ extend [ now , f ]) ∘ D₁ i₁ ∘ τ , (i₂ ∘ extend [ now , f ]) ∘ ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ ([]-cong₂ inject₁ (pullʳ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ))))) ∘[] ⟩∘⟨refl ⟩ - -- out⁻¹ ∘ [ [ [ i₁ , out ∘ f ] ∘ i₁ , (i₂ ∘ extend [ now , f ]) ∘ D₁ i₁ ∘ σ ] , (i₂ ∘ extend [ now , f ]) ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ (([]-cong₂ []∘+₁ (pullˡ inject₂)) ⟩∘⟨refl) ⟩ - -- out⁻¹ ∘ [ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ (i₁ +₁ D₁ i₁ ∘ σ) , [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ - -- out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ Iso⇒Mono (_≅_.iso out-≅) (out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w) (extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w) helper ⟩ - -- extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ∎ - -- where - -- helper = begin - -- out ∘ out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ cancelˡ (_≅_.isoʳ out-≅) ⟩ - -- [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ ([]-cong₂ (∘[] ○ []-cong₂ unitlaw refl) refl) ⟩∘⟨refl ⟩ - -- [ out ∘ [ now , f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ pullʳ (cancelˡ (_≅_.isoʳ out-≅)) ⟩ - -- ([ out ∘ [ now , f ] , i₂ ∘ extend [ now , f ] ] ∘ out) ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ pullˡ (extendlaw [ now , f ]) ⟩ - -- out ∘ extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ 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 ⟩ + out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ f ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (refl⟩∘⟨ ([]-cong₂ refl (pullʳ inject₂))) ⟩∘⟨refl ⟩ + out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , (▷ ∘ [ now , f ]) ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (sym ∘[] ○ refl⟩∘⟨ []-cong₂ (elimˡ (extend-≈ inject₁ ○ k-identityˡ)) (pullˡ k-identityʳ)) ⟩∘⟨refl ⟩ + out⁻¹ ∘ [ idC +₁ σ , [ i₂ ∘ extend ([ now , f ] ∘ i₁) ∘ τ , i₂ ∘ extend (▷ ∘ [ now , f ]) ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ ([]-cong₂ (sym identityʳ) (refl⟩∘⟨ (elimˡ ((extend-≈ inject₁) ○ k-identityˡ)))) ([]-cong₂ (pullʳ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ)))) (pullʳ (pullˡ (▷∘extendʳ [ now , f ])))) ⟩∘⟨refl ⟩ + out⁻¹ ∘ [ [ i₁ , i₂ ∘ extend ([ now , f ] ∘ i₁) ∘ σ ] , [ (i₂ ∘ extend [ now , f ]) ∘ D₁ i₁ ∘ τ , (i₂ ∘ extend [ now , f ]) ∘ ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ ([]-cong₂ inject₁ (pullʳ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ))))) ∘[] ⟩∘⟨refl ⟩ + out⁻¹ ∘ [ [ [ i₁ , out ∘ f ] ∘ i₁ , (i₂ ∘ extend [ now , f ]) ∘ D₁ i₁ ∘ σ ] , (i₂ ∘ extend [ now , f ]) ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ (([]-cong₂ []∘+₁ (pullˡ inject₂)) ⟩∘⟨refl) ⟩ + out⁻¹ ∘ [ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ (i₁ +₁ D₁ i₁ ∘ σ) , [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ + out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ Iso⇒Mono (_≅_.iso out-≅) (out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w) (extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w) helper ⟩ + extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ∎ + where + helper = begin + out ∘ out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈⟨ cancelˡ (_≅_.isoʳ out-≅) ⟩ + [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ ([]-cong₂ (∘[] ○ []-cong₂ unitlaw refl) refl) ⟩∘⟨refl ⟩ + [ out ∘ [ now , f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ pullʳ (cancelˡ (_≅_.isoʳ out-≅)) ⟩ + ([ out ∘ [ now , f ] , i₂ ∘ extend [ now , f ] ] ∘ out) ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ pullˡ (extendlaw [ now , f ]) ⟩ + out ∘ extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w ∎ {- TODO there's an error in the paper, at the end of the proof of proposition two: the last line of the 3 line calulation 'f = ....'