From eaa955f3179162d76e7d98cf720e2e4d618bb18d Mon Sep 17 00:00:00 2001
From: Tom de Jong <43781735+tomdjong@users.noreply.github.com>
Date: Mon, 13 Nov 2023 16:25:42 +0000
Subject: [PATCH] Change the universal property of epimorphisms, so that it is
 stated with respect to all universe levels (#917)

---
 ...epimorphisms-with-respect-to-sets.lagda.md | 12 +++---
 ...s-with-respect-to-truncated-types.lagda.md | 37 ++++++++++---------
 2 files changed, 25 insertions(+), 24 deletions(-)

diff --git a/src/foundation/epimorphisms-with-respect-to-sets.lagda.md b/src/foundation/epimorphisms-with-respect-to-sets.lagda.md
index 59df999c3b..2812a2585b 100644
--- a/src/foundation/epimorphisms-with-respect-to-sets.lagda.md
+++ b/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
diff --git a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
index 3671f502fb..670a8b3df0 100644
--- a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
+++ b/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,10 +54,10 @@ 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)
 ```
 
@@ -64,8 +65,8 @@ is-epimorphism-is-epimorphism-succ-Truncated-Type l k f H X =
 
 ```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,10 +77,10 @@ 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)
 ```
 
@@ -87,12 +88,12 @@ is-epimorphism-is-truncation-equivalence-Truncated-Type l k f H X =
 
 ```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))