sync

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 : ℕ → ℕ

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)
 ```

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,95 @@ 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)) in eqr
+        -- ...                                                       | inj₁ r = {! eq {now (x , n)} {now (y , m)}  !} -- problem: recursive call to eq does not pass termination checker
+        --   where
+        --     help : [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ inj₁ r ]
+        --     help = cong [ inj₁ₛ , (inj₂ₛ ∘ μₛ∼ A ∘ liftFₛ∼ ιₛ') ]ₛ (≡→≡ eqr)
+        -- ...                                                       | inj₂ r = {!   !}
+        -- eq {.(later _)} {.(later _)} (later∼ x≡y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x≡y)))
+
+        eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
+        eq {now (x , n)} {now (y , m)} (now∼ p∼q) = eq' {n} {m} {x} {y} (now∼ p∼q)
+          where
+            eq' : ∀ {n m x y} → [ A ×ₛ ℕ-setoid ][ now (x , n) ∼ now (y , m) ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) (now (y , m)) ]
+            eq' {zero} {zero} {x} {y} (now∼ (x≡y , _)) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y)
+            eq' {suc n} {suc m} {x} {y} (now∼ (x≡y , sn≡sm)) with helper₁' (now (x , n)) in eqr 
+            ...                     | inj₁ r = ≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ' A) (≡-sym (⟦ B ⟧ ⊎ₛ Delayₛ' A) help) (≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ' A) (eq' {n} {m} {x} {y} (now∼ (x≡y , suc-inj sn≡sm))) {! -should this be provable?-  !})
+              where
+                help : [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ inj₁ r ]
+                help = cong [ inj₁ₛ , (inj₂ₛ ∘ μₛ∼ A ∘ liftFₛ∼ ιₛ') ]ₛ (≡→≡ eqr)
+            ...                     | inj₂ r = {!   !}
+        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