From cfd5bf49681a579c4afa7a98b1d38ec6946c4514 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 16 Oct 2023 18:08:34 +0200 Subject: [PATCH] =?UTF-8?q?=F0=9F=9A=A7=20Great=20progress=20on=20commutat?= =?UTF-8?q?ivity=20proof=20of=20delay=20monad?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Instance/AmbientCategory.lagda.md | 33 +++-- src/Monad/Instance/Delay/Commutative.lagda.md | 124 +++++++++++------- src/Monad/Instance/Delay/Strong.lagda.md | 11 -- 3 files changed, 97 insertions(+), 71 deletions(-) diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index 471f9a0..2a7545d 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -65,6 +65,9 @@ module Category.Instance.AmbientCategory where distributive = Extensive×Cartesian⇒Distributive C extensive cartesian open Distributive distributive hiding (cartesian; cocartesian) public open M' C + open HomReasoning + open MR' C + open Equiv distributeˡ⁻¹ : ∀ {A B C : Obj} → A × (B + C) ⇒ A × B + A × C distributeˡ⁻¹ = IsIso.inv isIsoˡ @@ -81,10 +84,22 @@ module Category.Instance.AmbientCategory where [ 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 + + + 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ˡ)) + dstr-law₃ : ∀ {A B C} → distributeʳ⁻¹ {A} {B} {C} ∘ (i₁ ⁂ idC) ≈ i₁ + dstr-law₃ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ)) + dstr-law₄ : ∀ {A B C} → distributeʳ⁻¹ {A} {B} {C} ∘ (i₂ ⁂ idC) ≈ 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 M = M' module MR = MR' @@ -99,10 +114,6 @@ 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)) ∎ - where - open MR C - open HomReasoning - open Equiv iso-epi-from : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.from iso) iso-epi-from iso = λ f g eq → begin @@ -110,16 +121,10 @@ module Category.Instance.AmbientCategory where (f ∘ M'._≅_.from iso ∘ M'._≅_.to iso) ≈⟨ pullˡ eq ⟩ ((g ∘ M'._≅_.from iso) ∘ M'._≅_.to iso) ≈⟨ cancelʳ (_≅_.isoʳ iso) ⟩ g ∎ - where - open HomReasoning - open MR C iso-epi-to : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.to iso) iso-epi-to iso = λ f g eq → begin f ≈⟨ introʳ (_≅_.isoˡ iso) ⟩ (f ∘ M'._≅_.to iso ∘ M'._≅_.from iso) ≈⟨ pullˡ eq ⟩ ((g ∘ M'._≅_.to iso) ∘ M'._≅_.from iso) ≈⟨ cancelʳ (_≅_.isoˡ iso) ⟩ g ∎ - where - open HomReasoning - open MR C ``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay/Commutative.lagda.md b/src/Monad/Instance/Delay/Commutative.lagda.md index 69aaf9d..46a6fc5 100644 --- a/src/Monad/Instance/Delay/Commutative.lagda.md +++ b/src/Monad/Instance/Delay/Commutative.lagda.md @@ -15,6 +15,7 @@ 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 +open import Categories.NaturalTransformation ``` --> @@ -40,10 +41,11 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D 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 Functor functor using () renaming (F₁ to D₁; identity to D-identity; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈) + open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ) open Monad monad using (η; μ) - open StrongMonad strongMonad using () + -- open StrongMonad strongMonad using (strengthen) + open NaturalTransformation (StrongMonad.strengthen strongMonad) using () renaming (commute to τ-commute) ``` # The Delay Monad is commutative @@ -68,48 +70,78 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D (((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) ∎ } + σ-helper : ∀ {X Y : Obj} → σ {X} {Y} ∘ (out⁻¹ ⁂ idC) ≈ out⁻¹ ∘ (idC +₁ σ) ∘ distributeʳ⁻¹ + σ-helper {X} {Y} = begin + σ ∘ (out⁻¹ ⁂ idC) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ + (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ʳ⁻¹ ∎ 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 - -} - + commutes' {X} {Y} = guarded-unique g (extend σ ∘ τ) (extend τ ∘ σ) guarded (fixpoint-eq fixpoint₁) (fixpoint-eq fixpoint₂) + where + w = (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) + g = out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , ▷ ∘ now ∘ i₂ ] ] ∘ w + 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 ⟩ + -- [ (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 ∎) + fixpoint₂ = {! !} + 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 = ....' +should be ▷ ∘ η ∘ inr, but is η ∘ inr!! +-} ``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay/Strong.lagda.md b/src/Monad/Instance/Delay/Strong.lagda.md index 46dfe56..755cc25 100644 --- a/src/Monad/Instance/Delay/Strong.lagda.md +++ b/src/Monad/Instance/Delay/Strong.lagda.md @@ -38,17 +38,6 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De 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