From 58bab7cbf477340abc663502a22ab12df0f23d52 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 11 Sep 2023 19:52:11 +0200 Subject: [PATCH] =?UTF-8?q?=F0=9F=8E=89=20Finished=20proof=20that=20delay?= =?UTF-8?q?=20is=20a=20monad?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Monad/Instance/Delay.lagda.md | 277 ++++++++++++++---------------- 1 file changed, 133 insertions(+), 144 deletions(-) diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index fe9283e..14ee386 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -54,7 +54,8 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ open Equiv open HomReasoning open CoLambek - open F-Coalgebra-Morphism + open F-Coalgebra-Morphism renaming (f to u) + open F-Coalgebra ``` ### *Proposition 1*: Characterization of the delay monad ***D*** @@ -92,16 +93,15 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ later : DX ⇒ DX later = out⁻¹ ∘ i₂ - -- TODO inline unitlaw : out ∘ now ≈ i₁ unitlaw = cancelˡ (_≅_.isoʳ out-≅) module _ {Y : Obj} where coit : Y ⇒ X + Y → Y ⇒ DX - coit f = F-Coalgebra-Morphism.f (! {A = record { A = Y ; α = f }}) + coit f = u (! {A = record { A = Y ; α = f }}) coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f - coit-commutes f = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }}) + coit-commutes f = commutes (! {A = record { A = Y ; α = f }}) module _ (ℕ : ParametrizedNNO) where open ParametrizedNNO ℕ @@ -110,7 +110,7 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ iso = Lambek.lambek (record { ⊥ = PNNO-Algebra CC coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ CC coproducts ℕ X }) ι : X × N ⇒ DX - ι = f (! {A = record { A = X × N ; α = _≅_.from iso }}) + ι = u (! {A = record { A = X × N ; α = _≅_.from iso }}) monad : Monad C @@ -118,164 +118,153 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ { F₀ = D₀ ; unit = λ {X} → now X ; extend = extend - ; identityʳ = λ {X} {Y} {f} → begin - extend f ∘ now X ≈⟨ (insertˡ (_≅_.isoˡ (out-≅ Y))) ⟩∘⟨refl ⟩ - (out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ - (out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩ - out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ - out⁻¹ Y ∘ out Y ∘ f ≈⟨ cancelˡ (_≅_.isoˡ (out-≅ Y)) ⟩ - f ∎ - ; identityˡ = λ {X} → Terminal.⊤-id (algebras X) (record { f = extend (now X) ; commutes = begin - out X ∘ extend (now X) ≈⟨ pullˡ ((F-Coalgebra-Morphism.commutes (Terminal.! (algebras X) {A = alg (now X)}))) ⟩ - ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ F-Coalgebra.α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ - (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) - ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ (unitlaw X)) ○ inject₁) refl ⟩∘⟨refl ⟩ - (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ - [ (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ - , (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ - [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ refl assoc) ⟩∘⟨refl ⟩ - [ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ - ([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X ≈⟨ (elimˡ +-η) ⟩∘⟨refl ⟩ - (idC +₁ extend (now X)) ∘ out X ∎ }) - ; assoc = λ {X} {Y} {Z} {g} {h} → {! !} - - -- begin - -- extend (extend h ∘ g) ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Z)) ⟩ - -- out⁻¹ Z ∘ out Z ∘ extend (extend h ∘ g) ≈⟨ refl⟩∘⟨ (pullˡ (commutes (! (algebras Z)))) ⟩ - -- out⁻¹ Z ∘ ((idC +₁ (f (! (algebras Z)))) ∘ F-Coalgebra.α (alg (extend h ∘ g))) ∘ i₁ ≈⟨ refl⟩∘⟨ (pullʳ inject₁) ⟩ - -- out⁻¹ Z ∘ (idC +₁ (f (! (algebras Z)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ pullˡ ∘[] ⟩ - -- out⁻¹ Z ∘ [ (idC +₁ (f (! (algebras Z)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , (idC +₁ (f (! (algebras Z)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ [ (idC +₁ (f (! (algebras Z)))) ∘ i₁ , (idC +₁ (f (! (algebras Z)))) ∘ i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ out Z ∘ extend h ∘ g - -- , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ - -- ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (refl⟩∘⟨ (pullˡ (pullˡ (commutes (! (algebras Z)))))) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ (((idC +₁ f (! (algebras Z))) ∘ F-Coalgebra.α (alg h)) ∘ i₁) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (refl⟩∘⟨ ((pullʳ inject₁) ⟩∘⟨refl)) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ ((idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ (pullˡ []∘+₁)) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ ([ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ ([ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y)) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((pullˡ ∘[]) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ ([ [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₂ ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((([]-cong₂ (pullˡ ∘[]) (pullˡ inject₂)) ⟩∘⟨refl) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ ([ [ [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₁ , [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₂ ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((([]-cong₂ (([]-cong₂ inject₁ (pullˡ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ ([ [ i₁ ∘ idC , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₁ ] ∘ out Y) ∘ g - -- , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ - -- ] ∘ out X ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈˘⟨ {! _○_ !} ⟩ - -- {! !} ≈˘⟨ {! !} ⟩ - -- {! !} ≈˘⟨ {! !} ⟩ - -- out⁻¹ Z ∘ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₂ ] ∘ out Y ∘ g - -- , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₁ - -- ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ inject₁ (pullˡ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₁ , [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₂ ∘ i₂ ] ∘ out Y ∘ g - -- , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ ∘[]) (pullˡ inject₂)) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g - -- , [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ - -- out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ [ (idC +₁ f (! (algebras Z))) ∘ i₁ , (idC +₁ f (! (algebras Z))) ∘ i₂ ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ ((refl⟩∘⟨ identityʳ) ○ (pullˡ ∘[])) (pullˡ (pullˡ +₁∘i₂))) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ (idC +₁ f (! (algebras Z))) ∘ ([ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h) ∘ idC , (idC +₁ f (! (algebras Z))) ∘ (i₂ ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ - -- out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ ([ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h) ∘ idC , (i₂ ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (pullˡ []∘+₁)) ⟩ - -- out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] - -- ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ identityˡ)) ⟩ - -- out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ idC - -- ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ pullʳ (pullʳ (pullʳ (pullˡ (_≅_.isoʳ (out-≅ Y))))) ⟩ - -- (out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y) - -- ∘ (out⁻¹ Y ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X) ≈˘⟨ (refl⟩∘⟨ (pullʳ inject₁)) ⟩∘⟨ (refl⟩∘⟨ (pullʳ inject₁)) ⟩ - -- (out⁻¹ Z ∘ ((idC +₁ (f (! (algebras Z)))) ∘ F-Coalgebra.α (alg h)) ∘ i₁) ∘ (out⁻¹ Y ∘ ((idC +₁ (f (! (algebras Y)))) ∘ F-Coalgebra.α (alg g)) ∘ i₁) ≈˘⟨ (refl⟩∘⟨ (pullˡ (commutes (! (algebras Z))))) ⟩∘⟨ refl⟩∘⟨ (pullˡ (commutes (! (algebras Y)))) ⟩ - -- (out⁻¹ Z ∘ out Z ∘ extend h) ∘ (out⁻¹ Y ∘ out Y ∘ extend g) ≈˘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Z)))) ⟩∘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Y)))) ⟩ - -- extend h ∘ extend g ∎ - - - -- begin - -- extend (extend h ∘ g) ≈⟨ (insertˡ (_≅_.isoˡ (out-≅ Z))) ⟩ - -- out⁻¹ Z ∘ out Z ∘ extend (extend h ∘ g) ≈⟨ refl⟩∘⟨ extendlaw (extend h ∘ g) ⟩ - -- out⁻¹ Z ∘ [ out Z ∘ extend h ∘ g , i₂ ∘ extend (extend h ∘ g) ] ∘ out X ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈˘⟨ {! !} ⟩ - -- {! !} ≈˘⟨ {! !} ⟩ - -- out⁻¹ Z ∘ [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ refl (pullˡ inject₂)) ⟩∘⟨refl) ⟩ - -- out⁻¹ Z ∘ [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g , [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ - -- out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ identityˡ) ⟩ - -- out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ idC ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ pullʳ (pullʳ (pullˡ (_≅_.isoʳ (out-≅ Y)))) ⟩ - -- (out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ out⁻¹ Y ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ (refl⟩∘⟨ extendlaw h) ⟩∘⟨ (refl⟩∘⟨ extendlaw g) ⟩ - -- (out⁻¹ Z ∘ out Z ∘ extend h) ∘ (out⁻¹ Y ∘ out Y ∘ extend g) ≈˘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Z)))) ⟩∘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Y)))) ⟩ - -- extend h ∘ extend g ∎ - - - --begin - -- f (! (algebras Z) {A = alg (extend h ∘ g)}) ∘ i₁ {A = D₀ X} {B = D₀ Z} ≈⟨ (!-unique (algebras Z) (record { f = {! (f (! (algebras Z) {A = alg h}) ∘ i₁) ∘ f (! (algebras Y) {A = alg g}) !} ; commutes = {! !} })) ⟩∘⟨refl ⟩ - -- {! !} ∘ i₁ ≈⟨ {! !} ⟩ - -- (f (! (algebras Z) {A = alg h}) ∘ i₁) ∘ f (! (algebras Y) {A = alg g}) ∘ i₁ ∎ - ; sym-assoc = λ {X} {Y} {Z} {g} {h} → {! !} - ; extend-≈ = λ {X} {Y} {f} {g} eq → begin - F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (Terminal.!-unique (algebras Y) (record { f = (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ; commutes = begin - F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ - F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ≈⟨ F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y)) ⟩ - Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y))) ∘ F-Coalgebra.α (alg g) ≈˘⟨ (Functor.F-resp-≈ (delayF Y) identityʳ) ⟩∘⟨ (αf≈αg eq) ⟩ - Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC) ∘ F-Coalgebra.α (alg f) ∎ })) ⟩∘⟨refl ⟩ - (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩ - extend g ∎ + ; identityʳ = identityʳ' + ; identityˡ = identityˡ' + ; assoc = assoc' + ; sym-assoc = sym assoc' + ; extend-≈ = extend-≈' }) where open Terminal - alg' : ∀ {X Y} → F-Coalgebra (delayF Y) - alg' {X} {Y} = record { A = D₀ X ; α = i₂ } module _ {X Y : Obj} (f : X ⇒ D₀ Y) where - -- open Terminal (algebras Y) using (!; ⊤-id) alg : F-Coalgebra (delayF Y) - alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] } -- (idC +₁ (idC +₁ [ idC , idC ]) ∘ _≅_.to +-assoc ∘ _≅_.to +-comm) + alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] } + extend : D₀ X ⇒ D₀ Y - extend = F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} - !∘i₂ : F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₂ ≈ idC + extend = u (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} + + !∘i₂ : u (! (algebras Y) {A = alg}) ∘ i₂ ≈ idC !∘i₂ = ⊤-id (algebras Y) (F-Coalgebras (delayF Y) [ ! (algebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) + extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X extendlaw = begin - out Y ∘ extend ≈⟨ pullˡ (F-Coalgebra-Morphism.commutes (! (algebras Y) {A = alg})) ⟩ - ((idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ F-Coalgebra.α alg) ∘ coproduct.i₁ ≈⟨ pullʳ inject₁ ⟩ - (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ - [ (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ - [ [ (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ - , (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩ - [ [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) assoc) ⟩∘⟨refl ⟩ - [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ - extend-unique : (g : D₀ X ⇒ D₀ Y) → extend ≈ g - extend-unique g = {! !} - -- begin - -- F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (algebras Y) (record { f = [ g , idC ] ; commutes = begin - -- out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ - -- [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ {! !} identityʳ ⟩ - -- {! !} ≈˘⟨ {! !} ⟩ - -- [ ([ out Y , i₂ ] ∘ (f +₁ g)) ∘ out X , out Y ] ≈˘⟨ []-cong₂ (sym []∘+₁ ⟩∘⟨refl) refl ⟩ - -- [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ {! !} ⟩ - -- [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) refl ⟩ - -- [ [ [ i₁ ∘ idC , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) (pullʳ inject₁)) ⟩∘⟨refl) (elimˡ (Functor.identity (delayF Y))) ⟩ - -- [ [ [ (idC +₁ [ g , idC ]) ∘ i₁ , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out X , (idC +₁ idC) ∘ out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩ - -- [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out X , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out Y ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩ - -- [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ] ≈˘⟨ ∘[] ⟩ - -- (idC +₁ [ g , idC ]) ∘ F-Coalgebra.α alg ∎ })) ⟩∘⟨refl ⟩ - -- [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩ - -- g ∎ - αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → F-Coalgebra.α (alg f) ≈ F-Coalgebra.α (alg g) + out Y ∘ extend ≈⟨ pullˡ (commutes (! (algebras Y) {A = alg})) ⟩ + ((idC +₁ (u (! (algebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ + (idC +₁ (u (! (algebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] + ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ + [ (idC +₁ (u (! (algebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) + , (idC +₁ (u (! (algebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ + [ [ (idC +₁ (u (! (algebras Y)))) ∘ i₁ + , (idC +₁ (u (! (algebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) + , (i₂ ∘ (u (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ + (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) + refl) ⟩∘⟨refl ⟩ + [ [ i₁ ∘ idC , (i₂ ∘ (u (! (algebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) + , (i₂ ∘ (u (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ + (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) + assoc) ⟩∘⟨refl ⟩ + [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ + + extend-unique : (g : D₀ X ⇒ D₀ Y) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g + extend-unique g g-commutes = begin + extend ≈⟨ (!-unique (algebras Y) (record { f = [ g , idC ] ; commutes = begin + out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ + [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩ + [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ + (([]-cong₂ + (([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η)) + refl) + ⟩∘⟨refl) + refl ⟩ + [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) + , i₂ ∘ g ] ∘ out X + , out Y ] ≈˘⟨ []-cong₂ + (([]-cong₂ + (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) + refl) + ⟩∘⟨refl) + refl + ⟩ + [ [ [ i₁ ∘ idC + , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f) + , i₂ ∘ g ] ∘ out X + , out Y ] ≈˘⟨ []-cong₂ + (([]-cong₂ + (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) + (pullʳ inject₁)) + ⟩∘⟨refl) + (elimˡ (Functor.identity (delayF Y))) + ⟩ + [ [ [ (idC +₁ [ g , idC ]) ∘ i₁ + , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) + , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out X + , (idC +₁ idC) ∘ out Y ] ≈˘⟨ []-cong₂ + (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) + ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩ + [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) + , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out X + , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out Y ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩ + [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X + , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ] ≈˘⟨ ∘[] ⟩ + (idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩ + [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩ + g ∎ + + αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → α (alg f) ≈ α (alg g) αf≈αg {X} {Y} {f} {g} eq = []-cong₂ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ eq) refl ⟩∘⟨refl) refl + alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (delayF Y)) (alg f) (alg g) alg-f≈alg-g {X} {Y} {f} {g} eq = record { from = record { f = idC ; commutes = begin - F-Coalgebra.α (alg g) ∘ idC ≈⟨ identityʳ ⟩ - F-Coalgebra.α (alg g) ≈⟨ ⟺ (αf≈αg eq) ⟩ - F-Coalgebra.α (alg f) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ - Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg f) ∎ } + α (alg g) ∘ idC ≈⟨ identityʳ ⟩ + α (alg g) ≈⟨ ⟺ (αf≈αg eq) ⟩ + α (alg f) ≈˘⟨ elimˡ identity ⟩ + (idC +₁ idC) ∘ α (alg f) ∎ } ; to = record { f = idC ; commutes = begin - F-Coalgebra.α (alg f) ∘ idC ≈⟨ identityʳ ⟩ - F-Coalgebra.α (alg f) ≈⟨ αf≈αg eq ⟩ - F-Coalgebra.α (alg g) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ - Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg g) ∎ } + α (alg f) ∘ idC ≈⟨ identityʳ ⟩ + α (alg f) ≈⟨ αf≈αg eq ⟩ + α (alg g) ≈˘⟨ elimˡ identity ⟩ + (idC +₁ idC) ∘ α (alg g) ∎ } ; iso = record { isoˡ = identity² ; isoʳ = identity² } } + where open Functor (delayF Y) using (identity) + + identityʳ' : ∀ {X} {Y} {f} → extend f ∘ now X ≈ f + identityʳ' {X} {Y} {f} = begin + extend f ∘ now X ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩∘⟨refl ⟩ + (out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ + (out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩ + out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ + out⁻¹ Y ∘ out Y ∘ f ≈⟨ cancelˡ (_≅_.isoˡ (out-≅ Y)) ⟩ + f ∎ + + identityˡ' : ∀ {X} → extend (now X) ≈ idC + identityˡ' {X} = Terminal.⊤-id (algebras X) (record { f = extend (now X) ; commutes = begin + out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (algebras X) {A = alg (now X)}))) ⟩ + ((idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ + (idC +₁ (u (! (algebras X) {A = alg (now X)}))) + ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw X) ○ inject₁) refl ⟩∘⟨refl ⟩ + (idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ + [ (idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ i₁ + , (idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩ + [ i₁ ∘ idC , (i₂ ∘ (u (! (algebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩ + [ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ + ([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩ + (idC +₁ extend (now X)) ∘ out X ∎ }) + + assoc' : ∀ {X} {Y} {Z} {g} {h} → 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 Z ∘ extend h ∘ extend g ≈⟨ pullˡ (extendlaw h) ⟩ + ([ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ extend g ≈⟨ pullʳ (extendlaw g) ⟩ + [ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ + [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g + , [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩ + [ (out Z ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩ + [ out Z ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out X ∎) + + extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g + extend-≈' {X} {Y} {f} {g} eq = begin + u (! (algebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (algebras Y) (record { f = (u (! (algebras Y) {A = alg g }) ∘ idC) ; commutes = begin + α (⊤ (algebras Y)) ∘ u (! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ + α (⊤ (algebras Y)) ∘ u (! (algebras Y)) ≈⟨ commutes (! (algebras Y)) ⟩ + (idC +₁ u (! (algebras Y))) ∘ α (alg g) ≈˘⟨ Functor.F-resp-≈ (delayF Y) identityʳ ⟩∘⟨ αf≈αg eq ⟩ + (idC +₁ u (! (algebras Y)) ∘ idC) ∘ α (alg f) ∎ })) + ⟩∘⟨refl ⟩ + (u (! (algebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩ + extend g ∎ ``` ### Definition 30: Search-Algebras