From 2f085f5675066c0e1708752587ae788c036ade87 Mon Sep 17 00:00:00 2001 From: Andrew Swan Date: Mon, 6 Jan 2025 00:11:17 -0500 Subject: [PATCH] another minor universe level generalisation (#1177) --- 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)