diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md
index 0d74036950..114fa26c30 100644
--- a/src/foundation-core.lagda.md
+++ b/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
diff --git a/src/foundation-core/families-of-equivalences.lagda.md b/src/foundation-core/families-of-equivalences.lagda.md
new file mode 100644
index 0000000000..a3578dcaaa
--- /dev/null
+++ b/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).
diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md
index c25178f54f..7d338028e7 100644
--- a/src/foundation-core/fibers-of-maps.lagda.md
+++ b/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
diff --git a/src/foundation-core/functoriality-dependent-function-types.lagda.md b/src/foundation-core/functoriality-dependent-function-types.lagda.md
index 3b46394efe..09a535f1f4 100644
--- a/src/foundation-core/functoriality-dependent-function-types.lagda.md
+++ b/src/foundation-core/functoriality-dependent-function-types.lagda.md
@@ -8,7 +8,6 @@ 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
@@ -16,6 +15,7 @@ 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
diff --git a/src/foundation-core/functoriality-dependent-pair-types.lagda.md b/src/foundation-core/functoriality-dependent-pair-types.lagda.md
index c28397fc83..ff1ecec37d 100644
--- a/src/foundation-core/functoriality-dependent-pair-types.lagda.md
+++ b/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
diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
index b0f4ec9cd8..1b80b0bd79 100644
--- a/src/foundation-core/pullbacks.lagda.md
+++ b/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
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 0ce657f8ec..3ce72252c2 100644
--- a/src/foundation.lagda.md
+++ b/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
diff --git a/src/foundation/connected-maps.lagda.md b/src/foundation/connected-maps.lagda.md
index 72540db3b2..c0b1ae60a2 100644
--- a/src/foundation/connected-maps.lagda.md
+++ b/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))
 
diff --git a/src/foundation/equality-fibers-of-maps.lagda.md b/src/foundation/equality-fibers-of-maps.lagda.md
index ee8a19acdc..bbf9b42b2e 100644
--- a/src/foundation/equality-fibers-of-maps.lagda.md
+++ b/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
diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md
index 38b3006946..8b403c518a 100644
--- a/src/foundation/equivalences.lagda.md
+++ b/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
diff --git a/src/foundation/families-of-equivalences.lagda.md b/src/foundation/families-of-equivalences.lagda.md
index b9056d45b1..3cfded46ff 100644
--- a/src/foundation/families-of-equivalences.lagda.md
+++ b/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
diff --git a/src/foundation/function-types.lagda.md b/src/foundation/function-types.lagda.md
index 6c4afd3ec9..5dedd121e5 100644
--- a/src/foundation/function-types.lagda.md
+++ b/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
diff --git a/src/foundation/fundamental-theorem-of-identity-types.lagda.md b/src/foundation/fundamental-theorem-of-identity-types.lagda.md
index 4c2a1aa8b8..5090cca6f8 100644
--- a/src/foundation/fundamental-theorem-of-identity-types.lagda.md
+++ b/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
diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md
index 7c8d5789fb..6b4503a13a 100644
--- a/src/foundation/identity-systems.lagda.md
+++ b/src/foundation/identity-systems.lagda.md
@@ -9,12 +9,12 @@ module foundation.identity-systems where
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
-open import foundation.families-of-equivalences
 open import foundation.fundamental-theorem-of-identity-types
 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.identity-types
 open import foundation-core.sections
 open import foundation-core.torsorial-type-families
diff --git a/src/foundation/precomposition-dependent-functions.lagda.md b/src/foundation/precomposition-dependent-functions.lagda.md
index dfafc597a6..7070783975 100644
--- a/src/foundation/precomposition-dependent-functions.lagda.md
+++ b/src/foundation/precomposition-dependent-functions.lagda.md
@@ -18,11 +18,9 @@ open import foundation.truncation-levels
 open import foundation.universe-levels
 
 open import foundation-core.coherently-invertible-maps
-open import foundation-core.constant-maps
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
-open import foundation-core.functoriality-dependent-function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.path-split-maps
@@ -34,27 +32,6 @@ open import foundation-core.truncated-maps
 
 ## Properties
 
-### For any map `f : A → B` and any family `C` over `B`, if `f` satisfies the property that `C b → (fiber f b → C b)` is an equivalence for every `b : B` then the precomposition function `((b : B) → C b) → ((a : A) → C (f a))` is an equivalence
-
-This condition simplifies, for example, the proof that connected maps satisfy a
-dependent universal property.
-
-```agda
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {f : A → B} {C : B → UU l3}
-  where
-
-  is-equiv-precomp-Π-fiber-condition :
-    ((b : B) → is-equiv (λ (c : C b) → const (fiber f b) (C b) c)) →
-    is-equiv (precomp-Π f C)
-  is-equiv-precomp-Π-fiber-condition H =
-    is-equiv-comp
-      ( map-reduce-Π-fiber f (λ b u → C b))
-      ( map-Π (λ b u t → u))
-      ( is-equiv-map-Π-is-fiberwise-equiv H)
-      ( is-equiv-map-reduce-Π-fiber f (λ b u → C b))
-```
-
 ### Equivalences induce an equivalence from the type of homotopies between two dependent functions to the type of homotopies between their precomposites
 
 ```agda
diff --git a/src/foundation/precomposition-type-families.lagda.md b/src/foundation/precomposition-type-families.lagda.md
new file mode 100644
index 0000000000..e2c95284a3
--- /dev/null
+++ b/src/foundation/precomposition-type-families.lagda.md
@@ -0,0 +1,40 @@
+# Precomposition of type families
+
+```agda
+module foundation.precomposition-type-families where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Any map `f : A → B` induces a
+{{#concept "precomposition operation" Disambiguation="of type families"}}
+
+```text
+  (B → 𝒰) → (A → 𝒰)
+```
+
+given by [precomposing](foundation-core.precomposition-functions.md) any
+`Q : B → 𝒰` to `Q ∘ f : A → 𝒰`.
+
+## Definitions
+
+### The precomposition operation on type familes
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  precomp-family : (l : Level) → (B → UU l) → (A → UU l)
+  precomp-family l Q = Q ∘ f
+```
diff --git a/src/foundation/retracts-of-maps.lagda.md b/src/foundation/retracts-of-maps.lagda.md
index 6deb9ffa2c..ca69c47a5f 100644
--- a/src/foundation/retracts-of-maps.lagda.md
+++ b/src/foundation/retracts-of-maps.lagda.md
@@ -139,7 +139,7 @@ module _
     coherence-htpy-hom-arrow f f (comp-hom-arrow f g f r i) id-hom-arrow
 ```
 
-### The binary relation `g f ↦ g retract-of-map f` asserting that `g` is a retract of the map `f`
+### The binary relation `f g ↦ f retract-of-map g` asserting that `f` is a retract of the map `g`
 
 ```agda
 module _
diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md
index 61bd607522..411a8ca0dd 100644
--- a/src/foundation/surjective-maps.lagda.md
+++ b/src/foundation/surjective-maps.lagda.md
@@ -32,6 +32,7 @@ open import foundation.truncated-types
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.univalence
 open import foundation.universal-property-dependent-pair-types
+open import foundation.universal-property-family-of-fibers-of-maps
 open import foundation.universal-property-propositional-truncation
 open import foundation.universe-levels
 
@@ -335,7 +336,7 @@ module _
                 ( type-Prop (P y))))
           ( is-equiv-map-Π-is-fiberwise-equiv
             ( λ b → is-propositional-truncation-trunc-Prop (fiber f b) (P b))))
-        ( is-equiv-map-reduce-Π-fiber f ( λ y z → type-Prop (P y)))
+        ( universal-property-family-of-fibers-fiber f (is-in-subtype P))
 
   equiv-dependent-universal-property-surj-is-surjective :
     is-surjective f →
diff --git a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
new file mode 100644
index 0000000000..fa50fc60b7
--- /dev/null
+++ b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
@@ -0,0 +1,424 @@
+# The universal property of the family of fibers of maps
+
+```agda
+module foundation.universal-property-family-of-fibers-of-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.families-of-equivalences
+open import foundation.function-extensionality
+open import foundation.subtype-identity-principle
+open import foundation.universe-levels
+
+open import foundation-core.constant-maps
+open import foundation-core.contractible-maps
+open import foundation-core.contractible-types
+open import foundation-core.equivalences
+open import foundation-core.fibers-of-maps
+open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-function-types
+open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.precomposition-dependent-functions
+open import foundation-core.retractions
+open import foundation-core.sections
+
+open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements
+open import orthogonal-factorization-systems.lifts-families-of-elements
+```
+
+</details>
+
+## Idea
+
+Any map `f : A → B` induces a type family `fiber f : B → 𝒰` of
+[fibers](foundation-core.fibers-of-maps.md) of `f`. By
+[precomposing](foundation.precomposition-type-families.md) with `f`, we obtain
+the type family `(fiber f) ∘ f : A → 𝒰`, which always has a section given by
+
+```text
+  λ a → (a , refl) : (a : A) → fiber f (f a).
+```
+
+We can uniquely characterize the family of fibers `fiber f : B → 𝒰` as the
+initial type family equipped with such a section. Explicitly, the
+{{#concept "universal property of the family of fibers" Disambiguation="of a map"}}
+`fiber f : B → 𝒰` of a map `f` is that the precomposition operation
+
+```text
+  ((b : B) → fiber f b → X b) → ((a : A) → X (f a))
+```
+
+is an [equivalence](foundation-core.equivalences.md) for any type family
+`X : B → 𝒰`. Note that for any type family `X` over `B` and any map `f : A → B`,
+the type of
+[lifts](orthogonal-factorization-systems.lifts-families-of-elements.md) of `f`
+to `X` is precisely the type of sections
+
+```text
+  (a : A) → X (f a).
+```
+
+The family of fibers of `f` is therefore the initial type family over `B`
+equipped with a lift of `f`.
+
+This universal property is especially useful when `A` or `B` enjoy mapping out
+universal properties. This lets us characterize the sections `(a : A) → X (f a)`
+in terms of the mapping out properties of `A` and the descent data of `B`.
+
+**Note:** We disambiguate between the _universal property of the family of
+fibers of a map_ and the _universal property of the fiber of a map_ at a point
+in the codomain. The universal property of the family of fibers of a map is as
+described above, while the universal property of the fiber `fiber f b` of a map
+`f` at `b` is a special case of the universal property of pullbacks.
+
+## Definitions
+
+### The dependent universal property of the family of fibers of a map
+
+Consider a map `f : A → B` and a type family `F : B → 𝒰` equipped with a lift
+`δ : (a : A) → F (f a)` of `f` to `F`. Then there is an evaluation map
+
+```text
+  ((b : B) (z : F b) → X b z) → ((a : A) → X (f a) (δ a))
+```
+
+for any binary type family `X : (b : B) → F b → 𝒰`. This evaluation map takes a
+binary family of elements of `X` to a
+[double lift](orthogonal-factorization-systems.double-lifts-families-of-elements.md)
+of `f` and `δ`. The
+{{#concept "dependent universal property of the family of fibers of a map"}} `f`
+asserts that this evaluation map is an equivalence.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  dependent-universal-property-family-of-fibers :
+    {f : A → B} (F : B → UU l3) (δ : lift-family-of-elements f F) → UUω
+  dependent-universal-property-family-of-fibers F δ =
+    {l : Level} (X : (b : B) → F b → UU l) →
+    is-equiv (ev-double-lift-family-of-elements {B = F} δ {X})
+```
+
+### The universal property of the family of fibers of a map
+
+Consider a map `f : A → B` and a type family `F : B → 𝒰` equipped with a lift
+`δ : (a : A) → F (f a)` of `f` to `F`. Then there is an evaluation map
+
+```text
+  ((b : B) → F b → X b) → ((a : A) → X (f a))
+```
+
+for any binary type family `X : B → 𝒰`. This evaluation map takes a binary
+family of elements of `X` to a double lift of `f` and `δ`. The universal
+property of the family of fibers of `f` asserts that this evaluation map is an
+equivalence.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  universal-property-family-of-fibers :
+    {f : A → B} (F : B → UU l3) (δ : lift-family-of-elements f F) → UUω
+  universal-property-family-of-fibers F δ =
+    {l : Level} (X : B → UU l) →
+    is-equiv (ev-double-lift-family-of-elements {B = F} δ {λ b _ → X b})
+```
+
+### The lift of any map to its family of fibers
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  lift-family-of-elements-fiber : lift-family-of-elements f (fiber f)
+  pr1 (lift-family-of-elements-fiber a) = a
+  pr2 (lift-family-of-elements-fiber a) = refl
+```
+
+## Properties
+
+### The family of fibers of a map satisfies the dependent universal property of the family of fibers of a map
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  module _
+    {l3 : Level} (C : (y : B) (z : fiber f y) → UU l3)
+    where
+
+    ev-lift-family-of-elements-fiber :
+      ((y : B) (z : fiber f y) → C y z) → ((x : A) → C (f x) (x , refl))
+    ev-lift-family-of-elements-fiber =
+      ev-double-lift-family-of-elements (lift-family-of-elements-fiber f)
+
+    extend-lift-family-of-elements-fiber :
+      ((x : A) → C (f x) (x , refl)) → ((y : B) (z : fiber f y) → C y z)
+    extend-lift-family-of-elements-fiber h .(f x) (x , refl) = h x
+
+    is-section-extend-lift-family-of-elements-fiber :
+      is-section
+        ( ev-lift-family-of-elements-fiber)
+        ( extend-lift-family-of-elements-fiber)
+    is-section-extend-lift-family-of-elements-fiber h = refl
+
+    is-retraction-extend-lift-family-of-elements-fiber' :
+      (h : (y : B) (z : fiber f y) → C y z) (y : B) →
+      extend-lift-family-of-elements-fiber
+        ( ev-lift-family-of-elements-fiber h)
+        ( y) ~
+      h y
+    is-retraction-extend-lift-family-of-elements-fiber' h .(f z) (z , refl) =
+      refl
+
+    is-retraction-extend-lift-family-of-elements-fiber :
+      is-retraction
+        ( ev-lift-family-of-elements-fiber)
+        ( extend-lift-family-of-elements-fiber)
+    is-retraction-extend-lift-family-of-elements-fiber h =
+      eq-htpy (eq-htpy ∘ is-retraction-extend-lift-family-of-elements-fiber' h)
+
+    is-equiv-extend-lift-family-of-elements-fiber :
+      is-equiv extend-lift-family-of-elements-fiber
+    is-equiv-extend-lift-family-of-elements-fiber =
+      is-equiv-is-invertible
+        ( ev-lift-family-of-elements-fiber)
+        ( is-retraction-extend-lift-family-of-elements-fiber)
+        ( is-section-extend-lift-family-of-elements-fiber)
+
+    inv-equiv-dependent-universal-property-family-of-fibers :
+      ((x : A) → C (f x) (x , refl)) ≃ ((y : B) (z : fiber f y) → C y z)
+    pr1 inv-equiv-dependent-universal-property-family-of-fibers =
+      extend-lift-family-of-elements-fiber
+    pr2 inv-equiv-dependent-universal-property-family-of-fibers =
+      is-equiv-extend-lift-family-of-elements-fiber
+
+  dependent-universal-property-family-of-fibers-fiber :
+    dependent-universal-property-family-of-fibers
+      ( fiber f)
+      ( lift-family-of-elements-fiber f)
+  dependent-universal-property-family-of-fibers-fiber C =
+    is-equiv-is-invertible
+      ( extend-lift-family-of-elements-fiber C)
+      ( is-section-extend-lift-family-of-elements-fiber C)
+      ( is-retraction-extend-lift-family-of-elements-fiber C)
+
+  equiv-dependent-universal-property-family-of-fibers :
+    {l3 : Level} (C : (y : B) (z : fiber f y) → UU l3) →
+    ((y : B) (z : fiber f y) → C y z) ≃
+    ((x : A) → C (f x) (x , refl))
+  pr1 (equiv-dependent-universal-property-family-of-fibers C) =
+    ev-lift-family-of-elements-fiber C
+  pr2 (equiv-dependent-universal-property-family-of-fibers C) =
+    dependent-universal-property-family-of-fibers-fiber C
+```
+
+### The family of fibers of a map satisfies the universal property of the family of fibers of a map
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  universal-property-family-of-fibers-fiber :
+    universal-property-family-of-fibers
+      ( fiber f)
+      ( lift-family-of-elements-fiber f)
+  universal-property-family-of-fibers-fiber C =
+    dependent-universal-property-family-of-fibers-fiber f (λ y _ → C y)
+
+  equiv-universal-property-family-of-fibers :
+    {l3 : Level} (C : B → UU l3) →
+    ((y : B) → fiber f y → C y) ≃ lift-family-of-elements f C
+  equiv-universal-property-family-of-fibers C =
+    equiv-dependent-universal-property-family-of-fibers f (λ y _ → C y)
+```
+
+### The inverse equivalence of the universal property of the family of fibers of a map
+
+The inverse of the equivalence `equiv-universal-property-family-of-fibers` has a
+reasonably nice definition, so we also record it here.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (C : B → UU l3)
+  where
+
+  inv-equiv-universal-property-family-of-fibers :
+    (lift-family-of-elements f C) ≃ ((y : B) → fiber f y → C y)
+  inv-equiv-universal-property-family-of-fibers =
+    inv-equiv-dependent-universal-property-family-of-fibers f (λ y _ → C y)
+```
+
+### If a type family equipped with a lift of a map satisfies the universal property of the family of fibers, then it satisfies a unique extension property
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {f : A → B}
+  {F : B → UU l3} {δ : (a : A) → F (f a)}
+  (u : universal-property-family-of-fibers F δ)
+  (G : B → UU l4) (γ : (a : A) → G (f a))
+  where
+
+  abstract
+    uniqueness-extension-universal-property-family-of-fibers :
+      is-contr
+        ( extension-double-lift-family-of-elements δ (λ y (_ : F y) → G y) γ)
+    uniqueness-extension-universal-property-family-of-fibers =
+      is-contr-equiv
+        ( fiber (ev-double-lift-family-of-elements δ) γ)
+        ( equiv-tot (λ h → equiv-eq-htpy))
+        ( is-contr-map-is-equiv (u G) γ)
+
+  abstract
+    extension-universal-property-family-of-fibers :
+      extension-double-lift-family-of-elements δ (λ y (_ : F y) → G y) γ
+    extension-universal-property-family-of-fibers =
+      center uniqueness-extension-universal-property-family-of-fibers
+
+  fiberwise-map-universal-property-family-of-fibers :
+    (b : B) → F b → G b
+  fiberwise-map-universal-property-family-of-fibers =
+    family-of-elements-extension-double-lift-family-of-elements
+      extension-universal-property-family-of-fibers
+
+  is-extension-fiberwise-map-universal-property-family-of-fibers :
+    is-extension-double-lift-family-of-elements δ
+      ( λ y _ → G y)
+      ( γ)
+      ( fiberwise-map-universal-property-family-of-fibers)
+  is-extension-fiberwise-map-universal-property-family-of-fibers =
+    is-extension-extension-double-lift-family-of-elements
+      extension-universal-property-family-of-fibers
+```
+
+### The family of fibers of a map is uniquely unique
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f : A → B) (F : B → UU l3)
+  (δ : (a : A) → F (f a)) (u : universal-property-family-of-fibers F δ)
+  (G : B → UU l4) (γ : (a : A) → G (f a))
+  (v : universal-property-family-of-fibers G γ)
+  where
+
+  is-retraction-extension-universal-property-family-of-fibers :
+    comp-extension-double-lift-family-of-elements
+      ( extension-universal-property-family-of-fibers v F δ)
+      ( extension-universal-property-family-of-fibers u G γ) ＝
+    id-extension-double-lift-family-of-elements δ
+  is-retraction-extension-universal-property-family-of-fibers =
+    eq-is-contr
+      ( uniqueness-extension-universal-property-family-of-fibers u F δ)
+
+  is-section-extension-universal-property-family-of-fibers :
+    comp-extension-double-lift-family-of-elements
+      ( extension-universal-property-family-of-fibers u G γ)
+      ( extension-universal-property-family-of-fibers v F δ) ＝
+    id-extension-double-lift-family-of-elements γ
+  is-section-extension-universal-property-family-of-fibers =
+    eq-is-contr
+      ( uniqueness-extension-universal-property-family-of-fibers v G γ)
+
+  is-retraction-fiberwise-map-universal-property-family-of-fibers :
+    (b : B) →
+    is-retraction
+      ( fiberwise-map-universal-property-family-of-fibers u G γ b)
+      ( fiberwise-map-universal-property-family-of-fibers v F δ b)
+  is-retraction-fiberwise-map-universal-property-family-of-fibers b =
+    htpy-eq
+      ( htpy-eq
+        ( ap
+          ( pr1)
+          ( is-retraction-extension-universal-property-family-of-fibers))
+        ( b))
+
+  is-section-fiberwise-map-universal-property-family-of-fibers :
+    (b : B) →
+    is-section
+      ( fiberwise-map-universal-property-family-of-fibers u G γ b)
+      ( fiberwise-map-universal-property-family-of-fibers v F δ b)
+  is-section-fiberwise-map-universal-property-family-of-fibers b =
+    htpy-eq
+      ( htpy-eq
+        ( ap
+          ( pr1)
+          ( is-section-extension-universal-property-family-of-fibers))
+        ( b))
+
+  is-fiberwise-equiv-fiberwise-map-universal-property-family-of-fibers :
+    is-fiberwise-equiv (fiberwise-map-universal-property-family-of-fibers u G γ)
+  is-fiberwise-equiv-fiberwise-map-universal-property-family-of-fibers b =
+    is-equiv-is-invertible
+      ( family-of-elements-extension-double-lift-family-of-elements
+        ( extension-universal-property-family-of-fibers v F δ)
+        ( b))
+      ( is-section-fiberwise-map-universal-property-family-of-fibers b)
+      ( is-retraction-fiberwise-map-universal-property-family-of-fibers b)
+
+  uniquely-unique-family-of-fibers :
+    is-contr
+      ( Σ ( fiberwise-equiv F G)
+          ( λ h →
+            ev-double-lift-family-of-elements δ (map-fiberwise-equiv h) ~ γ))
+  uniquely-unique-family-of-fibers =
+    is-torsorial-Eq-subtype
+      ( uniqueness-extension-universal-property-family-of-fibers u G γ)
+      ( is-property-is-fiberwise-equiv)
+      ( fiberwise-map-universal-property-family-of-fibers u G γ)
+      ( is-extension-fiberwise-map-universal-property-family-of-fibers u G γ)
+      ( is-fiberwise-equiv-fiberwise-map-universal-property-family-of-fibers)
+
+  extension-by-fiberwise-equiv-universal-property-family-of-fibers :
+    Σ ( fiberwise-equiv F G)
+      ( λ h → ev-double-lift-family-of-elements δ (map-fiberwise-equiv h) ~ γ)
+  extension-by-fiberwise-equiv-universal-property-family-of-fibers =
+    center uniquely-unique-family-of-fibers
+
+  fiberwise-equiv-universal-property-of-fibers :
+    fiberwise-equiv F G
+  fiberwise-equiv-universal-property-of-fibers =
+    pr1 extension-by-fiberwise-equiv-universal-property-family-of-fibers
+
+  is-extension-fiberwise-equiv-universal-property-of-fibers :
+    is-extension-double-lift-family-of-elements δ
+      ( λ y _ → G y)
+      ( γ)
+      ( map-fiberwise-equiv
+        ( fiberwise-equiv-universal-property-of-fibers))
+  is-extension-fiberwise-equiv-universal-property-of-fibers =
+    pr2 extension-by-fiberwise-equiv-universal-property-family-of-fibers
+```
+
+### A type family `C` over `B` satisfies the universal property of the family of fibers of a map `f : A → B` if and only if the diagonal map `C b → (fiber f b → C b)` is an equivalence for every `b : B`
+
+This condition simplifies, for example, the proof that connected maps satisfy a
+dependent universal property.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  is-equiv-precomp-Π-fiber-condition :
+    {l3 : Level} {C : B → UU l3} →
+    ((b : B) → is-equiv (λ (c : C b) → const (fiber f b) (C b) c)) →
+    is-equiv (precomp-Π f C)
+  is-equiv-precomp-Π-fiber-condition {l3} {C} H =
+    is-equiv-comp
+      ( ev-lift-family-of-elements-fiber f (λ b _ → C b))
+      ( map-Π (λ b u _ → u))
+      ( is-equiv-map-Π-is-fiberwise-equiv H)
+      ( universal-property-family-of-fibers-fiber f C)
+```
diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md
index b76f1e211b..48114b75b7 100644
--- a/src/foundation/universal-property-image.lagda.md
+++ b/src/foundation/universal-property-image.lagda.md
@@ -15,6 +15,7 @@ open import foundation.propositional-truncations
 open import foundation.slice
 open import foundation.surjective-maps
 open import foundation.transport-along-identifications
+open import foundation.universal-property-family-of-fibers-of-maps
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
@@ -322,7 +323,9 @@ abstract
   is-image-is-surjective' f i q H B' m =
     map-equiv
       ( ( equiv-hom-slice-fiberwise-hom (map-emb i) (map-emb m)) ∘e
-        ( ( inv-equiv (reduce-Π-fiber (map-emb i) (fiber (map-emb m)))) ∘e
+        ( ( inv-equiv-universal-property-family-of-fibers
+            ( map-emb i)
+            ( fiber (map-emb m))) ∘e
           ( inv-equiv
             ( equiv-dependent-universal-property-surj-is-surjective
               ( pr1 q)
@@ -333,7 +336,8 @@ abstract
                   ( is-prop-map-emb m (pr1 i b)))) ∘e
             ( ( equiv-Π-equiv-family
                 ( λ a → equiv-tr (fiber (map-emb m)) (pr2 q a))) ∘e
-              ( ( reduce-Π-fiber f (fiber (map-emb m))) ∘e
+              ( ( equiv-universal-property-family-of-fibers f
+                  ( fiber (map-emb m))) ∘e
                 ( equiv-fiberwise-hom-hom-slice f (map-emb m)))))))
 
 abstract
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index 79e056afb2..178dac2fd7 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -12,6 +12,9 @@ module orthogonal-factorization-systems where
 open import orthogonal-factorization-systems.cd-structures public
 open import orthogonal-factorization-systems.cellular-maps public
 open import orthogonal-factorization-systems.closed-modalities public
+open import orthogonal-factorization-systems.double-lifts-families-of-elements public
+open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public
+open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public
 open import orthogonal-factorization-systems.extensions-of-maps public
 open import orthogonal-factorization-systems.factorization-operations public
 open import orthogonal-factorization-systems.factorization-operations-function-classes public
@@ -27,6 +30,7 @@ open import orthogonal-factorization-systems.higher-modalities public
 open import orthogonal-factorization-systems.identity-modality public
 open import orthogonal-factorization-systems.lifting-operations public
 open import orthogonal-factorization-systems.lifting-squares public
+open import orthogonal-factorization-systems.lifts-families-of-elements public
 open import orthogonal-factorization-systems.lifts-of-maps public
 open import orthogonal-factorization-systems.local-families public
 open import orthogonal-factorization-systems.local-maps public
diff --git a/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md
new file mode 100644
index 0000000000..032f76b87d
--- /dev/null
+++ b/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md
@@ -0,0 +1,93 @@
+# Double lifts of families of elements
+
+```agda
+module orthogonal-factorization-systems.double-lifts-families-of-elements where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.lifts-families-of-elements
+```
+
+</details>
+
+## Idea
+
+Consider a family of elements `b : (i : I) → B i (a i)` over a family of
+elements `a : (i : I) → A i` and consider a family of types
+
+```text
+  C : (i : I) (x : A i) → B i x → 𝒰.
+```
+
+Recall that `b` is also a
+[dependent lift](orthogonal-factorization-systems.lifts-families-of-elements.md)
+of the family of elements `a`. The type of
+{{#concept "dependent double lifts" Disambiguation="family of elements"}} of `b`
+and `a` to `C` is defined to be the type
+
+```text
+  (i : I) → C i (a i) (b i).
+```
+
+Note that this is the type of double lifts in the sense that it simultaneously
+lifts `a` and `b` to the type family `C`.
+
+The definition of (ordinary) double lifts is somewhat simpler: Given a lift `b`
+of `a : I → A` to a type family `B : A → 𝒰`, a
+{{#concept "double lift" Disambiguation="families of elements"}} of `a` and `b`
+to a type family
+
+```text
+  C : (x : A) → B x → 𝒰
+```
+
+is a family of elements
+
+```text
+  (i : I) → C (a i) (b i).
+```
+
+Note that this is the type of double lifts in the sense that it simultaneously
+lifts `a` and `b` to the type family `C`.
+
+The type of double lifts plays a role in the
+[universal property of the family of fibers of a map](foundation.universal-property-family-of-fibers-of-maps.md).
+
+## Definitions
+
+### Dependent double lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
+  {B : (i : I) → A i → UU l3} (b : dependent-lift-family-of-elements a B)
+  (C : (i : I) (x : A i) → B i x → UU l4)
+  where
+
+  dependent-double-lift-family-of-elements : UU (l1 ⊔ l4)
+  dependent-double-lift-family-of-elements =
+    dependent-lift-family-of-elements b (λ i → C i (a i))
+```
+
+### Double lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {a : I → A}
+  {B : A → UU l3} (b : lift-family-of-elements a B) (C : (x : A) → B x → UU l4)
+  where
+
+  double-lift-family-of-elements : UU (l1 ⊔ l4)
+  double-lift-family-of-elements =
+    dependent-lift-family-of-elements b (λ i → C (a i))
+```
+
+## See also
+
+- [Lifts of families of elements](orthogonal-factorization-systems.lifts-families-of-elements.md)
+- [Lifts of maps](orthogonal-factorization-systems.lifts-of-maps.md)
+- [The universal property of the family of fibers of a map](foundation.universal-property-family-of-fibers-of-maps.md)
diff --git a/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md
new file mode 100644
index 0000000000..5a617ec37c
--- /dev/null
+++ b/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md
@@ -0,0 +1,291 @@
+# Extensions of double lifts of families of elements
+
+```agda
+module
+  orthogonal-factorization-systems.extensions-double-lifts-families-of-elements
+  where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+
+open import orthogonal-factorization-systems.double-lifts-families-of-elements
+open import orthogonal-factorization-systems.lifts-families-of-elements
+```
+
+</details>
+
+## Idea
+
+Consider a
+[dependent lift](orthogonal-factorization-systems.lifts-families-of-elements.md)
+`b : (i : I) → B i (a i)` of a family of elements `a : I → A`, a type family `C`
+over `B` and a
+[double lift](orthogonal-factorization-systems.double-lifts-families-of-elements.md)
+
+```text
+  c : (i : I) → C i (a i) (b i)
+```
+
+of the lift `b` of `a`. An
+{{#concept "extension" Disambiguation="dependent double family of elements"}} of
+`b` to `A` consists of a family of elements
+`f : (i : I) (x : A i) (y : B i x) → C i x y` equipped with a
+[homotopy](foundation-core.homotopies.md) witnessing that the
+[identification](foundation-core.identity-types.md) `f i (a i) (b i) ＝ c i`
+holds for every `i : I`.
+
+Extensions of dependent double lifts play a role in the
+[universal property of the family of fibers of a map](foundation.universal-property-family-of-fibers-of-maps.md)
+
+## Definitions
+
+### Evaluating families of elements at dependent double lifts of families of elements
+
+Any family of elements `b : (i : I) → B i (a i)` dependent over a family of
+elements `a : (i : I) → A i` induces an evaluation map
+
+```text
+  ((i : I) (x : A i) (y : B i x) → C i x y) → ((i : I) → C i (a i) (b i))
+```
+
+given by `c ↦ (λ i → c i (a i) (b i))`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
+  {B : (i : I) → A i → UU l3} (b : dependent-lift-family-of-elements a B)
+  {C : (i : I) (x : A i) → B i x → UU l4}
+  where
+
+  ev-dependent-double-lift-family-of-elements :
+    ((i : I) (x : A i) (y : B i x) → C i x y) →
+    dependent-double-lift-family-of-elements b C
+  ev-dependent-double-lift-family-of-elements h i = h i (a i) (b i)
+```
+
+### Evaluating families of elements at double lifts of families of elements
+
+Any family of elements `b : (i : I) → B (a i)` dependent over a family of
+elements `a : I → A` induces an evaluation map
+
+```text
+  ((x : A) (y : B x) → C x y) → ((i : I) → C (a i) (b i))
+```
+
+given by `c ↦ (λ i → c (a i) (b i))`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {a : I → A}
+  {B : A → UU l3} (b : lift-family-of-elements a B)
+  {C : (x : A) → B x → UU l4}
+  where
+
+  ev-double-lift-family-of-elements :
+    ((x : A) (y : B x) → C x y) → double-lift-family-of-elements b C
+  ev-double-lift-family-of-elements h i = h (a i) (b i)
+```
+
+### Dependent extensions of double lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
+  {B : (i : I) → A i → UU l3} (b : dependent-lift-family-of-elements a B)
+  (C : (i : I) (x : A i) (y : B i x) → UU l4)
+  (c : dependent-double-lift-family-of-elements b C)
+  where
+
+  is-extension-dependent-double-lift-family-of-elements :
+    (f : (i : I) (x : A i) (y : B i x) → C i x y) → UU (l1 ⊔ l4)
+  is-extension-dependent-double-lift-family-of-elements f =
+    ev-dependent-double-lift-family-of-elements b f ~ c
+
+  extension-dependent-double-lift-family-of-elements : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  extension-dependent-double-lift-family-of-elements =
+    Σ ( (i : I) (x : A i) (y : B i x) → C i x y)
+      ( is-extension-dependent-double-lift-family-of-elements)
+
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
+  {B : (i : I) → A i → UU l3} {b : dependent-lift-family-of-elements a B}
+  {C : (i : I) (x : A i) (y : B i x) → UU l4}
+  {c : dependent-double-lift-family-of-elements b C}
+  (f : extension-dependent-double-lift-family-of-elements b C c)
+  where
+
+  family-of-elements-extension-dependent-double-lift-family-of-elements :
+    (i : I) (x : A i) (y : B i x) → C i x y
+  family-of-elements-extension-dependent-double-lift-family-of-elements =
+    pr1 f
+
+  is-extension-extension-dependent-double-lift-family-of-elements :
+    is-extension-dependent-double-lift-family-of-elements b C c
+      ( family-of-elements-extension-dependent-double-lift-family-of-elements)
+  is-extension-extension-dependent-double-lift-family-of-elements = pr2 f
+```
+
+### Extensions of double lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {a : I → A}
+  {B : A → UU l3} (b : lift-family-of-elements a B)
+  (C : (x : A) (y : B x) → UU l4) (c : double-lift-family-of-elements b C)
+  where
+
+  is-extension-double-lift-family-of-elements :
+    (f : (x : A) (y : B x) → C x y) → UU (l1 ⊔ l4)
+  is-extension-double-lift-family-of-elements f =
+    ev-double-lift-family-of-elements b f ~ c
+
+  extension-double-lift-family-of-elements : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  extension-double-lift-family-of-elements =
+    Σ ((x : A) (y : B x) → C x y) is-extension-double-lift-family-of-elements
+
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {a : I → A}
+  {B : A → UU l3} {b : lift-family-of-elements a B}
+  {C : (x : A) (y : B x) → UU l4} {c : double-lift-family-of-elements b C}
+  (f : extension-double-lift-family-of-elements b C c)
+  where
+
+  family-of-elements-extension-double-lift-family-of-elements :
+    (x : A) (y : B x) → C x y
+  family-of-elements-extension-double-lift-family-of-elements = pr1 f
+
+  is-extension-extension-double-lift-family-of-elements :
+    is-extension-double-lift-family-of-elements b C c
+      ( family-of-elements-extension-double-lift-family-of-elements)
+  is-extension-extension-double-lift-family-of-elements = pr2 f
+```
+
+### Identity extensions of dependent double lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
+  {B : (i : I) → A i → UU l3} (b : dependent-lift-family-of-elements a B)
+  where
+
+  id-extension-dependent-double-lift-family-of-elements :
+    extension-dependent-double-lift-family-of-elements b (λ i x y → B i x) b
+  pr1 id-extension-dependent-double-lift-family-of-elements i x = id
+  pr2 id-extension-dependent-double-lift-family-of-elements = refl-htpy
+```
+
+### Identity extensions of double lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {a : I → A}
+  {B : A → UU l3} (b : lift-family-of-elements a B)
+  where
+
+  id-extension-double-lift-family-of-elements :
+    extension-double-lift-family-of-elements b (λ x (y : B x) → B x) b
+  pr1 id-extension-double-lift-family-of-elements x = id
+  pr2 id-extension-double-lift-family-of-elements = refl-htpy
+```
+
+### Composition of extensions of dependent double lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
+  {A : I → UU l2} {a : (i : I) → A i}
+  {B : (i : I) → A i → UU l3} {b : dependent-lift-family-of-elements a B}
+  {C : (i : I) → A i → UU l4} {c : dependent-lift-family-of-elements a C}
+  {D : (i : I) → A i → UU l5} {d : dependent-lift-family-of-elements a D}
+  (g :
+    extension-dependent-double-lift-family-of-elements c
+      ( λ i x (_ : C i x) → D i x)
+      ( d))
+  (f :
+    extension-dependent-double-lift-family-of-elements b
+      ( λ i x (_ : B i x) → C i x)
+      ( c))
+  where
+
+  family-of-elements-comp-extension-dependent-double-lift-family-of-elements :
+    (i : I) (x : A i) → B i x → D i x
+  family-of-elements-comp-extension-dependent-double-lift-family-of-elements
+    i x =
+    family-of-elements-extension-dependent-double-lift-family-of-elements
+      g i x ∘
+    family-of-elements-extension-dependent-double-lift-family-of-elements
+      f i x
+
+  is-extension-comp-extension-dependent-double-lift-family-of-elements :
+    is-extension-dependent-double-lift-family-of-elements b
+      ( λ i x _ → D i x)
+      ( d)
+      ( family-of-elements-comp-extension-dependent-double-lift-family-of-elements)
+  is-extension-comp-extension-dependent-double-lift-family-of-elements i =
+    ( ap
+      ( family-of-elements-extension-dependent-double-lift-family-of-elements
+        g i (a i))
+      ( is-extension-extension-dependent-double-lift-family-of-elements f i)) ∙
+    ( is-extension-extension-dependent-double-lift-family-of-elements g i)
+
+  comp-extension-dependent-double-lift-family-of-elements :
+    extension-dependent-double-lift-family-of-elements b
+      ( λ i x (_ : B i x) → D i x)
+      ( d)
+  pr1 comp-extension-dependent-double-lift-family-of-elements =
+    family-of-elements-comp-extension-dependent-double-lift-family-of-elements
+  pr2 comp-extension-dependent-double-lift-family-of-elements =
+    is-extension-comp-extension-dependent-double-lift-family-of-elements
+```
+
+### Composition of extensions of double lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {I : UU l1} {A : UU l2} {a : I → A}
+  {B : A → UU l3} {b : lift-family-of-elements a B}
+  {C : A → UU l4} {c : lift-family-of-elements a C}
+  {D : A → UU l5} {d : lift-family-of-elements a D}
+  (g : extension-double-lift-family-of-elements c (λ x (_ : C x) → D x) d)
+  (f : extension-double-lift-family-of-elements b (λ x (_ : B x) → C x) c)
+  where
+
+  family-of-elements-comp-extension-double-lift-family-of-elements :
+    (x : A) → B x → D x
+  family-of-elements-comp-extension-double-lift-family-of-elements x =
+    family-of-elements-extension-double-lift-family-of-elements g x ∘
+    family-of-elements-extension-double-lift-family-of-elements f x
+
+  is-extension-comp-extension-double-lift-family-of-elements :
+    is-extension-double-lift-family-of-elements b
+      ( λ x _ → D x)
+      ( d)
+      ( family-of-elements-comp-extension-double-lift-family-of-elements)
+  is-extension-comp-extension-double-lift-family-of-elements i =
+    ( ap
+      ( family-of-elements-extension-double-lift-family-of-elements g (a i))
+      ( is-extension-extension-double-lift-family-of-elements f i)) ∙
+    ( is-extension-extension-double-lift-family-of-elements g i)
+
+  comp-extension-double-lift-family-of-elements :
+    extension-double-lift-family-of-elements b (λ x (_ : B x) → D x) d
+  pr1 comp-extension-double-lift-family-of-elements =
+    family-of-elements-comp-extension-double-lift-family-of-elements
+  pr2 comp-extension-double-lift-family-of-elements =
+    is-extension-comp-extension-double-lift-family-of-elements
+```
+
+## See also
+
+- [Extensions of lifts of families of elements](orthogonal-factorization-systems.extensions-lifts-families-of-elements.md)
+- [Extensions of maps](orthogonal-factorization-systems.extensions-of-maps.md)
+- [The universal property of the family of fibers of a map](foundation.universal-property-family-of-fibers-of-maps.md)
diff --git a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md
new file mode 100644
index 0000000000..f7998568ba
--- /dev/null
+++ b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md
@@ -0,0 +1,311 @@
+# Extensions of families of elements
+
+```agda
+module
+  orthogonal-factorization-systems.extensions-lifts-families-of-elements
+  where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+
+open import orthogonal-factorization-systems.lifts-families-of-elements
+```
+
+</details>
+
+## Idea
+
+Consider a family of elements `a : I → A`, a type family `B` over `A` and a
+[lift](orthogonal-factorization-systems.lifts-families-of-elements.md)
+
+```text
+  b : (i : I) → B (a i)
+```
+
+of the family of elements `a`. An
+{{#concept "extension" Disambiguation="family of elements"}} of `b` to `A`
+consists of a family of elements `f : (x : A) → B x` equipped with a
+[homotopy](foundation-core.homotopies.md) `f ∘ a ~ b`.
+
+More generally, given a family of elements `a : (i : I) → A i`, a type family
+`B` over `A`, and a dependent lift
+
+```text
+  b : (i : I) → B i (a i)
+```
+
+of the family of elements `A`, a
+{{#concet "dependent extension" Disambiguation"family of elements"}} of `b` to
+`A` consists of a family of elements
+
+```text
+  f : (i : I) (x : A i) → B i x
+```
+
+equipped with a homotopy `(i : I) → f i (a i) ＝ b i`.
+
+## Definitions
+
+### Evaluating families of elements at lifts of families of elements
+
+Any family of elements `a : (i : I) → A i` induces an evaluation map
+
+```text
+  ((i : I) (x : A i) → B i x) → ((i : I) → B i (a i))
+```
+
+defined by `b ↦ (λ i → b i (a i))`.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
+  {B : (i : I) → A i → UU l3}
+  where
+
+  ev-dependent-lift-family-of-elements :
+    ((i : I) (x : A i) → B i x) → dependent-lift-family-of-elements a B
+  ev-dependent-lift-family-of-elements b i = b i (a i)
+
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} (a : I → A) {B : A → UU l3}
+  where
+
+  ev-lift-family-of-elements :
+    ((x : A) → B x) → lift-family-of-elements a B
+  ev-lift-family-of-elements b i = b (a i)
+```
+
+### Dependent extensions of dependent lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
+  (B : (i : I) → A i → UU l3) (b : dependent-lift-family-of-elements a B)
+  where
+
+  is-extension-dependent-lift-family-of-elements :
+    (f : (i : I) (x : A i) → B i x) → UU (l1 ⊔ l3)
+  is-extension-dependent-lift-family-of-elements f =
+    ev-dependent-lift-family-of-elements a f ~ b
+
+  extension-dependent-lift-family-of-elements : UU (l1 ⊔ l2 ⊔ l3)
+  extension-dependent-lift-family-of-elements =
+    Σ ((i : I) (x : A i) → B i x) is-extension-dependent-lift-family-of-elements
+
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
+  {B : (i : I) → A i → UU l3} {b : dependent-lift-family-of-elements a B}
+  (f : extension-dependent-lift-family-of-elements a B b)
+  where
+
+  family-of-elements-extension-dependent-lift-family-of-elements :
+    (i : I) (x : A i) → B i x
+  family-of-elements-extension-dependent-lift-family-of-elements = pr1 f
+
+  is-extension-extension-dependent-lift-family-of-elements :
+    is-extension-dependent-lift-family-of-elements a B b
+      ( family-of-elements-extension-dependent-lift-family-of-elements)
+  is-extension-extension-dependent-lift-family-of-elements = pr2 f
+```
+
+### Extensions of lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} (a : I → A)
+  (B : A → UU l3) (b : lift-family-of-elements a B)
+  where
+
+  is-extension-lift-family-of-elements : (f : (x : A) → B x) → UU (l1 ⊔ l3)
+  is-extension-lift-family-of-elements f = ev-lift-family-of-elements a f ~ b
+
+  extension-lift-family-of-elements : UU (l1 ⊔ l2 ⊔ l3)
+  extension-lift-family-of-elements =
+    Σ ((x : A) → B x) is-extension-lift-family-of-elements
+
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {a : I → A}
+  {B : A → UU l3} {b : lift-family-of-elements a B}
+  (f : extension-lift-family-of-elements a B b)
+  where
+
+  family-of-elements-extension-lift-family-of-elements : (x : A) → B x
+  family-of-elements-extension-lift-family-of-elements = pr1 f
+
+  is-extension-extension-lift-family-of-elements :
+    is-extension-lift-family-of-elements a B b
+      ( family-of-elements-extension-lift-family-of-elements)
+  is-extension-extension-lift-family-of-elements = pr2 f
+```
+
+### Identity extensions of dependent lifts of families of elements
+
+```agda
+module _
+  {l1 l2 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
+  where
+
+  id-extension-dependent-lift-family-of-elements :
+    extension-dependent-lift-family-of-elements a (λ i _ → A i) a
+  pr1 id-extension-dependent-lift-family-of-elements i = id
+  pr2 id-extension-dependent-lift-family-of-elements = refl-htpy
+```
+
+### Identity extensions of lifts of families of elements
+
+```agda
+module _
+  {l1 l2 : Level} {I : UU l1} {A : UU l2} (a : I → A)
+  where
+
+  id-extension-lift-family-of-elements :
+    extension-lift-family-of-elements a (λ _ → A) a
+  pr1 id-extension-lift-family-of-elements = id
+  pr2 id-extension-lift-family-of-elements = refl-htpy
+```
+
+### Composition of extensions of dependent lifts of families of elements
+
+Consider three type families `A`, `B`, and `C` over a type `I` equipped with
+sections
+
+```text
+  a : (i : I) → A i
+  b : (i : I) → B i
+  c : (i : I) → C i.
+```
+
+Furthermore, suppose that `g` is an extension of `c` along `b`, and suppose that
+`f` is an extension of `b` along `a`. In other words, `g` consists of a family
+of maps
+
+```text
+  g : (i : I) → B i → C i
+```
+
+equipped with a homotopy witnessing that `g i (b i) ＝ c i` for all `i : I`, and
+`f` consists of a family of maps
+
+```text
+  f : (i : I) → A i → B i
+```
+
+equipped with a homotopy witnessing that `f i (a i) ＝ b i` for all `i : I`.
+Then we can compose `g` and `f` fiberwise, resulting in a family of maps
+
+```text
+  λ i → g i ∘ f i : (i : I) → A i → C i
+```
+
+equipped with a homotopy witnessing that `g i (f i (a i)) ＝ c i` for all
+`i : I`. In other words, extensions of `c` along `b` can be composed with
+extensions of `b` along `a` to obtain extensions of `c` along `a`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1}
+  {A : I → UU l2} {a : (i : I) → A i}
+  {B : I → UU l3} {b : (i : I) → B i}
+  {C : I → UU l4} {c : (i : I) → C i}
+  (g : extension-dependent-lift-family-of-elements b (λ i _ → C i) c)
+  (f : extension-dependent-lift-family-of-elements a (λ i _ → B i) b)
+  where
+
+  family-of-elements-comp-extension-dependent-lift-family-of-elements :
+    (i : I) → A i → C i
+  family-of-elements-comp-extension-dependent-lift-family-of-elements i =
+    family-of-elements-extension-dependent-lift-family-of-elements g i ∘
+    family-of-elements-extension-dependent-lift-family-of-elements f i
+
+  is-extension-comp-extension-dependent-lift-family-of-elements :
+    is-extension-dependent-lift-family-of-elements a
+      ( λ i _ → C i)
+      ( c)
+      ( family-of-elements-comp-extension-dependent-lift-family-of-elements)
+  is-extension-comp-extension-dependent-lift-family-of-elements i =
+    ( ap
+      ( family-of-elements-extension-dependent-lift-family-of-elements g i)
+      ( is-extension-extension-dependent-lift-family-of-elements f i)) ∙
+    ( is-extension-extension-dependent-lift-family-of-elements g i)
+
+  comp-extension-dependent-lift-family-of-elements :
+    extension-dependent-lift-family-of-elements a (λ i _ → C i) c
+  pr1 comp-extension-dependent-lift-family-of-elements =
+    family-of-elements-comp-extension-dependent-lift-family-of-elements
+  pr2 comp-extension-dependent-lift-family-of-elements =
+    is-extension-comp-extension-dependent-lift-family-of-elements
+```
+
+### Composition of extensions of lifts of families of elements
+
+Consider three types `A`, `B`, and `C` equipped with maps
+
+```text
+  a : I → A
+  b : I → B
+  c : I → C.
+```
+
+Furthermore, suppose that `g` is an extension of `c` along `b`, and suppose that
+`f` is an extension of `b` along `a`. In other words, we assume a commuting
+diagram
+
+```text
+        I
+      / | \
+    a/  |  \c
+    /   |b  \
+   V    V    V
+  A --> B --> C
+     f     g
+```
+
+The composite `g ∘ f` is then an extension of `c` along `a.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1}
+  {A : UU l2} {a : I → A}
+  {B : UU l3} {b : I → B}
+  {C : UU l4} {c : I → C}
+  (g : extension-lift-family-of-elements b (λ _ → C) c)
+  (f : extension-lift-family-of-elements a (λ _ → B) b)
+  where
+
+  map-comp-extension-lift-family-of-elements : A → C
+  map-comp-extension-lift-family-of-elements =
+    family-of-elements-extension-lift-family-of-elements g ∘
+    family-of-elements-extension-lift-family-of-elements f
+
+  is-extension-comp-extension-lift-family-of-elements :
+    is-extension-lift-family-of-elements a
+      ( λ _ → C)
+      ( c)
+      ( map-comp-extension-lift-family-of-elements)
+  is-extension-comp-extension-lift-family-of-elements x =
+    ( ap
+      ( family-of-elements-extension-lift-family-of-elements g)
+      ( is-extension-extension-lift-family-of-elements f x)) ∙
+    ( is-extension-extension-lift-family-of-elements g x)
+
+  comp-extension-lift-family-of-elements :
+    extension-lift-family-of-elements a (λ _ → C) c
+  pr1 comp-extension-lift-family-of-elements =
+    map-comp-extension-lift-family-of-elements
+  pr2 comp-extension-lift-family-of-elements =
+    is-extension-comp-extension-lift-family-of-elements
+```
+
+## See also
+
+- [Extensions of double lifts of families of elements](orthogonal-factorization-systems.extensions-double-lifts-families-of-elements.md)
+- [Extensions of maps](orthogonal-factorization-systems.extensions-of-maps.md)
diff --git a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
new file mode 100644
index 0000000000..e3a3aa1f13
--- /dev/null
+++ b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
@@ -0,0 +1,93 @@
+# Lifts of families of elements
+
+```agda
+module orthogonal-factorization-systems.lifts-families-of-elements where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a family of elements `a : (i : I) → A i` and a type family
+
+```text
+  B : (i : I) → A i → 𝒰.
+```
+
+A {{#concept "dependent lift" Disambiguation="family of elements"}} of the
+family of elements `a` to the type family `B` is a family of elements
+
+```text
+  (i : I) → B i (a i).
+```
+
+An important special case occurs when `a : I → A` is a family of elements of a
+fixed type `A`, and `B` is a type family over `A`. In this case, a
+{{#concept "lift" Disambiguation="family of elements"}} of the family of
+elements `a` is a family of elements
+
+```text
+  (i : I) → B (a i).
+```
+
+## Definitions
+
+### Dependent lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
+  (B : (i : I) → A i → UU l3)
+  where
+
+  dependent-lift-family-of-elements : UU (l1 ⊔ l3)
+  dependent-lift-family-of-elements = (i : I) → B i (a i)
+```
+
+### Lifts of families of elements
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} (a : I → A) (B : A → UU l3)
+  where
+
+  lift-family-of-elements : UU (l1 ⊔ l3)
+  lift-family-of-elements = dependent-lift-family-of-elements a (λ _ → B)
+```
+
+### Dependent lifts of binary families of elements
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
+  {B : (i : I) → A i → UU l3} (C : (i : I) (x : A i) → B i x → UU l4)
+  where
+
+  dependent-lift-binary-family-of-elements : UU (l1 ⊔ l3 ⊔ l4)
+  dependent-lift-binary-family-of-elements =
+    dependent-lift-family-of-elements a (λ i x → (y : B i x) → C i x y)
+```
+
+### Lifts of binary families of elements
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (a : I → A)
+  {B : A → UU l3} {C : (x : A) → B x → UU l4}
+  where
+
+  lift-binary-family-of-elements : UU (l1 ⊔ l3 ⊔ l4)
+  lift-binary-family-of-elements =
+    dependent-lift-binary-family-of-elements a (λ _ → C)
+```
+
+## See also
+
+- [Double lifts of families of elements](orthogonal-factorization-systems.double-lifts-families-of-elements.md)
+- [Lifts of maps](orthogonal-factorization-systems.lifts-of-maps.md)
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index c86b59ed51..0558cae6e7 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -77,6 +77,7 @@ open import synthetic-homotopy-theory.pullback-property-pushouts public
 open import synthetic-homotopy-theory.pushout-products public
 open import synthetic-homotopy-theory.pushouts public
 open import synthetic-homotopy-theory.pushouts-of-pointed-types public
+open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public
diff --git a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
index cbace8a721..1bca6b7e9a 100644
--- a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
@@ -19,12 +19,15 @@ open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
+open import foundation.retractions
+open import foundation.retracts-of-types
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies
 
 open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams
 open import synthetic-homotopy-theory.morphisms-sequential-diagrams
+open import synthetic-homotopy-theory.retracts-of-sequential-diagrams
 open import synthetic-homotopy-theory.sequential-colimits
 open import synthetic-homotopy-theory.sequential-diagrams
 open import synthetic-homotopy-theory.universal-property-sequential-colimits
@@ -69,7 +72,7 @@ module _
     comp-hom-sequential-diagram A B (constant-sequential-diagram X) c f
 ```
 
-### A morphism of sequential diagrams induces a map of sequential colimits
+### A morphism of sequential diagrams induces a map of standard sequential colimits
 
 The induced map
 
@@ -202,7 +205,7 @@ module _
       ( inv-htpy (coherence-htpy-cocone-map-hom-standard-sequential-colimit n))
 ```
 
-### Homotopies between morphisms of sequential diagrams induce homotopies of maps of sequential colimits
+### Homotopies between morphisms of sequential diagrams induce homotopies of maps of standard sequential colimits
 
 ```agda
 module _
@@ -255,7 +258,7 @@ module _
       ( htpy-preserves-id-map-hom-standard-sequential-colimit)
 ```
 
-### Forming sequential colimits preserves composition of morphisms of sequential diagrams
+### Forming standard sequential colimits preserves composition of morphisms of sequential diagrams
 
 We have `(f ∘ g)∞ ~ (f∞ ∘ g∞) : A∞ → C∞`.
 
@@ -374,7 +377,7 @@ module _
       htpy-preserves-comp-map-hom-standard-sequential-colimit
 ```
 
-### An equivalence of sequential diagrams induces an equivalence of cocones
+### An equivalence of sequential diagrams induces an equivalence of standard sequential colimits
 
 Additionally, the underlying map of the inverse equivalence is definitionally
 equal to the map induced by the inverse of the equivalence of sequential
@@ -441,6 +444,61 @@ module _
     is-equiv-map-hom-standard-sequential-colimit
 ```
 
+### A retract of sequential diagrams induces a retract of standard sequential colimits
+
+Additionally, the underlying map of the retraction is definitionally equal to
+the map induced by the retraction of sequential diagrams.
+
+```agda
+module _
+  { l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2}
+  ( R : A retract-of-sequential-diagram B)
+  where
+
+  map-inclusion-retract-standard-sequential-colimit :
+    standard-sequential-colimit A → standard-sequential-colimit B
+  map-inclusion-retract-standard-sequential-colimit =
+    map-hom-standard-sequential-colimit B
+      ( inclusion-retract-sequential-diagram A B R)
+
+  map-hom-retraction-retract-standard-sequential-colimit :
+    standard-sequential-colimit B → standard-sequential-colimit A
+  map-hom-retraction-retract-standard-sequential-colimit =
+    map-hom-standard-sequential-colimit A
+      ( hom-retraction-retract-sequential-diagram A B R)
+
+  abstract
+    is-retraction-map-hom-retraction-retract-standard-sequential-colimit :
+      is-retraction
+        ( map-inclusion-retract-standard-sequential-colimit)
+        ( map-hom-retraction-retract-standard-sequential-colimit)
+    is-retraction-map-hom-retraction-retract-standard-sequential-colimit =
+      ( inv-htpy
+        ( preserves-comp-map-hom-standard-sequential-colimit
+          ( hom-retraction-retract-sequential-diagram A B R)
+          ( inclusion-retract-sequential-diagram A B R))) ∙h
+      ( htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram
+        ( is-retraction-hom-retraction-retract-sequential-diagram A B R)) ∙h
+      ( preserves-id-map-hom-standard-sequential-colimit)
+
+  retraction-retract-standard-sequential-colimit :
+    retraction
+      ( map-hom-standard-sequential-colimit B
+        ( inclusion-retract-sequential-diagram A B R))
+  pr1 retraction-retract-standard-sequential-colimit =
+    map-hom-retraction-retract-standard-sequential-colimit
+  pr2 retraction-retract-standard-sequential-colimit =
+    is-retraction-map-hom-retraction-retract-standard-sequential-colimit
+
+  retract-retract-standard-sequential-colimit :
+    (standard-sequential-colimit A) retract-of (standard-sequential-colimit B)
+  pr1 retract-retract-standard-sequential-colimit =
+    map-hom-standard-sequential-colimit B
+      ( inclusion-retract-sequential-diagram A B R)
+  pr2 retract-retract-standard-sequential-colimit =
+    retraction-retract-standard-sequential-colimit
+```
+
 ## References
 
 1. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. 2020. Sequential
diff --git a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
index d906a3862b..ca081ffb0b 100644
--- a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
@@ -174,13 +174,13 @@ module _
   ( f g : hom-sequential-diagram A B)
   where
 
-  coherence-htpy-sequential-diagram :
+  coherence-htpy-hom-sequential-diagram :
     ( H :
       ( n : ℕ) →
       ( map-hom-sequential-diagram B f n) ~
       ( map-hom-sequential-diagram B g n)) →
     UU (l1 ⊔ l2)
-  coherence-htpy-sequential-diagram H =
+  coherence-htpy-hom-sequential-diagram H =
     ( n : ℕ) →
     coherence-square-homotopies
       ( map-sequential-diagram B n ·l H n)
@@ -193,7 +193,7 @@ module _
     Σ ( ( n : ℕ) →
         ( map-hom-sequential-diagram B f n) ~
         ( map-hom-sequential-diagram B g n))
-      ( coherence-htpy-sequential-diagram)
+      ( coherence-htpy-hom-sequential-diagram)
 ```
 
 ### Components of homotopies between morphisms of sequential diagrams
@@ -212,7 +212,7 @@ module _
   htpy-htpy-hom-sequential-diagram = pr1 H
 
   coherence-htpy-htpy-hom-sequential-diagram :
-    coherence-htpy-sequential-diagram B f g htpy-htpy-hom-sequential-diagram
+    coherence-htpy-hom-sequential-diagram B f g htpy-htpy-hom-sequential-diagram
   coherence-htpy-htpy-hom-sequential-diagram = pr2 H
 ```
 
@@ -244,7 +244,7 @@ module _
       is-torsorial (htpy-hom-sequential-diagram B f)
     is-torsorial-htpy-sequential-diagram f =
       is-torsorial-Eq-structure
-        ( ev-pair (coherence-htpy-sequential-diagram B f))
+        ( ev-pair (coherence-htpy-hom-sequential-diagram B f))
         ( is-torsorial-binary-htpy (map-hom-sequential-diagram B f))
         ( map-hom-sequential-diagram B f , ev-pair refl-htpy)
         ( is-torsorial-Eq-Π _
diff --git a/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md
new file mode 100644
index 0000000000..33a6e0ae22
--- /dev/null
+++ b/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md
@@ -0,0 +1,204 @@
+# Retracts of sequential diagrams
+
+```agda
+module synthetic-homotopy-theory.retracts-of-sequential-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-function-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.retractions
+open import foundation.retracts-of-types
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.morphisms-sequential-diagrams
+open import synthetic-homotopy-theory.sequential-diagrams
+```
+
+</details>
+
+## Idea
+
+A {{#concept "retract" Disambiguation="sequential diagram"}} of sequential
+diagrams `A` of `B` is a
+[morphism of sequential diagrams](synthetic-homotopy-theory.morphisms-sequential-diagrams.md)
+`B → A` that is a retraction.
+
+## Definitions
+
+### The predicate of being a retraction of sequential diagrams
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  (i : hom-sequential-diagram A B) (r : hom-sequential-diagram B A)
+  where
+
+  is-retraction-hom-sequential-diagram : UU l1
+  is-retraction-hom-sequential-diagram =
+    htpy-hom-sequential-diagram A
+      ( comp-hom-sequential-diagram A B A r i)
+      ( id-hom-sequential-diagram A)
+```
+
+### The type of retractions of a morphism of sequential diagrams
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  (i : hom-sequential-diagram A B)
+  where
+
+  retraction-hom-sequential-diagram : UU (l1 ⊔ l2)
+  retraction-hom-sequential-diagram =
+    Σ (hom-sequential-diagram B A) (is-retraction-hom-sequential-diagram A B i)
+
+  module _
+    (r : retraction-hom-sequential-diagram)
+    where
+
+    hom-retraction-hom-sequential-diagram : hom-sequential-diagram B A
+    hom-retraction-hom-sequential-diagram = pr1 r
+
+    is-retraction-hom-retraction-hom-sequential-diagram :
+      is-retraction-hom-sequential-diagram A B i
+        ( hom-retraction-hom-sequential-diagram)
+    is-retraction-hom-retraction-hom-sequential-diagram = pr2 r
+```
+
+### The predicate that a sequential diagram `A` is a retract of a sequential diagram `B`
+
+```agda
+retract-sequential-diagram :
+  {l1 l2 : Level} (B : sequential-diagram l2) (A : sequential-diagram l1) →
+  UU (l1 ⊔ l2)
+retract-sequential-diagram B A =
+  Σ (hom-sequential-diagram A B) (retraction-hom-sequential-diagram A B)
+```
+
+### The higher coherence in the definition of retracts of sequential diagrams
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  (i : hom-sequential-diagram A B) (r : hom-sequential-diagram B A)
+  where
+
+  coherence-retract-sequential-diagram :
+    ( (n : ℕ) →
+      is-retraction
+        ( map-hom-sequential-diagram B i n)
+        ( map-hom-sequential-diagram A r n)) →
+    UU l1
+  coherence-retract-sequential-diagram =
+    coherence-htpy-hom-sequential-diagram A
+      ( comp-hom-sequential-diagram A B A r i)
+      ( id-hom-sequential-diagram A)
+```
+
+### The binary relation `A B ↦ A retract-of-sequential-diagram B` asserting that `A` is a retract of the sequential diagram `B`
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  where
+
+  infix 6 _retract-of-sequential-diagram_
+
+  _retract-of-sequential-diagram_ : UU (l1 ⊔ l2)
+  _retract-of-sequential-diagram_ = retract-sequential-diagram B A
+
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  (R : A retract-of-sequential-diagram B)
+  where
+
+  inclusion-retract-sequential-diagram : hom-sequential-diagram A B
+  inclusion-retract-sequential-diagram = pr1 R
+
+  map-inclusion-retract-sequential-diagram :
+    (n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n
+  map-inclusion-retract-sequential-diagram =
+    map-hom-sequential-diagram B inclusion-retract-sequential-diagram
+
+  naturality-inclusion-retract-sequential-diagram :
+    naturality-hom-sequential-diagram A B
+      ( map-inclusion-retract-sequential-diagram)
+  naturality-inclusion-retract-sequential-diagram =
+    naturality-map-hom-sequential-diagram B
+      ( inclusion-retract-sequential-diagram)
+
+  retraction-retract-sequential-diagram :
+    retraction-hom-sequential-diagram A B inclusion-retract-sequential-diagram
+  retraction-retract-sequential-diagram = pr2 R
+
+  hom-retraction-retract-sequential-diagram : hom-sequential-diagram B A
+  hom-retraction-retract-sequential-diagram =
+    hom-retraction-hom-sequential-diagram A B
+      ( inclusion-retract-sequential-diagram)
+      ( retraction-retract-sequential-diagram)
+
+  map-hom-retraction-retract-sequential-diagram :
+    (n : ℕ) → family-sequential-diagram B n → family-sequential-diagram A n
+  map-hom-retraction-retract-sequential-diagram =
+    map-hom-sequential-diagram A hom-retraction-retract-sequential-diagram
+
+  naturality-hom-retraction-retract-sequential-diagram :
+    naturality-hom-sequential-diagram B A
+      ( map-hom-retraction-retract-sequential-diagram)
+  naturality-hom-retraction-retract-sequential-diagram =
+    naturality-map-hom-sequential-diagram A
+      ( hom-retraction-retract-sequential-diagram)
+
+  is-retraction-hom-retraction-retract-sequential-diagram :
+    is-retraction-hom-sequential-diagram A B
+      ( inclusion-retract-sequential-diagram)
+      ( hom-retraction-retract-sequential-diagram)
+  is-retraction-hom-retraction-retract-sequential-diagram =
+    is-retraction-hom-retraction-hom-sequential-diagram A B
+      ( inclusion-retract-sequential-diagram)
+      ( retraction-retract-sequential-diagram)
+
+  is-retraction-map-hom-retraction-retract-sequential-diagram :
+    (n : ℕ) →
+    is-retraction
+      ( map-inclusion-retract-sequential-diagram n)
+      ( map-hom-retraction-retract-sequential-diagram n)
+  is-retraction-map-hom-retraction-retract-sequential-diagram =
+    htpy-htpy-hom-sequential-diagram A
+      ( is-retraction-hom-retraction-retract-sequential-diagram)
+
+  retract-family-retract-sequential-diagram :
+    (n : ℕ) →
+    ( family-sequential-diagram A n) retract-of
+    ( family-sequential-diagram B n)
+  pr1 (retract-family-retract-sequential-diagram n) =
+    map-inclusion-retract-sequential-diagram n
+  pr1 (pr2 (retract-family-retract-sequential-diagram n)) =
+    map-hom-retraction-retract-sequential-diagram n
+  pr2 (pr2 (retract-family-retract-sequential-diagram n)) =
+    is-retraction-map-hom-retraction-retract-sequential-diagram n
+
+  coh-retract-sequential-diagram :
+    coherence-retract-sequential-diagram A B
+      ( inclusion-retract-sequential-diagram)
+      ( hom-retraction-retract-sequential-diagram)
+      ( is-retraction-map-hom-retraction-retract-sequential-diagram)
+  coh-retract-sequential-diagram =
+    coherence-htpy-htpy-hom-sequential-diagram A
+      ( is-retraction-hom-retraction-retract-sequential-diagram)
+```
+
+## See also
+
+- [Retracts of maps](foundation.retracts-of-maps.md)
diff --git a/tables/fibers-of-maps.md b/tables/fibers-of-maps.md
index 83de16f22c..2d788dd534 100644
--- a/tables/fibers-of-maps.md
+++ b/tables/fibers-of-maps.md
@@ -1,8 +1,9 @@
-| Concept                          | File                                                                                    |
-| -------------------------------- | --------------------------------------------------------------------------------------- |
-| Fibers of maps (foundation-core) | [`foundation-core.fibers-of-maps`](foundation-core.fibers-of-maps.md)                   |
-| Fibers of maps (foundation)      | [`foundation.fibers-of-maps`](foundation.fibers-of-maps.md)                             |
-| Equality in the fibers of a map  | [`foundation.equality-fibers-of-maps`](foundation.equality-fibers-of-maps.md)           |
-| Functoriality of fibers of maps  | [`foundation.functoriality-fibers-of-maps`](foundation.functoriality-fibers-of-maps.md) |
-| Fibers of pointed maps           | [`structured-types.fibers-of-pointed-maps`](structured-types.fibers-of-pointed-maps.md) |
-| Fibers of maps of finite types   | [`univalent-combinatorics.fibers-of-maps`](univalent-combinatorics.fibers-of-maps.md)   |
+| Concept                                                | File                                                                                                                  |
+| ------------------------------------------------------ | --------------------------------------------------------------------------------------------------------------------- |
+| Fibers of maps (foundation-core)                       | [`foundation-core.fibers-of-maps`](foundation-core.fibers-of-maps.md)                                                 |
+| Fibers of maps (foundation)                            | [`foundation.fibers-of-maps`](foundation.fibers-of-maps.md)                                                           |
+| Equality in the fibers of a map                        | [`foundation.equality-fibers-of-maps`](foundation.equality-fibers-of-maps.md)                                         |
+| Functoriality of fibers of maps                        | [`foundation.functoriality-fibers-of-maps`](foundation.functoriality-fibers-of-maps.md)                               |
+| Fibers of pointed maps                                 | [`structured-types.fibers-of-pointed-maps`](structured-types.fibers-of-pointed-maps.md)                               |
+| Fibers of maps of finite types                         | [`univalent-combinatorics.fibers-of-maps`](univalent-combinatorics.fibers-of-maps.md)                                 |
+| The universal property of the family of fibers of maps | [`foundation.universal-property-family-of-fibers-of-maps`](foundation.universal-property-family-of-fibers-of-maps.md) |