From 9ff33adfda542416c75bfc83522d7c07f994bac5 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 15 Oct 2023 17:55:42 +0200 Subject: [PATCH] =?UTF-8?q?=F0=9F=9A=A7=20Work=20on=20=20commutativity?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Instance/AmbientCategory.lagda.md | 16 +++ src/Monad/Instance/Delay.lagda.md | 8 +- src/Monad/Instance/Delay/Commutative.lagda.md | 89 +++++++++++++- src/Monad/Instance/Delay/Quotienting.lagda.md | 30 ----- src/Monad/Instance/Delay/Strong.lagda.md | 112 +++++++++--------- 5 files changed, 161 insertions(+), 94 deletions(-) diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index 9a39709..471f9a0 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -1,5 +1,6 @@ ```agda @@ -234,6 +232,12 @@ and second that `extend f` is the unique morphism satisfying the commutative dia ▷∘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₀ diff --git a/src/Monad/Instance/Delay/Commutative.lagda.md b/src/Monad/Instance/Delay/Commutative.lagda.md index 91778d2..69aaf9d 100644 --- a/src/Monad/Instance/Delay/Commutative.lagda.md +++ b/src/Monad/Instance/Delay/Commutative.lagda.md @@ -1,32 +1,115 @@ ```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 - open Monoidal monoidal + 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 = {! !} } + 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 + -} + ``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay/Quotienting.lagda.md b/src/Monad/Instance/Delay/Quotienting.lagda.md index d22d956..137703d 100644 --- a/src/Monad/Instance/Delay/Quotienting.lagda.md +++ b/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 ⟩ diff --git a/src/Monad/Instance/Delay/Strong.lagda.md b/src/Monad/Instance/Delay/Strong.lagda.md index 36b7122..46dfe56 100644 --- a/src/Monad/Instance/Delay/Strong.lagda.md +++ b/src/Monad/Instance/Delay/Strong.lagda.md @@ -38,7 +38,60 @@ 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 + 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 @@ -56,58 +109,6 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De ; strength-assoc = strength-assoc' -- square } where - 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 ∎ - - -- TODO add to agda-categories - 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 = 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 })) - 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 @@ -141,13 +142,6 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De diag₂ = τ-law diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out diag₃ = out-law π₂ - -- TODO add to agda-categories - 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