diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md
index 0f9dde78f7..af5aa60f28 100644
--- a/src/foundation/surjective-maps.lagda.md
+++ b/src/foundation/surjective-maps.lagda.md
@@ -52,7 +52,9 @@ open import foundation-core.torsorial-type-families
 open import foundation-core.truncated-maps
 open import foundation-core.truncation-levels
 
+open import orthogonal-factorization-systems.equality-extensions-maps
 open import orthogonal-factorization-systems.extensions-maps
+open import orthogonal-factorization-systems.postcomposition-extensions-maps
 ```
 
 </details>
@@ -831,8 +833,8 @@ module _
           ( g ∘ i)
           ( postcomp-extension f i g (j , N))
           ( h , L)
-          ( M)
-          ( λ a →
+          ( M ,
+            λ a →
             ( ap
               ( concat' (g (i a)) (M (f a)))
               ( is-section-map-inv-is-equiv
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index e2a8bf7286..e412d0e8ef 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -16,6 +16,8 @@ open import orthogonal-factorization-systems.closed-modalities public
 open import orthogonal-factorization-systems.continuation-modalities public
 open import orthogonal-factorization-systems.double-lifts-families-of-elements public
 open import orthogonal-factorization-systems.double-negation-sheaves public
+open import orthogonal-factorization-systems.equality-extensions-maps public
+open import orthogonal-factorization-systems.extensions-dependent-maps 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-maps public
@@ -56,6 +58,7 @@ open import orthogonal-factorization-systems.null-types public
 open import orthogonal-factorization-systems.open-modalities public
 open import orthogonal-factorization-systems.orthogonal-factorization-systems public
 open import orthogonal-factorization-systems.orthogonal-maps public
+open import orthogonal-factorization-systems.postcomposition-extensions-maps public
 open import orthogonal-factorization-systems.precomposition-lifts-families-of-elements public
 open import orthogonal-factorization-systems.pullback-hom public
 open import orthogonal-factorization-systems.raise-modalities public
diff --git a/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md
new file mode 100644
index 0000000000..fca5f920a3
--- /dev/null
+++ b/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md
@@ -0,0 +1,189 @@
+# Equality of extensions of maps
+
+```agda
+module orthogonal-factorization-systems.equality-extensions-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.structure-identity-principle
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.torsorial-type-families
+
+open import orthogonal-factorization-systems.extensions-dependent-maps
+```
+
+</details>
+
+## Idea
+
+We characterize equality of
+[extensions](orthogonal-factorization-systems.extensions-maps.md) of
+([dependent](orthogonal-factorization-systems.extensions-dependent-maps.md))
+maps.
+
+On this page we conflate extensions of dependent maps and extensions of
+nondependent maps, as the characterization of equality coincides for the two
+notions.
+
+## Definition
+
+### Homotopies of extensions
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  {P : B → UU l3} (f : (x : A) → P (i x))
+  where
+
+  coherence-htpy-extension :
+    (e e' : extension-dependent-type i P f) →
+    map-extension-dependent-type e ~ map-extension-dependent-type e' →
+    UU (l1 ⊔ l3)
+  coherence-htpy-extension e e' K =
+    ( is-extension-map-extension-dependent-type e ∙h (K ·r i)) ~
+    ( is-extension-map-extension-dependent-type e')
+
+  htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3)
+  htpy-extension e e' =
+    Σ ( map-extension-dependent-type e ~ map-extension-dependent-type e')
+      ( coherence-htpy-extension e e')
+
+  refl-htpy-extension :
+    (e : extension-dependent-type i P f) → htpy-extension e e
+  pr1 (refl-htpy-extension e) = refl-htpy
+  pr2 (refl-htpy-extension e) = right-unit-htpy
+```
+
+### Homotopies of extensions with homotopies going the other way
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  {P : B → UU l3} (f : (x : A) → P (i x))
+  where
+
+  coherence-htpy-extension' :
+    (e e' : extension-dependent-type' i P f) →
+    map-extension-dependent-type' e ~ map-extension-dependent-type' e' →
+    UU (l1 ⊔ l3)
+  coherence-htpy-extension' e e' K =
+    ( is-extension-map-extension-dependent-type' e) ~
+    ( K ·r i ∙h is-extension-map-extension-dependent-type' e')
+
+  htpy-extension' :
+    (e e' : extension-dependent-type' i P f) → UU (l1 ⊔ l2 ⊔ l3)
+  htpy-extension' e e' =
+    Σ ( map-extension-dependent-type' e ~ map-extension-dependent-type' e')
+      ( coherence-htpy-extension' e e')
+
+  refl-htpy-extension' :
+    (e : extension-dependent-type' i P f) → htpy-extension' e e
+  pr1 (refl-htpy-extension' e) = refl-htpy
+  pr2 (refl-htpy-extension' e) = refl-htpy
+```
+
+## Properties
+
+### Homotopies characterize equality
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  {P : B → UU l3} (f : (x : A) → P (i x))
+  where
+
+  htpy-eq-extension :
+    (e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension i f e e'
+  htpy-eq-extension e .e refl = refl-htpy-extension i f e
+
+  abstract
+    is-torsorial-htpy-extension :
+      (e : extension-dependent-type i P f) → is-torsorial (htpy-extension i f e)
+    is-torsorial-htpy-extension e =
+      is-torsorial-Eq-structure
+        ( is-torsorial-htpy (map-extension-dependent-type e))
+        ( map-extension-dependent-type e , refl-htpy)
+        ( is-torsorial-htpy
+          ( is-extension-map-extension-dependent-type e ∙h
+            refl-htpy))
+
+  abstract
+    is-equiv-htpy-eq-extension :
+      (e e' : extension-dependent-type i P f) →
+      is-equiv (htpy-eq-extension e e')
+    is-equiv-htpy-eq-extension e =
+      fundamental-theorem-id
+        ( is-torsorial-htpy-extension e)
+        ( htpy-eq-extension e)
+
+  extensionality-extension :
+    (e e' : extension-dependent-type i P f) →
+    (e ＝ e') ≃ htpy-extension i f e e'
+  pr1 (extensionality-extension e e') = htpy-eq-extension e e'
+  pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e'
+
+  eq-htpy-extension :
+    (e e' : extension-dependent-type i P f) →
+    htpy-extension i f e e' → e ＝ e'
+  eq-htpy-extension e e' =
+    map-inv-equiv (extensionality-extension e e')
+```
+
+### Characterizing equality of extensions of dependent maps with homotopies going the other way
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  {P : B → UU l3} (f : (x : A) → P (i x))
+  where
+
+  htpy-eq-extension' :
+    (e e' : extension-dependent-type' i P f) →
+    e ＝ e' → htpy-extension' i f e e'
+  htpy-eq-extension' e .e refl =
+    refl-htpy-extension' i f e
+
+  abstract
+    is-torsorial-htpy-extension' :
+      (e : extension-dependent-type' i P f) →
+      is-torsorial (htpy-extension' i f e)
+    is-torsorial-htpy-extension' e =
+      is-torsorial-Eq-structure
+        ( is-torsorial-htpy (map-extension-dependent-type' e))
+        ( map-extension-dependent-type' e , refl-htpy)
+        ( is-torsorial-htpy
+          ( is-extension-map-extension-dependent-type' e))
+
+  abstract
+    is-equiv-htpy-eq-extension' :
+      (e e' : extension-dependent-type' i P f) →
+      is-equiv (htpy-eq-extension' e e')
+    is-equiv-htpy-eq-extension' e =
+      fundamental-theorem-id
+        ( is-torsorial-htpy-extension' e)
+        ( htpy-eq-extension' e)
+
+  extensionality-extension' :
+    (e e' : extension-dependent-type' i P f) →
+    (e ＝ e') ≃ (htpy-extension' i f e e')
+  pr1 (extensionality-extension' e e') =
+    htpy-eq-extension' e e'
+  pr2 (extensionality-extension' e e') =
+    is-equiv-htpy-eq-extension' e e'
+
+  eq-htpy-extension' :
+    (e e' : extension-dependent-type' i P f) →
+    htpy-extension' i f e e' → e ＝ e'
+  eq-htpy-extension' e e' =
+    map-inv-equiv (extensionality-extension' e e')
+```
diff --git a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md
new file mode 100644
index 0000000000..4c827b9f7c
--- /dev/null
+++ b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md
@@ -0,0 +1,319 @@
+# Extensions of dependent maps
+
+```agda
+module orthogonal-factorization-systems.extensions-dependent-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-dependent-functions
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
+open import foundation.dependent-pair-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.propositions
+open import foundation.sets
+open import foundation.transport-along-identifications
+open import foundation.truncated-types
+open import foundation.truncation-levels
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "extension" Disambiguation="of a dependent map along a map, types" Agda=extension-dependent-type}}
+of a dependent map `f : (x : A) → P (i x)` along a map `i : A → B` is a map
+`g : (y : B) → P y` such that `g` restricts along `i` to `f`.
+
+```text
+      A
+      |  \
+    i |    \ f
+      |      \
+      ∨   g   ∨
+  b ∈ B -----> P b
+```
+
+## Definition
+
+### Extensions of dependent maps
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  where
+
+  is-extension-dependent-type :
+    {P : B → UU l3} →
+    ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3)
+  is-extension-dependent-type f g = (f ~ g ∘ i)
+
+  extension-dependent-type :
+    (P : B → UU l3) →
+    ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3)
+  extension-dependent-type P f =
+    Σ ((y : B) → P y) (is-extension-dependent-type f)
+
+  total-extension-dependent-type : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
+  total-extension-dependent-type P =
+    Σ ((x : A) → P (i x)) (extension-dependent-type P)
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B}
+  {P : B → UU l3} {f : (x : A) → P (i x)}
+  where
+
+  map-extension-dependent-type : extension-dependent-type i P f → (y : B) → P y
+  map-extension-dependent-type = pr1
+
+  is-extension-map-extension-dependent-type :
+    (E : extension-dependent-type i P f) →
+    is-extension-dependent-type i f (map-extension-dependent-type E)
+  is-extension-map-extension-dependent-type = pr2
+```
+
+### Extensions of dependent maps with homotopies going the other way
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  where
+
+  is-extension-dependent-type' :
+    {P : B → UU l3} →
+    ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3)
+  is-extension-dependent-type' f g = (g ∘ i ~ f)
+
+  extension-dependent-type' :
+    (P : B → UU l3) →
+    ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3)
+  extension-dependent-type' P f =
+    Σ ((y : B) → P y) (is-extension-dependent-type' f)
+
+  total-extension-dependent-type' : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
+  total-extension-dependent-type' P =
+    Σ ((x : A) → P (i x)) (extension-dependent-type' P)
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B}
+  {P : B → UU l3} {f : (x : A) → P (i x)}
+  where
+
+  map-extension-dependent-type' :
+    extension-dependent-type' i P f → (y : B) → P y
+  map-extension-dependent-type' = pr1
+
+  is-extension-map-extension-dependent-type' :
+    (E : extension-dependent-type' i P f) →
+    is-extension-dependent-type' i f (map-extension-dependent-type' E)
+  is-extension-map-extension-dependent-type' = pr2
+```
+
+## Operations
+
+### Vertical composition of extensions of dependent maps
+
+```text
+    A
+    |  \
+  i |    \ f
+    |      \
+    ∨   g    ∨
+    B ------> P
+    |        ∧
+  j |      /
+    |    / h
+    ∨  /
+    C
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
+  {i : A → B} {j : B → C}
+  {f : (x : A) → P (j (i x))} {g : (x : B) → P (j x)} {h : (x : C) → P x}
+  where
+
+  is-extension-dependent-type-comp-vertical :
+    is-extension-dependent-type j g h →
+    is-extension-dependent-type i f g →
+    is-extension-dependent-type (j ∘ i) f h
+  is-extension-dependent-type-comp-vertical H G x = G x ∙ H (i x)
+```
+
+### Horizontal composition of extensions of dependent maps
+
+```text
+            A
+         /  |  \
+     f /  g |    \ h
+     /      |      \
+   ∨   i    ∨    j   ∨
+  B ------> C ------> P
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
+  {f : A → B} {g : A → C} {h : (x : A) → P (g x)}
+  {i : B → C} {j : (z : C) → P z}
+  where
+
+  is-extension-dependent-type-comp-horizontal :
+    (I : is-extension-dependent-type f g i) →
+    is-extension-dependent-type g h j →
+    is-extension-dependent-type f (λ x → tr P (I x) (h x)) (j ∘ i)
+  is-extension-dependent-type-comp-horizontal I J x =
+    ap (tr P (I x)) (J x) ∙ apd j (I x)
+```
+
+### Left whiskering of extensions of dependent maps
+
+```text
+    A
+    |  \
+  i |    \ f
+    |      \
+    ∨    g   ∨     h
+    B ------> C ------> P
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
+  {i : A → B} {f : A → C} {g : B → C}
+  where
+
+  is-extension-dependent-type-left-whisker :
+    (h : (x : C) → P x) (F : is-extension-dependent-type i f g) →
+    is-extension-dependent-type i (λ x → tr P (F x) (h (f x))) (h ∘ g)
+  is-extension-dependent-type-left-whisker h F = apd h ∘ F
+```
+
+### Right whiskering of extensions of dependent maps
+
+```text
+       h
+  X ------> A
+            |  \
+          i |    \ f
+            |      \
+            ∨    g   ∨
+            B ------> P
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : B → UU l3} {X : UU l4}
+  {i : A → B} {f : (x : A) → P (i x)} {g : (y : B) → P y}
+  where
+
+  is-extension-dependent-type-right-whisker :
+    is-extension-dependent-type i f g →
+    (h : X → A) →
+    is-extension-dependent-type (i ∘ h) (f ∘ h) g
+  is-extension-dependent-type-right-whisker F h = F ∘ h
+```
+
+## Properties
+
+### The total type of extensions is equivalent to `(y : B) → P y`
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  where
+
+  inv-compute-total-extension-dependent-type :
+    {P : B → UU l3} → total-extension-dependent-type i P ≃ ((y : B) → P y)
+  inv-compute-total-extension-dependent-type =
+    ( right-unit-law-Σ-is-contr (λ f → is-torsorial-htpy' (f ∘ i))) ∘e
+    ( equiv-left-swap-Σ)
+
+  compute-total-extension-dependent-type :
+    {P : B → UU l3} → ((y : B) → P y) ≃ total-extension-dependent-type i P
+  compute-total-extension-dependent-type =
+    inv-equiv (inv-compute-total-extension-dependent-type)
+```
+
+### The truncation level of the type of extensions is bounded by the truncation level of the codomain
+
+```agda
+module _
+  {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (i : A → B)
+  where
+
+  is-trunc-is-extension-dependent-type :
+    {P : B → UU l3} (f : (x : A) → P (i x)) →
+    ((x : A) → is-trunc (succ-𝕋 k) (P (i x))) →
+    (g : (x : B) → P x) → is-trunc k (is-extension-dependent-type i f g)
+  is-trunc-is-extension-dependent-type f is-trunc-P g =
+    is-trunc-Π k (λ x → is-trunc-P x (f x) (g (i x)))
+
+  is-trunc-extension-dependent-type :
+    {P : B → UU l3} (f : (x : A) → P (i x)) →
+    ((x : B) → is-trunc k (P x)) → is-trunc k (extension-dependent-type i P f)
+  is-trunc-extension-dependent-type f is-trunc-P =
+    is-trunc-Σ
+      ( is-trunc-Π k is-trunc-P)
+      ( is-trunc-is-extension-dependent-type f
+        ( is-trunc-succ-is-trunc k ∘ (is-trunc-P ∘ i)))
+
+  is-trunc-total-extension-dependent-type :
+    {P : B → UU l3} →
+    ((x : B) → is-trunc k (P x)) →
+    is-trunc k (total-extension-dependent-type i P)
+  is-trunc-total-extension-dependent-type {P} is-trunc-P =
+    is-trunc-equiv' k
+      ( (y : B) → P y)
+      ( compute-total-extension-dependent-type i)
+      ( is-trunc-Π k is-trunc-P)
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  where
+
+  is-contr-is-extension-dependent-type :
+    {P : B → UU l3} (f : (x : A) → P (i x)) →
+    ((x : A) → is-prop (P (i x))) →
+    (g : (x : B) → P x) → is-contr (is-extension-dependent-type i f g)
+  is-contr-is-extension-dependent-type f is-prop-P g =
+    is-contr-Π (λ x → is-prop-P x (f x) (g (i x)))
+
+  is-prop-is-extension-dependent-type :
+    {P : B → UU l3} (f : (x : A) → P (i x)) →
+    ((x : A) → is-set (P (i x))) →
+    (g : (x : B) → P x) → is-prop (is-extension-dependent-type i f g)
+  is-prop-is-extension-dependent-type f is-set-P g =
+    is-prop-Π (λ x → is-set-P x (f x) (g (i x)))
+```
+
+## Examples
+
+### Every dependent map is an extension of itself along the identity
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {P : A → UU l2} (f : (x : A) → P x)
+  where
+
+  is-extension-dependent-type-self : is-extension-dependent-type id f f
+  is-extension-dependent-type-self = refl-htpy
+
+  extension-self : extension-dependent-type id P f
+  extension-self = (f , is-extension-dependent-type-self)
+```
+
+## See also
+
+- [`orthogonal-factorization-systems.lifts-maps`](orthogonal-factorization-systems.lifts-maps.md)
+  for the dual notion.
diff --git a/src/orthogonal-factorization-systems/extensions-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-maps.lagda.md
index ccdc296bd0..fed94382cf 100644
--- a/src/orthogonal-factorization-systems/extensions-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/extensions-maps.lagda.md
@@ -7,151 +7,69 @@ module orthogonal-factorization-systems.extensions-maps where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
-open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.function-types
-open import foundation.functoriality-dependent-function-types
-open import foundation.functoriality-dependent-pair-types
-open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopies
-open import foundation.homotopy-induction
 open import foundation.identity-types
-open import foundation.monomorphisms
-open import foundation.postcomposition-functions
-open import foundation.propositions
-open import foundation.sets
-open import foundation.structure-identity-principle
-open import foundation.transport-along-identifications
-open import foundation.truncated-types
-open import foundation.truncation-levels
-open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
-open import foundation.whiskering-homotopies-composition
 
-open import foundation-core.torsorial-type-families
+open import orthogonal-factorization-systems.extensions-dependent-maps
 ```
 
 </details>
 
 ## Idea
 
-An **extension** of a map `f : (x : A) → P x` along a map `i : A → B` is a map
-`g : (y : B) → Q y` such that `Q` restricts along `i` to `P` and `g` restricts
-along `i` to `f`.
+An
+{{#concept "extension" Disambiguation="of a map along a map, types" Agda=extension}}
+of a map `f : A → X` along a map `i : A → B` is a map `g : B → X` such that `g`
+restricts along `i` to `f`.
 
 ```text
-  A
-  |  \
-  i    f
-  |      \
-  ∨       ∨
-  B - g -> P
+    A
+    |  \
+  i |    \ f
+    |      \
+    ∨    g   ∨
+    B ------> X
 ```
 
 ## Definition
 
-### Extensions of dependent functions
+### Extensions of functions
 
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
   where
 
-  is-extension :
-    {P : B → UU l3} →
-    ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3)
-  is-extension f g = f ~ (g ∘ i)
-
-  extension-dependent-type :
-    (P : B → UU l3) →
-    ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3)
-  extension-dependent-type P f = Σ ((y : B) → P y) (is-extension f)
+  is-extension : {X : UU l3} → (A → X) → (B → X) → UU (l1 ⊔ l3)
+  is-extension = is-extension-dependent-type i
 
   extension :
     {X : UU l3} → (A → X) → UU (l1 ⊔ l2 ⊔ l3)
-  extension {X} = extension-dependent-type (λ _ → X)
-
-  total-extension-dependent-type : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
-  total-extension-dependent-type P =
-    Σ ((x : A) → P (i x)) (extension-dependent-type P)
+  extension {X} = extension-dependent-type i (λ _ → X)
 
   total-extension : (X : UU l3) → UU (l1 ⊔ l2 ⊔ l3)
-  total-extension X = total-extension-dependent-type (λ _ → X)
+  total-extension X = total-extension-dependent-type i (λ _ → X)
 
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B}
-  {P : B → UU l3} {f : (x : A) → P (i x)}
+  {X : UU l3} {f : A → X}
   where
 
-  map-extension : extension-dependent-type i P f → (y : B) → P y
+  map-extension : extension i f → B → X
   map-extension = pr1
 
   is-extension-map-extension :
-    (E : extension-dependent-type i P f) → is-extension i f (map-extension E)
+    (E : extension i f) → is-extension i f (map-extension E)
   is-extension-map-extension = pr2
 ```
 
 ## Operations
 
-### Vertical composition of extensions of maps
-
-```text
-  A
-  |  \
-  i    f
-  |      \
-  ∨       ∨
-  B - g -> P
-  |       ∧
-  j      /
-  |    h
-  ∨  /
-  C
-```
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
-  {i : A → B} {j : B → C}
-  {f : (x : A) → P (j (i x))} {g : (x : B) → P (j x)} {h : (x : C) → P x}
-  where
-
-  is-extension-comp-vertical :
-    is-extension j g h → is-extension i f g → is-extension (j ∘ i) f h
-  is-extension-comp-vertical H G x = G x ∙ H (i x)
-```
-
-### Horizontal composition of extensions of maps
-
-```text
-           A
-        /  |  \
-      f    g    h
-    /      |      \
-   ∨       ∨       ∨
-  B - i -> C - j -> P
-```
-
-#### Horizontal composition of extensions of dependent functions
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
-  {f : A → B} {g : A → C} {h : (x : A) → P (g x)}
-  {i : B → C} {j : (z : C) → P z}
-  where
-
-  is-extension-dependent-type-comp-horizontal :
-    (I : is-extension f g i) →
-    is-extension g h j → is-extension f (λ x → tr P (I x) (h x)) (j ∘ i)
-  is-extension-dependent-type-comp-horizontal I J x =
-    ap (tr P (I x)) (J x) ∙ apd j (I x)
-```
-
 #### Horizontal composition of extensions of ordinary maps
 
 ```agda
@@ -162,223 +80,30 @@ module _
   where
 
   is-extension-comp-horizontal :
-    (I : is-extension f g i) → is-extension g h j → is-extension f h (j ∘ i)
-  is-extension-comp-horizontal I J x = (J x) ∙ ap j (I x)
-```
-
-### Left whiskering of extensions of maps
-
-```text
-  A
-  |  \
-  i    f
-  |      \
-  ∨       ∨
-  B - g -> C - h -> P
-```
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
-  {i : A → B} {f : A → C} {g : B → C}
-  where
-
-  is-extension-left-whisker :
-    (h : (x : C) → P x) (F : is-extension i f g) →
-    (is-extension i (λ x → tr P (F x) (h (f x))) (h ∘ g))
-  is-extension-left-whisker h F = apd h ∘ F
-```
-
-### Right whiskering of extensions of maps
-
-```text
-  X - h -> A
-           |  \
-           i    f
-           |      \
-           ∨       ∨
-           B - g -> P
-```
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : B → UU l3} {X : UU l4}
-  {i : A → B} {f : (x : A) → P (i x)} {g : (y : B) → P y}
-  where
-
-  is-extension-right-whisker :
-    (F : is-extension i f g) (h : X → A) → is-extension (i ∘ h) (f ∘ h) g
-  is-extension-right-whisker F h = F ∘ h
-```
-
-### Postcomposition of extensions
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
-  where
-
-  postcomp-extension :
-    (f : A → B) (i : A → X) (g : X → Y) →
-    extension f i → extension f (g ∘ i)
-  postcomp-extension f i g =
-    map-Σ (is-extension f (g ∘ i)) (postcomp B g) (λ j H → g ·l H)
+    is-extension f g i → is-extension g h j → is-extension f h (j ∘ i)
+  is-extension-comp-horizontal I J x = J x ∙ ap j (I x)
 ```
 
 ## Properties
 
-### Characterizing identifications of extensions of maps
-
-```agda
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
-  {P : B → UU l3}
-  (f : (x : A) → P (i x))
-  where
-
-  coherence-htpy-extension :
-    (e e' : extension-dependent-type i P f) →
-    map-extension e ~ map-extension e' → UU (l1 ⊔ l3)
-  coherence-htpy-extension e e' K =
-    (is-extension-map-extension e ∙h (K ·r i)) ~ is-extension-map-extension e'
-
-  htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3)
-  htpy-extension e e' =
-    Σ ( map-extension e ~ map-extension e')
-      ( coherence-htpy-extension e e')
-
-  refl-htpy-extension :
-    (e : extension-dependent-type i P f) → htpy-extension e e
-  pr1 (refl-htpy-extension e) = refl-htpy
-  pr2 (refl-htpy-extension e) = right-unit-htpy
-
-  htpy-eq-extension :
-    (e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension e e'
-  htpy-eq-extension e .e refl = refl-htpy-extension e
-
-  is-torsorial-htpy-extension :
-    (e : extension-dependent-type i P f) → is-torsorial (htpy-extension e)
-  is-torsorial-htpy-extension e =
-    is-torsorial-Eq-structure
-      ( is-torsorial-htpy (map-extension e))
-      ( map-extension e , refl-htpy)
-      ( is-torsorial-htpy (is-extension-map-extension e ∙h refl-htpy))
-
-  is-equiv-htpy-eq-extension :
-    (e e' : extension-dependent-type i P f) → is-equiv (htpy-eq-extension e e')
-  is-equiv-htpy-eq-extension e =
-    fundamental-theorem-id
-      ( is-torsorial-htpy-extension e)
-      ( htpy-eq-extension e)
-
-  extensionality-extension :
-    (e e' : extension-dependent-type i P f) → (e ＝ e') ≃ (htpy-extension e e')
-  pr1 (extensionality-extension e e') = htpy-eq-extension e e'
-  pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e'
-
-  eq-htpy-extension :
-    (e e' : extension-dependent-type i P f)
-    (H : map-extension e ~ map-extension e') →
-    coherence-htpy-extension e e' H → e ＝ e'
-  eq-htpy-extension e e' H K =
-    map-inv-equiv (extensionality-extension e e') (H , K)
-```
-
-### The total type of extensions is equivalent to `(y : B) → P y`
+### The total type of extensions is equivalent to `B → X`
 
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
   where
 
-  inv-compute-total-extension-dependent-type :
-    {P : B → UU l3} → total-extension-dependent-type i P ≃ ((y : B) → P y)
-  inv-compute-total-extension-dependent-type =
-    ( right-unit-law-Σ-is-contr (λ f → is-torsorial-htpy' (f ∘ i))) ∘e
-    ( equiv-left-swap-Σ)
-
-  compute-total-extension-dependent-type :
-    {P : B → UU l3} → ((y : B) → P y) ≃ total-extension-dependent-type i P
-  compute-total-extension-dependent-type =
-    inv-equiv (inv-compute-total-extension-dependent-type)
-
   inv-compute-total-extension :
     {X : UU l3} → total-extension i X ≃ (B → X)
-  inv-compute-total-extension = inv-compute-total-extension-dependent-type
+  inv-compute-total-extension = inv-compute-total-extension-dependent-type i
 
   compute-total-extension :
     {X : UU l3} → (B → X) ≃ total-extension i X
-  compute-total-extension = compute-total-extension-dependent-type
-```
-
-### The truncation level of the type of extensions is bounded by the truncation level of the codomains
-
-```agda
-module _
-  {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (i : A → B)
-  where
-
-  is-trunc-is-extension-dependent-type :
-    {P : B → UU l3} (f : (x : A) → P (i x)) →
-    ((x : A) → is-trunc (succ-𝕋 k) (P (i x))) →
-    (g : (x : B) → P x) → is-trunc k (is-extension i f g)
-  is-trunc-is-extension-dependent-type f is-trunc-P g =
-    is-trunc-Π k λ x → is-trunc-P x (f x) (g (i x))
-
-  is-trunc-extension-dependent-type :
-    {P : B → UU l3} (f : (x : A) → P (i x)) →
-    ((x : B) → is-trunc k (P x)) → is-trunc k (extension-dependent-type i P f)
-  is-trunc-extension-dependent-type f is-trunc-P =
-    is-trunc-Σ
-      ( is-trunc-Π k is-trunc-P)
-      ( is-trunc-is-extension-dependent-type f
-        ( is-trunc-succ-is-trunc k ∘ (is-trunc-P ∘ i)))
-
-  is-trunc-total-extension-dependent-type :
-    {P : B → UU l3} →
-    ((x : B) → is-trunc k (P x)) →
-    is-trunc k (total-extension-dependent-type i P)
-  is-trunc-total-extension-dependent-type {P} is-trunc-P =
-    is-trunc-equiv' k
-      ( (y : B) → P y)
-      ( compute-total-extension-dependent-type i)
-      ( is-trunc-Π k is-trunc-P)
-
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
-  where
-
-  is-contr-is-extension :
-    {P : B → UU l3} (f : (x : A) → P (i x)) →
-    ((x : A) → is-prop (P (i x))) →
-    (g : (x : B) → P x) → is-contr (is-extension i f g)
-  is-contr-is-extension f is-prop-P g =
-    is-contr-Π λ x → is-prop-P x (f x) (g (i x))
-
-  is-prop-is-extension :
-    {P : B → UU l3} (f : (x : A) → P (i x)) →
-    ((x : A) → is-set (P (i x))) →
-    (g : (x : B) → P x) → is-prop (is-extension i f g)
-  is-prop-is-extension f is-set-P g =
-    is-prop-Π (λ x → is-set-P x (f x) (g (i x)))
+  compute-total-extension = compute-total-extension-dependent-type i
 ```
 
 ## Examples
 
-### Every map is an extension of itself along the identity
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} {P : A → UU l2} (f : (x : A) → P x)
-  where
-
-  is-extension-self : is-extension id f f
-  is-extension-self = refl-htpy
-
-  extension-self : extension-dependent-type id P f
-  extension-self = f , is-extension-self
-```
-
 ### The identity is an extension of every map along themselves
 
 ```agda
@@ -390,27 +115,7 @@ module _
   is-extension-along-self = refl-htpy
 
   extension-along-self : extension f f
-  extension-along-self = id , is-extension-along-self
-```
-
-### Postcomposition of extensions by an embedding is an embedding
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
-  where
-
-  is-emb-postcomp-extension :
-    (f : A → B) (i : A → X) (g : X → Y) → is-emb g →
-    is-emb (postcomp-extension f i g)
-  is-emb-postcomp-extension f i g H =
-    is-emb-map-Σ
-      ( is-extension f (g ∘ i))
-      ( is-mono-is-emb g H B)
-      ( λ j →
-        is-emb-is-equiv
-          ( is-equiv-map-Π-is-fiberwise-equiv
-            ( λ x → H (i x) (j (f x)))))
+  extension-along-self = (id , is-extension-along-self)
 ```
 
 ## See also
diff --git a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md
new file mode 100644
index 0000000000..5383538aef
--- /dev/null
+++ b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md
@@ -0,0 +1,137 @@
+# Postcomposition of extensions of maps
+
+```agda
+module orthogonal-factorization-systems.postcomposition-extensions-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-function-types
+open import foundation.monomorphisms
+open import foundation.postcomposition-functions
+open import foundation.truncated-maps
+open import foundation.truncation-levels
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import orthogonal-factorization-systems.extensions-maps
+```
+
+</details>
+
+## Idea
+
+Given a map `i : A → B` and a map `f : A → X`, then we may
+{{#concept "postcompose" Disambiguation="extension of map by map" Agda=postcomp-extension}}
+any [extension](orthogonal-factorization-systems.extensions-maps.md)
+`α : extension i f` by a map `g : X → Y` to obtain an extension of `g ∘ f` along
+`i`, `gα : extension i (g ∘ f)`.
+
+## Definition
+
+### Postcomposition of extensions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  where
+
+  postcomp-extension :
+    (i : A → B) (f : A → X) (g : X → Y) →
+    extension i f → extension i (g ∘ f)
+  postcomp-extension i f g =
+    map-Σ (is-extension i (g ∘ f)) (postcomp B g) (λ j H → g ·l H)
+```
+
+## Properties
+
+### Postcomposition of extensions by an equivalence is an equivalence
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  where
+
+  is-equiv-postcomp-extension :
+    (f : A → B) (i : A → X) (g : X → Y) → is-equiv g →
+    is-equiv (postcomp-extension f i g)
+  is-equiv-postcomp-extension f i g G =
+    is-equiv-map-Σ
+      ( is-extension f (g ∘ i))
+      ( is-equiv-postcomp-is-equiv g G B)
+      ( λ j →
+        is-equiv-map-Π-is-fiberwise-equiv
+          ( λ x → is-emb-is-equiv G (i x) (j (f x))))
+
+  equiv-postcomp-extension :
+    (f : A → B) (i : A → X) (g : X ≃ Y) →
+    extension f i ≃ extension f (map-equiv g ∘ i)
+  equiv-postcomp-extension f i (g , G) =
+    ( postcomp-extension f i g , is-equiv-postcomp-extension f i g G)
+```
+
+### Postcomposition of extensions by an embedding is an embedding
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  where
+
+  is-emb-postcomp-extension :
+    (f : A → B) (i : A → X) (g : X → Y) → is-emb g →
+    is-emb (postcomp-extension f i g)
+  is-emb-postcomp-extension f i g H =
+    is-emb-map-Σ
+      ( is-extension f (g ∘ i))
+      ( is-mono-is-emb g H B)
+      ( λ j →
+        is-emb-is-equiv
+          ( is-equiv-map-Π-is-fiberwise-equiv
+            (λ x → H (i x) (j (f x)))))
+
+  emb-postcomp-extension :
+    (f : A → B) (i : A → X) (g : X ↪ Y) →
+    extension f i ↪ extension f (map-emb g ∘ i)
+  emb-postcomp-extension f i (g , G) =
+    postcomp-extension f i g , is-emb-postcomp-extension f i g G
+```
+
+### Postcomposition of extensions by a `k`-truncated map is `k`-truncated
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  where
+
+  is-trunc-map-postcomp-extension :
+    (f : A → B) (i : A → X) (g : X → Y) → is-trunc-map k g →
+    is-trunc-map k (postcomp-extension f i g)
+  is-trunc-map-postcomp-extension f i g G =
+    is-trunc-map-map-Σ k
+      ( is-extension f (g ∘ i))
+      ( is-trunc-map-postcomp-is-trunc-map k g G B)
+      ( λ j →
+        is-trunc-map-map-Π k
+          ( λ a → ap g)
+          ( λ a → is-trunc-map-ap-is-trunc-map k g G (i a) (j (f a))))
+
+  trunc-map-postcomp-extension :
+    (f : A → B) (i : A → X) (g : trunc-map k X Y) →
+    trunc-map k (extension f i) (extension f (map-trunc-map g ∘ i))
+  trunc-map-postcomp-extension f i (g , G) =
+    ( postcomp-extension f i g , is-trunc-map-postcomp-extension f i g G)
+```
+
+## See also
+
+- In [`foundation.surjective-maps`](foundation.surjective-maps.md) it is shown
+  that postcomposition of extensions along surjective maps by an embedding is an
+  equivalence.
diff --git a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
index 1ebbc9e3de..6d9f82230b 100644
--- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
@@ -41,6 +41,7 @@ open import foundation.universal-property-empty-type
 open import foundation.universal-property-equivalences
 open import foundation.universe-levels
 
+open import orthogonal-factorization-systems.extensions-dependent-maps
 open import orthogonal-factorization-systems.extensions-maps
 ```
 
diff --git a/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md
index a3c2143af4..74825118eb 100644
--- a/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md
@@ -28,6 +28,7 @@ open import foundation.unit-type
 open import foundation.univalence
 open import foundation.universe-levels
 
+open import orthogonal-factorization-systems.extensions-dependent-maps
 open import orthogonal-factorization-systems.extensions-maps
 open import orthogonal-factorization-systems.types-local-at-maps
 ```