From 22306ddb27f218c80b9599c7f17a286f3ad7167d Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Wed, 4 Oct 2023 22:44:48 +0200 Subject: [PATCH] =?UTF-8?q?=E2=9A=A1=EF=B8=8F=20Proof=20that=20quotiented?= =?UTF-8?q?=20D=20is=20a=20functor?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Search.lagda.md | 12 +- src/Monad/Instance/Delay/Quotienting.lagda.md | 129 ++++++++++++++++-- 2 files changed, 130 insertions(+), 11 deletions(-) diff --git a/src/Algebra/Search.lagda.md b/src/Algebra/Search.lagda.md index 9bb28bc..9bbca48 100644 --- a/src/Algebra/Search.lagda.md +++ b/src/Algebra/Search.lagda.md @@ -21,9 +21,17 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where module _ (D : DelayM) where open DelayM D - record IsSearchAlgebra (algebra : F-Algebra functor) : Set e where - open F-Algebra algebra using (A; α) + record Search-Algebra-on (A : Obj) : Set (ℓ ⊔ e) where + field + α : F-Algebra-on functor A + field identity₁ : α ∘ now ≈ idC identity₂ : α ∘ ▷ ≈ α + + record Search-Algebra : Set (o ⊔ ℓ ⊔ e) where + field + A : Obj + search-algebra-on : Search-Algebra-on A + open Search-Algebra-on search-algebra-on public ``` \ 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 8c9c5dd..2d4049d 100644 --- a/src/Monad/Instance/Delay/Quotienting.lagda.md +++ b/src/Monad/Instance/Delay/Quotienting.lagda.md @@ -5,8 +5,13 @@ open import Level open import Categories.Functor open import Category.Instance.AmbientCategory using (Ambient) +open import Categories.Monad open import Categories.Monad.Construction.Kleisli open import Categories.Monad.Relative renaming (Monad to RMonad) +open import Data.Product using (_,_; Σ; Σ-syntax) +open import Categories.Functor.Algebra +open import Categories.Functor.Coalgebra +open import Categories.Object.Terminal ``` --> @@ -15,6 +20,8 @@ module Monad.Instance.Delay.Quotienting {o ℓ e} (ambient : Ambient o ℓ e) wh open Ambient ambient open import Categories.Diagram.Coequalizer C open import Monad.Instance.Delay ambient + open import Algebra.Search ambient + open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes) ``` @@ -34,7 +41,7 @@ Existence of the coequalizer doesn't suffice, we will need some conditions havin ```agda preserves : ∀ {X Y} {f g : X ⇒ Y} → Endofunctor C → Coequalizer f g → Set (o ⊔ ℓ ⊔ e) - preserves {X} {Y} {f} {g} F coeq = Coequalizer (Functor.₁ F f) (Functor.₁ F g) + preserves {X} {Y} {f} {g} F coeq = IsCoequalizer (Functor.₁ F f) (Functor.₁ F g) (Functor.₁ F (Coequalizer.arr coeq)) ``` We will now show that the following conditions are equivalent: @@ -46,28 +53,132 @@ We will now show that the following conditions are equivalent: ```agda module _ (D : DelayM) where - open DelayM D renaming (functor to D-Fun; monad to D-Monad; kleisli to D-Kleisli) + open DelayM D renaming (functor to D-Functor; monad to D-Monad; kleisli to D-Kleisli) - open Functor D-Fun using () renaming (F₁ to D₁) - open RMonad 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 Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ) + open HomReasoning + open M C + open MR C + open Equiv module _ (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where Ď₀ : Obj → Obj Ď₀ X = Coequalizer.obj (coeqs X) + ρ : ∀ {X} → D₀ X ⇒ Ď₀ X + ρ {X} = Coequalizer.arr (coeqs X) + + ρ-epi : ∀ {X} → Epi (ρ {X}) + ρ-epi {X} = Coequalizer⇒Epi (coeqs X) + + -- TODO maybe needs that ρ is natural in X + ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X} + ρ▷ {X} = sym {! coeq-universal !} + where + open Coequalizer (coeqs X) using () renaming (universal to coeq-universal) + + Ď-Functor : Endofunctor C + Ď-Functor = record + { F₀ = Ď₀ + ; F₁ = F₁' + ; identity = λ {X} → Coequalizer.coequalize-resp-≈ (coeqs X) (elimʳ D-identity) ○ sym (Coequalizer.id-coequalize (coeqs X)) + ; homomorphism = λ {X} {Y} {Z} {f} {g} → sym (Coequalizer.unique (coeqs X) (sym (begin + (F₁' g ∘ F₁' f) ∘ ρ ≈⟨ pullʳ (sym (Coequalizer.universal (coeqs X))) ⟩ + F₁' g ∘ ρ ∘ D₁ f ≈⟨ pullˡ (sym (Coequalizer.universal (coeqs Y))) ⟩ + (ρ ∘ D₁ g) ∘ D₁ f ≈⟨ pullʳ (sym D-homomorphism) ⟩ + ρ ∘ D₁ (g ∘ f) ∎))) + ; F-resp-≈ = λ {X} {Y} {f} {g} eq → Coequalizer.coequalize-resp-≈ (coeqs X) (refl⟩∘⟨ (D-resp-≈ eq)) + } + where + F₁' : ∀ {X} {Y} (f : X ⇒ Y) → Ď₀ X ⇒ Ď₀ Y + F₁' {X} {Y} f = coequalize {h = ρ ∘ D₁ f} (begin + (ρ ∘ D₁ f) ∘ extend ι ≈⟨ pullʳ (sym k-assoc) ⟩ + ρ ∘ extend (extend (now ∘ f) ∘ ι) ≈⟨ refl⟩∘⟨ (extend-≈ (sym (Terminal.!-unique (coalgebras Y) (record { f = extend (now ∘ f) ∘ ι ; commutes = begin + out ∘ extend (now ∘ f) ∘ ι ≈⟨ pullˡ (extendlaw (now ∘ f)) ⟩ + ([ out ∘ now ∘ f , i₂ ∘ D₁ f ] ∘ out) ∘ ι ≈⟨ pullʳ (coalg-commutes (Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})) ⟩ + [ out ∘ now ∘ f , i₂ ∘ D₁ f ] ∘ (idC +₁ ι) ∘ _≅_.from nno-iso ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩ + (f +₁ D₁ f) ∘ (idC +₁ ι) ∘ _≅_.from nno-iso ≈⟨ pullˡ +₁∘+₁ ⟩ + (f ∘ idC +₁ D₁ f ∘ ι) ∘ _≅_.from nno-iso ≈⟨ ((+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl) ⟩ + (idC ∘ f +₁ (D₁ f ∘ ι) ∘ idC) ∘ _≅_.from nno-iso ≈⟨ sym (pullˡ +₁∘+₁) ⟩ + (idC +₁ extend (now ∘ f) ∘ ι) ∘ (f +₁ idC) ∘ _≅_.from nno-iso ∎ })))) ⟩ + ρ ∘ extend (u (Terminal.! (coalgebras Y) {A = record { A = X × N ; α = (f +₁ idC) ∘ _≅_.from nno-iso }})) ≈⟨ (refl⟩∘⟨ (extend-≈ (Terminal.!-unique (coalgebras Y) (record { f = ι ∘ (f ⁂ idC) ; commutes = begin + out ∘ ι ∘ (f ⁂ idC) ≈⟨ pullˡ (coalg-commutes (Terminal.! (coalgebras Y) {A = record { A = Y × N ; α = _≅_.from nno-iso }})) ⟩ + ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (f ⁂ idC) ≈⟨ assoc ⟩ + (idC +₁ ι) ∘ _≅_.from nno-iso ∘ (f ⁂ idC) ≈⟨ (refl⟩∘⟨ (introʳ (_≅_.isoˡ nno-iso))) ⟩ + (idC +₁ ι) ∘ (_≅_.from nno-iso ∘ (f ⁂ idC)) ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ , idC ⁂ s ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ pullʳ (pullˡ ∘[])) ⟩ + (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ (f ⁂ idC) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ , (f ⁂ idC) ∘ (idC ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ (([]-cong₂ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ)) ⟩∘⟨refl))) ⟩ + (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ f , z ∘ Terminal.! terminal ⟩ , (f ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ refl (refl⟩∘⟨ Terminal.!-unique terminal (Terminal.! terminal ∘ f))) refl ⟩∘⟨refl) ⟩ + (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ f , z ∘ Terminal.! terminal ∘ f ⟩ , (f ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ assoc) (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ + (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ ∘ f , (idC ⁂ s) ∘ (f ⁂ idC) ] ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ []∘+₁))) ⟩ + (idC +₁ ι) ∘ (_≅_.from nno-iso ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ , idC ⁂ s ]) ∘ (f +₁ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ introˡ (_≅_.isoʳ nno-iso)) ⟩ + (idC +₁ ι) ∘ (f +₁ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩ + (f +₁ ι ∘ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩ + (idC +₁ ι ∘ (f ⁂ idC)) ∘ (f +₁ idC) ∘ _≅_.from nno-iso ∎ })))) ⟩ + ρ ∘ extend (ι ∘ (f ⁂ idC)) ≈⟨ (refl⟩∘⟨ extend-≈ (pushˡ (sym k-identityʳ))) ⟩ + ρ ∘ extend (extend ι ∘ now ∘ (f ⁂ idC)) ≈⟨ pushʳ k-assoc ⟩ + (ρ ∘ extend ι) ∘ D₁ (f ⁂ idC) ≈⟨ pushˡ (Coequalizer.equality (coeqs Y)) ⟩ + ρ ∘ D₁ π₁ ∘ D₁ (f ⁂ idC) ≈⟨ refl⟩∘⟨ sym D-homomorphism ⟩ + ρ ∘ D₁ (π₁ ∘ (f ⁂ idC)) ≈⟨ (refl⟩∘⟨ (D-resp-≈ project₁)) ⟩ + ρ ∘ D₁ (f ∘ π₁) ≈⟨ pushʳ D-homomorphism ⟩ + (ρ ∘ D₁ f) ∘ D₁ π₁ ∎) + where + open Coequalizer (coeqs X) using (coequalize; equality) renaming (universal to coeq-universal) + cond-1 : Set (o ⊔ ℓ ⊔ e) - cond-1 = ∀ {X} → preserves D-Fun (coeqs X) + cond-1 = ∀ X → preserves D-Functor (coeqs X) cond-2 : Set (o ⊔ ℓ ⊔ e) - cond-2 = {! !} + cond-2 = ∀ X → Σ[ s-alg-on ∈ Search-Algebra-on D (Ď₀ X) ] is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X}) cond-3 : Set (o ⊔ ℓ ⊔ e) cond-3 = {! !} cond-4 : Set (o ⊔ ℓ ⊔ e) cond-4 = {! !} + + 1⇒2 : cond-1 → cond-2 + 1⇒2 c-1 X = s-alg-on , {! !} + where + open Coequalizer (coeqs X) renaming (universal to coeq-universal) + open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique) + s-alg-on : Search-Algebra-on D (Ď₀ X) + s-alg-on = record + { α = α' + ; identity₁ = ρ-epi (α' ∘ now) idC (begin + (α' ∘ now) ∘ ρ ≈⟨ pullʳ (η.commute ρ) ⟩ + α' ∘ D₁ ρ ∘ now ≈⟨ pullˡ (sym D-universal) ⟩ + (ρ ∘ μ.η X) ∘ now ≈⟨ cancelʳ M-identityʳ ⟩ + ρ ≈⟨ sym identityˡ ⟩ + idC ∘ ρ ∎) + ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin + (α' ∘ ▷) ∘ D₁ ρ ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + α' ∘ D₁ ρ ∎) + } + where + μ∘Dι : μ.η X ∘ D₁ ι ≈ extend ι + μ∘Dι = sym k-assoc ○ extend-≈ (cancelˡ k-identityʳ) + eq₁ : D₁ (extend ι) ≈ D₁ (μ.η X) ∘ D₁ (D₁ ι) + eq₁ = sym (begin + D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ sym D-homomorphism ⟩ + D₁ (μ.η X ∘ D₁ ι) ≈⟨ D-resp-≈ μ∘Dι ⟩ + D₁ (extend ι) ∎) + α' = D-coequalize {h = ρ {X} ∘ μ.η X} (begin + (ρ ∘ μ.η X) ∘ D₁ (extend ι) ≈⟨ (refl⟩∘⟨ eq₁) ⟩ + (ρ ∘ μ.η X) ∘ D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ pullʳ (pullˡ M-assoc) ⟩ + ρ ∘ (μ.η X ∘ μ.η (D₀ X)) ∘ D₁ (D₁ ι) ≈⟨ (refl⟩∘⟨ pullʳ (μ.commute ι)) ⟩ + ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N) ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩ + ρ ∘ extend ι ∘ μ.η (X × N) ≈⟨ pullˡ equality ⟩ + (ρ ∘ D₁ π₁) ∘ μ.η (X × N) ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩ + (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁) ∎) + ▷extend : ∀ {X} {Y} (f : X ⇒ D₀ Y) → ▷ ∘ extend f ≈ extend f ∘ ▷ + ▷extend {X} {Y} f = {! !} + where + helper₁ : [ f , extend (▷ ∘ f) ] ∘ out ≈ extend f + helper₁ = {! !} ``` \ No newline at end of file