diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index 6da595f..fa0a904 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -72,17 +72,6 @@ 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
@@ -366,14 +355,14 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
         → (<< h >> ∘ (ηₛ A)) ≋ f
         → << g >> ≋ << h >>
       *-uniq' {B} f g h eqᵍ eqʰ {x} = ≡-trans ⟦ B ⟧ (cong << g >> iter-id) 
-                                     (≡-trans ⟦ B ⟧ (preserves g {Delayₛ∼ A} {[ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now} {x = x}) 
+                                     (≡-trans ⟦ B ⟧ (preserves g {Delayₛ∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x}) 
                                      (≡-trans ⟦ B ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x}) 
-                                     (≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delayₛ∼ A} {[ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now} {x = x})) 
+                                     (≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delayₛ∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x})) 
                                                     (≡-sym ⟦ B ⟧ (cong << h >> iter-id)))))
         where
         open Elgot-Algebra B using (_#)
-        quot-morph : ∀ {A : Setoid ℓ ℓ} → Delayₛ∼ A ⟶ Delayₛ A
-        quot-morph {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq }
+        D∼⇒D≈ : ∀ {A : Setoid ℓ ℓ} → Delayₛ∼ A ⟶ Delayₛ A
+        D∼⇒D≈ {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq }
 
         helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣))
         helper-now₁ (now x) = inj₁ (now x)
@@ -382,13 +371,13 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
         helper-now = record { to = helper-now₁ ; cong = λ { (now∼ eq)   → inj₁ (now∼ eq) 
                                                           ; (later∼ eq) → inj₂ (force∼ eq) } }
 
-        helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x 
-                                                   ≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
+        helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x 
+                                                   ≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
         helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ))
         helper-eq' {later x} = inj₂ (∼-refl A)
 
-        iter-id :  ∀ {x} → [ A ][ x ≈  iterₛ ([ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
-        iter-id′ : ∀ {x} → [ A ][ x ≈′ iterₛ ([ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
+        iter-id :  ∀ {x} → [ A ][ x ≈  iterₛ ([ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
+        iter-id′ : ∀ {x} → [ A ][ x ≈′ iterₛ ([ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
         force≈ (iter-id′ {x}) = iter-id {x}
         iter-id {now x} = ≈-refl A
         iter-id {later x} = later≈ (iter-id′ {force x})