diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index af52c8b..3fa14ce 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -7,7 +7,6 @@ open import Cat.Prelude as P
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
-open import Cat.Wishlist
 open import Cat.Equivalence
 
 _⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index d8b20a8..1a7223d 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -25,7 +25,6 @@ module Nat = Data.Nat
 
 open import Cat.Category
 open import Cat.Category.Functor
-open import Cat.Wishlist
 
 module Cat.Category.NaturalTransformation
   {ℓc ℓc' ℓd ℓd' : Level}
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index 71e5cbd..6835262 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -98,4 +98,10 @@ module _ {ℓ : Level} {A : Set ℓ} {a : A} where
     _ ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
     a ∎
 
-open import Cat.Wishlist public
+module _ {ℓ : Level} {A : Set ℓ} where
+  open import Cubical.NType
+  open import Data.Nat using (_≤′_ ;  ≤′-refl ;  ≤′-step ; zero ; suc)
+  open import Cubical.NType.Properties
+  ntypeCumulative : ∀ {n m} → n ≤′ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+  ntypeCumulative {m}         ≤′-refl      lvl = lvl
+  ntypeCumulative {n} {suc m} (≤′-step le) lvl = HasLevel+1 ⟨ m ⟩₋₂ (ntypeCumulative le lvl)
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
deleted file mode 100644
index 37b8c87..0000000
--- a/src/Cat/Wishlist.agda
+++ /dev/null
@@ -1,16 +0,0 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-module Cat.Wishlist where
-
-open import Level hiding (suc; zero)
-open import Cubical
-open import Cubical.NType
-open import Data.Nat using (_≤′_ ;  ≤′-refl ;  ≤′-step ; zero ; suc)
-open import Agda.Builtin.Sigma
-
-open import Cubical.NType.Properties
-
-
-module _ {ℓ : Level} {A : Set ℓ} where
-  ntypeCumulative : ∀ {n m} → n ≤′ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
-  ntypeCumulative {m}         ≤′-refl      lvl = lvl
-  ntypeCumulative {n} {suc m} (≤′-step le) lvl = HasLevel+1 ⟨ m ⟩₋₂ (ntypeCumulative le lvl)