diff --git a/agda/src/FreeObject.lagda.md b/agda/src/FreeObject.lagda.md new file mode 100644 index 0000000..78cc414 --- /dev/null +++ b/agda/src/FreeObject.lagda.md @@ -0,0 +1,56 @@ + + +```agda +module 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/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md index 54488e7..a8acf51 100644 --- a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md +++ b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md @@ -11,6 +11,7 @@ open import Codata.Musical.Notation open import Function using (_∘′_) renaming (_∘_ to _∘f_) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_) renaming (sym to ≡-sym) +open import FreeObject ``` --> @@ -21,6 +22,8 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where open import Monad.Instance.K.Instance.Delay {ℓ} {ℓ} open import Category.Ambient.Setoids open import Algebra.Elgot (setoidAmbient {ℓ}) + open import Algebra.Elgot.Free (setoidAmbient {ℓ}) + open import Category.Construction.ElgotAlgebras (setoidAmbient {ℓ}) open import Monad.PreElgot (setoidAmbient {ℓ}) open Equality @@ -65,6 +68,17 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where ... | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy ... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx ... | inj₂ a | inj₂ b = ≈-sym (later-eq (later≈ (♯ iter-cong f (∼-sym X (inj₂-helper f x∼y eqx eqy))))) + + -- iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ] + -- iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y = ≈-trans (helper x) (iter-cong g (cong h x∼y)) + -- where + -- helper : ∀ (x : Setoid.Carrier X) → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ x) ] + -- helper x with f ⟨$⟩ x in eqa | g ⟨$⟩ (h ⟨$⟩ x) in eqb + -- ... | inj₁ a | inj₁ b = {! !} + -- ... | inj₁ a | inj₂ b = {! !} -- absurd + -- ... | inj₂ a | inj₁ b = {! !} -- absurd + -- ... | inj₂ a | inj₂ b rewrite (≡-sym eqb) = {! !} -- later≈ (♯ {! iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {a} {(h ⟨$⟩ a)} !}) -- ≈-trans {_} {{! !}} (later≈ {{! !}} {{! !}} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ helper a)) (later≈ (♯ {! !})) + {-# TERMINATING #-} iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ] iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy @@ -152,8 +166,8 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where helper : (X ⊎ₛ Y) [ inj₂ a ∼ inj₂ b ] helper rewrite (≡-sym eqx) | (≡-sym eqy) = cong h (drop-inj₂ ix∼iy) - delay-algebras : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A) - delay-algebras {A} = record + delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A) + delay-algebras-on {A} = record { _# = λ {X} f → record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = λ {x} {y} x∼y → iter-cong {A} {X} f {x} {y} x∼y } ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f} ; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h} @@ -161,13 +175,25 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where ; #-resp-≈ = λ {X} {f} {g} → iter-resp-≈ {A} {X} f g } - -- kleisli lifting (just for making the code cleaner) - -- TODO - -- TODO, freealgebras approach is probably easier + delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra + delay-algebras A = record { A = delaySetoid A ; algebra = delay-algebras-on {A} } + isFreeAlgebra : ∀ {A : Setoid ℓ ℓ} → IsFreeObject elgotForgetfulF (delaySetoid A) (delay-algebras A) + isFreeAlgebra {A} = record + { η = SΠ.id + ; _* = λ {B} f → record { h = f ; preserves = λ {X} {g} {x} {y} x∼y → *-preserves {B} f {X} {g} {x} {y} x∼y } + ; *-lift = λ {B} f {x} {y} x∼y → cong f x∼y + ; *-uniq = λ {B} f g g≋f {x} {y} x∼y → g≋f x∼y + } + where + -- TODO use fixpoint for this + *-preserves : ∀ {B : Elgot-Algebra} (f : delaySetoid A ⟶ Elgot-Algebra.A B) {X : Setoid ℓ ℓ} {g : X ⟶ (delaySetoid A) ⊎ₛ X} → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → Elgot-Algebra.A B [ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ∼ ((B Elgot-Algebra.#) _) ⟨$⟩ y ] + *-preserves {B} f {X} {g} {x} {y} x∼y = {! !} + + -- TODO remove delayPreElgot : IsPreElgot delayMonad delayPreElgot = record - { elgotalgebras = delay-algebras + { elgotalgebras = delay-algebras-on ; extend-preserves = {! !} }