From 3b7b80cb4657da588b646893512fef8539a7453f Mon Sep 17 00:00:00 2001 From: Andrew Swan Date: Sun, 5 Jan 2025 15:48:26 +0100 Subject: [PATCH] another minor universe level generalisation --- Cubical/HITs/Nullification/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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)