Change the universal property of epimorphisms, so that it is stated w…

…ith respect to all universe levels (#917)

src/foundation/epimorphisms-with-respect-to-sets.lagda.md

@@ -38,10 +38,10 @@ every set `C` the precomposition function `(B → C) → (A → C)` is an embedd
 
 ```agda
 is-epimorphism-Set :
-  {l1 l2 : Level} (l : Level) {A : UU l1} {B : UU l2}
-  (f : A → B) → UU (l1 ⊔ l2 ⊔ lsuc l)
-is-epimorphism-Set l f =
-  is-epimorphism-Truncated-Type l zero-𝕋 f
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  (f : A → B) → UUω
+is-epimorphism-Set f =
+  is-epimorphism-Truncated-Type zero-𝕋 f
 ```
 
 ## Properties
@@ -52,7 +52,7 @@ is-epimorphism-Set l f =
 abstract
   is-epimorphism-is-surjective-Set :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
-    is-surjective f → {l : Level} → is-epimorphism-Set l f
+    is-surjective f → is-epimorphism-Set f
   is-epimorphism-is-surjective-Set H C =
     is-emb-is-injective
       ( is-set-function-type (is-set-type-Set C))
@@ -73,7 +73,7 @@ abstract
 abstract
   is-surjective-is-epimorphism-Set :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
-    ({l : Level} → is-epimorphism-Set l f) → is-surjective f
+    is-epimorphism-Set f → is-surjective f
   is-surjective-is-epimorphism-Set {l1} {l2} {A} {B} {f} H b =
     map-equiv
       ( equiv-eq

src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md

@@ -41,10 +41,11 @@ is an embedding for every `k`-truncated type `X`.
 
 ```agda
 is-epimorphism-Truncated-Type :
-  {l1 l2 : Level} (l : Level) (k : 𝕋) {A : UU l1} {B : UU l2} →
-  (A → B) → UU (l1 ⊔ l2 ⊔ lsuc l)
-is-epimorphism-Truncated-Type l k f =
-  (X : Truncated-Type l k) → is-emb (precomp f (type-Truncated-Type X))
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
+  (A → B) → UUω
+is-epimorphism-Truncated-Type k f =
+  {l : Level} (X : Truncated-Type l k) →
+  is-emb (precomp f (type-Truncated-Type X))
 ```
 
 ## Properties
@@ -53,19 +54,19 @@ is-epimorphism-Truncated-Type l k f =
 
 ```agda
 is-epimorphism-is-epimorphism-succ-Truncated-Type :
-  {l1 l2 : Level} (l : Level) (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) →
-  is-epimorphism-Truncated-Type l (succ-𝕋 k) f →
-  is-epimorphism-Truncated-Type l k f
-is-epimorphism-is-epimorphism-succ-Truncated-Type l k f H X =
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) →
+  is-epimorphism-Truncated-Type (succ-𝕋 k) f →
+  is-epimorphism-Truncated-Type k f
+is-epimorphism-is-epimorphism-succ-Truncated-Type k f H X =
   H (truncated-type-succ-Truncated-Type k X)
 ```
 
 ### Every map is a `-1`-epimorphism
 
 ```agda
 is-neg-one-epimorphism :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
-  is-epimorphism-Truncated-Type l3 neg-one-𝕋 f
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
+  is-epimorphism-Truncated-Type neg-one-𝕋 f
 is-neg-one-epimorphism f P =
   is-emb-is-prop
     ( is-prop-function-type (is-prop-type-Prop P))
@@ -76,23 +77,23 @@ is-neg-one-epimorphism f P =
 
 ```agda
 is-epimorphism-is-truncation-equivalence-Truncated-Type :
-  {l1 l2 : Level} (l : Level) (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) →
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) →
   is-truncation-equivalence k f →
-  is-epimorphism-Truncated-Type l k f
-is-epimorphism-is-truncation-equivalence-Truncated-Type l k f H X =
+  is-epimorphism-Truncated-Type k f
+is-epimorphism-is-truncation-equivalence-Truncated-Type k f H X =
   is-emb-is-equiv (is-equiv-precomp-is-truncation-equivalence k f H X)
 ```
 
 ### A map is a `k`-epimorphism if and only if its `k`-truncation is a `k`-epimorphism
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B)
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B)
   where
 
   is-epimorphism-is-epimorphism-map-trunc-Truncated-Type :
-    is-epimorphism-Truncated-Type l3 k (map-trunc k f) →
-    is-epimorphism-Truncated-Type l3 k f
+    is-epimorphism-Truncated-Type k (map-trunc k f) →
+    is-epimorphism-Truncated-Type k f
   is-epimorphism-is-epimorphism-map-trunc-Truncated-Type H X =
     is-emb-bottom-is-emb-top-is-equiv-coherence-square-maps
       ( precomp (map-trunc k f) (type-Truncated-Type X))
@@ -111,8 +112,8 @@ module _
       ( H X)
 
   is-epimorphism-map-trunc-is-epimorphism-Truncated-Type :
-    is-epimorphism-Truncated-Type l3 k f →
-    is-epimorphism-Truncated-Type l3 k (map-trunc k f)
+    is-epimorphism-Truncated-Type k f →
+    is-epimorphism-Truncated-Type k (map-trunc k f)
   is-epimorphism-map-trunc-is-epimorphism-Truncated-Type H X =
     is-emb-top-is-emb-bottom-is-equiv-coherence-square-maps
       ( precomp (map-trunc k f) (type-Truncated-Type X))