From dd0b385f1ac1a88da95b4dc4575555d51d4d6a81 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sat, 23 Nov 2024 17:08:58 +0530
Subject: [PATCH] Update Powerset.agda

Made it polymorphic in the level of the hProp being returned
---
 Cubical/Foundations/Powerset.agda | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/Cubical/Foundations/Powerset.agda b/Cubical/Foundations/Powerset.agda
index 043a0dfed8..1ef5b656eb 100644
--- a/Cubical/Foundations/Powerset.agda
+++ b/Cubical/Foundations/Powerset.agda
@@ -21,44 +21,44 @@ open import Cubical.Data.Sigma
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' : Level
     X : Type ℓ
 
-ℙ : Type ℓ → Type (ℓ-suc ℓ)
-ℙ X = X → hProp _
+ℙ : Type ℓ → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
+ℙ X ℓ' = X → hProp ℓ'
 
-isSetℙ : isSet (ℙ X)
+isSetℙ : isSet (ℙ X ℓ')
 isSetℙ = isSetΠ λ x → isSetHProp
 
 infix 5 _∈_
 
-_∈_ : {X : Type ℓ} → X → ℙ X → Type ℓ
+_∈_ : {X : Type ℓ} → X → ℙ X ℓ' → Type ℓ'
 x ∈ A = ⟨ A x ⟩
 
-_⊆_ : {X : Type ℓ} → ℙ X → ℙ X → Type ℓ
+_⊆_ : {X : Type ℓ} → ℙ X ℓ' → ℙ X ℓ' → Type (ℓ-max ℓ ℓ')
 A ⊆ B = ∀ x → x ∈ A → x ∈ B
 
-∈-isProp : (A : ℙ X) (x : X) → isProp (x ∈ A)
+∈-isProp : (A : ℙ X _) (x : X) → isProp (x ∈ A)
 ∈-isProp A = snd ∘ A
 
-⊆-isProp : (A B : ℙ X) → isProp (A ⊆ B)
+⊆-isProp : (A B : ℙ X _) → isProp (A ⊆ B)
 ⊆-isProp A B = isPropΠ2 (λ x _ → ∈-isProp B x)
 
-⊆-refl : (A : ℙ X) → A ⊆ A
+⊆-refl : (A : ℙ X _) → A ⊆ A
 ⊆-refl A x = idfun (x ∈ A)
 
-subst-∈ : (A : ℙ X) {x y : X} → x ≡ y → x ∈ A → y ∈ A
+subst-∈ : (A : ℙ X _) {x y : X} → x ≡ y → x ∈ A → y ∈ A
 subst-∈ A = subst (_∈ A)
 
-⊆-refl-consequence : (A B : ℙ X) → A ≡ B → (A ⊆ B) × (B ⊆ A)
+⊆-refl-consequence : (A B : ℙ X _) → A ≡ B → (A ⊆ B) × (B ⊆ A)
 ⊆-refl-consequence A B p = subst (A ⊆_) p (⊆-refl A)
                          , subst (B ⊆_) (sym p) (⊆-refl B)
 
-⊆-extensionality : (A B : ℙ X) → (A ⊆ B) × (B ⊆ A) → A ≡ B
+⊆-extensionality : (A B : ℙ X _) → (A ⊆ B) × (B ⊆ A) → A ≡ B
 ⊆-extensionality A B (φ , ψ) =
   funExt (λ x → TypeOfHLevel≡ 1 (hPropExt (A x .snd) (B x .snd) (φ x) (ψ x)))
 
-⊆-extensionalityEquiv : (A B : ℙ X) → (A ⊆ B) × (B ⊆ A) ≃ (A ≡ B)
+⊆-extensionalityEquiv : (A B : ℙ X _) → (A ⊆ B) × (B ⊆ A) ≃ (A ≡ B)
 ⊆-extensionalityEquiv A B = isoToEquiv (iso (⊆-extensionality A B)
                                             (⊆-refl-consequence A B)
                                             (λ _ → isSetℙ A B _ _)