diff --git a/agda/src/Algebra/Elgot/Properties.lagda.md b/agda/src/Algebra/Elgot/Properties.lagda.md index 55df6a9..7dda378 100644 --- a/agda/src/Algebra/Elgot/Properties.lagda.md +++ b/agda/src/Algebra/Elgot/Properties.lagda.md @@ -26,10 +26,11 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive : open Category C open HomReasoning open Equiv + open MR C open Distributive distributive open import Categories.Category.Distributive.Properties distributive open Cartesian cartesian - open BinaryProducts products + open BinaryProducts products hiding (η) renaming (unique to ⟨⟩-unique) open Cocartesian cocartesian ccc : CartesianClosed C ccc = record { cartesian = cartesian ; exp = expos } @@ -39,19 +40,43 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive : open import Category.Construction.ElgotAlgebras {C = C} open Cat cocartesian open Exponentials distributive expos + open import Algebra.Elgot cocartesian open import Algebra.Elgot.Free cocartesian open import Algebra.Elgot.Stable distributive open CartesianClosed Elgot-CCC using () renaming (λg to λg#; _^_ to _^#_) + open Elgot-Algebra-Morphism renaming (h to <_>) + stable : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ fe - IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (stable {Y} fe) {X} A f = (eval′ ∘ (Elgot-Algebra-Morphism.h ((fe FreeObject.*) {A = B^A-Helper {A} {X}} (λg f)) ⁂ id)) + IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (stable {Y} fe) {X} A f = (eval′ ∘ (< FreeObject._* fe {B^A-Helper {A} {X}} (λg f) > ⁂ id)) + where open FreeObject fe IsStableFreeElgotAlgebraˡ.♯ˡ-law (stable {Y} fe) {X} {A} f = sym (begin - {! [ stable fe , A ]♯ˡ f ∘ (η fe ⁂ id) !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - f ∎) - IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (stable {Y} fe) {X} {B} f {Z} h = {! !} - IsStableFreeElgotAlgebraˡ.♯ˡ-unique (stable {Y} fe) {X} {B} f g eq₁ eq₂ = {! !} + (eval′ ∘ (< (λg f)* > ⁂ id)) ∘ (η ⁂ id) ≈⟨ pullʳ ⁂∘⁂ ⟩ + eval′ ∘ ((< (λg f)* > ∘ η) ⁂ id ∘ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-lift (λg f)) identity²) ⟩ + eval′ ∘ (λg f ⁂ id) ≈⟨ β′ ⟩ + f ∎) + where open FreeObject fe + IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (stable {Y} fe) {X} {B} f {Z} h = begin + (eval′ ∘ (< (λg f)* > ⁂ id)) ∘ (h #ʸ ⁂ id) ≈⟨ pullʳ ⁂∘⁂ ⟩ + eval′ ∘ (< (λg f)* > ∘ h #ʸ ⁂ id ∘ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (preserves ((λg f)*)) identity²) ⟩ + eval′ ∘ (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((< (λg f)* > +₁ id) ∘ h ⁂ id)) #ᵇ) ⁂ id) ≈⟨ β′ ⟩ + ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((< (λg f)* > +₁ id) ∘ h ⁂ id)) #ᵇ ≈˘⟨ #ᵇ-resp-≈ (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩ + ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((< (λg f)* > +₁ id) ⁂ id) ∘ (h ⁂ id)) #ᵇ ≈⟨ #ᵇ-resp-≈ (refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural id < (λg f) * > id))) ⟩ + ((eval′ +₁ id) ∘ ((< (λg f)* > ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ (h ⁂ id)) #ᵇ ≈⟨ #ᵇ-resp-≈ (refl⟩∘⟨ assoc ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ + ((eval′ ∘ (< (λg f)* > ⁂ id) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∎ + where + open FreeObject fe renaming (FX to KY) + open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈) + open Elgot-Algebra KY using () renaming (_# to _#ʸ) + IsStableFreeElgotAlgebraˡ.♯ˡ-unique (stable {Y} fe) {X} {B} f g eq₁ eq₂ = sym (begin + eval′ ∘ (< (λg f)* > ⁂ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-cong (λ-cong eq₁)) refl) ⟩ + eval′ ∘ (< (λg (g ∘ (η ⁂ id)))* > ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂-cong₂ (*-cong subst) refl) ⟩ + eval′ ∘ (< (λg g ∘ η)* > ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂-cong₂ (*-uniq (λg g ∘ η) (record { h = λg g ; preserves = {! !} }) refl) refl) ⟩ + eval′ ∘ (λg g ⁂ id) ≈⟨ β′ ⟩ + g ∎) + where + open FreeObject fe renaming (FX to KY) + open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈) + open Elgot-Algebra KY using () renaming (_# to _#ʸ) ``` \ No newline at end of file diff --git a/agda/src/Category/Construction/ElgotAlgebras.lagda.md b/agda/src/Category/Construction/ElgotAlgebras.lagda.md index 5f0cff6..95fe405 100644 --- a/agda/src/Category/Construction/ElgotAlgebras.lagda.md +++ b/agda/src/Category/Construction/ElgotAlgebras.lagda.md @@ -314,7 +314,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩ ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎) - <_> = Elgot-Algebra-Morphism.h + open Elgot-Algebra-Morphism renaming (h to <_>) cccc : CanonicalCartesianClosed Elgot-Algebras CanonicalCartesianClosed.⊤ cccc = Terminal.⊤ Terminal-Elgot-Algebras @@ -366,21 +366,60 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher (eval′ +₁ id) ∘ (i₂ ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ pullˡ (pullˡ inject₂) ⟩ ((i₂ ∘ id) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩ i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎ - Elgot-Algebra-Morphism.h (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) = λg < f > - Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin - eval′ ∘ ((λg < f > ∘ (Elgot-Algebra._# A) g) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩ - eval′ ∘ ((λg (< f > ∘ (((Elgot-Algebra._# A) g) ⁂ id))) ⁂ id) ≈⟨ β′ ⟩ - < f > ∘ (((Elgot-Algebra._# A) g) ⁂ id) ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈˘⟨ {! !} ⟩ - {! !} ≈˘⟨ {! !} ⟩ - {! !} ≈˘⟨ {! !} ⟩ - < f > ∘ ⟨ [ id , (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ] ∘ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ] ∘ ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈˘⟨ refl⟩∘⟨ (⟨⟩-cong₂ (Elgot-Algebra.#-Fixpoint A) (Elgot-Algebra.#-Fixpoint B)) ⟩ - < f > ∘ ⟨ (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩ - (Elgot-Algebra._# C) ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ≈˘⟨ {! !} ⟩ - (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩ - (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ - (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) ∎) + < CanonicalCartesianClosed.curry cccc {A} {B} {C} f > = λg < f > + preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin + λg < f > ∘ g #ᵃ ≈⟨ subst ⟩ + λg (< f > ∘ (g #ᵃ ⁂ id)) ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + λg (< f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩) ≈⟨ λ-cong (preserves f) ⟩ + λg (((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ) ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ) ∎ + where + open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity) + open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈) + -- Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin + -- eval′ ∘ ((λg < f > ∘ g #ᵃ) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩ + -- eval′ ∘ ((λg (< f > ∘ (g #ᵃ ⁂ id))) ⁂ id) ≈⟨ β′ ⟩ + -- < f > ∘ (g #ᵃ ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique by-π₁ by-π₂) ⟩ + -- < f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩ + -- ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ ≈˘⟨ #ᶜ-resp-≈ (refl⟩∘⟨ assoc ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ + -- ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) #ᶜ ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩ + -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) #ᶜ ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ + -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ ∎) + -- where + -- open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity) + -- open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + -- open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈) + -- by-π₁ : π₁ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ g #ᵃ ∘ π₁ + -- by-π₁ = project₁ ○ #ᵃ-Uniformity by-uni + -- where + -- by-uni : (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈ g ∘ π₁ + -- by-uni = begin + -- (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ + -- (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ distributeʳ⁻¹-π₁ ⟩ + -- π₁ ∘ (g ⁂ id) ≈⟨ project₁ ⟩ + -- g ∘ π₁ ∎ + -- by-π₂ : π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ id ∘ π₂ + -- by-π₂ = begin + -- π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ project₂ ⟩ + -- ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ≈⟨ #ᵇ-Uniformity by-uni ⟩ + -- {! !} #ᵇ ∘ π₂ ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- id ∘ π₂ ∎ + -- where + -- by-uni : (id +₁ π₂) ∘ (π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)) ≈ {! !} ∘ π₂ + -- by-uni = begin + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ∎ CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = β′ CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = λ-unique′ eq