diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index 1a73528..b205bd4 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -244,12 +244,14 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
             out-cong {.(now _)} {.(now _)} (now∼ x≡y) = inj₁ x≡y
             out-cong {.(later _)} {.(later _)} (later∼ x∼y) = inj₂ (record { force∼′′ = force∼ x∼y })
 
+        -- TODO move
+        nowₛ∼ : ∀ {X} → X ⟶ Delayₛ∼ X
+        nowₛ∼ {X} = record { _⟨$⟩_ = now ; cong = {!   !} }
+        laterₛ∼ : ∀ {X} → Delayₛ∼′ X ⟶ Delayₛ∼ X
+        laterₛ∼ {X} = record { _⟨$⟩_ = later ; cong = {!   !} }
+
         out⁻¹∼ : ∀ {X} → X ⊎ₛ Delayₛ∼′ X ⟶ Delayₛ∼ X
-        out⁻¹∼ {X} = record { _⟨$⟩_ = out⁻¹ ; cong = out⁻¹-cong }
-          where
-            out⁻¹-cong : ∀ {x y} → [ X ⊎ₛ (Delayₛ∼′ X) ][ x ≡ y ] → [ X ][ out⁻¹ x ∼ out⁻¹ y ]
-            out⁻¹-cong {.(inj₁ _)} {.(inj₁ _)} (inj₁ x≡y) = now∼ x≡y
-            out⁻¹-cong {.(inj₂ _)} {.(inj₂ _)} (inj₂ x∼y) = later∼ (record { force∼ = force∼′′ x∼y })
+        out⁻¹∼ {X} = [ nowₛ∼ , laterₛ∼ ]ₛ
 
         -- TODO out∘out⁻¹≡id and out⁻¹∘out≡id