Make supertype implicit in raise-subtype (#1281)

This seems redundant in practice from my attempts to use it.
UniMath · Feb 5, 2025 · 83e7741 · 83e7741
1 parent eb58aa1
commit 83e7741
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/src/foundation/raising-universe-levels.lagda.md b/src/foundation/raising-universe-levels.lagda.md
@@ -102,8 +102,12 @@ pr2 (raise-Set l A) =
 
 ```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)
+  (l : Level) →
+  {l1 l2 : Level} →
+  {A : UU l1} →
+  subtype l2 A →
+  subtype (l2 ⊔ l) A
+raise-subtype l B x = raise-Prop l (B x)
 ```
 
 ### Raising equivalent types