diff --git a/agda/src/Monad/Instance/K/Instance/D.lagda.md b/agda/src/Monad/Instance/K/Instance/D.lagda.md
index 9739860..4b9aee6 100644
--- a/agda/src/Monad/Instance/K/Instance/D.lagda.md
+++ b/agda/src/Monad/Instance/K/Instance/D.lagda.md
@@ -179,6 +179,8 @@ open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼
 module DelayMonad where
   Delayₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
   Delayₛ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }
+  Delayₛ' : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
+  Delayₛ' A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
   <_> = Π._⟨$⟩_
 
   ∼⇒≈ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ A ][ x ≈ y ]
diff --git a/agda/src/Monad/Instance/Setoids/K'.lagda.md b/agda/src/Monad/Instance/Setoids/K'.lagda.md
new file mode 100644
index 0000000..9c70809
--- /dev/null
+++ b/agda/src/Monad/Instance/Setoids/K'.lagda.md
@@ -0,0 +1,195 @@
+<!--
+```agda
+{-# OPTIONS --allow-unsolved-metas --guardedness #-}
+open import Level
+open import Relation.Binary
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
+open import Data.Sum.Function.Setoid
+open import Data.Sum.Relation.Binary.Pointwise
+open import Function.Equality as SΠ renaming (id to idₛ)
+open import Function using (_∘′_) renaming (_∘_ to _∘f_)
+import Relation.Binary.PropositionalEquality as Eq
+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 (_×ₛ_)
+open import Categories.Category.Instance.Properties.Setoids.Choice using ()
+``` 
+-->
+
+# The delay monad on the category of setoids is an instance of K
+
+```agda
+module Monad.Instance.Setoids.K' {ℓ : Level} where
+  open import Monad.Instance.K.Instance.D {ℓ} {ℓ}
+  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 Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
+  open DelayMonad
+  open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
+  open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
+
+  iter : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay ∣ A ∣
+  iter′ : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay′ ∣ A ∣
+  force (iter′ {A} {X} f x) = iter {A} {X} f x
+  iter {A} {X} f x with f x 
+  ...              | inj₁ a = a
+  ...              | inj₂ b = later (iter′ {A} {X} f x)
+
+  conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''}
+    {x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z
+  conflict X Y ()
+
+  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 : ∣ 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 : ∣ 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 ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} (f ._⟨$⟩_) x) ≈ (iter {A} {X} (f ._⟨$⟩_) y) ]
+  iter-cong′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} (f ._⟨$⟩_) x) ≈′ (iter {A} {X} (f ._⟨$⟩_) y) ]
+  force≈ (iter-cong′ {A} {X} f {x} {y} x≡y) = iter-cong f x≡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′ f x≡y)
+
+  iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A
+  iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f }
+
+  iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ 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 = ≈-trans A (≈-sym A later-self) (iter-cong f {!   !})
+
+  iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ 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 : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈′ iter {A} {X} (g ._⟨$⟩_) y ]
+  force≈ (iter-resp-≈′ {A} {X} f g f≋g {x} {y} x≡y) = iter-resp-≈ f g f≋g x≡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 : [ Delayₛ A ⊎ₛ X ][ inj₁ a ≡ inj₁ b ]
+      helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y
+  ...                                     | inj₁ a        | inj₂ b     = conflict (Delayₛ A) X helper
+    where
+      helper : [ Delayₛ A ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
+      helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y
+  ...                                     | inj₂ a        | inj₁ b     = conflict (Delayₛ A) X (≡-sym (Delayₛ A ⊎ₛ X) helper)
+    where
+      helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ]
+      helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y
+  ...                                     | inj₂ a        | inj₂ b     = later≈ (iter-resp-≈′ f g f≋g x≡y)
+
+
+  iter-folding' : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ 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 : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ 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 ]
+  force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x} {y} x≡y) = iter-folding' {A} {X} {Y} {f} {h} x≡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≈ helper
+    where
+      helper' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ]
+      helper'' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ]
+      helper'' b with f ⟨$⟩ b in eqb 
+      ...               | inj₁ c = ≈-refl A
+      ...               | inj₂ c = later≈ (helper' b)
+      force≈ (helper' b) with f ⟨$⟩ b in eqb 
+      ...               | inj₁ c = ≈-refl A
+      ...               | inj₂ c = later≈ (helper' b)
+      helper : [ A ][ iter < f > x ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ y) ]
+      force≈ helper = ≈-trans A (iter-cong f (drop-inj₁ ix≡iy)) (helper'' y)
+
+  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  !}
+    where
+      helper : [ X ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ]
+      helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
+  ...                                                       | inj₁ a            | inj₂ b          = absurd-helper h (drop-inj₂ ix≡iy) eqx eqy
+  ...                                                       | inj₂ a            | inj₁ b          = absurd-helper h (≡-sym Y (drop-inj₂ ix≡iy)) eqy eqx
+  ...                                                       | inj₂ a            | inj₂ b          = later≈ {!   !}
+    where
+      helper' : [ A ][ iter [ inj₁ ∘′ iter < f > , inj₂ ∘′ < h > ] (inj₂ x) ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₂ y) ]
+      force≈ helper' = later≈ {! iter-folding' {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} ?  !}
+      helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ]
+      helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
+
+
+  iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ 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≈ {!   !} -- later≈ (♯ ≈-trans A (iter-cong f (inj₂-helper f (drop-inj₁ ix≡iy) eqx eqy)) (helper b))
+    where
+      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 (Delayₛ A)
+      ...    | inj₂ c = later≈ {!   !} -- 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)
+    where
+      helper : [ X ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ]
+      helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
+  ...                                                      | inj₁ a            | inj₂ b         = absurd-helper h (drop-inj₂ ix≡iy) eqx eqy
+  ...                                                      | inj₂ a            | inj₁ b         = absurd-helper h (≡-sym Y (drop-inj₂ ix≡iy)) eqy eqx
+  ...                                                      | inj₂ a            | inj₂ b         = {!   !} -- later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} helper) 
+    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 (Delayₛ A)
+  delay-algebras-on {A} = record
+    { _# = 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
+    ; #-resp-≈ = λ {X} {f} {g} → iter-resp-≈ {A} {X} f g
+    }
+
+  delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
+  delay-algebras A = record { A = Delayₛ A ; algebra = delay-algebras-on {A}}
+
+  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 = {!   !} }
+    where
+    -- (f + id) ∘ out
+    helper₁ : Delay ∣ A ∣ → ∣ ⟦ B ⟧ ∣ ⊎ Delay ∣ A ∣
+    helper₁ (now x) = inj₁ (< f > x)
+    helper₁ (later x) = inj₂ (force x)
+    -- -- setoid-morphism that preserves strong-bisimilarity
+    helper : Delayₛ' A ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' A
+    helper = record { _⟨$⟩_ = helper₁ ; cong = {!   !} }
+
+  freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
+  freeAlgebra A = record 
+    { FX = delay-algebras A
+    ; η = ηₛ A
+    ; _* = delay-lift 
+    ; *-lift = {!   !} 
+    ; *-uniq = {!   !} 
+    }
+
+```
\ No newline at end of file