From c166f40576f0d77e6c640859afdfabe297c74da9 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 12 Oct 2023 18:11:28 +0200 Subject: [PATCH] =?UTF-8?q?=F0=9F=9A=A7=20Small=20progress,=20stuck=20on?= =?UTF-8?q?=20multiple=20fronts?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Properties.lagda.md | 124 +++++++++++++++++ src/Algebra/Search.lagda.md | 9 ++ src/Misc/FreeObject.lagda.md | 56 ++++++++ src/Monad/Instance/Delay.lagda.md | 6 + src/Monad/Instance/Delay/Properties.lagda.md | 127 ++++++++++++++++++ src/Monad/Instance/Delay/Quotienting.lagda.md | 58 +------- src/Monad/Instance/K.lagda.md | 30 +++-- 7 files changed, 349 insertions(+), 61 deletions(-) create mode 100644 src/Misc/FreeObject.lagda.md create mode 100644 src/Monad/Instance/Delay/Properties.lagda.md diff --git a/src/Algebra/Properties.lagda.md b/src/Algebra/Properties.lagda.md index a671248..68beb07 100644 --- a/src/Algebra/Properties.lagda.md +++ b/src/Algebra/Properties.lagda.md @@ -5,6 +5,11 @@ open import Level open import Category.Instance.AmbientCategory using (Ambient) open import Categories.FreeObjects.Free open import Categories.Functor.Core +open import Categories.Functor.Algebra +open import Categories.Functor.Coalgebra +open import Categories.Object.Terminal +open import Categories.Category.Construction.EilenbergMoore +open import Categories.Monad.Relative renaming (Monad to RMonad) ``` --> @@ -15,8 +20,14 @@ module Algebra.Properties {o ℓ e} (ambient : Ambient o ℓ e) where open import Algebra.UniformIterationAlgebra ambient open import Category.Construction.ElgotAlgebras ambient open import Category.Construction.UniformIterationAlgebras ambient + open import Algebra.Search ambient + open import Monad.Instance.Delay ambient + open import Categories.Morphism.Properties C open Equiv + open HomReasoning + open MR C + open M C ``` # Properties of algebras @@ -144,3 +155,116 @@ This file contains some typedefs and records concerning different algebras. where open Functor elgot-to-uniformF open Functor (FO⇒Functor elgotForgetfulF free-elgots) using () renaming (F₀ to FO₀; F₁ to FO₁) + + + +## **D**-Algebra + Search-Algebra ⇒ Elgot algebra +```agda + Search⇒Uniform : (D : DelayM) → Search-Algebra D → Uniform-Iteration-Algebra + Search⇒Uniform D S = record + { A = A + ; algebra = record + { _# = λ {X} f → α ∘ coit f + ; #-Fixpoint = λ {X} {f} → begin + α ∘ coit f ≈⟨ intro-center (_≅_.isoˡ out-≅) ⟩ + α ∘ (out⁻¹ ∘ out) ∘ coit f ≈⟨ (refl⟩∘⟨ ((sym +-g-η) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + α ∘ ([ now , later ] ∘ out) ∘ coit f ≈⟨ pullˡ (pullˡ ∘[]) ⟩ + ([ α ∘ now , α ∘ later ] ∘ out) ∘ coit f ≈⟨ ([]-cong₂ identity₁ identity₂ ⟩∘⟨refl ⟩∘⟨refl) ⟩ + ([ idC , α ] ∘ out) ∘ coit f ≈⟨ pullʳ (coit-commutes f) ⟩ + [ idC , α ] ∘ (idC +₁ coit f) ∘ f ≈⟨ pullˡ []∘+₁ ⟩ + [ idC ∘ idC , α ∘ coit f ] ∘ f ≈⟨ (([]-cong₂ identity² refl) ⟩∘⟨refl) ⟩ + [ idC , α ∘ coit f ] ∘ f ∎ + ; #-Uniformity = λ {X} {Y} {f} {g} {h} eq → begin + α ∘ coit f ≈⟨ sym (pullʳ (sym (Terminal.!-unique (coalgebras A) (record { f = coit g ∘ h ; commutes = begin + out ∘ coit g ∘ h ≈⟨ pullˡ (coit-commutes g) ⟩ + ((idC +₁ coit g) ∘ g) ∘ h ≈⟨ pullʳ (sym eq) ⟩ + (idC +₁ coit g) ∘ (idC +₁ h) ∘ f ≈⟨ pullˡ +₁∘+₁ ⟩ + (idC ∘ idC +₁ coit g ∘ h) ∘ f ≈⟨ ((+₁-cong₂ identity² refl) ⟩∘⟨refl) ⟩ + (idC +₁ coit g ∘ h) ∘ f ∎ })))) ⟩ + (α ∘ coit g) ∘ h ∎ + ; #-resp-≈ = λ {X} {f} {g} eq → refl⟩∘⟨ coit-resp-≈ eq + } + } + where + open Search-Algebra S + open DelayM D + + -- TODO use IsElgot + D-Algebra+Search⇒Elgot : (D : DelayM) → (mod : Module (DelayM.monad D)) → IsSearchAlgebra D (Module.action mod) → Elgot-Algebra + D-Algebra+Search⇒Elgot D mod search = record { A = A ; algebra = record + { _# = _# + ; #-Fixpoint = #-Fixpoint + ; #-Uniformity = #-Uniformity + ; #-Folding = #-Folding' + ; #-resp-≈ = #-resp-≈ + } } + where + open Module mod using (A) renaming (action to α; commute to D-commute) + open DelayM D + open IsSearchAlgebra search using () + open Uniform-Iteration-Algebra (Search⇒Uniform D (IsSearchAlgebra⇒Search-Algebra D α search)) using (_#; #-Fixpoint; #-Uniformity; #-resp-≈) + #-Folding' : ∀ {X Y : Obj} {f : X ⇒ A + X} {h : Y ⇒ X + Y} → α ∘ DelayM.coit D (α ∘ DelayM.coit D f +₁ h) ≈ α ∘ DelayM.coit D [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] + #-Folding' {X} {Y} {f} {h} = + begin + α ∘ coit (α ∘ coit f +₁ h) ≈⟨ refl⟩∘⟨ (coit-resp-≈ (sym (+₁∘+₁ ○ +₁-cong₂ refl identityˡ))) ⟩ + α ∘ coit ((α +₁ idC) ∘ (coit f +₁ h)) ≈⟨ refl⟩∘⟨ sym (helper''' (coit f +₁ h) α) ⟩ + α ∘ extend (now ∘ α) ∘ coit (coit f +₁ h) ≈⟨ pullˡ D-commute ⟩ + (α ∘ extend idC) ∘ coit (coit f +₁ h) ≈⟨ pullʳ (sym ([]-unique goal₁ goal₂)) ⟩ + α ∘ [ coit f , coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ ∘[] ⟩ + [ α ∘ coit f , α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ([]-cong₂ (sym #-Fixpoint) refl) ⟩ + [ [ idC , α ∘ coit f ] ∘ f , α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ([]-cong₂ (([]-cong₂ identity² (assoc ○ helper'')) ⟩∘⟨refl) assoc) ⟩ + [ [ idC ∘ idC , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₁ ] ∘ f , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ h ] ≈⟨ sym ([]-cong₂ (pullˡ []∘+₁) (pullˡ inject₂)) ⟩ + [ [ idC , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ] ∘ (idC +₁ i₁) ∘ f , [ idC , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ] ∘ i₂ ∘ h ] ≈⟨ sym ∘[] ⟩ + [ idC , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ≈⟨ sym #-Fixpoint ⟩ + α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∎ + -- refl⟩∘⟨ Terminal.!-unique (coalgebras A) (record { f = coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ; commutes = begin + -- out ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ≈⟨ coit-commutes [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ⟩ + -- (idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ≈⟨ ∘[] ⟩ + -- [ (idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ (idC +₁ i₁) ∘ f , (idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ∘ h ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂) ⟩ + -- [ (idC ∘ idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁) ∘ f , (i₂ ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ h ] ≈⟨ []-cong₂ ((+₁-cong₂ identity² refl) ⟩∘⟨refl) assoc ⟩ + -- [ (idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁) ∘ f , i₂ ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ []-cong₂ helper refl ⟩ + -- (α ∘ coit f +₁ (coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ h) ≈⟨ sym (+₁-cong₂ identityˡ refl) ⟩ + -- (idC ∘ α ∘ coit f +₁ (coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ h) ≈⟨ sym +₁∘+₁ ⟩ + -- (idC +₁ (coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])) ∘ (α ∘ coit f +₁ h) ∎ }) + where + helper'' : α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ ≈ α ∘ coit f + helper'' = sym-assoc ○ sym (#-Uniformity (sym inject₁)) + open RMonad (DelayM.kleisli D) using (extend) + helper''' : ∀ {X B A} (e : X ⇒ B + X) (g : B ⇒ A) → extend (now ∘ g) ∘ coit e ≈ coit ((g +₁ idC) ∘ e) + helper''' {X} {B} {A} e g = sym (Terminal.!-unique (coalgebras A) (record { f = extend (now ∘ g) ∘ coit e ; commutes = begin + out ∘ extend (now ∘ g) ∘ coit e ≈⟨ pullˡ (extendlaw (now ∘ g)) ⟩ + ([ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out) ∘ coit e ≈⟨ pullʳ (coit-commutes e) ⟩ + [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ (idC +₁ coit e) ∘ e ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩ + (g +₁ extend (now ∘ g)) ∘ (idC +₁ coit e) ∘ e ≈⟨ pullˡ +₁∘+₁ ⟩ + (g ∘ idC +₁ extend (now ∘ g) ∘ coit e) ∘ e ≈⟨ (+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl ⟩ + ((idC ∘ g +₁ (extend (now ∘ g) ∘ coit e) ∘ idC)) ∘ e ≈⟨ sym (pullˡ +₁∘+₁) ⟩ + (idC +₁ extend (now ∘ g) ∘ coit e) ∘ (g +₁ idC) ∘ e ∎ })) + goal₁ : (extend idC ∘ coit (coit f +₁ h)) ∘ i₁ ≈ coit f + goal₁ = sym (Terminal.!-unique (coalgebras A) (record { f = (extend idC ∘ coit (coit f +₁ h)) ∘ i₁ ; commutes = begin + out ∘ (extend idC ∘ coit (coit f +₁ h)) ∘ i₁ ≈⟨ pullˡ (pullˡ (extendlaw idC)) ⟩ + (([ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ∘ coit (coit f +₁ h)) ∘ i₁ ≈⟨ (pullʳ (coit-commutes (coit f +₁ h))) ⟩∘⟨refl ⟩ + ([ out ∘ idC , i₂ ∘ extend idC ] ∘ (idC +₁ coit (coit f +₁ h)) ∘ (coit f +₁ h)) ∘ i₁ ≈⟨ (pullˡ []∘+₁) ⟩∘⟨refl ⟩ + ([ (out ∘ idC) ∘ idC , (i₂ ∘ extend idC) ∘ coit (coit f +₁ h) ] ∘ (coit f +₁ h)) ∘ i₁ ≈⟨ pullʳ +₁∘i₁ ⟩ + [ (out ∘ idC) ∘ idC , (i₂ ∘ extend idC) ∘ coit (coit f +₁ h) ] ∘ i₁ ∘ coit f ≈⟨ pullˡ inject₁ ⟩ + ((out ∘ idC) ∘ idC) ∘ coit f ≈⟨ (identityʳ ○ identityʳ) ⟩∘⟨refl ⟩ + out ∘ coit f ≈⟨ coit-commutes f ⟩ + (idC +₁ coit f) ∘ f ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + (idC +₁ (extend idC ∘ coit (coit f +₁ h)) ∘ i₁) ∘ f ∎ })) + goal₂ : (extend idC ∘ coit (coit f +₁ h)) ∘ i₂ ≈ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h + goal₂ = {! !} + +{- +NOTES: +From D-module we get: +1. commute: α ∘ (now ∘ α)* ≈ α ∘ id* +2. identity: α ∘ now ≈ id +From Search: +1. identity₁ : α ∘ now ≈ id +2. identity² α ∘ later ≈ α +From Uniform: +1. Fixpoint: α ∘ coit f ≈ [ idC , α ∘ coit f ] ∘ f +2. Uniformity: α ∘ coit f ≈ (α ∘ coit g) ∘ h iff g ∘ h ≈ (idC +₁ h) ∘ f + +-} +``` diff --git a/src/Algebra/Search.lagda.md b/src/Algebra/Search.lagda.md index 9bbca48..313dbaa 100644 --- a/src/Algebra/Search.lagda.md +++ b/src/Algebra/Search.lagda.md @@ -21,6 +21,11 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where module _ (D : DelayM) where open DelayM D + record IsSearchAlgebra {A : Obj} (α : F-Algebra-on functor A) : Set (ℓ ⊔ e) where + field + identity₁ : α ∘ now ≈ idC + identity₂ : α ∘ ▷ ≈ α + record Search-Algebra-on (A : Obj) : Set (ℓ ⊔ e) where field α : F-Algebra-on functor A @@ -34,4 +39,8 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where A : Obj search-algebra-on : Search-Algebra-on A open Search-Algebra-on search-algebra-on public + + IsSearchAlgebra⇒Search-Algebra : ∀ {A} (α : F-Algebra-on functor A) → IsSearchAlgebra α → Search-Algebra + IsSearchAlgebra⇒Search-Algebra {A} α is = record { A = A ; search-algebra-on = record { α = α ; identity₁ = identity₁ ; identity₂ = identity₂ } } + where open IsSearchAlgebra is ``` \ No newline at end of file diff --git a/src/Misc/FreeObject.lagda.md b/src/Misc/FreeObject.lagda.md new file mode 100644 index 0000000..e981941 --- /dev/null +++ b/src/Misc/FreeObject.lagda.md @@ -0,0 +1,56 @@ + + +```agda +module Misc.FreeObject where +private + variable + o ℓ e o' ℓ' e' : Level +``` + +# Free objects +The notion of free object has been formalized in agda-categories: + +```agda +open import Categories.FreeObjects.Free +``` + +but we need a predicate expressing that an object 'is free': + +```agda +record IsFreeObject {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) : Set (suc (e ⊔ e' ⊔ o ⊔ ℓ ⊔ o' ⊔ ℓ')) where + + private + module C = Category C using (Obj; id; identityʳ; identityˡ; _⇒_; _∘_; equiv; module Equiv) + module D = Category D using (Obj; _⇒_; _∘_; equiv) + module U = Functor U using (₀; ₁) + + field + η : C [ X , U.₀ FX ] + _* : ∀ {A : D.Obj} → C [ X , U.₀ A ] → D [ FX , A ] + *-lift : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) → C [ (U.₁ (f *) C.∘ η) ≈ f ] + *-uniq : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ FX , A ]) → C [ (U.₁ g) C.∘ η ≈ f ] → D [ g ≈ f * ] +``` + +and some way to convert between these notions: + +```agda +IsFreeObject⇒FreeObject : ∀ {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) → IsFreeObject U X FX → FreeObject U X +IsFreeObject⇒FreeObject U X FX isFO = record + { FX = FX + ; η = η + ; _* = _* + ; *-lift = *-lift + ; *-uniq = *-uniq + } + where open IsFreeObject isFO + + -- TODO FreeObject⇒IsFreeObject + +``` + diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index ed83cd5..00d0bc8 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -88,6 +88,12 @@ Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the fina coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f coit-commutes f = commutes (! {A = record { A = Y ; α = f }}) + + coit-resp-≈ : ∀ {f g : Y ⇒ X + Y} → f ≈ g → coit f ≈ coit g + coit-resp-≈ {f} {g} eq = Terminal.!-unique (coalgebras X) (record { f = coit g ; commutes = begin + out ∘ coit g ≈⟨ coit-commutes g ⟩ + (idC +₁ coit g) ∘ g ≈⟨ (refl⟩∘⟨ sym eq) ⟩ + (idC +₁ coit g) ∘ f ∎ }) ``` Furthermore if we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`. diff --git a/src/Monad/Instance/Delay/Properties.lagda.md b/src/Monad/Instance/Delay/Properties.lagda.md new file mode 100644 index 0000000..5c266b1 --- /dev/null +++ b/src/Monad/Instance/Delay/Properties.lagda.md @@ -0,0 +1,127 @@ + + +```agda +module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) where + open Ambient ambient + open import Categories.Diagram.Coequalizer C + open import Monad.Instance.Delay ambient + open import Algebra.Search ambient + open import Algebra.ElgotAlgebra ambient + open import Algebra.Properties ambient + open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes) + open import Monad.Instance.Delay.Quotienting ambient +``` + +# Properties of the quotiented delay monad + +```agda + module _ (D : DelayM) where + 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ʳ; 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 + open Quotiented D coeqs + + cond-1 : Set (o ⊔ ℓ ⊔ e) + cond-1 = ∀ X → preserves D-Functor (coeqs X) + + -- cond-2' : Set (o ⊔ ℓ ⊔ e) + -- 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}) + record cond-2' (X : Obj) : Set (o ⊔ ℓ ⊔ e) where + field + s-alg-on : Search-Algebra-on D (Ď₀ X) + ρ-algebra-morphism : is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X}) + cond-2 = ∀ X → cond-2' X + + + record cond-3' (X : Obj) : Set (suc o ⊔ suc ℓ ⊔ suc e) where + -- Ď₀ X is stable free elgot algebra + field + elgot : Elgot-Algebra-on (Ď₀ X) + elgot-alg = record { A = Ď₀ X ; algebra = elgot } + + open Elgot-Algebra-on elgot + field + isFO : IsFreeObject elgotForgetfulF X elgot-alg + freeobject = IsFreeObject⇒FreeObject elgotForgetfulF X elgot-alg isFO + field + isStable : IsStableFreeElgotAlgebra freeobject + + -- ρ is D-algebra morphism + field + ρ-algebra-morphism : is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = out # }) (ρ {X}) + ρ-law : ρ ≈ ((ρ ∘ now +₁ idC) ∘ out) # + cond-3 = ∀ X → cond-3' X + + record cond-4 : Set (o ⊔ ℓ ⊔ e) where + + 2⇒3 : cond-2 → cond-3 + 2⇒3 c-2 X = record + { elgot = {! !} + ; isFO = {! !} + ; isStable = {! !} + ; ρ-algebra-morphism = {! !} + ; ρ-law = {! !} + } + + 1⇒2 : cond-1 → cond-2 + 1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎ } + 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₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ + α' ∘ D₁ ρ ∘ ▷ ≈⟨ pullˡ (sym D-universal) ⟩ + (ρ ∘ μ.η X) ∘ ▷ ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩ + ρ ∘ ▷ ∘ extend idC ≈⟨ pullˡ ρ▷ ⟩ + ρ ∘ extend idC ≈⟨ D-universal ⟩ + α' ∘ 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₁ π₁) ∎) +``` \ 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 7d6f6bd..d22d956 100644 --- a/src/Monad/Instance/Delay/Quotienting.lagda.md +++ b/src/Monad/Instance/Delay/Quotienting.lagda.md @@ -13,6 +13,7 @@ open import Categories.Functor.Algebra open import Categories.Functor.Coalgebra open import Categories.Object.Terminal open import Categories.NaturalTransformation.Core +open import Misc.FreeObject ``` --> @@ -22,6 +23,8 @@ module Monad.Instance.Delay.Quotienting {o ℓ e} (ambient : Ambient o ℓ e) wh open import Categories.Diagram.Coequalizer C open import Monad.Instance.Delay ambient open import Algebra.Search ambient + open import Algebra.ElgotAlgebra ambient + open import Algebra.Properties ambient open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes) ``` @@ -64,7 +67,7 @@ We will now show that the following conditions are equivalent: open MR C open Equiv - module _ (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where + module Quotiented (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where Ď₀ : Obj → Obj Ď₀ X = Coequalizer.obj (coeqs X) @@ -188,55 +191,4 @@ We will now show that the following conditions are equivalent: { η = λ X → ρ {X} ; commute = λ {X} {Y} f → Coequalizer.universal (coeqs X) }) - - cond-1 : Set (o ⊔ ℓ ⊔ e) - cond-1 = ∀ X → preserves D-Functor (coeqs X) - - cond-2 : Set (o ⊔ ℓ ⊔ e) - 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 , (begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎) - 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₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ - α' ∘ D₁ ρ ∘ ▷ ≈⟨ pullˡ (sym D-universal) ⟩ - (ρ ∘ μ.η X) ∘ ▷ ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩ - ρ ∘ ▷ ∘ extend idC ≈⟨ pullˡ ρ▷ ⟩ - ρ ∘ extend idC ≈⟨ D-universal ⟩ - α' ∘ 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₁ π₁) ∎) -``` \ No newline at end of file +``` diff --git a/src/Monad/Instance/K.lagda.md b/src/Monad/Instance/K.lagda.md index b036de6..29e3206 100644 --- a/src/Monad/Instance/K.lagda.md +++ b/src/Monad/Instance/K.lagda.md @@ -11,6 +11,7 @@ open import Categories.Monad open import Categories.Monad.Strong open import Category.Instance.AmbientCategory using (Ambient) open import Categories.NaturalTransformation +open import Categories.Object.Terminal -- open import Data.Product using (_,_; Σ; Σ-syntax) ``` --> @@ -37,6 +38,7 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra) open Equiv + open HomReasoning ``` @@ -55,9 +57,6 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where K : Monad C K = adjoint⇒monad adjoint - - -- EilenbergMoore⇒UniformIterationAlgebras : StrongEquivalence (EilenbergMoore K) (Uniform-Iteration-Algebras D) - -- EilenbergMoore⇒UniformIterationAlgebras = {! !} ``` ### *Proposition 19* If the algebras are stable then K is strong @@ -78,11 +77,18 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where KStrong = record { M = K ; strength = record - { strengthen = ntHelper (record { η = τ ; commute = λ f → {! !} }) - ; identityˡ = {! !} - ; η-comm = {! !} - ; μ-η-comm = {! !} - ; strength-assoc = {! !} + { strengthen = ntHelper (record { η = τ ; commute = commute' }) + ; identityˡ = λ {X} → begin + K₁ π₂ ∘ τ _ ≈⟨ refl ⟩ + Uniform-Iteration-Algebra-Morphism.h ((algebras (Terminal.⊤ terminal × X) FreeObject.*) (FreeObject.η (algebras X) ∘ π₂)) ∘ τ _ ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + π₂ ∎ + ; η-comm = λ {A} {B} → begin τ _ ∘ (idC ⁂ η (A , B) B) ≈⟨ τ-η (A , B) ⟩ η (A , B) (A × B) ∎ + ; μ-η-comm = λ {A} {B} → {! !} + ; strength-assoc = λ {A} {B} {D} → begin + K₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ τ _ ≈⟨ {! !} ⟩ + τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎ } } where @@ -107,4 +113,12 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ [ FreeObject.FX (algebras Y) , h ]#) ≈ [ FreeObject.FX (algebras (X × Y)) , (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ]# τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X , Y) (X × Y)) h + + commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) + → τ P₂ ∘ ((fst fg) ⁂ K₁ (snd fg)) ≈ K₁ ((fst fg) ⁂ (snd fg)) ∘ τ P₁ + commute' {(U , V)} {(W , X)} (f , g) = begin + τ _ ∘ (f ⁂ Uniform-Iteration-Algebra-Morphism.h ((algebras V FreeObject.*) (FreeObject.η (algebras X) ∘ g))) ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + Uniform-Iteration-Algebra-Morphism.h ((algebras (U × V) FreeObject.*) (FreeObject.η (algebras (W × X)) ∘ (f ⁂ g))) ∘ τ _ ∎ ```