Universal property of fibers (#944)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

src/foundation-core.lagda.md

@@ -25,6 +25,7 @@ open import foundation-core.endomorphisms public
 open import foundation-core.equality-dependent-pair-types public
 open import foundation-core.equivalence-relations public
 open import foundation-core.equivalences public
+open import foundation-core.families-of-equivalences public
 open import foundation-core.fibers-of-maps public
 open import foundation-core.function-types public
 open import foundation-core.functoriality-dependent-function-types public

src/foundation-core/families-of-equivalences.lagda.md

@@ -0,0 +1,103 @@
+# Families of equivalences
+
+```agda
+module foundation-core.families-of-equivalences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.equivalences
+open import foundation-core.type-theoretic-principle-of-choice
+```
+
+</details>
+
+## Idea
+
+A **family of equivalences** is a family
+
+```text
+  eᵢ : A i ≃ B i
+```
+
+of [equivalences](foundation-core.equivalences.md). Families of equivalences are
+also called **fiberwise equivalences**.
+
+## Definitions
+
+### The predicate of being a fiberwise equivalence
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
+  where
+
+  is-fiberwise-equiv : (f : (x : A) → B x → C x) → UU (l1 ⊔ l2 ⊔ l3)
+  is-fiberwise-equiv f = (x : A) → is-equiv (f x)
+```
+
+### Fiberwise equivalences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1}
+  where
+
+  fiberwise-equiv : (B : A → UU l2) (C : A → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
+  fiberwise-equiv B C = Σ ((x : A) → B x → C x) is-fiberwise-equiv
+
+  map-fiberwise-equiv :
+    {B : A → UU l2} {C : A → UU l3} →
+    fiberwise-equiv B C → (a : A) → B a → C a
+  map-fiberwise-equiv = pr1
+
+  is-fiberwise-equiv-fiberwise-equiv :
+    {B : A → UU l2} {C : A → UU l3} →
+    (e : fiberwise-equiv B C) →
+    is-fiberwise-equiv (map-fiberwise-equiv e)
+  is-fiberwise-equiv-fiberwise-equiv = pr2
+```
+
+### Families of equivalences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1}
+  where
+
+  fam-equiv : (B : A → UU l2) (C : A → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
+  fam-equiv B C = (x : A) → B x ≃ C x
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
+  (e : fam-equiv B C)
+  where
+
+  map-fam-equiv : (x : A) → B x → C x
+  map-fam-equiv x = map-equiv (e x)
+
+  is-equiv-map-fam-equiv : is-fiberwise-equiv map-fam-equiv
+  is-equiv-map-fam-equiv x = is-equiv-map-equiv (e x)
+```
+
+## Properties
+
+### Families of equivalences are equivalent to fiberwise equivalences
+
+```agda
+equiv-fiberwise-equiv-fam-equiv :
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3) →
+  fam-equiv B C ≃ fiberwise-equiv B C
+equiv-fiberwise-equiv-fam-equiv B C = distributive-Π-Σ
+```
+
+## See also
+
+- In
+  [Functoriality of dependent pair types](foundation-core.functoriality-dependent-pair-types.md)
+  we show that a family of maps is a fiberwise equivalence if and only if it
+  induces an equivalence on [total spaces](foundation.dependent-pair-types.md).

src/foundation-core/fibers-of-maps.lagda.md

@@ -366,54 +366,6 @@ module _
   pr2 inv-compute-fiber-comp = is-equiv-inv-map-compute-fiber-comp
 ```
 
-### When a product is taken over all fibers of a map, then we can equivalently take the product over the domain of that map
-
-```agda
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
-  (C : (y : B) (z : fiber f y) → UU l3)
-  where
-
-  map-reduce-Π-fiber :
-    ((y : B) (z : fiber f y) → C y z) → ((x : A) → C (f x) (x , refl))
-  map-reduce-Π-fiber h x = h (f x) (x , refl)
-
-  inv-map-reduce-Π-fiber :
-    ((x : A) → C (f x) (x , refl)) → ((y : B) (z : fiber f y) → C y z)
-  inv-map-reduce-Π-fiber h .(f x) (x , refl) = h x
-
-  is-section-inv-map-reduce-Π-fiber :
-    (map-reduce-Π-fiber ∘ inv-map-reduce-Π-fiber) ~ id
-  is-section-inv-map-reduce-Π-fiber h = refl
-
-  is-retraction-inv-map-reduce-Π-fiber' :
-    (h : (y : B) (z : fiber f y) → C y z) (y : B) →
-    (inv-map-reduce-Π-fiber (map-reduce-Π-fiber h) y) ~ (h y)
-  is-retraction-inv-map-reduce-Π-fiber' h .(f z) (z , refl) = refl
-
-  is-retraction-inv-map-reduce-Π-fiber :
-    (inv-map-reduce-Π-fiber ∘ map-reduce-Π-fiber) ~ id
-  is-retraction-inv-map-reduce-Π-fiber h =
-    eq-htpy (eq-htpy ∘ is-retraction-inv-map-reduce-Π-fiber' h)
-
-  is-equiv-map-reduce-Π-fiber : is-equiv map-reduce-Π-fiber
-  is-equiv-map-reduce-Π-fiber =
-    is-equiv-is-invertible
-      ( inv-map-reduce-Π-fiber)
-      ( is-section-inv-map-reduce-Π-fiber)
-      ( is-retraction-inv-map-reduce-Π-fiber)
-
-  reduce-Π-fiber' :
-    ((y : B) (z : fiber f y) → C y z) ≃ ((x : A) → C (f x) (x , refl))
-  pr1 reduce-Π-fiber' = map-reduce-Π-fiber
-  pr2 reduce-Π-fiber' = is-equiv-map-reduce-Π-fiber
-
-reduce-Π-fiber :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
-  (C : B → UU l3) → ((y : B) → fiber f y → C y) ≃ ((x : A) → C (f x))
-reduce-Π-fiber f C = reduce-Π-fiber' f (λ y z → C y)
-```
-
 ## Table of files about fibers of maps
 
 The following table lists files that are about fibers of maps as a general

src/foundation-core/functoriality-dependent-function-types.lagda.md

@@ -8,14 +8,14 @@ module foundation-core.functoriality-dependent-function-types where
 
 ```agda
 open import foundation.dependent-pair-types
-open import foundation.families-of-equivalences
 open import foundation.function-extensionality
 open import foundation.implicit-function-types
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
 open import foundation-core.contractible-types
 open import foundation-core.equivalences
+open import foundation-core.families-of-equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types

src/foundation-core/functoriality-dependent-pair-types.lagda.md

@@ -8,13 +8,13 @@ module foundation-core.functoriality-dependent-pair-types where
 
 ```agda
 open import foundation.dependent-pair-types
-open import foundation.families-of-equivalences
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
 open import foundation-core.contractible-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
+open import foundation-core.families-of-equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.homotopies

src/foundation-core/pullbacks.lagda.md

@@ -11,7 +11,6 @@ open import foundation.action-on-identifications-functions
 open import foundation.cones-over-cospans
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
-open import foundation.families-of-equivalences
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-fibers-of-maps
 open import foundation.identity-types
@@ -23,6 +22,7 @@ open import foundation-core.cartesian-product-types
 open import foundation-core.diagonal-maps-of-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
+open import foundation-core.families-of-equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types

src/foundation.lagda.md

@@ -233,6 +233,7 @@ open import foundation.powersets public
 open import foundation.precomposition-dependent-functions public
 open import foundation.precomposition-functions public
 open import foundation.precomposition-functions-into-subuniverses public
+open import foundation.precomposition-type-families public
 open import foundation.preidempotent-maps public
 open import foundation.preimages-of-subtypes public
 open import foundation.preunivalence public
@@ -350,6 +351,7 @@ open import foundation.universal-property-coproduct-types public
 open import foundation.universal-property-dependent-pair-types public
 open import foundation.universal-property-empty-type public
 open import foundation.universal-property-equivalences public
+open import foundation.universal-property-family-of-fibers-of-maps public
 open import foundation.universal-property-fiber-products public
 open import foundation.universal-property-identity-systems public
 open import foundation.universal-property-identity-types public

src/foundation/connected-maps.lagda.md

@@ -22,6 +22,7 @@ open import foundation.truncation-levels
 open import foundation.truncations
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.univalence
+open import foundation.universal-property-family-of-fibers-of-maps
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
@@ -392,7 +393,7 @@ module _
       ( λ b →
         function-dependent-universal-property-trunc
           ( Id-Truncated-Type' (trunc k (fiber f b)) _))
-      ( inv-map-reduce-Π-fiber f
+      ( extend-lift-family-of-elements-fiber f
         ( λ b u → _ ＝ unit-trunc u)
         ( compute-center-is-connected-map-dependent-universal-property-connected-map))
 

src/foundation/equality-fibers-of-maps.lagda.md

@@ -9,13 +9,13 @@ module foundation.equality-fibers-of-maps where
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
-open import foundation.families-of-equivalences
 open import foundation.identity-types
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
+open import foundation-core.families-of-equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types

src/foundation/equivalences.lagda.md

@@ -25,6 +25,7 @@ open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.contractible-maps
 open import foundation-core.contractible-types
 open import foundation-core.embeddings
+open import foundation-core.families-of-equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types

src/foundation/families-of-equivalences.lagda.md

@@ -2,16 +2,17 @@
 
 ```agda
 module foundation.families-of-equivalences where
+
+open import foundation-core.families-of-equivalences public
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.dependent-pair-types
+open import foundation.equivalences
 open import foundation.universe-levels
 
-open import foundation-core.equivalences
-open import foundation-core.type-theoretic-principle-of-choice
+open import foundation-core.propositions
 ```
 
 </details>
@@ -27,61 +28,19 @@ A **family of equivalences** is a family
 of [equivalences](foundation-core.equivalences.md). Families of equivalences are
 also called **fiberwise equivalences**.
 
-## Definitions
-
-### The predicate of being a fiberwise equivalence
-
-```agda
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
-  where
-
-  is-fiberwise-equiv : (f : (x : A) → B x → C x) → UU (l1 ⊔ l2 ⊔ l3)
-  is-fiberwise-equiv f = (x : A) → is-equiv (f x)
-```
-
-### Fiberwise equivalences
-
-```agda
-module _
-  {l1 l2 l3 : Level} {A : UU l1}
-  where
-
-  fiberwise-equiv : (B : A → UU l2) (C : A → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
-  fiberwise-equiv B C = Σ ((x : A) → B x → C x) is-fiberwise-equiv
-```
+## Properties
 
-### Families of equivalences
+### Being a fiberwise equivalence is a proposition
 
 ```agda
-module _
-  {l1 l2 l3 : Level} {A : UU l1}
-  where
-
-  fam-equiv : (B : A → UU l2) (C : A → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
-  fam-equiv B C = (x : A) → B x ≃ C x
-
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
-  (e : fam-equiv B C)
   where
 
-  map-fam-equiv : (x : A) → B x → C x
-  map-fam-equiv x = map-equiv (e x)
-
-  is-equiv-map-fam-equiv : is-fiberwise-equiv map-fam-equiv
-  is-equiv-map-fam-equiv x = is-equiv-map-equiv (e x)
-```
-
-## Properties
-
-### Families of equivalences are equivalent to fiberwise equivalences
-
-```agda
-equiv-fiberwise-equiv-fam-equiv :
-  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3) →
-  fam-equiv B C ≃ fiberwise-equiv B C
-equiv-fiberwise-equiv-fam-equiv B C = distributive-Π-Σ
+  is-property-is-fiberwise-equiv :
+    (f : (a : A) → B a → C a) → is-prop (is-fiberwise-equiv f)
+  is-property-is-fiberwise-equiv f =
+    is-prop-Π (λ a → is-property-is-equiv (f a))
 ```
 
 ## See also

src/foundation/function-types.lagda.md

@@ -148,6 +148,19 @@ module _
         ( eq-htpy-refl-htpy (h (i s))))
 ```
 
+### Composing families of functions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
+  {D : A → UU l4}
+  where
+
+  dependent-comp :
+    ((a : A) → C a → D a) → ((a : A) → B a → C a) → (a : A) → B a → D a
+  dependent-comp g f a b = g a (f a b)
+```
+
 ## See also
 
 ### Table of files about function types, composition, and equivalences

src/foundation/fundamental-theorem-of-identity-types.lagda.md

@@ -8,11 +8,11 @@ module foundation.fundamental-theorem-of-identity-types where
 
 ```agda
 open import foundation.dependent-pair-types
-open import foundation.families-of-equivalences
 open import foundation.universe-levels
 
 open import foundation-core.contractible-types
 open import foundation-core.equivalences
+open import foundation-core.families-of-equivalences
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types