diff --git a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
index 3dde1cb..1133c00 100644
--- a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
+++ b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
@@ -65,6 +65,9 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
 
   open StrongBisimilarity renaming (_∼_ to [_][_∼_])
 
+  _⊥ₛ' : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
+  _⊥ₛ' A = record { Carrier = ∣ A ∣ ⊥ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
+
   module WeakBisimilarity (A : Setoid c (c ⊔ ℓ)) where
     data _↓_ : ∣ A ∣ ⊥ → ∣ A ∣ → Set (c ⊔ ℓ) where
       now↓ : ∀ {x y} (x≡y : [ A ][ x ≡ y ]) → now x ↓ y
@@ -251,4 +254,21 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
     ; identityˡ = identityˡ
     ; identityʳ = identityʳ
     }
+
+  strongMonad : Monad (Setoids c (c ⊔ ℓ))
+  strongMonad = record
+    { F = record
+      { F₀ = _⊥ₛ' 
+      ; F₁ = λ {A} {B} f → record { _⟨$⟩_ = liftF (f ._⟨$⟩_) ; cong = {!   !} }
+      ; identity = {!   !}
+      ; homomorphism = {!   !}
+      ; F-resp-≈ = {!   !}
+      }
+    ; η = {!   !}
+    ; μ = {!   !}
+    ; assoc = {!   !}
+    ; sym-assoc = {!   !}
+    ; identityˡ = {!   !}
+    ; identityʳ = {!   !}
+    }
 ```
\ No newline at end of file
diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index fd1876b..7d4ee8b 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -10,7 +10,7 @@ open import Function.Equality as SΠ renaming (id to idₛ)
 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 Eq using (_≡_) renaming (sym to ≣-sym; refl to ≣-refl; trans to ≣-trans)
 open import FreeObject
 open import Categories.FreeObjects.Free
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
@@ -75,6 +75,13 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
   ...                                   | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
   ...                                   | inj₂ a | inj₂ b = ≈-sym A (later-eq (later≈ (♯ iter-cong f (≡-sym X (inj₂-helper f x≡y eqx eqy)))))
 
+  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 A {!   !} -- ≈-sym A (later-eq (later≈ (♯ iter-cong f (≡-sym X (inj₂-helper f x≡y eqx eqy)))))
+
   iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (A ⊥ₛ ⊎ₛ X)) → X ⟶ A ⊥ₛ
   iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f }
 
@@ -216,21 +223,23 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
       out-cong {later x} {now y} x≡y = {!   !}
       out-cong {later x} {later y} x≡y = {!   !}
 
+  set-setoid : ∀ {c} → Set c → Setoid c c
+  set-setoid A = record { Carrier = A ; _≈_ = _≡_ ; isEquivalence = record { refl = ≣-refl ; sym = ≣-sym ; trans = ≣-trans } }
+
+  
+
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
-  delay-lift {A} {B} f = record { h = (B Elgot-Algebra.#) helper ; preserves = {!   !} }
+  delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = ((B Elgot-Algebra.#) helper) ._⟨$⟩_ ; cong = λ {x} {y} x≈y → ? } ; preserves = {!   !} }
     where
-    -- this definition of helper₁ corresponds to `(f + id) ∘ out`, but using the representation of _⊥ as a positive coinductive type
+    -- (f + id) ∘ out, this is just on sets
     helper₁ : ∣ A ∣ ⊥ → ∣ ⟦ B ⟧ ∣ ⊎ ∣ A ∣ ⊥
     helper₁ (now x) = inj₁ (< f > x)
     helper₁ (later x) = inj₂ (♭ x)
-    helper₁-cong : ∀ {x y : ∣ A ∣ ⊥} → [ A ][ x ≈ y ] → [ ⟦ B ⟧ ⊎ₛ A ⊥ₛ ][ helper₁ x ≡ helper₁ y ]
-    helper₁-cong {now x} {now y} x≈y = {!   !} -- yes
-    helper₁-cong {now x} {later y} x≈y = {!   !} -- problematic, need to show inj₁ (f x) ≈ inj₂ y, which is contradictory, while the assumption now x ≈ later y is not contradictory.
-    helper₁-cong {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = {!   !}
-    helper₁-cong {later x} {later y} (later≈ x≈y) = {!   !} -- cong inj₂ₛ (♭ x≈y)
-    helper₁-cong {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = {!   !} --cong inj₂ₛ (↓≈ a≡b x↓a y↓b)
-    helper : A ⊥ₛ ⟶ ⟦ B ⟧ ⊎ₛ A ⊥ₛ
-    helper = record { _⟨$⟩_ = helper₁ ; cong = helper₁-cong }
+    -- setoid-morphism that preserves strong-bisimilarity
+    helper : A ⊥ₛ' ⟶ ⟦ B ⟧ ⊎ₛ A ⊥ₛ'
+    helper = record { _⟨$⟩_ = helper₁ ; cong = {!   !} }
+    -- helper' : 
+    -- is-cong : 
 
   freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
   freeAlgebra A = record