Universal property of fibers

src/foundation.lagda.md

@@ -349,6 +349,7 @@ 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-fiber-products public
+open import foundation.universal-property-fibers-of-maps public
 open import foundation.universal-property-identity-systems public
 open import foundation.universal-property-identity-types public
 open import foundation.universal-property-image public

src/foundation/equivalences.lagda.md

@@ -13,6 +13,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.cones-over-cospans
 open import foundation.dependent-pair-types
 open import foundation.equivalence-extensionality
+open import foundation.families-of-equivalences
 open import foundation.function-extensionality
 open import foundation.functoriality-fibers-of-maps
 open import foundation.identity-types
@@ -248,6 +249,19 @@ module _
   pr2 emb-map-equiv = is-emb-map-equiv
 ```
 
+### Being a fiberwise equivalence is a proposition
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
+  where
+
+  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))
+```
+
 ### The 3-for-2 property of being an equivalence
 
 #### If the right factor is an equivalence, then the left factor being an equivalence is equivalent to the composite being one

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

@@ -49,6 +49,17 @@ module _
 
   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

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

@@ -13,10 +13,13 @@ open import foundation.action-on-identifications-functions
 open import foundation.cones-over-cospans
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-universal-property-equivalences
 open import foundation.equivalences
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universal-property-fibers-of-maps
 open import foundation.universe-levels
 
 open import foundation-core.constant-maps
@@ -110,6 +113,69 @@ module _
     inv-equiv equiv-total-fiber-terminal-map
 ```
 
+### The family of fibers has the universal property of fibers of maps
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  section-family-of-fibers :
+    (a : A) → fiber f (f a)
+  pr1 (section-family-of-fibers a) = a
+  pr2 (section-family-of-fibers a) = refl
+
+  equiv-up-family-of-fibers :
+    {l : Level} → (P : B → UU l) →
+    ((b : B) → fiber f b → P b) ≃ ((a : A) → P (f a))
+  equiv-up-family-of-fibers P =
+    equivalence-reasoning
+      ( (b : B) → fiber f b → P b)
+      ≃ ((w : Σ B (λ b → fiber f b)) → P (pr1 w))
+        by equiv-ind-Σ
+      ≃ ((a : A) → P (f a))
+        by
+          equiv-precomp-Π
+            ( inv-equiv-total-fiber f)
+            ( λ w → P (pr1 w))
+
+  up-family-of-fibers :
+    universal-property-fiber f (fiber f) (section-family-of-fibers)
+  up-family-of-fibers P =
+    is-equiv-map-equiv (equiv-up-family-of-fibers P)
+```
+
+### The family of fibers has the dependent universal property of fibers of maps
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  equiv-dependent-up-family-of-fibers :
+    {l : Level} (P : (b : B) → fiber f b → UU l) →
+    ( ( b : B) (z : fiber f b) → P b z) ≃
+    ( ( a : A) → P (f a) (section-family-of-fibers f a))
+  equiv-dependent-up-family-of-fibers P =
+    equivalence-reasoning
+      ( ( b : B) (z : fiber f b) → P b z)
+      ≃ ((w : Σ B (λ b → fiber f b)) → P (pr1 w) (pr2 w))
+        by equiv-ind-Σ
+      ≃ ((a : A) → P (f a) (section-family-of-fibers f a))
+        by
+          equiv-precomp-Π
+            ( inv-equiv-total-fiber f)
+            ( λ w → P (pr1 w) (pr2 w))
+
+  dependent-up-family-of-fibers :
+    dependent-universal-property-fiber
+      ( f)
+      ( fiber f)
+      ( section-family-of-fibers f)
+  dependent-up-family-of-fibers P =
+    is-equiv-map-equiv (equiv-dependent-up-family-of-fibers P)
+```
+
 ### Transport in fibers
 
 ```agda

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