diff --git a/agda/src/Monad/Instance/Setoids/Delay.lagda.md b/agda/src/Monad/Instance/Setoids/Delay.lagda.md
index 95f81a5..7818ce7 100644
--- a/agda/src/Monad/Instance/Setoids/Delay.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/Delay.lagda.md
@@ -375,6 +375,24 @@ module DelayMonad where
 
 open DelayMonad
 
+-- custom definition of natural numbers together with the setoid on ℕ with propositional equality
+module nat {ℓ} where
+  data ℕ : Set ℓ where
+    zero : ℕ
+    suc : ℕ → ℕ
+
+  ℕ-setoid : Setoid ℓ ℓ
+  ℕ-setoid = record 
+    { Carrier = ℕ 
+    ; _≈_ = _≡_ 
+    ; isEquivalence = Eq.isEquivalence 
+    }
+
+  suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
+  suc-inj Eq.refl = Eq.refl
+
+open nat
+
 module extra {A : Setoid c (c ⊔ ℓ)} where
   ≲→≈  : {x y : Delay ∣ A ∣}  → [ A ][ x ≲ y ] → [ A ][ x ≈ y ]
   ≲→≈′ : {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
index a461c5b..8c1f19e 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -30,17 +30,18 @@ open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-C
 module Monad.Instance.Setoids.K {ℓ : Level} where
   open _⟶_ using (cong)
   open import Category.Ambient.Setoids
-  open Ambient (setoidAmbient {ℓ}) using (cocartesian; distributive)
+  open Ambient (setoidAmbient {ℓ} {ℓ}) using (cocartesian; distributive)
   open import Monad.Instance.Setoids.Delay {ℓ} {ℓ}
-  open import Monad.Instance.K (setoidAmbient {ℓ})
+  open import Monad.Instance.K (setoidAmbient {ℓ} {ℓ})
   open import Algebra.Elgot cocartesian
   open import Algebra.Elgot.Free cocartesian
   open import Algebra.Elgot.Stable distributive
   open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ} cocartesian
-  open import Monad.PreElgot (setoidAmbient {ℓ})
+  open import Monad.PreElgot (setoidAmbient {ℓ} {ℓ})
   open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
   open DelayMonad
   open extra
+  open nat
   open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
   open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
 
@@ -297,6 +298,14 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
     delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
 
+
+    -- interesting note:
+    -- the following definition prevents more general universe levels, i.e. we would like to parametrize this module by two levels c and ℓ, one for carriers and one for proofs.
+    -- but adopting this approach would force us to talk about setoids of type Setoid ℓ (c ⊔ ℓ), this does not work with the definition below,
+    -- since propositional equality lives on the same level as values, this means the type below would have to look like:
+    -- ‖_‖ : Setoid c (c ⊔ ℓ) → Setoid c c
+    -- this in turn does not play together nicely with later definition.
+
     -- discretize a setoid
     ‖_‖ : Setoid ℓ ℓ → Setoid ℓ ℓ
     ∣_∣ ‖ X ‖      = ∣ X ∣