Refactor universal properties for various limits (#963)

UniMath · Dec 10, 2023 · 1d782a7 · 1d782a7
1 parent 2101307
commit 1d782a7
Show file tree

Hide file tree

Showing 24 changed files with 362 additions and 389 deletions.
diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
@@ -171,8 +171,7 @@ module _
 
   abstract
     universal-property-pullback-standard-pullback :
-      {l : Level} →
-      universal-property-pullback l f g (cone-standard-pullback f g)
+      universal-property-pullback f g (cone-standard-pullback f g)
     universal-property-pullback-standard-pullback C =
       is-equiv-comp
         ( tot (λ p → map-distributive-Π-Σ))
@@ -208,8 +207,7 @@ module _
 
   abstract
     is-pullback-universal-property-pullback :
-      (c : cone f g C) →
-      ({l : Level} → universal-property-pullback l f g c) → is-pullback f g c
+      (c : cone f g C) → universal-property-pullback f g c → is-pullback f g c
     is-pullback-universal-property-pullback c =
       is-equiv-up-pullback-up-pullback
         ( cone-standard-pullback f g)
@@ -221,7 +219,7 @@ module _
   abstract
     universal-property-pullback-is-pullback :
       (c : cone f g C) → is-pullback f g c →
-      {l : Level} → universal-property-pullback l f g c
+      universal-property-pullback f g c
     universal-property-pullback-is-pullback c is-pullback-c =
       up-pullback-up-pullback-is-equiv
         ( cone-standard-pullback f g)
@@ -652,8 +650,8 @@ module _
 
   abstract
     universal-property-pullback-is-fiberwise-equiv :
-      is-fiberwise-equiv g → {l : Level} →
-      universal-property-pullback l f pr1 cone-map-Σ
+      is-fiberwise-equiv g →
+      universal-property-pullback f pr1 cone-map-Σ
     universal-property-pullback-is-fiberwise-equiv is-equiv-g =
       universal-property-pullback-is-pullback f pr1 cone-map-Σ
         ( is-pullback-is-fiberwise-equiv is-equiv-g)
@@ -671,7 +669,7 @@ module _
 
   abstract
     is-fiberwise-equiv-universal-property-pullback :
-      ( {l : Level} → universal-property-pullback l f pr1 cone-map-Σ) →
+      ( universal-property-pullback f pr1 cone-map-Σ) →
       is-fiberwise-equiv g
     is-fiberwise-equiv-universal-property-pullback up =
       is-fiberwise-equiv-is-pullback

diff --git a/src/foundation-core/universal-property-pullbacks.lagda.md b/src/foundation-core/universal-property-pullbacks.lagda.md
@@ -31,28 +31,27 @@ open import foundation-core.identity-types
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (l : Level) {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) {C : UU l4}
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) {C : UU l4} (c : cone f g C)
   where
 
-  universal-property-pullback :
-    (c : cone f g C) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
-  universal-property-pullback c =
-    (C' : UU l) → is-equiv (cone-map f g c {C'})
+  universal-property-pullback : UUω
+  universal-property-pullback =
+    {l : Level} (C' : UU l) → is-equiv (cone-map f g c {C'})
 
 module _
   {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
   (f : A → X) (g : B → X) {C : UU l4} (c : cone f g C)
   where
 
   map-universal-property-pullback :
-    ({l : Level} → universal-property-pullback l f g c) →
+    universal-property-pullback f g c →
     {C' : UU l5} (c' : cone f g C') → C' → C
   map-universal-property-pullback up-c {C'} c' =
     map-inv-is-equiv (up-c C') c'
 
   compute-map-universal-property-pullback :
-    (up-c : {l : Level} → universal-property-pullback l f g c) →
+    (up-c : universal-property-pullback f g c) →
     {C' : UU l5} (c' : cone f g C') →
     cone-map f g c (map-universal-property-pullback up-c c') ＝ c'
   compute-map-universal-property-pullback up-c {C'} c' =
@@ -86,8 +85,8 @@ module _
 
   abstract
     is-equiv-up-pullback-up-pullback :
-      ({l : Level} → universal-property-pullback l f g c) →
-      ({l : Level} → universal-property-pullback l f g c') →
+      universal-property-pullback f g c →
+      universal-property-pullback f g c' →
       is-equiv h
     is-equiv-up-pullback-up-pullback up up' =
       is-equiv-is-equiv-postcomp h
@@ -103,8 +102,8 @@ module _
   abstract
     up-pullback-up-pullback-is-equiv :
       is-equiv h →
-      ({l : Level} → universal-property-pullback l f g c) →
-      ({l : Level} → universal-property-pullback l f g c')
+      universal-property-pullback f g c →
+      universal-property-pullback f g c'
     up-pullback-up-pullback-is-equiv is-equiv-h up D =
       is-equiv-left-map-triangle
         ( cone-map f g c')
@@ -116,9 +115,9 @@ module _
 
   abstract
     up-pullback-is-equiv-up-pullback :
-      ({l : Level} → universal-property-pullback l f g c') →
+      universal-property-pullback f g c' →
       is-equiv h →
-      ({l : Level} → universal-property-pullback l f g c)
+      universal-property-pullback f g c
     up-pullback-is-equiv-up-pullback up' is-equiv-h D =
       is-equiv-right-map-triangle
         ( cone-map f g c')
@@ -139,7 +138,7 @@ module _
 
   abstract
     uniqueness-universal-property-pullback :
-      ({l : Level} → universal-property-pullback l f g c) →
+      universal-property-pullback f g c →
       {l5 : Level} (C' : UU l5) (c' : cone f g C') →
       is-contr (Σ (C' → C) (λ h → htpy-cone f g (cone-map f g c h) c'))
     uniqueness-universal-property-pullback up C' c' =

diff --git a/src/foundation-core/universal-property-truncation.lagda.md b/src/foundation-core/universal-property-truncation.lagda.md
@@ -46,33 +46,35 @@ precomp-Trunc :
   (B → type-Truncated-Type C) → (A → type-Truncated-Type C)
 precomp-Trunc f C = precomp f (type-Truncated-Type C)
 
-is-truncation :
-  (l : Level) {l1 l2 : Level} {k : 𝕋} {A : UU l1}
-  (B : Truncated-Type l2 k) → (A → type-Truncated-Type B) →
-  UU (l1 ⊔ l2 ⊔ lsuc l)
-is-truncation l {k = k} B f =
-  (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C)
-
-equiv-is-truncation :
-  {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k)
-  (f : A → type-Truncated-Type B)
-  (H : {l : Level} → is-truncation l B f) →
-  (C : Truncated-Type l3 k) →
-  (type-Truncated-Type B → type-Truncated-Type C) ≃ (A → type-Truncated-Type C)
-pr1 (equiv-is-truncation B f H C) = precomp-Trunc f C
-pr2 (equiv-is-truncation B f H C) = H C
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1}
+  (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B)
+  where
+
+  is-truncation : UUω
+  is-truncation =
+    {l : Level} (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C)
+
+  equiv-is-truncation :
+    {l3 : Level} (H : is-truncation) (C : Truncated-Type l3 k) →
+    ( type-Truncated-Type B → type-Truncated-Type C) ≃
+    ( A → type-Truncated-Type C)
+  pr1 (equiv-is-truncation H C) = precomp-Trunc f C
+  pr2 (equiv-is-truncation H C) = H C
 ```
 
 ### The universal property of truncations
 
 ```agda
-universal-property-truncation :
-  (l : Level) {l1 l2 : Level} {k : 𝕋} {A : UU l1}
-  (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) →
-  UU (lsuc l ⊔ l1 ⊔ l2)
-universal-property-truncation l {k = k} {A} B f =
-  (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
-  is-contr (Σ (type-hom-Truncated-Type k B C) (λ h → (h ∘ f) ~ g))
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1}
+  (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B)
+  where
+
+  universal-property-truncation : UUω
+  universal-property-truncation =
+    {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
+    is-contr (Σ (type-hom-Truncated-Type k B C) (λ h → h ∘ f ~ g))
 ```
 
 ### The dependent universal property of truncations
@@ -85,12 +87,15 @@ precomp-Π-Truncated-Type :
   ((a : A) → type-Truncated-Type (C (f a)))
 precomp-Π-Truncated-Type f C h a = h (f a)
 
-dependent-universal-property-truncation :
-  {l1 l2 : Level} (l : Level) {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k)
-  (f : A → type-Truncated-Type B) → UU (l1 ⊔ l2 ⊔ lsuc l)
-dependent-universal-property-truncation l {k} B f =
-  (X : type-Truncated-Type B → Truncated-Type l k) →
-  is-equiv (precomp-Π-Truncated-Type f X)
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1}
+  (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B)
+  where
+
+  dependent-universal-property-truncation : UUω
+  dependent-universal-property-truncation =
+    {l : Level} (X : type-Truncated-Type B → Truncated-Type l k) →
+    is-equiv (precomp-Π-Truncated-Type f X)
 ```
 
 ## Properties
@@ -101,15 +106,15 @@ dependent-universal-property-truncation l {k} B f =
 abstract
   is-truncation-id :
     {l1 : Level} {k : 𝕋} {A : UU l1} (H : is-trunc k A) →
-    {l : Level} → is-truncation l (A , H) id
+    is-truncation (A , H) id
   is-truncation-id H B =
     is-equiv-precomp-is-equiv id is-equiv-id (type-Truncated-Type B)
 
 abstract
   is-truncation-equiv :
     {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k)
     (e : A ≃ type-Truncated-Type B) →
-    {l : Level} → is-truncation l B (map-equiv e)
+    is-truncation B (map-equiv e)
   is-truncation-equiv B e C =
     is-equiv-precomp-is-equiv
       ( map-equiv e)
@@ -127,8 +132,7 @@ module _
 
   abstract
     is-truncation-universal-property-truncation :
-      ({l : Level} → universal-property-truncation l B f) →
-      ({l : Level} → is-truncation l B f)
+      universal-property-truncation B f → is-truncation B f
     is-truncation-universal-property-truncation H C =
       is-equiv-is-contr-map
         ( λ g →
@@ -139,25 +143,24 @@ module _
 
   abstract
     universal-property-truncation-is-truncation :
-      ({l : Level} → is-truncation l B f) →
-      ({l : Level} → universal-property-truncation l B f)
+      is-truncation B f → universal-property-truncation B f
     universal-property-truncation-is-truncation H C g =
       is-contr-equiv'
         ( Σ (type-hom-Truncated-Type k B C) (λ h → (h ∘ f) ＝ g))
         ( equiv-tot (λ h → equiv-funext))
         ( is-contr-map-is-equiv (H C) g)
 
   map-is-truncation :
-    ({l : Level} → is-truncation l B f) →
-    ({l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
-    type-hom-Truncated-Type k B C)
+    is-truncation B f →
+    {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
+    type-hom-Truncated-Type k B C
   map-is-truncation H C g =
     pr1 (center (universal-property-truncation-is-truncation H C g))
 
   triangle-is-truncation :
-    (H : {l : Level} → is-truncation l B f) →
+    (H : is-truncation B f) →
     {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
-    (map-is-truncation H C g ∘ f) ~ g
+    map-is-truncation H C g ∘ f ~ g
   triangle-is-truncation H C g =
     pr2 (center (universal-property-truncation-is-truncation H C g))
 ```
@@ -172,8 +175,8 @@ module _
 
   abstract
     dependent-universal-property-truncation-is-truncation :
-      ({l : Level} → is-truncation l B f) →
-      {l : Level} → dependent-universal-property-truncation l B f
+      is-truncation B f →
+      dependent-universal-property-truncation B f
     dependent-universal-property-truncation-is-truncation H X =
       is-fiberwise-equiv-is-equiv-map-Σ
         ( λ (h : A → type-Truncated-Type B) →
@@ -191,20 +194,18 @@ module _
 
   abstract
     is-truncation-dependent-universal-property-truncation :
-      ({l : Level} → dependent-universal-property-truncation l B f) →
-      {l : Level} → is-truncation l B f
-    is-truncation-dependent-universal-property-truncation H X =
-      H (λ b → X)
+      dependent-universal-property-truncation B f → is-truncation B f
+    is-truncation-dependent-universal-property-truncation H X = H (λ _ → X)
 
   section-is-truncation :
-    ({l : Level} → is-truncation l B f) →
+    is-truncation B f →
     {l3 : Level} (C : Truncated-Type l3 k)
     (h : A → type-Truncated-Type C) (g : type-hom-Truncated-Type k C B) →
-    f ~ (g ∘ h) → section g
+    f ~ g ∘ h → section g
   section-is-truncation H C h g K =
     map-distributive-Π-Σ
       ( map-inv-is-equiv
         ( dependent-universal-property-truncation-is-truncation H
           ( fiber-Truncated-Type C B g))
-        ( λ a → h a , inv (K a)))
+        ( λ a → (h a , inv (K a))))
 ```
diff --git a/src/foundation/fibers-of-maps.lagda.md b/src/foundation/fibers-of-maps.lagda.md
@@ -55,7 +55,7 @@ module _
 
   abstract
     universal-property-pullback-cone-fiber :
-      {l : Level} → universal-property-pullback l f (const unit B b) cone-fiber
+      universal-property-pullback f (const unit B b) cone-fiber
     universal-property-pullback-cone-fiber =
       universal-property-pullback-is-pullback f
         ( const unit B b)

diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md
@@ -119,26 +119,26 @@ abstract
 ```agda
 abstract
   is-propositional-truncation-trunc-Prop :
-    {l1 l2 : Level} (A : UU l1) →
-    is-propositional-truncation l2 (trunc-Prop A) unit-trunc-Prop
+    {l : Level} (A : UU l) →
+    is-propositional-truncation (trunc-Prop A) unit-trunc-Prop
   is-propositional-truncation-trunc-Prop A =
     is-propositional-truncation-extension-property
       ( trunc-Prop A)
       ( unit-trunc-Prop)
-      ( λ {l} Q → ind-trunc-Prop (λ x → Q))
+      ( λ Q → ind-trunc-Prop (λ x → Q))
 ```
 
 ### The defined propositional truncations satisfy the universal property of propositional truncations
 
 ```agda
 abstract
   universal-property-trunc-Prop :
-    {l1 l2 : Level} (A : UU l1) →
-    universal-property-propositional-truncation l2
+    {l : Level} (A : UU l) →
+    universal-property-propositional-truncation
       ( trunc-Prop A)
       ( unit-trunc-Prop)
   universal-property-trunc-Prop A =
-    universal-property-is-propositional-truncation _
+    universal-property-is-propositional-truncation
       ( trunc-Prop A)
       ( unit-trunc-Prop)
       ( is-propositional-truncation-trunc-Prop A)
@@ -254,8 +254,8 @@ module _
 ```agda
 abstract
   dependent-universal-property-trunc-Prop :
-    {l1 : Level} {A : UU l1} {l : Level} →
-      dependent-universal-property-propositional-truncation l
+    {l : Level} {A : UU l} →
+      dependent-universal-property-propositional-truncation
       ( trunc-Prop A)
       ( unit-trunc-Prop)
   dependent-universal-property-trunc-Prop {A = A} =