Raise subtypes to a universe level (#1277)

UniMath · Feb 5, 2025 · 260f8ac · 260f8ac
1 parent 065c73c
commit 260f8ac
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/src/foundation/raising-universe-levels.lagda.md b/src/foundation/raising-universe-levels.lagda.md
@@ -22,6 +22,7 @@ open import foundation-core.homotopies
 open import foundation-core.propositional-maps
 open import foundation-core.propositions
 open import foundation-core.sets
+open import foundation-core.subtypes
 ```
 
 </details>
@@ -97,6 +98,14 @@ pr2 (raise-Set l A) =
   is-set-equiv' (type-Set A) (compute-raise l (type-Set A)) (is-set-type-Set A)
 ```
 
+### Raising universe levels of subtypes
+
+```agda
+raise-subtype :
+  (l : Level) {l1 l2 : Level} → (A : UU l1) → subtype l2 A → subtype (l2 ⊔ l) A
+raise-subtype l A B x = raise-Prop l (B x)
+```
+
 ### Raising equivalent types
 
 ```agda