diff --git a/Cubical/HITs/Nullification/Properties.agda b/Cubical/HITs/Nullification/Properties.agda
index abb809832..73fc3bdbf 100644
--- a/Cubical/HITs/Nullification/Properties.agda
+++ b/Cubical/HITs/Nullification/Properties.agda
@@ -175,7 +175,7 @@ isNullIsEquiv nullX nullY f =
 
 isNullEquiv :
   ∀ {ℓα ℓs ℓ} {A : Type ℓα} {S : A → Type ℓs}
-  {X Y : Type ℓ} → isNull S X → isNull S Y → isNull S (X ≃ Y)
+  {X : Type ℓ} {Y : Type ℓ'} → isNull S X → isNull S Y → isNull S (X ≃ Y)
 isNullEquiv nullX nullY = isNullΣ (isNullΠ (λ _ → nullY)) (isNullIsEquiv nullX nullY)
 
 isNullIsOfHLevel : (n : HLevel) → isNull S X → isNull S (isOfHLevel n X)