leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

🎉 Finished proof that delay is a monad

Browse source
This commit is contained in:
Leon Vatthauer 2023-09-11 19:52:11 +02:00
parent 6978b3098b
commit 58bab7cbf4
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 133 additions and 144 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

275
src/Monad/Instance/Delay.lagda.md
View file

@ -54,7 +54,8 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
open Equiv open Equiv
open HomReasoning open HomReasoning
open CoLambek 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*** ### *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 : DX ⇒ DX
later = out⁻¹ ∘ i₂ later = out⁻¹ ∘ i₂
-- TODO inline
unitlaw : out ∘ now ≈ i₁ unitlaw : out ∘ now ≈ i₁
unitlaw = cancelˡ (_≅_.isoʳ out-≅) unitlaw = cancelˡ (_≅_.isoʳ out-≅)
module _ {Y : Obj} where module _ {Y : Obj} where
coit : Y ⇒ X + Y → Y ⇒ DX 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 : 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 module _ (ℕ : ParametrizedNNO) where
open ParametrizedNNO ℕ 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 }) iso = Lambek.lambek (record { ⊥ = PNNO-Algebra CC coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ CC coproducts ℕ X })
ι : X × N ⇒ DX ι : X × N ⇒ DX
ι = f (! {A = record { A = X × N ; α = _≅_.from iso }}) ι = u (! {A = record { A = X × N ; α = _≅_.from iso }})
monad : Monad C monad : Monad C
@ -118,164 +118,153 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
{ F₀ = D₀ { F₀ = D₀
; unit = λ {X} → now X ; unit = λ {X} → now X
; extend = extend ; extend = extend
; identityʳ = λ {X} {Y} {f} → begin ; identityʳ = identityʳ'
extend f ∘ now X ≈⟨ (insertˡ (_≅_.isoˡ (out-≅ Y))) ⟩∘⟨refl ⟩ ; identityˡ = identityˡ'
(out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ ; assoc = assoc'
(out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩ ; sym-assoc = sym assoc'
out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ ; extend-≈ = extend-≈'
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 ∎
}) })
where where
open Terminal 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 module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
-- open Terminal (algebras Y) using (!; ⊤-id)
alg : F-Coalgebra (delayF Y) 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 : D₀ X ⇒ D₀ Y
extend = F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} extend = u (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
!∘i₂ : F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₂ ≈ idC
!∘i₂ : u (! (algebras Y) {A = alg}) ∘ i₂ ≈ idC
!∘i₂ = ⊤-id (algebras Y) (F-Coalgebras (delayF Y) [ ! (algebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) !∘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 : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X
extendlaw = begin extendlaw = begin
out Y ∘ extend ≈⟨ pullˡ (F-Coalgebra-Morphism.commutes (! (algebras Y) {A = alg})) ⟩ out Y ∘ extend ≈⟨ pullˡ (commutes (! (algebras Y) {A = alg})) ⟩
((idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ F-Coalgebra.α alg) ∘ coproduct.i₁ ≈⟨ pullʳ inject₁ ⟩ ((idC +₁ (u (! (algebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
(idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ (idC +₁ (u (! (algebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ]
[ (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
, (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ [ (idC +₁ (u (! (algebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f)
[ [ (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ , (idC +₁ (u (! (algebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
, (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) [ [ (idC +₁ (u (! (algebras Y)))) ∘ i₁
, (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩ , (idC +₁ (u (! (algebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f)
[ [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) , (i₂ ∘ (u (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂
, (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) assoc) ⟩∘⟨refl ⟩ (([]-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 ∎ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎
extend-unique : (g : D₀ X ⇒ D₀ Y) → extend ≈ g
extend-unique g = {! !} extend-unique : (g : D₀ X ⇒ D₀ Y) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g
-- begin extend-unique g g-commutes = begin
-- F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (algebras Y) (record { f = [ g , idC ] ; commutes = begin extend ≈⟨ (!-unique (algebras Y) (record { f = [ g , idC ] ; commutes = begin
-- out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩
-- [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ {! !} identityʳ ⟩ [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩
-- {! !} ≈˘⟨ {! !} ⟩ [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂
-- [ ([ out Y , i₂ ] ∘ (f +₁ g)) ∘ out X , out Y ] ≈˘⟨ []-cong₂ (sym []∘+₁ ⟩∘⟨refl) refl ⟩ (([]-cong₂
-- [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ {! !} ⟩ (([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η))
-- [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) 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))) ⟩ ⟩∘⟨refl)
-- [ [ [ (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) ⟩ 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ˡ +₁∘+₁) ⟩ [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f)
-- [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ] ≈˘⟨ ∘[] ⟩ , i₂ ∘ g ] ∘ out X
-- (idC +₁ [ g , idC ]) ∘ F-Coalgebra.α alg ∎ })) ⟩∘⟨refl ⟩ , out Y ] ≈˘⟨ []-cong₂
-- [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩ (([]-cong₂
-- g ∎ (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl)
αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → F-Coalgebra.α (alg f) ≈ F-Coalgebra.α (alg g) 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 α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 : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (delayF Y)) (alg f) (alg g)
alg-f≈alg-g {X} {Y} {f} {g} eq = record alg-f≈alg-g {X} {Y} {f} {g} eq = record
{ from = record { f = idC ; commutes = begin { from = record { f = idC ; commutes = begin
F-Coalgebra.α (alg g) ∘ idC ≈⟨ identityʳ ⟩ α (alg g) ∘ idC ≈⟨ identityʳ ⟩
F-Coalgebra.α (alg g) ≈⟨ ⟺ (αf≈αg eq) ⟩ α (alg g) ≈⟨ ⟺ (αf≈αg eq) ⟩
F-Coalgebra.α (alg f) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ α (alg f) ≈˘⟨ elimˡ identity ⟩
Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg f) ∎ } (idC +₁ idC) ∘ α (alg f) ∎ }
; to = record { f = idC ; commutes = begin ; to = record { f = idC ; commutes = begin
F-Coalgebra.α (alg f) ∘ idC ≈⟨ identityʳ ⟩ α (alg f) ∘ idC ≈⟨ identityʳ ⟩
F-Coalgebra.α (alg f) ≈⟨ αf≈αg eq ⟩ α (alg f) ≈⟨ αf≈αg eq ⟩
F-Coalgebra.α (alg g) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ α (alg g) ≈˘⟨ elimˡ identity ⟩
Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg g) ∎ } (idC +₁ idC) ∘ α (alg g) ∎ }
; iso = record ; iso = record
{ isoˡ = identity² { isoˡ = identity²
; 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 ### Definition 30: Search-Algebras