diff --git a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md index 5129f2c..6e4fe7b 100644 --- a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md +++ b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md @@ -17,7 +17,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Sum.Function.Setoid open import Data.Sum.Relation.Binary.Pointwise open import Data.Unit.Polymorphic using (tt; ⊤) -open import Data.Empty.Polymorphic using (⊥) +-- open import Data.Empty.Polymorphic using (⊥) open import Categories.NaturalTransformation using (ntHelper) open import Function.Base using (id) import Relation.Binary.PropositionalEquality as Eq @@ -37,23 +37,24 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where # Capretta's Delay Monad is an Instance of K in the Category of Setoids ```agda - data Delay (A : Set c) : Set c where - now : A → Delay A - later : ∞ (Delay A) → Delay A + open Setoid using () renaming (Carrier to ∣_∣) + data _⊥ (A : Set c) : Set c where + now : A → A ⊥ + later : ∞ (A ⊥) → A ⊥ module Equality {A : Setoid c (c ⊔ ℓ)} where open Setoid A renaming (Carrier to C; _≈_ to _∼_) open IsEquivalence (Setoid.isEquivalence A) renaming (refl to ∼-refl; sym to ∼-sym; trans to ∼-trans) - data _↓_ : Delay C → C → Set (c ⊔ ℓ) where + data _↓_ : C ⊥ → C → Set (c ⊔ ℓ) where now↓ : ∀ {x y} (x∼y : x ∼ y) → now x ↓ y later↓ : ∀ {x y} (x↓y : ♭ x ↓ y) → later x ↓ y - unique↓ : ∀ {c : Delay C} {x y : C} → c ↓ x → c ↓ y → x ∼ y + unique↓ : ∀ {c : C ⊥} {x y : C} → c ↓ x → c ↓ y → x ∼ y unique↓ (now↓ eq₁) (now↓ eq₂) = ∼-trans (∼-sym eq₁) eq₂ unique↓ (later↓ p) (later↓ q) = unique↓ p q - data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where + data _≈_ : C ⊥ → C ⊥ → Set (c ⊔ ℓ) where ↓≈ : ∀ {x y a b} (a∼b : a ∼ b) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y later≈ : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y @@ -65,11 +66,11 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where ≈-sym (↓≈ a∼b x↓a y↓b) = ↓≈ (∼-sym a∼b) y↓b x↓a ≈-sym (later≈ x≈y) = later≈ (♯ ≈-sym (♭ x≈y)) - ∼↓ : ∀ {x y : C} {z : Delay C} → x ∼ y → z ↓ x → z ↓ y + ∼↓ : ∀ {x y : C} {z : C ⊥} → x ∼ y → z ↓ x → z ↓ y ∼↓ {x} {y} {.(now _)} x∼y (now↓ a∼x) = now↓ (∼-trans a∼x x∼y) ∼↓ {x} {y} {.(later _)} x∼y (later↓ z↓x) = later↓ (∼↓ x∼y z↓x) - ≈↓ : ∀ {x y : Delay C} {z : C} → x ≈ y → x ↓ z → y ↓ z + ≈↓ : ∀ {x y : C ⊥} {z : C} → x ≈ y → x ↓ z → y ↓ z ≈↓ (↓≈ a∼b (now↓ x∼a) y↓b) (now↓ x∼z) = ∼↓ (∼-trans (∼-sym a∼b) (∼-trans (∼-sym x∼a) x∼z)) y↓b ≈↓ (↓≈ a∼b (later↓ x↓a) y↓b) (later↓ x↓z) with unique↓ x↓a x↓z ... | a∼z = ∼↓ (∼-trans (∼-sym a∼b) a∼z) y↓b @@ -82,76 +83,74 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where ≈-trans (later≈ x≈y) (↓≈ a∼b (later↓ y↓a) z↓b) = ↓≈ a∼b (later↓ (≈↓ (≈-sym (♭ x≈y)) y↓a)) z↓b ≈-trans (later≈ x≈y) (later≈ y≈z) = later≈ (♯ ≈-trans (♭ x≈y) (♭ y≈z)) - delaySetoid : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ) - delaySetoid A = record { Carrier = Delay Carrier ; _≈_ = _≈_ ; isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans } } + -- _⊥ₛ + _⊥ₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ) + _⊥ₛ A = record { Carrier = ∣ A ∣ ⊥ ; _≈_ = _≈_ ; isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans } } where - open Setoid A using (Carrier) open Equality {A} open Equality using (↓≈; later≈; now↓; later↓; _↓_; ≈↓; ∼↓; ≈-refl; ≈-sym; ≈-trans) - _[_≈_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : Delay (Setoid.Carrier A)) → Set (c ⊔ ℓ) + _[_≈_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : ∣ A ∣ ⊥) → Set (c ⊔ ℓ) A [ x ≈ y ] = Equality._≈_ {A} x y - _[_∼_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : Setoid.Carrier A) → Set (c ⊔ ℓ) + _[_∼_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : ∣ A ∣) → Set (c ⊔ ℓ) A [ x ∼ y ] = Setoid._≈_ A x y - ∼-refl : ∀ (A : Setoid c (c ⊔ ℓ)) {x : Setoid.Carrier A} → A [ x ∼ x ] + ∼-refl : ∀ (A : Setoid c (c ⊔ ℓ)) {x : ∣ A ∣} → A [ x ∼ x ] ∼-refl A = IsEquivalence.refl (Setoid.isEquivalence A) - ∼-sym : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Setoid.Carrier A} → A [ x ∼ y ] → A [ y ∼ x ] + ∼-sym : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : ∣ A ∣} → A [ x ∼ y ] → A [ y ∼ x ] ∼-sym A = IsEquivalence.sym (Setoid.isEquivalence A) - ∼-trans : ∀ (A : Setoid c (c ⊔ ℓ)) {x y z : Setoid.Carrier A} → A [ x ∼ y ] → A [ y ∼ z ] → A [ x ∼ z ] + ∼-trans : ∀ (A : Setoid c (c ⊔ ℓ)) {x y z : ∣ A ∣} → A [ x ∼ y ] → A [ y ∼ z ] → A [ x ∼ z ] ∼-trans A = IsEquivalence.trans (Setoid.isEquivalence A) - now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ x ∼ y ] → A [ now x ≈ now y ] + now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → A [ x ∼ y ] → A [ now x ≈ now y ] now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (∼-refl A)) (now↓ (∼-refl A)) -- slightly different types than later≈ -- TODO remove this is useless - later-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → A [ later (♯ x) ≈ later (♯ y) ] + later-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → A [ x ≈ y ] → A [ later (♯ x) ≈ later (♯ y) ] later-cong {A} {x} {y} x≈y = later≈ (♯ x≈y) - now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ now x ≈ now y ] → A [ x ∼ y ] + now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → A [ now x ≈ now y ] → A [ x ∼ y ] now-inj {A} {x} {y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b)) - liftF : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier B) + liftF : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → ∣ A ∣ ⊥ → ∣ B ∣ ⊥ liftF f (now x) = now (f ⟨$⟩ x) liftF f (later x) = later (♯ liftF f (♭ x)) - delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → delaySetoid A ⟶ delaySetoid B + delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → A ⊥ₛ ⟶ B ⊥ₛ delayFun {A} {B} f = record { _⟨$⟩_ = liftF f ; cong = cong' } where - ↓-cong : ∀ {x : Delay (Setoid.Carrier A)} {b : Setoid.Carrier A} → _↓_ {A} x b → _↓_ {B} (liftF f x) (f ⟨$⟩ b) + ↓-cong : ∀ {x : ∣ A ∣ ⊥} {b : ∣ A ∣} → _↓_ {A} x b → _↓_ {B} (liftF f x) (f ⟨$⟩ b) ↓-cong {now x} {b} (now↓ x∼y) = now↓ (cong f x∼y) ↓-cong {later x} {b} (later↓ x↓b) = later↓ (↓-cong x↓b) - cong' : ∀ {x y : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → B [ liftF f x ≈ liftF f y ] + cong' : ∀ {x y : ∣ A ∣ ⊥} → A [ x ≈ y ] → B [ liftF f x ≈ liftF f y ] cong' {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = now-cong (cong f (∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b)))) cong' {now x} {later y} (↓≈ a∼b (now↓ x∼a) (later↓ y↓b)) = ↓≈ (cong f (∼-trans A x∼a a∼b)) (now↓ (∼-refl B)) (later↓ (↓-cong y↓b)) cong' {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (cong f (∼-trans A a∼b (∼-sym A y∼b))) (later↓ (↓-cong x↓a)) (now↓ (∼-refl B)) cong' {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ cong' (↓≈ a∼b x↓a y↓b)) cong' {later x} {later y} (later≈ x≈y) = later≈ (♯ cong' (♭ x≈y)) - -- ↓-delay : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) {x : Setoid.Carrier → f ⟨$⟩ x - -- this needs polymorphic universe levels _≋_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ') _≋_ {c'} {ℓ'} {A} {B} f g = Setoid._≈_ (A ⇨ B) f g - later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay (Setoid.Carrier A)} → A [ later (♯ x) ≈ y ] → A [ x ≈ y ] + later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → A [ later (♯ x) ≈ y ] → A [ x ≈ y ] later-eq {A} {x} {y} (↓≈ a∼b (later↓ x↓a) y↓b) = ↓≈ a∼b x↓a y↓b later-eq {A} {now x} {later y} (later≈ x≈y) = ↓≈ (∼-refl A) (now↓ (∼-refl A)) (later↓ (≈↓ (♭ x≈y) (now↓ (∼-refl A)))) later-eq {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ later-eq (≈-trans (later≈ (♯ ≈-refl)) (♭ x≈y))) - later-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Setoid.Carrier A)} → A [ x ≈ later (♯ x) ] + later-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} → A [ x ≈ later (♯ x) ] later-self {A} {now x} = ↓≈ (∼-refl A) (now↓ (∼-refl A)) (later↓ (now↓ (∼-refl A))) later-self {A} {later x} = later-eq (later≈ (♯ ≈-refl)) - delayFun↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : Delay (Setoid.Carrier A)} {y : Setoid.Carrier A} → _↓_ {A} x y → _↓_ {B} (delayFun f ⟨$⟩ x) (f ⟨$⟩ y) + delayFun↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → _↓_ {A} x y → _↓_ {B} (delayFun f ⟨$⟩ x) (f ⟨$⟩ y) delayFun↓ {A} {B} f {now x} {y} (now↓ x∼y) = now↓ (cong f x∼y) delayFun↓ {A} {B} f {later x} {y} (later↓ x↓y) = later↓ (delayFun↓ f x↓y) - delayFun-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (delayFun idₛ) ≋ (idₛ {A = delaySetoid A}) + delayFun-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (delayFun idₛ) ≋ (idₛ {A = A ⊥ₛ}) delayFun-id {A} {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ↓≈ a∼b (now↓ x∼a) (now↓ y∼b) delayFun-id {A} {now x} {later y} x≈y = x≈y delayFun-id {A} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ a∼b (later↓ (delayFun↓ idₛ x↓a)) (now↓ y∼b) @@ -172,30 +171,30 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where delayFun-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ delayFun-resp-≈ f≋g (↓≈ a∼b x↓a y↓b)) delayFun-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (later≈ x≈y) = later≈ (♯ delayFun-resp-≈ f≋g (♭ x≈y)) - η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ delaySetoid A + η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ A ⊥ₛ η A = record { _⟨$⟩_ = now ; cong = id λ x∼y → now-cong x∼y } - η↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ x ∼ y ] → _↓_ {A} ((η A) ⟨$⟩ x) y + η↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → A [ x ∼ y ] → _↓_ {A} ((η A) ⟨$⟩ x) y η↓ {A} {x} {y} x∼y = now↓ x∼y η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (η B ∘ f) ≋ (delayFun f ∘ η A) η-natural {A} {B} f {x} {y} x≈y = now-cong (cong f x≈y) private - μ' : ∀ {A : Setoid c (c ⊔ ℓ)} → Setoid.Carrier (delaySetoid (delaySetoid A)) → Setoid.Carrier (delaySetoid A) + μ' : ∀ {A : Setoid c (c ⊔ ℓ)} → ∣ (A ⊥ₛ) ⊥ₛ ∣ → ∣ (A ⊥ₛ) ∣ μ' {A} (now x) = x μ' {A} (later x) = later (♯ μ' {A} (♭ x)) - μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid A} x y → A [ (μ' {A} x) ≈ y ] + μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → _↓_ {A ⊥ₛ} x y → A [ (μ' {A} x) ≈ y ] μ↓ {A} {now x} {y} (now↓ x≈y) = x≈y μ↓ {A} {later x} {y} (later↓ x↓y) = ≈-trans (later≈ (♯ μ↓ x↓y)) (≈-sym later-self) -- TODO do delayFun and η in the same style as μ - μ : ∀ (A : Setoid c (c ⊔ ℓ)) → delaySetoid (delaySetoid A) ⟶ delaySetoid A + μ : ∀ (A : Setoid c (c ⊔ ℓ)) → (A ⊥ₛ) ⊥ₛ ⟶ A ⊥ₛ μ A = record { _⟨$⟩_ = μ' {A} ; cong = cong' } where - cong' : ∀ {x y : Delay (Delay (Setoid.Carrier A))} → (delaySetoid A) [ x ≈ y ] → A [ μ' {A} x ≈ μ' {A} y ] + cong' : ∀ {x y : (∣ A ∣ ⊥) ⊥} → (A ⊥ₛ) [ x ≈ y ] → A [ μ' {A} x ≈ μ' {A} y ] cong' {x} {now y} (↓≈ a≈b x↓a (now↓ y≈b)) = μ↓ (∼↓ (≈-trans a≈b (≈-sym y≈b)) x↓a) cong' {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = ≈-sym (μ↓ (∼↓ (≈-trans (≈-sym a≈b) (≈-sym x≈a)) (later↓ y↓b))) cong' {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ cong' (↓≈ a≈b x↓a y↓b)) @@ -208,23 +207,23 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where μ-natural {A} {B} f {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-natural f (↓≈ a≈b x↓a y↓b)) μ-natural {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-natural f (♭ x≈y)) - μ-assoc↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid A} x y → A [ (μ A) ⟨$⟩ x ≈ y ] + μ-assoc↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → _↓_ {A ⊥ₛ} x y → A [ (μ A) ⟨$⟩ x ≈ y ] μ-assoc↓ {A} {now x} {y} (now↓ x≈y) = x≈y μ-assoc↓ {A} {later x} {y} (later↓ x↓y) = ≈-sym (later-eq (later≈ (♯ ≈-sym (μ-assoc↓ x↓y)))) -- TODO needs another μ↓-trans for when multiple μ's are concerned, i.e. a chain with 3 conditions... - μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} {z : Setoid.Carrier A} → _↓_ {delaySetoid A} x y → _↓_ {A} y z → _↓_ {A} (μ A ⟨$⟩ x) z + μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} {z : ∣ A ∣} → _↓_ {A ⊥ₛ} x y → _↓_ {A} y z → _↓_ {A} (μ A ⟨$⟩ x) z μ↓-trans {A} {now x} {y} {z} (now↓ x≈y) y↓z = ≈↓ (≈-sym x≈y) y↓z μ↓-trans {A} {later x} {y} {z} (later↓ x↓y) y↓z = later↓ (μ↓-trans x↓y y↓z) - μ↓-trans² : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay (Setoid.Carrier A)))} {y : Delay (Delay (Setoid.Carrier A))} {z : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid (delaySetoid A)} x y → _↓_ {delaySetoid A} y z → _↓_ {delaySetoid A} ((delayFun (μ A)) ⟨$⟩ x) z - μ↓-trans² {A} {now x} {y} {now x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} (μ↓-trans {! !} {! y↓z !}) (now↓ (∼-refl A))) - μ↓-trans² {A} {now x} {y} {later x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} {! !} {! !}) - μ↓-trans² {A} {later x} {y} {z} x↓y y↓z = {! !} + -- μ↓-trans² : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (∣ A ∣ ⊥))} {y : Delay (∣ A ∣ ⊥)} {z : ∣ A ∣ ⊥} → _↓_ {delaySetoid (A ⊥ₛ)} x y → _↓_ {A ⊥ₛ} y z → _↓_ {A ⊥ₛ} ((delayFun (μ A)) ⟨$⟩ x) z + -- μ↓-trans² {A} {now x} {y} {now x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} (μ↓-trans {! !} {! y↓z !}) (now↓ (∼-refl A))) + -- μ↓-trans² {A} {now x} {y} {later x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} {! !} {! !}) + -- μ↓-trans² {A} {later x} {y} {z} x↓y y↓z = {! !} - μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (delaySetoid A)) + μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (A ⊥ₛ)) μ-assoc {A} {now x} {now y} (↓≈ a≈b (now↓ x≈a) (now↓ y≈b)) = cong (μ A) (≈-trans x≈a (≈-trans a≈b (≈-sym y≈b))) μ-assoc {A} {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = later-eq (later≈ (♯ cong (μ A) (≈-sym (μ↓ (∼↓ (≈-sym (≈-trans x≈a a≈b)) y↓b))))) -- y , liftF (μ A) (♭ x) μ-assoc {A} {later x} {now y} (↓≈ {_} {_} {a} {b} (↓≈ c≈d a↓c b↓d) (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ cong (μ A) {y} {liftF (μ A) (♭ x)} (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) {! delayFun↓ (μ A) {♭ x} x↓a !})))) -- (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) (μ↓-trans {! x↓a !} a↓c)) @@ -232,7 +231,7 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where μ-assoc {A} {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-assoc (↓≈ a≈b x↓a y↓b)) μ-assoc {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-assoc (♭ x≈y)) - identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Setoid.Carrier A)} {y : Setoid.Carrier A} → _↓_ {A} x y → _↓_ {A} ((μ A) ⟨$⟩ ((delayFun (η A)) ⟨$⟩ x)) y + identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → _↓_ {A} x y → _↓_ {A} ((μ A) ⟨$⟩ ((delayFun (η A)) ⟨$⟩ x)) y identityˡ↓ {A} {now x} {y} x↓y = x↓y identityˡ↓ {A} {later x} {y} (later↓ x↓y) = later↓ (identityˡ↓ x↓y) @@ -242,14 +241,14 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where identityˡ {A} {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ identityˡ (↓≈ a∼b x↓a y↓b)) identityˡ {A} {later x} {.(later _)} (later≈ x≈y) = later≈ (♯ identityˡ (♭ x≈y)) - identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ η (delaySetoid A)) ≋ idₛ + identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ η (A ⊥ₛ)) ≋ idₛ identityʳ {A} {now x} {y} x≈y = x≈y identityʳ {A} {later x} {y} x≈y = x≈y delayMonad : Monad (Setoids c (c ⊔ ℓ)) delayMonad = record { F = record - { F₀ = delaySetoid + { F₀ = _⊥ₛ ; F₁ = delayFun ; identity = delayFun-id ; homomorphism = delayFun-comp diff --git a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md similarity index 56% rename from agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md rename to agda/src/Monad/Instance/Setoids/K.lagda.md index 8a8d607..96a00e4 100644 --- a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K.lagda.md @@ -12,67 +12,75 @@ open import Function using (_∘′_) renaming (_∘_ to _∘f_) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_) renaming (sym to ≡-sym) open import FreeObject +open import Categories.FreeObjects.Free +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Categories.Category.Instance.Properties.Setoids.Choice using () ``` --> -# The delay monad on the category of setoids is pre-Elgot +# The delay monad on the category of setoids is an instance of K ```agda -module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where +module Monad.Instance.Setoids.K {ℓ : Level} where open import Monad.Instance.K.Instance.Delay {ℓ} {ℓ} open import Category.Ambient.Setoids + open import Monad.Instance.K (setoidAmbient {ℓ}) open import Algebra.Elgot (setoidAmbient {ℓ}) open import Algebra.Elgot.Free (setoidAmbient {ℓ}) open import Category.Construction.ElgotAlgebras (setoidAmbient {ℓ}) open import Monad.PreElgot (setoidAmbient {ℓ}) open Equality + open Setoid using () renaming (Carrier to ∣_∣) conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''} - {x : Setoid.Carrier X} {y : Setoid.Carrier Y } → (X ⊎ₛ Y) [ inj₁ x ∼ inj₂ y ] → Z + {x : ∣ X ∣} {y : ∣ Y ∣} → (X ⊎ₛ Y) [ inj₁ x ∼ inj₂ y ] → Z conflict X Y () - iter : ∀ {A X : Setoid ℓ ℓ} → (Setoid.Carrier X → (Delay (Setoid.Carrier A) ⊎ Setoid.Carrier X)) → Setoid.Carrier X → Delay (Setoid.Carrier A) + iter : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (∣ A ∣ ⊥ ⊎ ∣ X ∣)) → ∣ X ∣ → ∣ A ∣ ⊥ iter {A} {X} f x with f x ... | inj₁ a = a ... | inj₂ b = later (♯ (iter {A} {X} f b)) - inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a b : Setoid.Carrier Y} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₁ b → Y [ a ∼ b ] + inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ Y ∣} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₁ b → Y [ a ∼ b ] inj₁-helper {X} {Y} f {x} {y} {a} {b} x∼y fi₁ fi₂ = drop-inj₁ {x = a} {y = b} helper where helper : (Y ⊎ₛ X) [ inj₁ a ∼ inj₁ b ] helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y - inj₂-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a b : Setoid.Carrier X} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₂ a → f ⟨$⟩ y ≡ inj₂ b → X [ a ∼ b ] + inj₂-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ X ∣} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₂ a → f ⟨$⟩ y ≡ inj₂ b → X [ a ∼ b ] inj₂-helper {X} {Y} f {x} {y} {a} {b} x∼y fi₁ fi₂ = drop-inj₂ {x = a} {y = b} helper where helper : (Y ⊎ₛ X) [ inj₂ a ∼ inj₂ b ] helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y - absurd-helper : ∀ {ℓ'} {X Y : Setoid ℓ ℓ} {A : Set ℓ'} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a : Setoid.Carrier Y} {b : Setoid.Carrier X} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₂ b → A + absurd-helper : ∀ {ℓ'} {X Y : Setoid ℓ ℓ} {A : Set ℓ'} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a : ∣ Y ∣} {b : ∣ X ∣} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₂ b → A absurd-helper {ℓ'} {X} {Y} {A} f {x} {y} {a} {b} x∼y fi₁ fi₂ = conflict Y X helper where helper : (Y ⊎ₛ X) [ inj₁ a ∼ inj₂ b ] helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y - iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (delaySetoid A ⊎ₛ X)) {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (f ._⟨$⟩_) y ] + iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (A ⊥ₛ ⊎ₛ X)) {x y : ∣ X ∣} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (f ._⟨$⟩_) y ] iter-cong {A} {X} f {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy ... | inj₁ a | inj₁ b = inj₁-helper f x∼y eqx eqy ... | 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 = later≈ (♯ iter-cong {A} {X} f (inj₂-helper f x∼y eqx eqy)) - iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ] + iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {x y : ∣ X ∣} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ] iter-fixpoint {A} {X} {f} {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy ... | inj₁ a | inj₁ b = inj₁-helper f x∼y eqx eqy ... | 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ₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (A ⊥ₛ ⊎ₛ X)) → X ⟶ A ⊥ₛ + iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f } + + -- iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {g : Y ⟶ (A ⊥ₛ ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : ∣ 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 : ∣ 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 @@ -80,79 +88,79 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where -- ... | 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 : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {g : Y ⟶ (A ⊥ₛ ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : ∣ 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 ... | inj₁ a | inj₁ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc ... | inj₁ c = drop-inj₁ {x = a} {y = c} helper where - helper'' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] + helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y) - helper' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ] - helper' = ∼-trans ((delaySetoid A) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y) - helper : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ inj₁ c ] + helper' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ] + helper' = ∼-trans ((A ⊥ₛ) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y) + helper : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ inj₁ c ] helper rewrite (≡-sym eqc) = helper' - ... | inj₂ c = conflict (delaySetoid A) Y helper + ... | inj₂ c = conflict (A ⊥ₛ) Y helper where - helper'' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] + helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y) - helper' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ] - helper' = ∼-trans ((delaySetoid A) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y) - helper : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ inj₂ c ] + helper' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ] + helper' = ∼-trans ((A ⊥ₛ) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y) + helper : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ inj₂ c ] helper rewrite (≡-sym eqc) = helper' iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₂ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc - ... | inj₁ c = conflict (delaySetoid A) Y (∼-sym (delaySetoid A ⊎ₛ Y) helper) + ... | inj₁ c = conflict (A ⊥ₛ) Y (∼-sym (A ⊥ₛ ⊎ₛ Y) helper) where - helper' : (delaySetoid A ⊎ₛ Y) [ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ∼ g ⟨$⟩ (h ⟨$⟩ y) ] + helper' : (A ⊥ₛ ⊎ₛ Y) [ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ∼ g ⟨$⟩ (h ⟨$⟩ y) ] helper' = hf≈gh {x} {y} x∼y - helper'' : (delaySetoid A ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ] - helper'' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y) - helper : (delaySetoid A ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ] - helper rewrite (≡-sym eqc) = ∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper' + helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ] + helper'' rewrite eqx = ∼-refl (A ⊥ₛ ⊎ₛ Y) + helper : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ] + helper rewrite (≡-sym eqc) = ∼-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper' ... | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper))) -- why does this not terminate?? -- | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper))) where - helper''' : (delaySetoid A ⊎ₛ Y) [ inj₂ c ∼ g ⟨$⟩ (h ⟨$⟩ y) ] - helper''' rewrite eqc = ∼-refl (delaySetoid A ⊎ₛ Y) - helper'' : (delaySetoid A ⊎ₛ Y) [ g ⟨$⟩ (h ⟨$⟩ y) ∼ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ] - helper'' = ∼-sym (delaySetoid A ⊎ₛ Y) (hf≈gh x∼y) - helper' : (delaySetoid A ⊎ₛ Y) [ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ∼ inj₂ (h ⟨$⟩ a) ] - helper' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y) + helper''' : (A ⊥ₛ ⊎ₛ Y) [ inj₂ c ∼ g ⟨$⟩ (h ⟨$⟩ y) ] + helper''' rewrite eqc = ∼-refl (A ⊥ₛ ⊎ₛ Y) + helper'' : (A ⊥ₛ ⊎ₛ Y) [ g ⟨$⟩ (h ⟨$⟩ y) ∼ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ] + helper'' = ∼-sym (A ⊥ₛ ⊎ₛ Y) (hf≈gh x∼y) + helper' : (A ⊥ₛ ⊎ₛ Y) [ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ∼ inj₂ (h ⟨$⟩ a) ] + helper' rewrite eqx = ∼-refl (A ⊥ₛ ⊎ₛ Y) helper : Y [ c ∼ h ⟨$⟩ a ] - helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (delaySetoid A ⊎ₛ Y) helper''' (∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper')) + helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (A ⊥ₛ ⊎ₛ Y) helper''' (∼-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper')) -- TODO maybe I can improve inj₁-helper etc. to handle this case as well - iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (delaySetoid A ⊎ₛ X)) → f ≋ g → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ] + iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (A ⊥ₛ ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ] iter-resp-≈ {A} {X} f g f≋g {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (g ._⟨$⟩_) y in eqy ... | inj₁ a | inj₁ b = drop-inj₁ helper where - helper : (delaySetoid A ⊎ₛ X) [ inj₁ a ∼ inj₁ b ] + helper : (A ⊥ₛ ⊎ₛ X) [ inj₁ a ∼ inj₁ b ] helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y - ... | inj₁ a | inj₂ b = conflict (delaySetoid A) X helper + ... | inj₁ a | inj₂ b = conflict (A ⊥ₛ) X helper where - helper : (delaySetoid A ⊎ₛ X) [ inj₁ a ∼ inj₂ b ] + helper : (A ⊥ₛ ⊎ₛ X) [ inj₁ a ∼ inj₂ b ] helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y - ... | inj₂ a | inj₁ b = conflict (delaySetoid A) X (∼-sym (delaySetoid A ⊎ₛ X) helper) + ... | inj₂ a | inj₁ b = conflict (A ⊥ₛ) X (∼-sym (A ⊥ₛ ⊎ₛ X) helper) where - helper : (delaySetoid A ⊎ₛ X) [ inj₂ a ∼ inj₁ b ] + helper : (A ⊥ₛ ⊎ₛ X) [ inj₂ a ∼ inj₁ b ] helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y ... | inj₂ a | inj₂ b = later≈ (♯ iter-resp-≈ {A} {X} f g f≋g (drop-inj₂ helper)) where - helper : (delaySetoid A ⊎ₛ X) [ inj₂ a ∼ inj₂ b ] + helper : (A ⊥ₛ ⊎ₛ X) [ inj₂ a ∼ inj₂ b ] helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y - iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : Setoid.Carrier (X ⊎ₛ Y)} → (X ⊎ₛ Y) [ x ∼ y ] → A [ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ] + iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → (X ⊎ₛ Y) [ x ∼ y ] → A [ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ] iter-folding {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix∼iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy ... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix∼iy) eqx eqy ... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix∼iy) eqx eqy ... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X (drop-inj₁ ix∼iy)) eqy eqx ... | inj₂ a | inj₂ b = later≈ (♯ ≈-trans (iter-cong f (inj₂-helper f (drop-inj₁ ix∼iy) eqx eqy)) (helper b)) where - helper : ∀ (b : Setoid.Carrier X) → A [ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ] + helper : ∀ (b : ∣ X ∣) → A [ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ] helper b with f ⟨$⟩ b in eqb - ... | inj₁ c = ∼-refl (delaySetoid A) + ... | inj₁ c = ∼-refl (A ⊥ₛ) ... | inj₂ c = later≈ (♯ helper c) iter-folding {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix∼iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy ... | inj₁ a | inj₁ b = later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper) @@ -166,9 +174,9 @@ 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-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A) + delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (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 } + { _# = iterₛ {A} ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f} ; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h} ; #-Folding = λ {X} {Y} {f} {h} {x} {y} x∼y → iter-folding {A} {X} {Y} {f} {h} {x} {y} x∼y @@ -176,32 +184,37 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where } delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra - delay-algebras A = record { A = delaySetoid A ; algebra = delay-algebras-on {A} } + delay-algebras A = record { A = 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 = ∼-sym (Elgot-Algebra.A B) (∼-trans (Elgot-Algebra.A B) (#-Fixpoint (∼-sym X x∼y)) helper) - where - open Elgot-Algebra B using (#-Fixpoint) - helper : Elgot-Algebra.A B [ {! !} x ∼ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ] -- ([ (f ._⟨$⟩_) , _ ] ∘′ g ._⟨$⟩_) - helper with g ⟨$⟩ x in eqx - ... | inj₁ a = {! !} - ... | inj₂ b = {! !} + open Elgot-Algebra using () renaming (A to ⟦_⟧) - -- TODO remove - delayPreElgot : IsPreElgot delayMonad - delayPreElgot = record - { elgotalgebras = delay-algebras-on - ; extend-preserves = {! !} + nowₛ : ∀ {A : Setoid ℓ ℓ} → A ⟶ A ⊥ₛ + nowₛ = record { _⟨$⟩_ = now ; cong = now-cong } + + delay-lift' : ∀ {A B : Set ℓ} → (A → B) → A ⊥ → B + delay-lift' {A} {B} f (now x) = f x + delay-lift' {A} {B} f (later x) = {! !} + + delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B + delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = delay-lift' {∣ A ∣} {∣ ⟦ B ⟧ ∣} (f ._⟨$⟩_) ; cong = {! !} } ; preserves = {! !} } + + freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A + freeAlgebra A = record + { FX = delay-algebras A + ; η = nowₛ {A} + ; _* = delay-lift + ; *-lift = {! !} + ; *-uniq = {! !} } + isStableFreeElgotAlgebra : ∀ (A : Setoid ℓ ℓ) → IsStableFreeElgotAlgebra (freeAlgebra A) + isStableFreeElgotAlgebra A = record + { [_,_]♯ = {! !} + ; ♯-law = {! !} + ; ♯-preserving = {! !} + ; ♯-unique = {! !} + } + delayK : MonadK + delayK = record { freealgebras = freeAlgebra ; stable = isStableFreeElgotAlgebra } ```