From 9beebd009d4279993b339970db20e62b97abea3b Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Tue, 9 Jan 2024 13:34:53 +0100 Subject: [PATCH] Some progress --- agda/src/Category/Ambient/Setoids.lagda.md | 2 +- agda/src/Monad/Instance/K/Instance/D.lagda.md | 94 ++++++++++++++++--- agda/src/Monad/Instance/Setoids/K'.lagda.md | 75 +++++++++++++-- 3 files changed, 152 insertions(+), 19 deletions(-) diff --git a/agda/src/Category/Ambient/Setoids.lagda.md b/agda/src/Category/Ambient/Setoids.lagda.md index 4361cf8..2ebcc03 100644 --- a/agda/src/Category/Ambient/Setoids.lagda.md +++ b/agda/src/Category/Ambient/Setoids.lagda.md @@ -36,7 +36,7 @@ module Category.Ambient.Setoids {ℓ} where ≋-trans : ∀ {A B : Setoid ℓ ℓ} {f g h : A ⟶ B} → f ≋ g → g ≋ h → f ≋ h ≋-trans {A} {B} {f} {g} {h} = IsEquivalence.trans (Setoid.isEquivalence (A ⇨ B)) {f} {g} {h} - -- we define ℕ ourselves, instead of importing it, to avoid lifting the universe lifting (builtin Nats are defined on Set₀) + -- we define ℕ ourselves, instead of importing it, to avoid lifting the universe levels (builtin Nats are defined on Set₀) data ℕ : Set ℓ where zero : ℕ suc : ℕ → ℕ diff --git a/agda/src/Monad/Instance/K/Instance/D.lagda.md b/agda/src/Monad/Instance/K/Instance/D.lagda.md index 4d77415..cedbbe5 100644 --- a/agda/src/Monad/Instance/K/Instance/D.lagda.md +++ b/agda/src/Monad/Instance/K/Instance/D.lagda.md @@ -13,7 +13,9 @@ open import Categories.Monad open import Categories.Category.Instance.Setoids open import Categories.NaturalTransformation hiding (id) open import Data.Product -open import Data.Nat using (ℕ; suc; zero) +open import Data.Product.Relation.Binary.Pointwise.NonDependent +-- open import Data.Nat using (ℕ; suc; zero) +open import Category.Ambient.Setoids module Monad.Instance.K.Instance.D {c ℓ} where @@ -204,6 +206,15 @@ module DelayMonad where ∼⇒≈ {A} {.(later _)} {.(later _)} (later∼ x∼y) = later≈ (∼′⇒≈′ x∼y) force≈ (∼′⇒≈′ {A} {x} {y} x∼y) = ∼⇒≈ (force∼ x∼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)) + + now-cong∼ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ x ≡ y ] → [ A ][ now x ∼ now y ] + now-cong∼ {A} {x} {y} x≡y = now∼ 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 : Set c} → (A → B) → Delay A → Delay B liftF′ : ∀ {A B : Set c} → (A → B) → Delay′ A → Delay′ B liftF f (now x) = now (f x) @@ -214,7 +225,6 @@ module DelayMonad where lift↓ {A} {B} f {now x} {b} (now↓ x≡a) = now↓ (cong f x≡a) lift↓ {A} {B} f {later x} {b} (later↓ x↓b) = later↓ (lift↓ f x↓b) - lift-cong : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x y : Delay ∣ A ∣} → [ A ][ x ≈ y ] → [ B ][ liftF < f > x ≈ liftF < f > y ] lift-cong′ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ B ][ liftF < f > x ≈′ liftF < f > y ] lift-cong {A} {B} f {now x} {now y} (↓≈ a≡b (now↓ x≡a) (now↓ y≡b)) = ↓≈ (cong f a≡b) (now↓ (cong f x≡a)) (now↓ (cong f y≡b)) @@ -227,11 +237,14 @@ module DelayMonad where liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ A ⟶ Delayₛ B liftFₛ {A} {B} f = record { _⟨$⟩_ = liftF < f > ; cong = lift-cong f } - 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)) - - 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ₛ' A ⟶ Delayₛ' B + liftFₛ∼ {A} {B} f = record { _⟨$⟩_ = liftF < f > ; cong = ∼-cong } + where + ∼-cong : ∀ {x y} → [ A ][ x ∼ y ] → [ B ][ liftF < f > x ∼ liftF < f > y ] + ∼-cong′ : ∀ {x y} → [ A ][ x ∼′ y ] → [ B ][ liftF < f > x ∼′ liftF < f > y ] + force∼ (∼-cong′ {x} {y} x∼y) = ∼-cong (force∼ x∼y) + ∼-cong {.(now _)} {.(now _)} (now∼ x≡y) = now-cong∼ (cong f x≡y) + ∼-cong {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (∼-cong′ x∼y) -- this needs polymorphic universe levels _≋_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ') @@ -316,6 +329,15 @@ module DelayMonad where μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ (Delayₛ A) ⟶ Delayₛ A μₛ A = record { _⟨$⟩_ = μ {A} ; cong = μ-cong A } + μₛ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ' (Delayₛ' A) ⟶ Delayₛ' A + μₛ∼ A = record { _⟨$⟩_ = μ {A} ; cong = μ-cong∼ A } + where + μ-cong∼ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ' A ][ x ∼ y ] → [ A ][ μ {A} x ∼ μ {A} y ] + μ-cong∼′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ' A ][ x ∼′ y ] → [ A ][ μ {A} x ∼′ μ {A} y ] + force∼ (μ-cong∼′ A {x} {y} x∼y) = μ-cong∼ A (force∼ x∼y) + μ-cong∼ A {.(now _)} {.(now _)} (now∼ x∼y) = x∼y + μ-cong∼ A {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (μ-cong∼′ A x∼y) + μ-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (μₛ B ∘ liftFₛ (liftFₛ f)) ≋ (liftFₛ f ∘ μₛ A) μ-natural′ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → ∀ {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ A ][ x ≈′ y ] → [ B ][ (μₛ B ∘ liftFₛ (liftFₛ f)) ⟨$⟩ x ≈′ (liftFₛ f ∘ μₛ A) ⟨$⟩ y ] force≈ (μ-natural′ {A} {B} f {x} {y} x≈y) = μ-natural f (force≈ x≈y) @@ -367,6 +389,8 @@ module DelayMonad where ; identityʳ = identityʳ } +open DelayMonad + module extra {A : Setoid c (c ⊔ ℓ)} where ≲→≈ : {x y : Delay ∣ A ∣} → [ A ][ x ≲ y ] → [ A ][ x ≈ y ] ≲→≈′ : {x y : Delay ∣ A ∣} → [ A ][ x ≲′ y ] → [ A ][ x ≈′ y ] @@ -385,6 +409,23 @@ module extra {A : Setoid c (c ⊔ ℓ)} where force (race′ x y) = race (force x) (force y) + race-sym : ∀ {x y} → [ A ][ x ∼ y ] → [ A ][ race x y ∼ race y x ] + race-sym′ : ∀ {x y} → [ A ][ x ∼′ y ] → [ A ][ race x y ∼′ race y x ] + force∼ (race-sym′ {x} {y} x∼y) = race-sym {x} {y} (force∼ x∼y) + race-sym {now x} {now y} x∼y = x∼y + race-sym {now x} {later y} x∼y = ∼-refl A + race-sym {later x} {now y} x∼y = ∼-refl A + race-sym {later x} {later y} (later∼ x∼y) = later∼ (race-sym′ x∼y) + + race-sym≈ : ∀ {x y} → [ A ][ x ≈ y ] → [ A ][ race x y ∼ race y x ] + race-sym≈′ : ∀ {x y} → [ A ][ x ≈′ y ] → [ A ][ race x y ∼′ race y x ] + force∼ (race-sym≈′ {x} {y} x∼y) = race-sym≈ {x} {y} (force≈ x∼y) + race-sym≈ {now x} {now y} (↓≈ a≡b (now↓ x≡a) (now↓ y≡b)) = now∼ (≡-trans A x≡a (≡-trans A a≡b (≡-sym A y≡b))) + race-sym≈ {now x} {later y} x≈y = ∼-refl A + race-sym≈ {later x} {now y} x≈y = ∼-refl A + race-sym≈ {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later∼ (race-sym≈′ (≈→≈′ A (↓≈ a≡b x↓a y↓b))) + race-sym≈ {later x} {later y} (later≈ x≈y) = later∼ (race-sym≈′ x≈y) + ≈→≲₀ : ∀ {x y a b} (x↓a : [ A ][ x ↓ a ]) (y↓b : [ A ][ y ↓ b ]) (a≡b : [ A ][ a ≡ b ]) → [ A ][ race x y ≲ y ] ≈→≲₀ (now↓ x≡a) y↓b a≡b = ↓≲ (≡↓ A (≡-sym A (≡-trans A x≡a a≡b)) y↓b) ≈→≲₀ (later↓ x↓a) (now↓ x≡y) a≡b = ↓≲ (now↓ (≡-refl A)) @@ -398,22 +439,51 @@ module extra {A : Setoid c (c ⊔ ℓ)} where force≲ (≈′→≲′ x≈′y) = ≈→≲ (force≈ x≈′y) - delta₀ : {x : Delay ∣ A ∣} {a : ∣ A ∣} → (x↓a : [ A ][ x ↓ a ]) → ℕ + delta₀ : {x : Delay ∣ A ∣} {a : ∣ A ∣} → (x↓a : [ A ][ x ↓ a ]) → ℕ {c} delta₀ {x} (now↓ x≡y) = zero delta₀ (later↓ x↓a) = suc (delta₀ x↓a) - delta : {x y : Delay ∣ A ∣} → [ A ][ x ≲ y ] → Delay (∣ A ∣ × ℕ) - delta′ : {x y : Delay ∣ A ∣} → [ A ][ x ≲′ y ] → Delay′ (∣ A ∣ × ℕ) + delta : {x y : Delay ∣ A ∣} → [ A ][ x ≲ y ] → Delay (∣ A ∣ × ℕ {c}) + delta′ : {x y : Delay ∣ A ∣} → [ A ][ x ≲′ y ] → Delay′ (∣ A ∣ × ℕ {c}) delta (↓≲ {x}{a} x↓a) = now (a , delta₀ x↓a) delta (later≲ x≲′y) = later (delta′ x≲′y) force (delta′ x≲′y) = delta (force≲ x≲′y) - ι : ∣ A ∣ × ℕ → Delay ∣ A ∣ - ι′ : ∣ A ∣ × ℕ → Delay′ ∣ A ∣ + ι : ∣ A ∣ × ℕ {c} → Delay ∣ A ∣ + ι′ : ∣ A ∣ × ℕ {c} → Delay′ ∣ A ∣ force (ι′ p) = ι p ι (x , zero) = now x ι (x , suc n) = later (ι′ (x , n)) + ιₛ' : A ×ₛ (ℕ-setoid {c}) ⟶ Delayₛ' A + ιₛ' = record { _⟨$⟩_ = ι ; cong = ι-cong } + where + ι-cong : ∀ {x y} → [ A ×ₛ (ℕ-setoid {c}) ][ x ≡ y ] → [ A ][ ι x ∼ ι y ] + ι-cong′ : ∀ {x y} → [ A ×ₛ (ℕ-setoid {c}) ][ x ≡ y ] → [ A ][ ι x ∼′ ι y ] + force∼ (ι-cong′ {x} {y} x≡y) = ι-cong x≡y + ι-cong {x , zero} {y , zero} (x≡y , n≡m) = now∼ x≡y + ι-cong {x , suc n} {y , suc m} (x≡y , n≡m) = later∼ (ι-cong′ (x≡y , suc-inj n≡m)) + + delta-prop₁ : {x y : Delay ∣ A ∣} (x≲y : [ A ][ x ≲ y ]) → [ A ][ liftF proj₁ (delta x≲y) ∼ x ] + delta-prop′₁ : {x y : Delay ∣ A ∣} (x≲y : [ A ][ x ≲′ y ]) → [ A ][ liftF proj₁ (force (delta′ x≲y)) ∼′ x ] + + delta-prop₁ {.(now _)} {x} (↓≲ x↓a) = now∼ (≡-refl A) + delta-prop₁ {.(later _)} {.(later _)} (later≲ x≲y) = later∼ (delta-prop′₁ x≲y) + + force∼ (delta-prop′₁ x≲y) = delta-prop₁ (force≲ x≲y) + + delta-prop₂ : {x y : Delay ∣ A ∣} (x≲y : [ A ][ x ≲ y ]) → [ A ][ μ {A} (liftF ι (delta x≲y)) ∼ y ] + delta-prop′₂ : {x y : Delay ∣ A ∣} (x≲y : [ A ][ x ≲′ y ]) → [ A ][ μ {A} (liftF ι (force (delta′ x≲y))) ∼′ y ] + + delta-prop₂ (↓≲ x↓a) = ∼-sym A (ι↓ x↓a) + where + ι↓ : {x : Delay ∣ A ∣}{a : ∣ A ∣} → (x↓a : [ A ][ x ↓ a ]) → [ A ][ x ∼ ι (a , delta₀ x↓a) ] + ι↓ {.(now _)} {a} (now↓ x≡y) = now∼ x≡y + ι↓ {.(later _)} {a} (later↓ x↓a) = later∼ (record { force∼ = ι↓ x↓a }) + + delta-prop₂ (later≲ x≲y) = later∼ (delta-prop′₂ x≲y) + + force∼ (delta-prop′₂ x≲y) = delta-prop₂ (force≲ x≲y) ``` diff --git a/agda/src/Monad/Instance/Setoids/K'.lagda.md b/agda/src/Monad/Instance/Setoids/K'.lagda.md index e3bab10..3319e7e 100644 --- a/agda/src/Monad/Instance/Setoids/K'.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K'.lagda.md @@ -15,6 +15,8 @@ open import Categories.FreeObjects.Free open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Categories.Category.Instance.Properties.Setoids.Choice using () open import Data.Product.Relation.Binary.Pointwise.NonDependent +open import Data.Product +-- open import Data.Nat ``` --> @@ -31,6 +33,7 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where open import Monad.PreElgot (setoidAmbient {ℓ}) open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_]) open DelayMonad + open extra open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_]) open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans) @@ -168,20 +171,80 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where open Elgot-Algebra using () 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 { _⟨$⟩_ = < (B Elgot-Algebra.#) helper > ; cong = λ {x} {y} x≈y → {! !} } ; preserves = {! !} } + delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = ((B Elgot-Algebra.#) helper) ._⟨$⟩_ ; cong = helper#≈-cong } ; preserves = {! !} } where -- (f + id) ∘ out helper₁ : Delay ∣ A ∣ → ∣ ⟦ B ⟧ ∣ ⊎ Delay ∣ A ∣ - helper₁ (now x) = inj₁ (< f > x) + helper₁ (now x) = inj₁ (< f > x) helper₁ (later x) = inj₂ (force x) + + helper₁-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ helper₁ x ≡ helper₁ y ] + helper₁-cong (now∼ x≡y) = inj₁ (cong f x≡y) + helper₁-cong (later∼ x≡y) = inj₂ (force∼ x≡y) + -- -- setoid-morphism that preserves strong-bisimilarity helper : Delayₛ' A ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' A - helper = record { _⟨$⟩_ = helper₁ ; cong = strong-cong } + helper = record { _⟨$⟩_ = helper₁ ; cong = helper₁-cong} + + helper#∼-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper ⟨$⟩ x ≡ (B Elgot-Algebra.#) helper ⟨$⟩ y ] + helper#∼-cong {x} {y} x∼y = cong ((B Elgot-Algebra.#) helper) x∼y + + helper#≈-cong : {x y : Delay ∣ A ∣} → (x≈y : [ A ][ x ≈ y ]) → [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper ⟨$⟩ x ≡ (B Elgot-Algebra.#) helper ⟨$⟩ y ] + + -- key special case + helper#≈-cong' : {z : Delay (∣ A ∣ × ℕ)} → [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper ⟨$⟩ liftF proj₁ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ μ {A} (liftF (ι {A}) z) ] + + helper#≈-cong x≈y = + ≡-trans ⟦ B ⟧ + (helper#∼-cong (∼-sym A (delta-prop₂ {A} ineq₂))) + (≡-trans ⟦ B ⟧ + (≡-trans ⟦ B ⟧ + (≡-sym ⟦ B ⟧ (helper#≈-cong' {z₂})) (≡-trans ⟦ B ⟧ (helper#∼-cong (∼-trans A (delta-prop₁ (≈→≲ (≈-sym A x≈y))) (∼-sym A (∼-trans A (delta-prop₁ (≈→≲ x≈y)) (race-sym≈ x≈y))))) (helper#≈-cong' {z₁}))) + (helper#∼-cong (delta-prop₂ {A} ineq₁))) where - strong-cong : ∀ {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ helper₁ x ≡ helper₁ y ] - strong-cong {.(now _)} {.(now _)} (now∼ x≡y) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y) - strong-cong {.(later _)} {.(later _)} (later∼ x∼y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (force∼ x∼y) + ineq₁ = ≈→≲ {A} x≈y + ineq₂ = ≈→≲ {A} (≈-sym A x≈y) + z₁ = delta {A} ineq₁ + z₂ = delta {A} ineq₂ + + helper#≈-cong' {z} = ≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ eq₁) eq₂ + where + helper₁' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ) + helper₁' (now (x , zero)) = inj₁ (< f > x) + helper₁' (now (x , suc n)) with helper₁' (now (x , n)) + ... | inj₁ r = inj₁ r + ... | inj₂ y = inj₂ (later (record { force = y })) + helper₁' (later y) = inj₂ (force y) + + helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ' (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ] + helper₁-cong' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y) + helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) with helper₁' (now (x , n)) | helper₁' (now (y , n)) | helper₁-cong' {now (x , n)} (now∼ (x≡y , ≣-refl)) + ... | inj₁ r | inj₁ s | inj₁ r≡s = inj₁ r≡s + ... | inj₂ x' | inj₂ y' | inj₂ x'∼y' = inj₂ (later∼ (record { force∼ = x'∼y' })) + helper₁-cong' (later∼ x≡y) = inj₂ (force∼ x≡y) + + helper' : Delayₛ' (A ×ₛ ℕ-setoid) ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' (A ×ₛ ℕ-setoid) + helper' = record { _⟨$⟩_ = helper₁' ; cong = helper₁-cong'} + + -- Should follow by compositionality + fixpoint + eq₁ : [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ liftF proj₁ z ] + eq₁ = {!!} + + eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ] + eq {now (x , zero)} {now (y , zero)} (now∼ (x≡y , _)) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y) + -- eq {now (x , suc n)} {now (y , suc m)} (now∼ (x≡y , n≡m)) with helper₁' (now (x , n)) + -- ... | inj₁ r = {! !} -- <- contradiction! + -- ... | inj₂ r = {! !} + eq {now (x , suc n)} {now (y , suc m)} (now∼ (x≡y , n≡m)) = {! !} + -- TODO induction, by a recursive call to eq, we will get info about helper₁' (now (x , n)) + eq {.(later _)} {.(later _)} (later∼ x≡y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x≡y))) + + -- Should follow by uniformity + eq₂ : [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ μ {A} (liftF (ι {A}) z)] + eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ' (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ' A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} eq + (∼-refl (A ×ₛ ℕ-setoid)) <<_>> = Elgot-Algebra-Morphism.h