From 11dd7f8f230f3fbfabdf19623753f5578812b2b9 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 28 Jan 2024 15:07:38 +0100 Subject: [PATCH] sync --- agda/src/Algebra/Elgot.lagda.md | 6 ++++-- agda/src/Algebra/Elgot/Free.lagda.md | 6 ++++++ agda/src/Category/Ambient.lagda.md | 2 ++ .../Construction/StrongPreElgotMonads.lagda.md | 2 +- agda/src/Monad/Instance/Setoids/K.lagda.md | 18 +++++++++++++----- 5 files changed, 26 insertions(+), 8 deletions(-) diff --git a/agda/src/Algebra/Elgot.lagda.md b/agda/src/Algebra/Elgot.lagda.md index cbb130f..c8b529d 100644 --- a/agda/src/Algebra/Elgot.lagda.md +++ b/agda/src/Algebra/Elgot.lagda.md @@ -47,8 +47,8 @@ Guarded Elgot algebras are algebras on an endofunctor together with an iteration ``` ## Unguarded Elgot algebras -Unguarded elgot algebras are `Id`-guarded elgot algebras. -Here we give a different Characterization and show that it is equal. +Unguarded elgot algebras are `Id`-guarded elgot algebras where the functor algebra is also trivial. +Here we give a different (easier) Characterization and show that it is equal. ```agda record Elgot-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where @@ -69,6 +69,7 @@ Here we give a different Characterization and show that it is equal. open HomReasoning open Equiv + -- Compositionality is derivable #-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} → (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ @@ -195,6 +196,7 @@ Here we give a different Characterization and show that it is equal. -- every elgot-algebra comes with a divergence constant !ₑ : ⊥ ⇒ A !ₑ = i₂ # + record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where field A : Obj diff --git a/agda/src/Algebra/Elgot/Free.lagda.md b/agda/src/Algebra/Elgot/Free.lagda.md index 586fac2..208d350 100644 --- a/agda/src/Algebra/Elgot/Free.lagda.md +++ b/agda/src/Algebra/Elgot/Free.lagda.md @@ -122,3 +122,9 @@ Stable free Elgot algebras have an additional universal iteration preserving mor open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public ``` + +In a cartesian closed category stability is derivable + +```agda + -- TODO +``` diff --git a/agda/src/Category/Ambient.lagda.md b/agda/src/Category/Ambient.lagda.md index f049811..253b86d 100644 --- a/agda/src/Category/Ambient.lagda.md +++ b/agda/src/Category/Ambient.lagda.md @@ -52,6 +52,8 @@ module Category.Ambient where open Extensive extensive public open Cocartesian cocartesian renaming (+-unique to []-unique) public open Cartesian cartesian public + + -- some helpers monoidal : Monoidal C monoidal = CartesianMonoidal.monoidal cartesian diff --git a/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md b/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md index 2c5ddf4..0ce0a39 100644 --- a/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md +++ b/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md @@ -14,7 +14,7 @@ open import Data.Product using (_,_) ``` --> -# The (functor) category of pre-Elgot monads. +# The (functor) category of strong pre-Elgot monads. ```agda module Category.Construction.StrongPreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md index bbaa1cc..6591004 100644 --- a/agda/src/Monad/Instance/Setoids/K.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K.lagda.md @@ -154,11 +154,11 @@ module Monad.Instance.Setoids.K {ℓ : Level} where delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra delay-algebras A = record { A = Delayₛ A ; algebra = delay-algebras-on {A}} - open Elgot-Algebra using () renaming (A to ⟦_⟧) + open Elgot-Algebra using (#-Fixpoint; #-Uniformity) renaming (A to ⟦_⟧) delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B - delay-lift {A} {B} f = record { h = record { to = < helper # > ; cong = helper#≈-cong } ; preserves = {! !} } + delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → ? } where open Elgot-Algebra B using (_#) -- (f + id) ∘ out @@ -265,6 +265,14 @@ module Monad.Instance.Setoids.K {ℓ : Level} where eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)] eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} {! !} -- eq (∼-refl (A ×ₛ ℕ-setoid)) + delay-lift' = record { to = < helper # > ; cong = helper#≈-cong } + + preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (< helper # > (iter {A} {X} < g > x)) ≡ < ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # > x ] + preserves' {X} {g} {x} = ≡-sym ⟦ B ⟧ (#-Uniformity B {! λ {x} → by-uni {x} !}) -- #-Uniformity B {! !} + where + by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ < [ inj₁ₛ ∘ delay-lift' , inj₂ₛ ∘ iterₛ {A} {X} g ]ₛ ∘ g > x ≡ (helper₁ ∘′ iter {A} {X} < g >) x ] + by-uni = {! !} + <<_>> = Elgot-Algebra-Morphism.h freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A @@ -276,9 +284,9 @@ module Monad.Instance.Setoids.K {ℓ : Level} where ; *-uniq = λ {B} f g eq {x} → *-uniq' {B} f g eq {x} } where - *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift f >>) ⟨$⟩ x) - *-uniq' {B} f g eq {now x} = {! !} -- ≡-trans ⟦ B ⟧ (eq {x} {y} (now-inj x≡y)) (≡-refl ⟦ B ⟧) - *-uniq' {B} f g eq {later x} = {! !} + *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift {A} {B} f >>) ⟨$⟩ x) + *-uniq' {B} f g eq {now x} = ≡-trans ⟦ B ⟧ (eq {x}) (≡-sym ⟦ B ⟧ (#-Fixpoint B)) + *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! !} (≡-sym ⟦ B ⟧ (#-Fixpoint B))