diff --git a/libs/cubical b/libs/cubical
index 3a125a0..5b35333 160000
--- a/libs/cubical
+++ b/libs/cubical
@@ -1 +1 @@
-Subproject commit 3a125a0cb010903e6aa80569a0ca5339424eaf86
+Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
index 8a63dc4..67eeccc 100644
--- a/src/Cat/Wishlist.agda
+++ b/src/Cat/Wishlist.agda
@@ -4,13 +4,6 @@ open import Level
 open import Cubical.NType
 open import Data.Nat using (_≤_ ; z≤n ; s≤s)
 
-open import Cubical.NType.Properties public using (propHasLevel)
+open import Cubical.NType.Properties
 
 postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
-
-module _ {ℓ : Level} {A : Set ℓ} where
-  isSetIsProp : isProp (isSet A)
-  isSetIsProp = propHasLevel (S (S ⟨-2⟩))
-
-  propIsProp : isProp (isProp A)
-  propIsProp = propHasLevel (S ⟨-2⟩)