diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index 51b89fe..bf67e95 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -72,6 +72,26 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
       helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
       helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y
 
+
+  -- TODO remove the following two later
+  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₁-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-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∼′ {A} {X} f (inj₂-helper f x≡y eqx eqy))
+
   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
@@ -81,6 +101,9 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
   ...                             | 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ₛ∼ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ∼ A ⊎ₛ X)) → X ⟶ Delayₛ∼ A
+  iterₛ∼ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong∼ {A} {X} f }
+
   iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A
   iterₛ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong {A} {X} f }
 
@@ -159,7 +182,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
 
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
-  delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → {!   !} }
+  delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → ≡-trans ⟦ B ⟧ (preserves' {X} {g} {x}) (#-resp-≈ B (≡-refl (⟦ B ⟧ ⊎ₛ X))) }
     where
     open Elgot-Algebra B using (_#)
     -- (f + id) ∘ out
@@ -179,7 +202,6 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
     helper#∼-cong {x} {y} x∼y = cong (helper #) x∼y
 
     helper#≈-cong : {x y : Delay ∣ A ∣} → (x≈y : [ A ][ x ≈ y ]) → [ ⟦ B ⟧ ][ helper # ⟨$⟩ x ≡ helper # ⟨$⟩ y ]
-    
     -- key special case
     helper#≈-cong' : {z : Delay (∣ A ∣ × ℕ)} → [ ⟦ B ⟧ ][ helper # ⟨$⟩ liftF proj₁ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z) ]
 
@@ -288,11 +310,18 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
     delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
 
-    preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (< helper # > (iter {A} {X} < g > x)) ≡ < ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # > x ] 
-    preserves' {X} {g} {x} = ≡-sym ⟦ B ⟧ (#-Uniformity B {!  λ {x} → by-uni {x} !}) -- #-Uniformity B {!   !}
+    preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
+    -- h would need iter-cong∼', which is not doable i think
+    preserves' {X} {g} {x} = ≡-sym ⟦ B ⟧ (#-Uniformity B {f = [ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g} {g = helper} {h = {!   !}} {!   !})--(≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ A) by-uni trivial))
       where
-        by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ < [ inj₁ₛ ∘ delay-lift' , inj₂ₛ ∘ iterₛ {A} {X} g ]ₛ ∘ g > x ≡ (helper₁ ∘′ iter {A} {X} < g >) x ]
-        by-uni = {!   !}
+        by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ < [ inj₁ₛ , inj₂ₛ ∘ iterₛ {A} {X} g ]ₛ ∘ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) > x ≡ (< helper > ∘′ (iter {A} {X} < g >)) x ]
+        by-uni {x} with g ⟨$⟩ x in eqa 
+        ...    | inj₁ a = {!   !}
+        -- ...    | inj₁ (now a) = {!   !} -- easy
+        -- ...    | inj₁ (later a) = {!   !} -- impossible?
+        ...    | inj₂ a = inj₂ (∼-refl A)
+        trivial : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ (< helper > ∘′ iter < g >) x ≡ helper₁ (iter < g > x) ]
+        trivial {x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A) 
 
   <<_>> = Elgot-Algebra-Morphism.h
 
@@ -308,6 +337,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
       *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift {A} {B} f >>) ⟨$⟩ x)
       *-uniq' {B} f g eq {now x} = ≡-trans ⟦ B ⟧ (eq {x}) (≡-sym ⟦ B ⟧ (#-Fixpoint B))
       *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {!   !} (≡-sym ⟦ B ⟧ (#-Fixpoint B)) 
+      -- *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! *-uniq' {B} f g eq {force x}  !} (≡-sym ⟦ B ⟧ (#-Fixpoint B))