another minor universe level generalisation (#1177)

agda · Jan 6, 2025 · 2f085f5 · 2f085f5
1 parent a126e3f
commit 2f085f5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)