diff --git a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
index 8c8e8f9..ae10bfd 100644
--- a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
+++ b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
@@ -4,7 +4,7 @@
 
 open import Level
 open import Category.Ambient using (Ambient)
-open import Categories.Category
+open import Categories.Category.Core
 open import Categories.Category.Instance.Setoids
 open import Categories.Monad
 open import Categories.Category.Monoidal.Instance.Setoids
@@ -23,6 +23,8 @@ open import Function.Base using (id)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_)
 open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
+open import Codata.Musical.Notation
+import Category.Monad.Partiality
 ```
 -->
 
@@ -33,125 +35,164 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
 # Capretta's Delay Monad is an Instance of K in the Category of Setoids
 
 ```agda
-  record Delay (A : Set c) : Set c where
-    coinductive
-    field
-      node : A ⊎ Delay A
-    
-  open Delay
+  data Delay (A : Set c) : Set c where
+    now : A → Delay A
+    later : ∞ (Delay A) → Delay A
 
-  now : ∀ {A : Set c} → A → Delay A
-  node (now {A} a) = inj₁ a
+  module Equality {A : Setoid c (c ⊔ ℓ)} where
+    open Setoid A renaming (Carrier to C; _≈_ to _∼_)
+    open IsEquivalence (Setoid.isEquivalence A) renaming (refl to ∼-refl; sym to ∼-sym; trans to ∼-trans)
 
-  later : ∀ {A : Set c} → Delay A → Delay A
-  node (later {A} a) = inj₂ a
-
-  never : ∀ {A : Set c} → Delay A
-  node (never {A}) = inj₂ never
-
-  module Equality {A : Setoid c ℓ} where
-    open Setoid A using () renaming (Carrier to C; _≈_ to _∼_)
     data _↓_ : Delay C → C → Set (c ⊔ ℓ) where
-      now↓ : ∀ {x y} (p : x ∼ y) → now x ↓ y
-      later↓ : ∀ {x y} (p : _↓_ x y) → later x ↓ y
+      now↓ : ∀ {x y} (x∼y : x ∼ y) → now x ↓ y
+      later↓ : ∀ {x y} (x↓y : ♭ x ↓ y) → later x ↓ y
+
+    unique↓ : ∀ {c : Delay C} {x y : C} → c ↓ x → c ↓ y → x ∼ y
+    unique↓ (now↓ eq₁) (now↓ eq₂) = ∼-trans (∼-sym eq₁) eq₂
+    unique↓ (later↓ p) (later↓ q) = unique↓ p q
 
     data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where
-      ↓≈ : ∀ {x y z} → x ↓ z → y ↓ z → x ≈ y
-      later-≈ : ∀ {x y} → x ≈ y → later x ≈ later y
+      ↓≈ : ∀ {x y a b} (a∼b : a ∼ b) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y
+      later≈ : ∀ {x y} → (∞ (♭ x ≈ ♭ y)) → later x ≈ later y
 
-    refl : ∀ {x} → x ≈ x
-    refl {x} with node x 
-    ...             | inj₁ z = ↓≈ {!   !} {!   !}
-    ...             | inj₂ z = {!   !}
+    ≈-refl : ∀ {x} → x ≈ x
+    ≈-refl {now x} = ↓≈ ∼-refl (now↓ ∼-refl) (now↓ ∼-refl)
+    ≈-refl {later x} = later≈ (♯ ≈-refl)
 
-  -- first try
-  delay-eq-strong : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ
-  delay-eq-strong A x y with node x | node y
-  ...                   | inj₁ a    | inj₁ b = Setoid._≈_ A a b
-  ...                   | inj₁ a    | inj₂ b = ⊥
-  ...                   | inj₂ a    | inj₁ b = ⊥
-  ...                   | inj₂ a    | inj₂ b = {!   !}
+    ≈-sym : ∀ {x y} → x ≈ y → y ≈ x
+    ≈-sym (↓≈ a∼b x↓a y↓b) = ↓≈ (∼-sym a∼b) y↓b x↓a
+    ≈-sym (later≈ x≈y) = later≈ (♯ ≈-sym (♭ x≈y))
+
+    ∼↓ : ∀ {x y : C} {z : Delay C} → x ∼ y → z ↓ x → z ↓ y
+    ∼↓ {x} {y} {.(now _)} x∼y (now↓ a∼x) = now↓ (∼-trans a∼x x∼y)
+    ∼↓ {x} {y} {.(later _)} x∼y (later↓ z↓x) = later↓ (∼↓ x∼y z↓x)
+
+    ≈↓ : ∀ {x y : Delay C} {z : C} → x ≈ y → x ↓ z → y ↓ z
+    ≈↓ (↓≈ a∼b (now↓ x∼a) y↓b) (now↓ x∼z) = ∼↓ (∼-trans (∼-sym a∼b) (∼-trans (∼-sym x∼a) x∼z)) y↓b
+    ≈↓ (↓≈ a∼b (later↓ x↓a) y↓b) (later↓ x↓z) with unique↓ x↓a x↓z 
+    ...                                         | a∼z = ∼↓ (∼-trans (∼-sym a∼b) a∼z) y↓b
+    ≈↓ (later≈ x) (later↓ x↓z) = later↓ (≈↓ (♭ x) x↓z)
+
+    ≈-trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
+    ≈-trans (↓≈ a∼b x↓a y↓b) (↓≈ c∼d y↓c z↓d) with unique↓ y↓b y↓c
+    ...                                 | b∼c = ↓≈ (∼-trans (∼-trans a∼b b∼c) c∼d) x↓a z↓d
+    ≈-trans (↓≈ a∼b z↓a (later↓ x↓b)) (later≈ x≈y) = ↓≈ a∼b z↓a (later↓ (≈↓ (♭ x≈y) x↓b))
+    ≈-trans (later≈ x≈y) (↓≈ a∼b (later↓ y↓a) z↓b) = ↓≈ a∼b (later↓ (≈↓ (≈-sym (♭ x≈y)) y↓a)) z↓b
+    ≈-trans (later≈ x≈y) (later≈ y≈z) = later≈ (♯ ≈-trans (♭ x≈y) (♭ y≈z)) 
+    
+  delaySetoid : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
+  delaySetoid A = record { Carrier = Delay Carrier ; _≈_ = _≈_ ; isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans } }
+    where 
+      open Setoid A using (Carrier)
+      open Equality {A}
+  open Equality using (↓≈; later≈; now↓; later↓; _↓_; ≈↓; ≈-refl; ≈-sym; ≈-trans)
+
+  _[_≈_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : Delay (Setoid.Carrier A)) → Set (c ⊔ ℓ)
+  A [ x ≈ y ] = Equality._≈_ {A} x y
+
+  _[_∼_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : Setoid.Carrier A) → Set (c ⊔ ℓ)
+  A [ x ∼ y ] = Setoid._≈_ A x y
+
+  ∼-refl : ∀ (A : Setoid c (c ⊔ ℓ)) {x : Setoid.Carrier A} → A [ x ∼ x ]
+  ∼-refl A = IsEquivalence.refl (Setoid.isEquivalence A) 
+
+  ∼-sym : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Setoid.Carrier A} → A [ x ∼ y ] → A [ y ∼ x ]
+  ∼-sym A = IsEquivalence.sym (Setoid.isEquivalence A)
+
+  ∼-trans : ∀ (A : Setoid c (c ⊔ ℓ)) {x y z : Setoid.Carrier A} → A [ x ∼ y ] → A [ y ∼ z ] → A [ x ∼ z ]
+  ∼-trans A = IsEquivalence.trans (Setoid.isEquivalence A)
+
+  now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ x ∼ y ] → A [ now x ≈ now y ]
+  now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (∼-refl A)) (now↓ (∼-refl A))
+
+  delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → delaySetoid A ⟶ delaySetoid B
+  delayFun {A} {B} f = record { _⟨$⟩_ = app ; cong = cong' }
+    where
+      app : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier B)
+      app (now x) = now (f ⟨$⟩ x)
+      app (later x) = later (♯ app (♭ x))
+      -- TODO a variant of this should be useful outside
+      ↓-cong : ∀ {x : Delay (Setoid.Carrier A)} {b : Setoid.Carrier A} → _↓_ {A} x b → _↓_ {B} (app x) (f ⟨$⟩ b)
+      ↓-cong {now x} {b} (now↓ x∼y) = now↓ (cong f x∼y) 
+      ↓-cong {later x} {b} (later↓ x↓b) = later↓ (↓-cong x↓b)
+      cong' : ∀ {x y : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → B [ app x ≈ app y ]
+      cong' {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = now-cong (cong f (∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b))))
+      cong' {now x} {later y} (↓≈ a∼b (now↓ x∼a) (later↓ y↓b)) = ↓≈ (cong f (∼-trans A x∼a a∼b)) (now↓ (∼-refl B)) (later↓ (↓-cong y↓b))
+      cong' {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (cong f (∼-trans A a∼b (∼-sym A y∼b))) (later↓ (↓-cong x↓a)) (now↓ (∼-refl B))
+      cong' {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ cong' (↓≈ a∼b x↓a y↓b))
+      cong' {later x} {later y} (later≈ x≈y) = later≈ (♯ cong' (♭ x≈y))
+
+  -- ↓-delay : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) {x : Setoid.Carrier  → f ⟨$⟩ x
+
+  -- this needs polymorphic universe levels
+  _≋_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ')
+  _≋_ {c'} {ℓ'} {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
+
+  later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay (Setoid.Carrier A)} → A [ later (♯ x) ≈ y ] → A [ x ≈ y ] 
+  later-eq {A} {x} {y} (↓≈ a∼b (later↓ x↓a) y↓b) = ↓≈ a∼b x↓a y↓b
+  later-eq {A} {now x} {later y} (later≈ x≈y) = ↓≈ (∼-refl A) (now↓ (∼-refl A)) (later↓ (≈↓ (♭ x≈y) (now↓ (∼-refl A))))
+  later-eq {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ later-eq (≈-trans (later≈ (♯ ≈-refl)) (♭ x≈y)))
+
+  later-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Setoid.Carrier A)} → A [ x ≈ later (♯ x) ]
+  later-self {A} {now x} = ↓≈ (∼-refl A) (now↓ (∼-refl A)) (later↓ (now↓ (∼-refl A)))
+  later-self {A} {later x} = later-eq (later≈ (♯ ≈-refl))
+
+  delayFun↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : Delay (Setoid.Carrier A)} {y : Setoid.Carrier A} → _↓_ {A} x y → _↓_ {B} (delayFun f ⟨$⟩ x) (f ⟨$⟩ y)
+  delayFun↓ {A} {B} f {now x} {y} (now↓ x∼y) = now↓ (cong f x∼y)
+  delayFun↓ {A} {B} f {later x} {y} (later↓ x↓y) = later↓ (delayFun↓ f x↓y)
+
+  delayFun-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (delayFun idₛ) ≋ (idₛ {A = delaySetoid A})
+  delayFun-id {A} {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ↓≈ a∼b (now↓ x∼a) (now↓ y∼b)
+  delayFun-id {A} {now x} {later y} x≈y = x≈y
+  delayFun-id {A} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ a∼b (later↓ (delayFun↓ idₛ x↓a)) (now↓ y∼b)
+  delayFun-id {A} {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ delayFun-id (↓≈ a∼b x↓a y↓b))
+  delayFun-id {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ delayFun-id (♭ x≈y))
+
+  η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ delaySetoid A
+  η A = record { _⟨$⟩_ = now ; cong = id λ x∼y → now-cong x∼y }
+
+  η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (η B ∘ f) ≋ (delayFun f ∘ η A)
+  η-natural {A} {B} f {x} {y} x≈y = now-cong (cong f x≈y)
+
+  private
+    μ' : ∀ {A : Setoid c (c ⊔ ℓ)} → Setoid.Carrier (delaySetoid (delaySetoid A)) → Setoid.Carrier (delaySetoid A)
+    μ' {A} (now x) = x
+    μ' {A} (later x) = later (♯ μ' {A} (♭ x))
+
+    μ↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid A} x y → A [ (μ' {A} x) ≈ y ]
+    μ↓ {A} {B} f {now x} {y} (now↓ x≈y) = x≈y
+    μ↓ {A} {B} f {later x} {y} (later↓ x↓y) = ≈-trans (later≈ (♯ μ↓ f x↓y)) (≈-sym later-self)
+
+    -- TODO μ≈
+    -- TODO do delayFun and η in the same style as μ
   
-  -- second try
-  record eq-strong (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set c where
-      field
-        node-eq₁ : (node x) ≡ (node y)
-
-  -- third try
-  mutual
-    node-eq : (A : Setoid c ℓ) (x y : Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
-    node-eq A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
-    node-eq A (inj₁ x) (inj₂ y) = ⊥
-    node-eq A (inj₂ x) (inj₁ y) = ⊥
-    node-eq A (inj₂ x) (inj₂ y) = delay-eq-strong' A x y
-    delay-eq-strong' : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ
-    delay-eq-strong' A x y = node-eq A {!   !} {!   !}
-
-  Delay-setoid : Setoid c ℓ → Setoid c ℓ
-  Delay-setoid A = record { Carrier = Delay A.Carrier ; _≈_ = {!   !} ; isEquivalence = {!   !} }
+  μ : ∀ (A : Setoid c (c ⊔ ℓ)) → delaySetoid (delaySetoid A) ⟶ delaySetoid A
+  μ A = record { _⟨$⟩_ = μ' {A} ; cong = {!   !} }
     where
-      module A = Setoid A
+      cong' : ∀ {x y : Delay (Delay (Setoid.Carrier A))} → (delaySetoid A) [ x ≈ y ] → A [ μ' x ≈ μ' y ]
+      cong' {now x} {now y} (↓≈ a≈b (now↓ x≈a) (now↓ y≈b)) = ≈-trans x≈a (≈-trans a≈b (≈-sym y≈b))
+      cong' {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = ↓≈ {A} {! a≈b  !} {!   !} (later↓ {!   !})
+      cong' {later x} {now y} (↓≈ a≈b (later↓ x↓a) (now↓ (↓≈ a∼b x↓a₁ y↓b))) = ↓≈ {!   !} (later↓ {!   !}) x↓a₁
+      cong' {later x} {now .(later _)} (↓≈ a≈b (later↓ x↓a) (now↓ (later≈ x₁))) = ↓≈ {!   !} {!   !} {!   !}
+      cong' {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ cong' (↓≈ a∼b x↓a y↓b))
+      cong' {later x} {later y} (later≈ x≈y) = later≈ (♯ cong' (♭ x≈y))
+      
 
+  delayMonad : Monad (Setoids c (c ⊔ ℓ))
+  delayMonad = record
+    { F = record
+      { F₀ = delaySetoid
+      ; F₁ = delayFun
+      ; identity = delayFun-id
+      ; homomorphism = {!   !}
+      ; F-resp-≈ = {!   !}
+      }
+    ; η = ntHelper (record { η = η ; commute = η-natural })
+    ; μ = {!   !}
+    ; assoc = {!   !}
+    ; sym-assoc = {!   !}
+    ; identityˡ = {!   !}
+    ; identityʳ = {!   !}
+    }
 
-  -- finally this should work
-  mutual
-    record eq-strong' (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set ℓ where
-      coinductive
-      field
-        eq : eq-strong'' A (node x) (node y)
-    eq-strong'' : (A : Setoid c ℓ) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
-    eq-strong'' A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
-    eq-strong'' A (inj₁ x) (inj₂ y) = ⊥
-    eq-strong'' A (inj₂ x) (inj₁ y) = ⊥
-    eq-strong'' A (inj₂ x) (inj₂ y) = eq-strong' A x y
-
-
-  -- this should also work
-  mutual
-    record eq-weak (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set ℓ where
-      coinductive
-      field
-        eq : eq-weak' A (node x) (node y)
-    eq-weak' : (A : Setoid c ℓ) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
-    eq-weak' A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
-    eq-weak' A (inj₁ x) (inj₂ y) = eq-weak A (now x) y
-    eq-weak' A (inj₂ x) (inj₁ y) = eq-weak A x (now y)
-    eq-weak' A (inj₂ x) (inj₂ y) = eq-weak A x y
-  open eq-weak
-
-  now-cong : ∀ {A : Setoid c ℓ} {a b : Setoid.Carrier A} → Setoid._≈_ A a b → eq-weak A (now a) (now b)
-  eq (now-cong {A} {a} {b} a≈b) = a≈b
-
-  now-inj : ∀ {A : Setoid c ℓ} {a b : Setoid.Carrier A} → eq-weak A (now a) (now b) → Setoid._≈_ A a b
-  now-inj {A} {a} {b} na≈nb with (eq na≈nb) 
-  ...                         | a≈b = a≈b
-
-  now-weak-eq : ∀ {A : Setoid c ℓ} {a : Setoid.Carrier A} {b : Delay (Setoid.Carrier A)} → eq-weak A (now a) b → Σ (Setoid.Carrier A) (λ c → Setoid._≈_ A a c)
-  now-weak-eq {A} {a} {b} na≈b with node b | eq na≈b 
-  ...                             | inj₁ x | a≈b = x , a≈b
-  ...                             | inj₂ x | a≈b = {!   !}
-
-  weak-setoid : Setoid c ℓ → Setoid c ℓ
-  weak-setoid A = record { Carrier = Delay (Setoid.Carrier A) ; _≈_ = eq-weak A ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } }
-    where
-      refl' : Reflexive (eq-weak A)
-      eq (refl' {a}) with node a
-      ...            | inj₁ x = IsEquivalence.refl (Setoid.isEquivalence A)
-      ...            | inj₂ x = refl'
-      sym' : Symmetric (eq-weak A)
-      eq (sym' {a} {b} a≈b) with node a | node b | eq a≈b
-      ...               | inj₁ x    | inj₁ y     | z = IsEquivalence.sym (Setoid.isEquivalence A) z
-      ...               | inj₂ x    | inj₁ y     | z = sym' z
-      ...               | inj₁ x    | inj₂ y     | z = sym' z
-      ...               | inj₂ x    | inj₂ y     | z = sym' z
-      trans' : Transitive (eq-weak A)
-      eq (trans' {a} {b} {c} a≈b b≈c) with node a | node b | node c | eq a≈b | eq b≈c 
-      ...                             | inj₂ x    | inj₂ y | inj₂ z | eq₁    | eq₂ = trans' eq₁ eq₂
-      ...                             | inj₁ x    | inj₂ y | inj₂ z | eq₁    | eq₂ = trans' eq₁ eq₂
-      ...                             | inj₂ x    | inj₁ y | inj₂ z | eq₁    | eq₂ = trans' eq₁ eq₂
-      ...                             | inj₁ x    | inj₁ y | inj₂ z | eq₁    | eq₂ = trans' (now-cong eq₁) eq₂ -- trans' (now-cong eq₁) eq₂
-      ...                             | inj₂ x    | inj₂ y | inj₁ z | eq₁    | eq₂ = trans' eq₁ eq₂
-      ...                             | inj₁ x    | inj₂ y | inj₁ z | eq₁    | eq₂ = {!  !} -- now-inj {A} {x} {z} (trans' eq₁ eq₂)
-      ...                             | inj₂ x    | inj₁ y | inj₁ z | eq₁    | eq₂ = trans' eq₁ (now-cong eq₂)
-      ...                             | inj₁ x    | inj₁ y | inj₁ z | eq₁    | eq₂ = IsEquivalence.trans (Setoid.isEquivalence A) eq₁ eq₂
 ```
\ No newline at end of file
diff --git a/agda/src/Monad/Instance/K/Instance/Delay'.lagda.md b/agda/src/Monad/Instance/K/Instance/DelayOld.lagda.md
similarity index 86%
rename from agda/src/Monad/Instance/K/Instance/Delay'.lagda.md
rename to agda/src/Monad/Instance/K/Instance/DelayOld.lagda.md
index 05ab1d5..edbda55 100644
--- a/agda/src/Monad/Instance/K/Instance/Delay'.lagda.md
+++ b/agda/src/Monad/Instance/K/Instance/DelayOld.lagda.md
@@ -29,7 +29,7 @@ import Category.Monad.Partiality
 -->
 
 ```agda
-module Monad.Instance.K.Instance.Delay' {c ℓ} where
+module Monad.Instance.K.Instance.DelayOld {c ℓ} where
 ```
 
 # Capretta's Delay Monad is an Instance of K in the Category of Setoids
@@ -39,11 +39,6 @@ module Monad.Instance.K.Instance.Delay' {c ℓ} where
     now : A → Delay A
     later : ∞ (Delay A) → Delay A
 
-  data _≈s_ {A : Setoid c ℓ} : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set (c ⊔ ℓ) where
-    now : ∀ {x y} → Setoid._≈_ A x y → (now x) ≈s (now y)
-    later : ∀ {x y : Delay (Setoid.Carrier A)} → _≈s_ {A} x y → (later (♯ x)) ≈s (later (♯ y))
-
-
   module Equality {A : Setoid c ℓ} where
     open Setoid A renaming (Carrier to C; _≈_ to _∼_)
     data _≈_ : Delay C → Delay C → Set ℓ where
@@ -130,20 +125,22 @@ module Monad.Instance.K.Instance.Delay' {c ℓ} where
     sym' (↓≈ a∼b x↓a y↓b) = ↓≈ (∼-sym a∼b) y↓b x↓a
     sym' (later≈ x≈y) = later≈ (♯ sym' (♭ x≈y))
 
-    -- TODO needed for trans'
+    ∼↓ : ∀ {x y : C} {z : Delay C} → x ∼ y → z ↓ x → z ↓ y
+    ∼↓ {x} {y} {.(now _)} x∼y (now↓ a∼x) = now↓ (∼-trans a∼x x∼y)
+    ∼↓ {x} {y} {.(later _)} x∼y (later↓ z↓x) = later↓ (∼↓ x∼y z↓x)
+
     ≈↓ : ∀ {x y : Delay C} {z : C} → x ≈ y → x ↓ z → y ↓ z
-    ≈↓ x≈y x↓z = {!   !}
-    -- ≈↓ (↓≈ a(now↓ refl) q) (now↓ refl) = q
-    -- ≈↓ (↓≈ (later↓ p) r) (later↓ q) with unique↓ p q
-    -- ≈↓ (↓≈ (later↓ p) r) (later↓ q) | refl = r
-    -- ≈↓ (later≈ p) (later↓ q) = later↓ (≈↓ (♭ p) q)
+    ≈↓ (↓≈ a∼b (now↓ x∼a) y↓b) (now↓ x∼z) = ∼↓ (∼-trans (∼-sym a∼b) (∼-trans (∼-sym x∼a) x∼z)) y↓b
+    ≈↓ (↓≈ a∼b (later↓ x↓a) y↓b) (later↓ x↓z) with unique↓ x↓a x↓z 
+    ...                                         | a∼z = ∼↓ (∼-trans (∼-sym a∼b) a∼z) y↓b
+    ≈↓ (later≈ x) (later↓ x↓z) = later↓ (≈↓ (♭ x) x↓z)
 
     trans' : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
     trans' (↓≈ a∼b x↓a y↓b) (↓≈ c∼d y↓c z↓d) with unique↓ y↓b y↓c
     ...                                 | b∼c = ↓≈ (∼-trans (∼-trans a∼b b∼c) c∼d) x↓a z↓d
-    trans' (↓≈ a∼b x↓a (later↓ y↓b)) (later≈ x) = ↓≈ a∼b x↓a {!   !}
-    trans' (later≈ x) (↓≈ a∼b x↓a y↓b) = {!   !}
-    trans' (later≈ x) (later≈ y) = {!   !} 
+    trans' (↓≈ a∼b z↓a (later↓ x↓b)) (later≈ x≈y) = ↓≈ a∼b z↓a (later↓ (≈↓ (♭ x≈y) x↓b))
+    trans' (later≈ x≈y) (↓≈ a∼b (later↓ y↓a) z↓b) = ↓≈ a∼b (later↓ (≈↓ (sym' (♭ x≈y)) y↓a)) z↓b
+    trans' (later≈ x≈y) (later≈ y≈z) = later≈ (♯ trans' (♭ x≈y) (♭ y≈z)) 
     
   delay-setoid' : Setoid c ℓ → Setoid c (c ⊔ ℓ)
   delay-setoid' A = record { Carrier = Delay Carrier ; _≈_ = _≈_ ; isEquivalence = record { refl = λ {x} → {!   !} ; sym = λ {x y} → {!   !} ; trans = λ {x y z} → {!   !} } }
diff --git a/agda/src/Monad/Instance/K/Instance/DelayRecord.lagda.md b/agda/src/Monad/Instance/K/Instance/DelayRecord.lagda.md
new file mode 100644
index 0000000..65f3176
--- /dev/null
+++ b/agda/src/Monad/Instance/K/Instance/DelayRecord.lagda.md
@@ -0,0 +1,157 @@
+<!--
+```agda 
+{-# OPTIONS --allow-unsolved-metas --guardedness #-}
+
+open import Level
+open import Category.Ambient using (Ambient)
+open import Categories.Category
+open import Categories.Category.Instance.Setoids
+open import Categories.Monad
+open import Categories.Category.Monoidal.Instance.Setoids
+open import Categories.Category.Cocartesian
+open import Categories.Object.Terminal
+open import Function.Equality as SΠ renaming (id to idₛ)
+import Categories.Morphism.Reasoning as MR
+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 Data.Unit.Polymorphic using (tt; ⊤)
+open import Data.Empty.Polymorphic using (⊥)
+open import Categories.NaturalTransformation using (ntHelper)
+open import Function.Base using (id)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_)
+open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
+```
+-->
+
+```agda
+module Monad.Instance.K.Instance.DelayRecord {c ℓ} where
+```
+
+# Capretta's Delay Monad is an Instance of K in the Category of Setoids
+
+```agda
+  record Delay (A : Set c) : Set c where
+    coinductive
+    field
+      node : A ⊎ Delay A
+    
+  open Delay
+
+  now : ∀ {A : Set c} → A → Delay A
+  node (now {A} a) = inj₁ a
+
+  later : ∀ {A : Set c} → Delay A → Delay A
+  node (later {A} a) = inj₂ a
+
+  never : ∀ {A : Set c} → Delay A
+  node (never {A}) = inj₂ never
+
+  module Equality {A : Setoid c ℓ} where
+    open Setoid A using () renaming (Carrier to C; _≈_ to _∼_)
+    data _↓_ : Delay C → C → Set (c ⊔ ℓ) where
+      now↓ : ∀ {x y} (p : x ∼ y) → now x ↓ y
+      later↓ : ∀ {x y} (p : _↓_ x y) → later x ↓ y
+
+    data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where
+      ↓≈ : ∀ {x y z} → x ↓ z → y ↓ z → x ≈ y
+      later-≈ : ∀ {x y} → x ≈ y → later x ≈ later y
+
+    refl : ∀ {x} → x ≈ x
+    refl {x} with node x 
+    ...             | inj₁ z = ↓≈ {!   !} {!   !}
+    ...             | inj₂ z = {!   !}
+
+  -- first try
+  delay-eq-strong : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ
+  delay-eq-strong A x y with node x | node y
+  ...                   | inj₁ a    | inj₁ b = Setoid._≈_ A a b
+  ...                   | inj₁ a    | inj₂ b = ⊥
+  ...                   | inj₂ a    | inj₁ b = ⊥
+  ...                   | inj₂ a    | inj₂ b = {!   !}
+  
+  -- second try
+  record eq-strong (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set c where
+      field
+        node-eq₁ : (node x) ≡ (node y)
+
+  -- third try
+  mutual
+    node-eq : (A : Setoid c ℓ) (x y : Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
+    node-eq A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
+    node-eq A (inj₁ x) (inj₂ y) = ⊥
+    node-eq A (inj₂ x) (inj₁ y) = ⊥
+    node-eq A (inj₂ x) (inj₂ y) = delay-eq-strong' A x y
+    delay-eq-strong' : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ
+    delay-eq-strong' A x y = node-eq A {!   !} {!   !}
+
+  Delay-setoid : Setoid c ℓ → Setoid c ℓ
+  Delay-setoid A = record { Carrier = Delay A.Carrier ; _≈_ = {!   !} ; isEquivalence = {!   !} }
+    where
+      module A = Setoid A
+
+
+  -- finally this should work
+  mutual
+    record eq-strong' (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set ℓ where
+      coinductive
+      field
+        eq : eq-strong'' A (node x) (node y)
+    eq-strong'' : (A : Setoid c ℓ) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
+    eq-strong'' A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
+    eq-strong'' A (inj₁ x) (inj₂ y) = ⊥
+    eq-strong'' A (inj₂ x) (inj₁ y) = ⊥
+    eq-strong'' A (inj₂ x) (inj₂ y) = eq-strong' A x y
+
+
+  -- this should also work
+  mutual
+    record eq-weak (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set ℓ where
+      coinductive
+      field
+        eq : eq-weak' A (node x) (node y)
+    eq-weak' : (A : Setoid c ℓ) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
+    eq-weak' A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
+    eq-weak' A (inj₁ x) (inj₂ y) = eq-weak A (now x) y
+    eq-weak' A (inj₂ x) (inj₁ y) = eq-weak A x (now y)
+    eq-weak' A (inj₂ x) (inj₂ y) = eq-weak A x y
+  open eq-weak
+
+  now-cong : ∀ {A : Setoid c ℓ} {a b : Setoid.Carrier A} → Setoid._≈_ A a b → eq-weak A (now a) (now b)
+  eq (now-cong {A} {a} {b} a≈b) = a≈b
+
+  now-inj : ∀ {A : Setoid c ℓ} {a b : Setoid.Carrier A} → eq-weak A (now a) (now b) → Setoid._≈_ A a b
+  now-inj {A} {a} {b} na≈nb with (eq na≈nb) 
+  ...                         | a≈b = a≈b
+
+  now-weak-eq : ∀ {A : Setoid c ℓ} {a : Setoid.Carrier A} {b : Delay (Setoid.Carrier A)} → eq-weak A (now a) b → Σ (Setoid.Carrier A) (λ c → Setoid._≈_ A a c)
+  now-weak-eq {A} {a} {b} na≈b with node b | eq na≈b 
+  ...                             | inj₁ x | a≈b = x , a≈b
+  ...                             | inj₂ x | a≈b = {!   !}
+
+  weak-setoid : Setoid c ℓ → Setoid c ℓ
+  weak-setoid A = record { Carrier = Delay (Setoid.Carrier A) ; _≈_ = eq-weak A ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } }
+    where
+      refl' : Reflexive (eq-weak A)
+      eq (refl' {a}) with node a
+      ...            | inj₁ x = IsEquivalence.refl (Setoid.isEquivalence A)
+      ...            | inj₂ x = refl'
+      sym' : Symmetric (eq-weak A)
+      eq (sym' {a} {b} a≈b) with node a | node b | eq a≈b
+      ...               | inj₁ x    | inj₁ y     | z = IsEquivalence.sym (Setoid.isEquivalence A) z
+      ...               | inj₂ x    | inj₁ y     | z = sym' z
+      ...               | inj₁ x    | inj₂ y     | z = sym' z
+      ...               | inj₂ x    | inj₂ y     | z = sym' z
+      trans' : Transitive (eq-weak A)
+      eq (trans' {a} {b} {c} a≈b b≈c) with node a | node b | node c | eq a≈b | eq b≈c 
+      ...                             | inj₂ x    | inj₂ y | inj₂ z | eq₁    | eq₂ = trans' eq₁ eq₂
+      ...                             | inj₁ x    | inj₂ y | inj₂ z | eq₁    | eq₂ = trans' eq₁ eq₂
+      ...                             | inj₂ x    | inj₁ y | inj₂ z | eq₁    | eq₂ = trans' eq₁ eq₂
+      ...                             | inj₁ x    | inj₁ y | inj₂ z | eq₁    | eq₂ = trans' (now-cong eq₁) eq₂ -- trans' (now-cong eq₁) eq₂
+      ...                             | inj₂ x    | inj₂ y | inj₁ z | eq₁    | eq₂ = trans' eq₁ eq₂
+      ...                             | inj₁ x    | inj₂ y | inj₁ z | eq₁    | eq₂ = {!  !} -- now-inj {A} {x} {z} (trans' eq₁ eq₂)
+      ...                             | inj₂ x    | inj₁ y | inj₁ z | eq₁    | eq₂ = trans' eq₁ (now-cong eq₂)
+      ...                             | inj₁ x    | inj₁ y | inj₁ z | eq₁    | eq₂ = IsEquivalence.trans (Setoid.isEquivalence A) eq₁ eq₂
+```
\ No newline at end of file