chore: Universal properties of colimits quantify over all universe le…

…vels (#1126)

Refactors all universal properties and induction principles of colimits
to quantify over all universe levels. This still leaves some lemmas
about pushout cocones in an awkward position, but I leave that for
future work.

src/foundation/epimorphisms.lagda.md

@@ -99,7 +99,7 @@ module _
 
   universal-property-pushout-is-epimorphism :
     is-epimorphism f →
-    {l : Level} → universal-property-pushout l f f (cocone-codiagonal-map f)
+    universal-property-pushout f f (cocone-codiagonal-map f)
   universal-property-pushout-is-epimorphism e X =
     is-equiv-comp
       ( map-equiv (compute-total-fiber-precomp f X))
@@ -134,7 +134,7 @@ If the map `f : A → B` is epi, then its codiagonal is an equivalence.
 ```agda
   is-epimorphism-universal-property-pushout-Level :
     {l : Level} →
-    universal-property-pushout l f f (cocone-codiagonal-map f) →
+    universal-property-pushout-Level l f f (cocone-codiagonal-map f) →
     is-epimorphism-Level l f
   is-epimorphism-universal-property-pushout-Level up-c X =
     is-emb-is-contr-fibers-values
@@ -153,7 +153,7 @@ If the map `f : A → B` is epi, then its codiagonal is an equivalence.
             ( g)))
 
   is-epimorphism-universal-property-pushout :
-    ({l : Level} → universal-property-pushout l f f (cocone-codiagonal-map f)) →
+    universal-property-pushout f f (cocone-codiagonal-map f) →
     is-epimorphism f
   is-epimorphism-universal-property-pushout up-c =
     is-epimorphism-universal-property-pushout-Level up-c

src/synthetic-homotopy-theory/26-descent.lagda.md

@@ -218,7 +218,7 @@ triangle-desc-fam {l = l} {S} {A} {B} {X} (pair i (pair j H)) P =
 is-equiv-desc-fam :
   {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   {f : S → A} {g : S → B} (c : cocone f g X) →
-  ({l' : Level} → universal-property-pushout l' f g c) →
+  universal-property-pushout f g c →
   is-equiv (desc-fam {l = l} {f = f} {g} c)
 is-equiv-desc-fam {l = l} {f = f} {g} c up-c =
   is-equiv-left-map-triangle
@@ -232,7 +232,7 @@ is-equiv-desc-fam {l = l} {f = f} {g} c up-c =
 equiv-desc-fam :
   {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   {f : S → A} {g : S → B} (c : cocone f g X) →
-  ({l' : Level} → universal-property-pushout l' f g c) →
+  universal-property-pushout f g c →
   (X → UU l) ≃ Fam-pushout l f g
 equiv-desc-fam c up-c =
   pair
@@ -246,7 +246,7 @@ equiv-desc-fam c up-c =
 uniqueness-Fam-pushout :
   {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   (f : S → A) (g : S → B) (c : cocone f g X) →
-  ({l' : Level} → universal-property-pushout l' f g c) →
+  universal-property-pushout f g c →
   ( P : Fam-pushout l f g) →
   is-contr
     ( Σ (X → UU l) (λ Q →
@@ -262,24 +262,24 @@ uniqueness-Fam-pushout {l = l} f g c up-c P =
 fam-Fam-pushout :
   {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   {f : S → A} {g : S → B} (c : cocone f g X) →
-  (up-X : {l' : Level} → universal-property-pushout l' f g c) →
-  Fam-pushout l f g → (X → UU l)
+  universal-property-pushout f g c →
+  Fam-pushout l f g → X → UU l
 fam-Fam-pushout {f = f} {g} c up-X P =
   pr1 (center (uniqueness-Fam-pushout f g c up-X P))
 
 is-section-fam-Fam-pushout :
   {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   {f : S → A} {g : S → B} (c : cocone f g X) →
-  (up-X : {l' : Level} → universal-property-pushout l' f g c) →
-  ((desc-fam {l = l} c) ∘ (fam-Fam-pushout c up-X)) ~ id
+  (up-X : universal-property-pushout f g c) →
+  desc-fam {l = l} c ∘ fam-Fam-pushout c up-X ~ id
 is-section-fam-Fam-pushout {f = f} {g} c up-X P =
   inv
     ( eq-equiv-Fam-pushout (pr2 (center (uniqueness-Fam-pushout f g c up-X P))))
 
 compute-left-fam-Fam-pushout :
   { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   { f : S → A} {g : S → B} (c : cocone f g X) →
-  ( up-X : {l' : Level} → universal-property-pushout l' f g c) →
+  ( up-X : universal-property-pushout f g c) →
   ( P : Fam-pushout l f g) →
   ( a : A) → (pr1 P a) ≃ (fam-Fam-pushout c up-X P (pr1 c a))
 compute-left-fam-Fam-pushout {f = f} {g} c up-X P =
@@ -288,7 +288,7 @@ compute-left-fam-Fam-pushout {f = f} {g} c up-X P =
 compute-right-fam-Fam-pushout :
   { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   { f : S → A} {g : S → B} (c : cocone f g X) →
-  ( up-X : {l' : Level} → universal-property-pushout l' f g c) →
+  ( up-X : universal-property-pushout f g c) →
   ( P : Fam-pushout l f g) →
   ( b : B) → (pr1 (pr2 P) b) ≃ (fam-Fam-pushout c up-X P (pr1 (pr2 c) b))
 compute-right-fam-Fam-pushout {f = f} {g} c up-X P =
@@ -297,7 +297,7 @@ compute-right-fam-Fam-pushout {f = f} {g} c up-X P =
 compute-path-fam-Fam-pushout :
   { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   { f : S → A} {g : S → B} (c : cocone f g X) →
-  ( up-X : {l' : Level} → universal-property-pushout l' f g c) →
+  ( up-X : universal-property-pushout f g c) →
   ( P : Fam-pushout l f g) →
   ( s : S) →
     ( ( map-equiv (compute-right-fam-Fam-pushout c up-X P (g s))) ∘

src/synthetic-homotopy-theory/26-id-pushout.lagda.md

@@ -247,7 +247,7 @@ triangle-hom-Fam-pushout-dependent-cocone {f = f} {g} c P Q h =
 is-equiv-hom-Fam-pushout-map :
   { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   { f : S → A} {g : S → B} (c : cocone f g X) →
-  ( up-X : {l : Level} → universal-property-pushout l f g c)
+  ( up-X : universal-property-pushout f g c)
   ( P : X → UU l5) (Q : X → UU l6) →
   is-equiv (hom-Fam-pushout-map c P Q)
 is-equiv-hom-Fam-pushout-map {l5 = l5} {l6} {f = f} {g} c up-X P Q =
@@ -263,7 +263,7 @@ is-equiv-hom-Fam-pushout-map {l5 = l5} {l6} {f = f} {g} c up-X P Q =
 equiv-hom-Fam-pushout-map :
   { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   { f : S → A} {g : S → B} (c : cocone f g X) →
-  ( up-X : {l : Level} → universal-property-pushout l f g c)
+  ( up-X : universal-property-pushout f g c)
   ( P : X → UU l5) (Q : X → UU l6) →
   ( (x : X) → P x → Q x) ≃
   hom-Fam-pushout (desc-fam c P) (desc-fam c Q)
@@ -308,7 +308,7 @@ triangle-is-universal-id-Fam-pushout' c a Q = refl-htpy
 is-universal-id-Fam-pushout' :
   { l l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   { f : S → A} {g : S → B} (c : cocone f g X)
-  ( up-X : {l' : Level} → universal-property-pushout l' f g c) (a : A) →
+  ( up-X : universal-property-pushout f g c) (a : A) →
   ( Q : (x : X) → UU l) →
   is-equiv
     ( ev-point-hom-Fam-pushout
@@ -331,7 +331,7 @@ is-universal-id-Fam-pushout :
   { l1 l2 l3 l4 l : Level}
   { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   { f : S → A} {g : S → B} (c : cocone f g X)
-  ( up-X : {l' : Level} → universal-property-pushout l' f g c) (a : A) →
+  ( up-X : universal-property-pushout f g c) (a : A) →
   is-universal-Fam-pushout l (desc-fam c (Id (pr1 c a))) a refl
 is-universal-id-Fam-pushout {S = S} {A} {B} {X} {f} {g} c up-X a Q =
   map-inv-equiv
@@ -440,7 +440,7 @@ equiv-is-equiv-hom-Fam-pushout P Q h is-equiv-h =
 hom-identity-is-universal-Fam-pushout :
   { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l5}
   { f : S → A} {g : S → B} (c : cocone f g X) →
-  ( up-X : (l : Level) → universal-property-pushout l f g c) →
+  ( up-X : universal-property-pushout f g c) →
   ( P : Fam-pushout l4 f g) (a : A) (p : pr1 P a) →
   is-universal-Fam-pushout l5 P a p →
   Σ ( hom-Fam-pushout P (desc-fam c (Id (pr1 c a))))
@@ -451,7 +451,7 @@ hom-identity-is-universal-Fam-pushout {f = f} {g} c up-X P a p is-univ-P =
 is-identity-is-universal-Fam-pushout :
   { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l5}
   { f : S → A} {g : S → B} (c : cocone f g X) →
-  ( up-X : (l : Level) → universal-property-pushout l f g c) →
+  ( up-X : universal-property-pushout f g c) →
   ( P : Fam-pushout l4 f g) (a : A) (p : pr1 P a) →
   is-universal-Fam-pushout l5 P a p →
   Σ ( equiv-Fam-pushout P (desc-fam c (Id (pr1 c a))))

src/synthetic-homotopy-theory/circle.lagda.md

@@ -67,7 +67,7 @@ free-loop-𝕊¹ = base-𝕊¹ , loop-𝕊¹
 𝕊¹-Pointed-Type = 𝕊¹ , base-𝕊¹
 
 postulate
-  ind-𝕊¹ : {l : Level} → induction-principle-circle l free-loop-𝕊¹
+  ind-𝕊¹ : induction-principle-circle free-loop-𝕊¹
 ```
 
 ## Properties
@@ -76,7 +76,7 @@ postulate
 
 ```agda
 dependent-universal-property-𝕊¹ :
-  {l : Level} → dependent-universal-property-circle l free-loop-𝕊¹
+  dependent-universal-property-circle free-loop-𝕊¹
 dependent-universal-property-𝕊¹ =
   dependent-universal-property-induction-principle-circle free-loop-𝕊¹ ind-𝕊¹
 
@@ -127,12 +127,11 @@ module _
 ### The universal property of the circle
 
 ```agda
-universal-property-𝕊¹ :
-  {l : Level} → universal-property-circle l free-loop-𝕊¹
+universal-property-𝕊¹ : universal-property-circle free-loop-𝕊¹
 universal-property-𝕊¹ =
   universal-property-dependent-universal-property-circle
-    free-loop-𝕊¹
-    dependent-universal-property-𝕊¹
+    ( free-loop-𝕊¹)
+    ( dependent-universal-property-𝕊¹)
 
 uniqueness-universal-property-𝕊¹ :
   {l : Level} {X : UU l} (α : free-loop X) →

src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md

@@ -109,8 +109,7 @@ module _
     cocone-hom-arrow f g hom-arrow-cocartesian-hom-arrow
 
   universal-property-cocartesian-hom-arrow :
-    {l : Level} →
-    universal-property-pushout l
+    universal-property-pushout
       ( f)
       ( map-domain-cocartesian-hom-arrow)
       ( cocone-cocartesian-hom-arrow)

src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md

@@ -93,7 +93,7 @@ module _
         ( terminal-map (fiber f b))
         ( terminal-map (fiber f b))
         ( fiber (codiagonal-map f) b))
-      ( universal-property-pushout l
+      ( universal-property-pushout-Level l
         ( terminal-map (fiber f b))
         ( terminal-map (fiber f b)))
   universal-property-suspension-cocone-fiber =
@@ -121,8 +121,7 @@ module _
     pr1 (universal-property-suspension-cocone-fiber {lzero})
 
   universal-property-suspension-fiber :
-    {l : Level} →
-    universal-property-pushout l
+    universal-property-pushout
       ( terminal-map (fiber f b))
       ( terminal-map (fiber f b))
       ( suspension-cocone-fiber)

src/synthetic-homotopy-theory/coequalizers.lagda.md

@@ -77,9 +77,7 @@ module _
           ( horizontal-map-span-cocone-cofork a))
 
     dup-standard-coequalizer :
-      {l : Level} →
-      dependent-universal-property-coequalizer l a
-        ( cofork-standard-coequalizer)
+      dependent-universal-property-coequalizer a cofork-standard-coequalizer
     dup-standard-coequalizer =
       dependent-universal-property-coequalizer-dependent-universal-property-pushout
         ( a)
@@ -105,8 +103,7 @@ module _
               ( P)))
 
     up-standard-coequalizer :
-      {l : Level} →
-      universal-property-coequalizer l a cofork-standard-coequalizer
+      universal-property-coequalizer a cofork-standard-coequalizer
     up-standard-coequalizer =
       universal-property-dependent-universal-property-coequalizer a
         ( cofork-standard-coequalizer)

src/synthetic-homotopy-theory/cofibers.lagda.md

@@ -58,8 +58,8 @@ module _
   pr2 (cofiber-Pointed-Type f) = point-cofiber f
 
   universal-property-cofiber :
-    (f : A → B) {l : Level} →
-    universal-property-pushout l f (terminal-map A) (cocone-cofiber f)
+    (f : A → B) →
+    universal-property-pushout f (terminal-map A) (cocone-cofiber f)
   universal-property-cofiber f = up-pushout f (terminal-map A)
 ```
 

src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md

@@ -68,11 +68,11 @@ pr2 (pr2 (cone-dependent-pullback-property-pushout f g (i , j , H) P)) h =
   eq-htpy (λ s → apd h (H s))
 
 dependent-pullback-property-pushout :
-  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
   (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
-  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
-dependent-pullback-property-pushout l {S} {A} {B} f g {X} (i , j , H) =
-  (P : X → UU l) →
+  UUω
+dependent-pullback-property-pushout {S = S} {A} {B} f g {X} (i , j , H) =
+  {l : Level} (P : X → UU l) →
   is-pullback
     ( λ (h : (a : A) → P (i a)) → λ s → tr P (H s) (h (f s)))
     ( λ (h : (b : B) → P (j b)) → λ s → h (g s))
@@ -105,8 +105,8 @@ module _
   where
 
   pullback-property-dependent-pullback-property-pushout :
-    ({l : Level} → dependent-pullback-property-pushout l f g c) →
-    ({l : Level} → pullback-property-pushout l f g c)
+    dependent-pullback-property-pushout f g c →
+    pullback-property-pushout f g c
   pullback-property-dependent-pullback-property-pushout dpp-c Y =
     is-pullback-htpy
       ( λ h →
@@ -222,7 +222,7 @@ pullback property.
 
   is-pullback-cone-family-dependent-pullback-family :
     {l : Level} (P : X → UU l) →
-    ({l : Level} → pullback-property-pushout l f g c) →
+    pullback-property-pushout f g c →
     (γ : X → X) →
     is-pullback
       ( ( tr
@@ -271,8 +271,8 @@ pullback property.
         ( pp-c (Σ X P)))
 
   dependent-pullback-property-pullback-property-pushout :
-    ({l : Level} → pullback-property-pushout l f g c) →
-    ({l : Level} → dependent-pullback-property-pushout l f g c)
+    pullback-property-pushout f g c →
+    dependent-pullback-property-pushout f g c
   dependent-pullback-property-pullback-property-pushout pp-c P =
     is-pullback-htpy'
       ( ( tr-lift-family-of-elements-precomp P id

src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md

@@ -44,18 +44,18 @@ dependent-cofork-map : ((x : X) → P x) → dependent-cocone e P.
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (l : Level) (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
   (e : cofork a X)
   where
 
-  dependent-universal-property-coequalizer : UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l)
+  dependent-universal-property-coequalizer : UUω
   dependent-universal-property-coequalizer =
-    (P : X → UU l) → is-equiv (dependent-cofork-map a e {P = P})
+    {l : Level} (P : X → UU l) → is-equiv (dependent-cofork-map a e {P = P})
 
 module _
   {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
   (e : cofork a X) {P : X → UU l4}
-  (dup-coequalizer : dependent-universal-property-coequalizer l4 a e)
+  (dup-coequalizer : dependent-universal-property-coequalizer a e)
   where
 
   map-dependent-universal-property-coequalizer :
@@ -73,7 +73,7 @@ module _
 module _
   {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
   (e : cofork a X) {P : X → UU l4}
-  (dup-coequalizer : dependent-universal-property-coequalizer l4 a e)
+  (dup-coequalizer : dependent-universal-property-coequalizer a e)
   (k : dependent-cofork a e P)
   where
 
@@ -127,13 +127,11 @@ module _
   where
 
   dependent-universal-property-coequalizer-dependent-universal-property-pushout :
-    ({l : Level} →
-      dependent-universal-property-pushout l
-        ( vertical-map-span-cocone-cofork a)
-        ( horizontal-map-span-cocone-cofork a)
-        ( cocone-codiagonal-cofork a e)) →
-    ({l : Level} →
-      dependent-universal-property-coequalizer l a e)
+    dependent-universal-property-pushout
+      ( vertical-map-span-cocone-cofork a)
+      ( horizontal-map-span-cocone-cofork a)
+      ( cocone-codiagonal-cofork a e) →
+    dependent-universal-property-coequalizer a e
   dependent-universal-property-coequalizer-dependent-universal-property-pushout
     ( dup-pushout)
     ( P) =
@@ -150,13 +148,11 @@ module _
       ( is-equiv-dependent-cofork-dependent-cocone-codiagonal a e P)
 
   dependent-universal-property-pushout-dependent-universal-property-coequalizer :
-    ({l : Level} →
-      dependent-universal-property-coequalizer l a e) →
-    ({l : Level} →
-      dependent-universal-property-pushout l
-        ( vertical-map-span-cocone-cofork a)
-        ( horizontal-map-span-cocone-cofork a)
-        ( cocone-codiagonal-cofork a e))
+    dependent-universal-property-coequalizer a e →
+    dependent-universal-property-pushout
+      ( vertical-map-span-cocone-cofork a)
+      ( horizontal-map-span-cocone-cofork a)
+      ( cocone-codiagonal-cofork a e)
   dependent-universal-property-pushout-dependent-universal-property-coequalizer
     ( dup-coequalizer)
     ( P) =
@@ -182,8 +178,8 @@ module _
   where
 
   universal-property-dependent-universal-property-coequalizer :
-    ({l : Level} → dependent-universal-property-coequalizer l a e) →
-    ({l : Level} → universal-property-coequalizer l a e)
+    dependent-universal-property-coequalizer a e →
+    universal-property-coequalizer a e
   universal-property-dependent-universal-property-coequalizer
     ( dup-coequalizer)
     ( Y) =
@@ -197,8 +193,8 @@ module _
         ( compute-dependent-cofork-constant-family a e Y))
 
   dependent-universal-property-universal-property-coequalizer :
-    ({l : Level} → universal-property-coequalizer l a e) →
-    ({l : Level} → dependent-universal-property-coequalizer l a e)
+    universal-property-coequalizer a e →
+    dependent-universal-property-coequalizer a e
   dependent-universal-property-universal-property-coequalizer up-coequalizer =
     dependent-universal-property-coequalizer-dependent-universal-property-pushout
       ( a)