From b6a89dbdc8bd9922bddceeb32b85cde19487d979 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 5 Oct 2023 12:48:06 +0200 Subject: [PATCH] =?UTF-8?q?=E2=9A=A1=EF=B8=8F=20Finished=20many=20helper?= =?UTF-8?q?=20lemmas=20and=20a=20small=20proof?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Monad/Instance/Delay.lagda.md | 3 + src/Monad/Instance/Delay/Quotienting.lagda.md | 88 ++++++++++++++----- 2 files changed, 67 insertions(+), 24 deletions(-) diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index 2cf1bf4..ed83cd5 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -71,6 +71,9 @@ We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inver unitlaw : out ∘ now ≈ i₁ unitlaw = cancelˡ (_≅_.isoʳ out-≅) + + laterlaw : out ∘ later ≈ i₂ + laterlaw = cancelˡ (_≅_.isoʳ out-≅) ``` Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the final coalgebras to get a *coiteration operator* `coit`: diff --git a/src/Monad/Instance/Delay/Quotienting.lagda.md b/src/Monad/Instance/Delay/Quotienting.lagda.md index f9b4b09..e194936 100644 --- a/src/Monad/Instance/Delay/Quotienting.lagda.md +++ b/src/Monad/Instance/Delay/Quotienting.lagda.md @@ -57,7 +57,7 @@ We will now show that the following conditions are equivalent: open DelayM D renaming (functor to D-Functor; monad to D-Monad; kleisli to D-Kleisli) open Functor D-Functor using () renaming (F₁ to D₁; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈; identity to D-identity) - open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ) + open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ) open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ) open HomReasoning open M C @@ -75,28 +75,67 @@ We will now show that the following conditions are equivalent: ρ-epi : ∀ {X} → Epi (ρ {X}) ρ-epi {X} = Coequalizer⇒Epi (coeqs X) - -- TODO this belongs in different module - ▷extend : ∀ {X} {Y} (f : X ⇒ D₀ Y) → ▷ ∘ extend f ≈ extend f ∘ ▷ - ▷extend {X} {Y} f = {! !} - where - helper₁ : [ f , extend (▷ ∘ f) ] ∘ out ≈ extend f - helper₁ = {! !} + -- 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ˡ + + - -- TODO maybe needs that ρ is natural in X ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X} - ρ▷ {X} = begin - ρ ∘ ▷ ≈⟨ coeq-universal {eq = eq'} ⟩ - coequalize eq' ∘ ρ ≈⟨ ({! !} ⟩∘⟨refl) ⟩ - coequalize equality ∘ ρ ≈⟨ elimˡ (sym id-coequalize) ⟩ - ρ ∎ + ρ▷ {X} = sym (begin + ρ ≈⟨ introʳ intro-helper ⟩ + ρ ∘ D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullˡ (sym equality) ⟩ + (ρ ∘ extend ι) ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (sym k-assoc) ⟩ + ρ ∘ extend (extend ι ∘ now ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ (pullˡ k-identityʳ)) ⟩ + ρ ∘ extend (ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ helper) ⟩ + ρ ∘ extend (▷ ∘ now) ≈⟨ (refl⟩∘⟨ sym (▷∘extendʳ now)) ⟩ + ρ ∘ extend now ∘ ▷ ≈⟨ elim-center k-identityˡ ⟩ + ρ ∘ ▷ ∎) where - open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′) - eq' = begin - (ρ ∘ ▷) ∘ extend ι ≈⟨ pullʳ (▷extend ι) ⟩ - ρ ∘ extend ι ∘ ▷ ≈⟨ pullˡ equality ⟩ - (ρ ∘ D₁ π₁) ∘ ▷ ≈⟨ assoc ⟩ - ρ ∘ D₁ π₁ ∘ ▷ ≈⟨ sym (pullʳ (▷extend (now ∘ π₁))) ⟩ - (ρ ∘ ▷) ∘ D₁ π₁ ∎ + open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize; coequalize-resp-≈) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′) + intro-helper : D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ idC + intro-helper = sym D-homomorphism ○ D-resp-≈ project₁ ○ D-identity + helper : ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ ▷ ∘ now + helper = begin + ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ + (out⁻¹ ∘ out) ∘ ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (pullˡ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩ + out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl)) ⟩ + out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₂ ⟩∘⟨refl) ⟩ + out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (_≅_.to nno-iso ∘ i₂) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (cancelˡ (_≅_.isoʳ nno-iso))))) ⟩ + out⁻¹ ∘ (idC +₁ ι) ∘ i₂ ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ pullˡ +₁∘i₂) ⟩ + out⁻¹ ∘ (i₂ ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₁) ⟩ + out⁻¹ ∘ (i₂ ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ intro-center (_≅_.isoˡ out-≅) ⟩∘⟨refl) ⟩ + out⁻¹ ∘ (i₂ ∘ (out⁻¹ ∘ out) ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ pullʳ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩∘⟨refl) ⟩ + out⁻¹ ∘ (i₂ ∘ out⁻¹ ∘ (idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (pullʳ (cancelʳ (_≅_.isoʳ nno-iso)))))) ⟩ + out⁻¹ ∘ i₂ ∘ (out⁻¹ ∘ (idC +₁ ι)) ∘ i₁ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullʳ +₁∘i₁) ⟩ + out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ∘ idC ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ) ⟩ + out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ≈⟨ ((refl⟩∘⟨ sym-assoc) ○ assoc²'') ⟩ + ▷ ∘ now ∎ +-- ⁂ ○ Ď-Functor : Endofunctor C Ď-Functor = record @@ -178,10 +217,11 @@ We will now show that the following conditions are equivalent: ρ ≈⟨ sym identityˡ ⟩ idC ∘ ρ ∎) ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin - (α' ∘ ▷) ∘ D₁ ρ ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ + (α' ∘ ▷) ∘ D₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ + α' ∘ D₁ ρ ∘ ▷ ≈⟨ pullˡ (sym D-universal) ⟩ + (ρ ∘ μ.η X) ∘ ▷ ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩ + ρ ∘ ▷ ∘ extend idC ≈⟨ pullˡ ρ▷ ⟩ + ρ ∘ extend idC ≈⟨ D-universal ⟩ α' ∘ D₁ ρ ∎) } where