diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md
index 8b303ff4dd..d86bdea803 100644
--- a/src/foundation-core/contractible-types.lagda.md
+++ b/src/foundation-core/contractible-types.lagda.md
@@ -92,8 +92,8 @@ module _
       is-contr-retract-of B (f , retraction-is-equiv is-equiv-f)
 
   abstract
-    is-contr-equiv : (e : A ≃ B) → is-contr B → is-contr A
-    is-contr-equiv (pair e is-equiv-e) is-contr-B =
+    is-contr-equiv : A ≃ B → is-contr B → is-contr A
+    is-contr-equiv (e , is-equiv-e) is-contr-B =
       is-contr-is-equiv e is-equiv-e is-contr-B
 
 module _
@@ -133,24 +133,6 @@ module _
     is-equiv-is-contr _ is-contr-A is-contr-B
 ```
 
-### Contractibility of the base of a contractible dependent sum
-
-Given a type `A` and a type family over it `B`, then if the dependent sum
-`Σ A B` is contractible, it follows that if there is a section `(x : A) → B x`
-then `A` is contractible.
-
-```agda
-module _
-  {l1 l2 : Level} (A : UU l1) (B : A → UU l2)
-  where
-
-  abstract
-    is-contr-base-is-contr-Σ' :
-      ((x : A) → B x) → is-contr (Σ A B) → is-contr A
-    is-contr-base-is-contr-Σ' s =
-      is-contr-retract-of (Σ A B) ((λ a → a , s a) , pr1 , refl-htpy)
-```
-
 ### Contractibility of cartesian product types
 
 Given two types `A` and `B`, the following are equivalent:
@@ -248,6 +230,24 @@ normalize the extracted information (in this case the first projection of the
 proof of contractibility), but it will normalize the entire proof of
 contractibility first, and then apply the projection.
 
+### Contractibility of the base of a contractible dependent sum
+
+Given a type `A` and a type family over it `B`, then if the dependent sum
+`Σ A B` is contractible and there is a section `(x : A) → B x`, then `A` is
+contractible.
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) (B : A → UU l2)
+  where
+
+  abstract
+    is-contr-base-is-contr-Σ' :
+      ((x : A) → B x) → is-contr (Σ A B) → is-contr A
+    is-contr-base-is-contr-Σ' s =
+      is-contr-retract-of (Σ A B) ((λ a → a , s a) , pr1 , refl-htpy)
+```
+
 ### Contractible types are propositions
 
 ```agda
diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md
index 066a033e3c..1c09641373 100644
--- a/src/foundation-core/fibers-of-maps.lagda.md
+++ b/src/foundation-core/fibers-of-maps.lagda.md
@@ -229,9 +229,7 @@ module _
   map-fiber-pr1 ((x , y) , p) = tr B p y
 
   map-inv-fiber-pr1 : B a → fiber (pr1 {B = B}) a
-  pr1 (pr1 (map-inv-fiber-pr1 b)) = a
-  pr2 (pr1 (map-inv-fiber-pr1 b)) = b
-  pr2 (map-inv-fiber-pr1 b) = refl
+  map-inv-fiber-pr1 b = (a , b) , refl
 
   is-section-map-inv-fiber-pr1 :
     is-section map-fiber-pr1 map-inv-fiber-pr1
diff --git a/src/foundation-core/function-types.lagda.md b/src/foundation-core/function-types.lagda.md
index 0fad64ab6a..e9ac42fc1f 100644
--- a/src/foundation-core/function-types.lagda.md
+++ b/src/foundation-core/function-types.lagda.md
@@ -24,6 +24,9 @@ Functions are primitive in Agda. Here we construct some basic functions
 id : {l : Level} {A : UU l} → A → A
 id a = a
 
+id' : {l : Level} (A : UU l) → A → A
+id' A = id
+
 idω : {A : UUω} → A → A
 idω a = a
 ```
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 78a7642b23..46bcc44c71 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -177,6 +177,8 @@ open import foundation.exclusive-sum public
 open import foundation.existential-quantification public
 open import foundation.exponents-set-quotients public
 open import foundation.extensions-types public
+open import foundation.extensions-types-global-subuniverses public
+open import foundation.extensions-types-subuniverses public
 open import foundation.faithful-maps public
 open import foundation.families-of-equivalences public
 open import foundation.families-of-maps public
diff --git a/src/foundation/commuting-squares-of-maps.lagda.md b/src/foundation/commuting-squares-of-maps.lagda.md
index 715937f221..347bb16120 100644
--- a/src/foundation/commuting-squares-of-maps.lagda.md
+++ b/src/foundation/commuting-squares-of-maps.lagda.md
@@ -720,7 +720,7 @@ module _
         ap-binary
           ( λ L q → eq-htpy L ∙ q)
           ( eq-htpy (preserves-comp-left-whisker-comp h bottom-right H))
-          ( inv (compute-eq-htpy-ap-precomp top-left (h ·l K)))
+          ( inv (coherence-eq-htpy-ap-precomp top-left (h ·l K)))
 
   distributive-precomp-pasting-vertical-coherence-square-maps :
     ( top : A → X) (left-top : A → B) (right-top : X → Y) (middle : B → Y) →
@@ -805,7 +805,7 @@ module _
         by
         ap-binary
           ( λ p L → p ∙ eq-htpy L)
-          ( inv (compute-eq-htpy-ap-precomp left-top (h ·l K)))
+          ( inv (coherence-eq-htpy-ap-precomp left-top (h ·l K)))
           ( eq-htpy (preserves-comp-left-whisker-comp h right-bottom H))
 ```
 
@@ -856,7 +856,7 @@ module _
     ( ( precomp f W) ·l
       ( precomp-coherence-square-maps top left right bottom H W))
   distributive-precomp-right-whisker-comp-coherence-square-maps f g =
-    inv (compute-eq-htpy-ap-precomp f (g ·l H))
+    inv (coherence-eq-htpy-ap-precomp f (g ·l H))
 ```
 
 Similarly, we can calculate transpositions of left-whiskered squares with the
diff --git a/src/foundation/composition-algebra.lagda.md b/src/foundation/composition-algebra.lagda.md
index e98e9e0260..d78d99cfee 100644
--- a/src/foundation/composition-algebra.lagda.md
+++ b/src/foundation/composition-algebra.lagda.md
@@ -78,7 +78,7 @@ module _
     (h : C → A) (H : f ~ g) (S : UU l4) →
     precomp h S ·l htpy-precomp H S ~ htpy-precomp (H ·r h) S
   inv-distributive-htpy-precomp-right-whisker h H S i =
-    compute-eq-htpy-ap-precomp h (i ·l H)
+    coherence-eq-htpy-ap-precomp h (i ·l H)
 
   distributive-htpy-precomp-right-whisker :
     (h : C → A) (H : f ~ g) (S : UU l4) →
diff --git a/src/foundation/continuations.lagda.md b/src/foundation/continuations.lagda.md
index 853df7969c..3c7d65926e 100644
--- a/src/foundation/continuations.lagda.md
+++ b/src/foundation/continuations.lagda.md
@@ -34,7 +34,7 @@ open import foundation-core.retractions
 open import foundation-core.sections
 open import foundation-core.transport-along-identifications
 
-open import orthogonal-factorization-systems.extensions-of-maps
+open import orthogonal-factorization-systems.extensions-maps
 open import orthogonal-factorization-systems.modal-operators
 open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
@@ -82,8 +82,8 @@ unit-continuation = ev
 ### Maps into `continuation R A` extend along the unit
 
 Every `f` as in the following diagram
-[extends](orthogonal-factorization-systems.extensions-of-maps.md) along the unit
-of its domain
+[extends](orthogonal-factorization-systems.extensions-maps.md) along the unit of
+its domain
 
 ```text
                f
diff --git a/src/foundation/equality-fibers-of-maps.lagda.md b/src/foundation/equality-fibers-of-maps.lagda.md
index e9f8f003d7..e5fa8e6684 100644
--- a/src/foundation/equality-fibers-of-maps.lagda.md
+++ b/src/foundation/equality-fibers-of-maps.lagda.md
@@ -121,7 +121,7 @@ module _
 
   abstract
     is-equiv-eq-fiber-fiber-ap :
-      (q : (f x) ＝ f y) → is-equiv (eq-fiber-fiber-ap q)
+      (q : f x ＝ f y) → is-equiv (eq-fiber-fiber-ap q)
     is-equiv-eq-fiber-fiber-ap q =
       is-equiv-comp
         ( tr (fiber (ap f)) right-unit)
diff --git a/src/foundation/extensions-types-global-subuniverses.lagda.md b/src/foundation/extensions-types-global-subuniverses.lagda.md
new file mode 100644
index 0000000000..a75184e2aa
--- /dev/null
+++ b/src/foundation/extensions-types-global-subuniverses.lagda.md
@@ -0,0 +1,231 @@
+# Extensions of types in a global subuniverse
+
+```agda
+module foundation.extensions-types-global-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-triangles-of-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.extensions-types
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.global-subuniverses
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.propositional-maps
+open import foundation.propositions
+open import foundation.torsorial-type-families
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.univalence
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a type `X`. An
+{{#concept "extension" Disambiguation="type in global subuniverse" Agda=extension-type-global-subuniverse}}
+of `X` in a [global subuniverse](foundation.global-subuniverses.md) `𝒫` is an
+object in the [coslice](foundation.coslice.md) under `X` in `𝒫`, i.e., it
+consists of a type `Y` in `𝒫` and a map `f : X → Y`.
+
+In the above definition of extensions of types in a global subuniverse our aim
+is to capture the most general concept of what it means to be an extension of a
+type in a subuniverse.
+
+Our notion of extensions of types are not to be confused with extension types of
+cubical type theory or
+[extension types of simplicial type theory](https://arxiv.org/abs/1705.07442).
+
+## Definitions
+
+### The predicate on an extension of types of being in a global subuniverse
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level}
+  (𝒫 : global-subuniverse α) {X : UU l1}
+  (E : extension-type l2 X)
+  where
+
+  is-in-global-subuniverse-extension-type-Prop : Prop (α l2)
+  is-in-global-subuniverse-extension-type-Prop =
+    is-in-global-subuniverse-Prop 𝒫 (type-extension-type E)
+
+  is-in-global-subuniverse-extension-type : UU (α l2)
+  is-in-global-subuniverse-extension-type =
+    is-in-global-subuniverse 𝒫 (type-extension-type E)
+
+  is-prop-is-in-global-subuniverse-extension-type :
+    is-prop is-in-global-subuniverse-extension-type
+  is-prop-is-in-global-subuniverse-extension-type =
+    is-prop-is-in-global-subuniverse 𝒫 (type-extension-type E)
+```
+
+### Extensions of types in a subuniverse
+
+```agda
+extension-type-global-subuniverse :
+  {α : Level → Level} {l1 : Level}
+  (𝒫 : global-subuniverse α) (l2 : Level) (X : UU l1) →
+  UU (α l2 ⊔ l1 ⊔ lsuc l2)
+extension-type-global-subuniverse 𝒫 l2 X =
+  Σ (type-global-subuniverse 𝒫 l2) (λ Y → X → inclusion-global-subuniverse 𝒫 Y)
+
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α) {X : UU l1}
+  (Y : extension-type-global-subuniverse 𝒫 l2 X)
+  where
+
+  type-global-subuniverse-extension-type-global-subuniverse :
+    type-global-subuniverse 𝒫 l2
+  type-global-subuniverse-extension-type-global-subuniverse = pr1 Y
+
+  type-extension-type-global-subuniverse : UU l2
+  type-extension-type-global-subuniverse =
+    inclusion-global-subuniverse 𝒫
+      type-global-subuniverse-extension-type-global-subuniverse
+
+  is-in-global-subuniverse-type-extension-type-global-subuniverse :
+    is-in-global-subuniverse 𝒫 type-extension-type-global-subuniverse
+  is-in-global-subuniverse-type-extension-type-global-subuniverse =
+    is-in-global-subuniverse-inclusion-global-subuniverse 𝒫
+      type-global-subuniverse-extension-type-global-subuniverse
+
+  inclusion-extension-type-global-subuniverse :
+    X → type-extension-type-global-subuniverse
+  inclusion-extension-type-global-subuniverse = pr2 Y
+
+  extension-type-extension-type-global-subuniverse : extension-type l2 X
+  extension-type-extension-type-global-subuniverse =
+    type-extension-type-global-subuniverse ,
+    inclusion-extension-type-global-subuniverse
+```
+
+## Properties
+
+### Extensions of types in a subuniverse are extensions of types by types in the subuniverse
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α) {X : UU l1}
+  where
+
+  compute-extension-type-global-subuniverse :
+    extension-type-global-subuniverse 𝒫 l2 X ≃
+    Σ (extension-type l2 X) (is-in-global-subuniverse-extension-type 𝒫)
+  compute-extension-type-global-subuniverse = equiv-right-swap-Σ
+```
+
+### The inclusion of extensions of types in a subuniverse into extensions of types is an embedding
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α) {X : UU l1}
+  where
+
+  compute-fiber-extension-type-extension-type-global-subuniverse :
+    (Y : extension-type l2 X) →
+    fiber (extension-type-extension-type-global-subuniverse 𝒫) Y ≃
+    is-in-global-subuniverse 𝒫 (type-extension-type Y)
+  compute-fiber-extension-type-extension-type-global-subuniverse Y =
+    equivalence-reasoning
+    Σ ( Σ (Σ (UU l2) (λ Z → is-in-global-subuniverse 𝒫 Z)) (λ Z → X → pr1 Z))
+      ( λ E → extension-type-extension-type-global-subuniverse 𝒫 E ＝ Y)
+    ≃ Σ ( Σ (extension-type l2 X) (is-in-global-subuniverse-extension-type 𝒫))
+        ( λ E → pr1 E ＝ Y)
+    by
+      equiv-Σ-equiv-base
+        ( λ E → pr1 E ＝ Y)
+        ( compute-extension-type-global-subuniverse 𝒫)
+    ≃ Σ ( Σ (extension-type l2 X) (λ E → E ＝ Y))
+        ( is-in-global-subuniverse-extension-type 𝒫 ∘ pr1)
+      by equiv-right-swap-Σ
+    ≃ is-in-global-subuniverse-extension-type 𝒫 Y
+    by left-unit-law-Σ-is-contr (is-torsorial-Id' Y) (Y , refl)
+
+  is-prop-map-extension-type-extension-type-global-subuniverse :
+    is-prop-map (extension-type-extension-type-global-subuniverse 𝒫)
+  is-prop-map-extension-type-extension-type-global-subuniverse Y =
+    is-prop-equiv
+      ( compute-fiber-extension-type-extension-type-global-subuniverse Y)
+      ( is-prop-is-in-global-subuniverse 𝒫 (type-extension-type Y))
+
+  is-emb-extension-type-extension-type-global-subuniverse :
+    is-emb (extension-type-extension-type-global-subuniverse 𝒫)
+  is-emb-extension-type-extension-type-global-subuniverse =
+    is-emb-is-prop-map
+      is-prop-map-extension-type-extension-type-global-subuniverse
+```
+
+### Characterization of identifications of extensions of types in a subuniverse
+
+```agda
+equiv-extension-type-global-subuniverse :
+  {α : Level → Level} {l1 l2 l3 : Level}
+  (𝒫 : global-subuniverse α) {X : UU l1} →
+  extension-type-global-subuniverse 𝒫 l2 X →
+  extension-type-global-subuniverse 𝒫 l3 X → UU (l1 ⊔ l2 ⊔ l3)
+equiv-extension-type-global-subuniverse 𝒫 U V =
+  equiv-extension-type
+    ( extension-type-extension-type-global-subuniverse 𝒫 U)
+    ( extension-type-extension-type-global-subuniverse 𝒫 V)
+
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α) {X : UU l1}
+  where
+
+  id-equiv-extension-type-global-subuniverse :
+    (U : extension-type-global-subuniverse 𝒫 l2 X) →
+    equiv-extension-type-global-subuniverse 𝒫 U U
+  id-equiv-extension-type-global-subuniverse U =
+    id-equiv-extension-type
+      ( extension-type-extension-type-global-subuniverse 𝒫 U)
+
+  equiv-eq-extension-type-global-subuniverse :
+    (U V : extension-type-global-subuniverse 𝒫 l2 X) →
+    U ＝ V → equiv-extension-type-global-subuniverse 𝒫 U V
+  equiv-eq-extension-type-global-subuniverse U V p =
+    equiv-eq-extension-type
+      ( extension-type-extension-type-global-subuniverse 𝒫 U)
+      ( extension-type-extension-type-global-subuniverse 𝒫 V)
+      ( ap (extension-type-extension-type-global-subuniverse 𝒫) p)
+
+  is-equiv-equiv-eq-extension-type-global-subuniverse :
+    (U V : extension-type-global-subuniverse 𝒫 l2 X) →
+    is-equiv (equiv-eq-extension-type-global-subuniverse U V)
+  is-equiv-equiv-eq-extension-type-global-subuniverse U V =
+    is-equiv-comp
+      ( equiv-eq-extension-type
+        ( extension-type-extension-type-global-subuniverse 𝒫 U)
+        ( extension-type-extension-type-global-subuniverse 𝒫 V))
+      ( ap (extension-type-extension-type-global-subuniverse 𝒫))
+      ( is-emb-extension-type-extension-type-global-subuniverse 𝒫 U V)
+      ( is-equiv-equiv-eq-extension-type
+        ( extension-type-extension-type-global-subuniverse 𝒫 U)
+        ( extension-type-extension-type-global-subuniverse 𝒫 V))
+
+  extensionality-extension-type-global-subuniverse :
+    (U V : extension-type-global-subuniverse 𝒫 l2 X) →
+    (U ＝ V) ≃ equiv-extension-type-global-subuniverse 𝒫 U V
+  extensionality-extension-type-global-subuniverse U V =
+    equiv-eq-extension-type-global-subuniverse U V ,
+    is-equiv-equiv-eq-extension-type-global-subuniverse U V
+
+  eq-equiv-extension-type-global-subuniverse :
+    (U V : extension-type-global-subuniverse 𝒫 l2 X) →
+    equiv-extension-type-global-subuniverse 𝒫 U V → U ＝ V
+  eq-equiv-extension-type-global-subuniverse U V =
+    map-inv-equiv (extensionality-extension-type-global-subuniverse U V)
+```
diff --git a/src/foundation/extensions-types-subuniverses.lagda.md b/src/foundation/extensions-types-subuniverses.lagda.md
new file mode 100644
index 0000000000..b76a1afee1
--- /dev/null
+++ b/src/foundation/extensions-types-subuniverses.lagda.md
@@ -0,0 +1,221 @@
+# Extensions of types in a subuniverse
+
+```agda
+module foundation.extensions-types-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-triangles-of-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.extensions-types
+open import foundation.fibers-of-maps
+open import foundation.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.propositional-maps
+open import foundation.propositions
+open import foundation.structure-identity-principle
+open import foundation.subtype-identity-principle
+open import foundation.subuniverses
+open import foundation.torsorial-type-families
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.univalence
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a type `X`. An
+{{#concept "extension" Disambiguation="type in subuniverse" Agda=extension-type-subuniverse}}
+of `X` in a [subuniverse](foundation.subuniverses.md) `𝒫` is an object in the
+[coslice](foundation.coslice.md) under `X` in `𝒫`, i.e., it consists of a type
+`Y` in `𝒫` and a map `f : X → Y`.
+
+In the above definition of extensions of types in a subuniverse our aim is to
+capture the most general concept of what it means to be an extension of a type
+in a subuniverse.
+
+Our notion of extensions of types are not to be confused with extension types of
+cubical type theory or
+[extension types of simplicial type theory](https://arxiv.org/abs/1705.07442).
+
+## Definitions
+
+### The predicate on an extension of types of being in a subuniverse
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒫 : subuniverse l1 l2) {X : UU l3}
+  (E : extension-type l1 X)
+  where
+
+  is-in-subuniverse-extension-type-Prop : Prop l2
+  is-in-subuniverse-extension-type-Prop = 𝒫 (type-extension-type E)
+
+  is-in-subuniverse-extension-type : UU l2
+  is-in-subuniverse-extension-type =
+    is-in-subuniverse 𝒫 (type-extension-type E)
+
+  is-prop-is-in-subuniverse-extension-type :
+    is-prop is-in-subuniverse-extension-type
+  is-prop-is-in-subuniverse-extension-type =
+    is-prop-is-in-subuniverse 𝒫 (type-extension-type E)
+```
+
+### Extensions of types in a subuniverse
+
+```agda
+extension-type-subuniverse :
+  {l1 l2 l3 : Level} (𝒫 : subuniverse l1 l2) (X : UU l3) →
+  UU (lsuc l1 ⊔ l2 ⊔ l3)
+extension-type-subuniverse 𝒫 X =
+  Σ (type-subuniverse 𝒫) (λ Y → X → inclusion-subuniverse 𝒫 Y)
+
+module _
+  {l1 l2 l3 : Level} (𝒫 : subuniverse l1 l2) {X : UU l3}
+  (Y : extension-type-subuniverse 𝒫 X)
+  where
+
+  type-subuniverse-extension-type-subuniverse : type-subuniverse 𝒫
+  type-subuniverse-extension-type-subuniverse = pr1 Y
+
+  type-extension-type-subuniverse : UU l1
+  type-extension-type-subuniverse =
+    inclusion-subuniverse 𝒫 type-subuniverse-extension-type-subuniverse
+
+  is-in-subuniverse-type-extension-type-subuniverse :
+    is-in-subuniverse 𝒫 type-extension-type-subuniverse
+  is-in-subuniverse-type-extension-type-subuniverse =
+    is-in-subuniverse-inclusion-subuniverse 𝒫
+      type-subuniverse-extension-type-subuniverse
+
+  inclusion-extension-type-subuniverse : X → type-extension-type-subuniverse
+  inclusion-extension-type-subuniverse = pr2 Y
+
+  extension-type-extension-type-subuniverse : extension-type l1 X
+  extension-type-extension-type-subuniverse =
+    type-extension-type-subuniverse , inclusion-extension-type-subuniverse
+```
+
+## Properties
+
+### Extensions of types in a subuniverse are extensions of types by types in the subuniverse
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒫 : subuniverse l1 l2) {X : UU l3}
+  where
+
+  compute-extension-type-subuniverse :
+    extension-type-subuniverse 𝒫 X ≃
+    Σ (extension-type l1 X) (is-in-subuniverse-extension-type 𝒫)
+  compute-extension-type-subuniverse = equiv-right-swap-Σ
+```
+
+### The inclusion of extensions of types in a subuniverse into extensions of types is an embedding
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒫 : subuniverse l1 l2) {X : UU l3}
+  where
+
+  compute-fiber-extension-type-extension-type-subuniverse :
+    (Y : extension-type l1 X) →
+    fiber (extension-type-extension-type-subuniverse 𝒫) Y ≃
+    is-in-subuniverse 𝒫 (type-extension-type Y)
+  compute-fiber-extension-type-extension-type-subuniverse Y =
+    equivalence-reasoning
+    Σ ( Σ (Σ (UU l1) (λ Z → is-in-subuniverse 𝒫 Z)) (λ Z → X → pr1 Z))
+      ( λ E → extension-type-extension-type-subuniverse 𝒫 E ＝ Y)
+    ≃ Σ ( Σ (extension-type l1 X) (is-in-subuniverse-extension-type 𝒫))
+        ( λ E → pr1 E ＝ Y)
+    by
+      equiv-Σ-equiv-base
+        ( λ E → pr1 E ＝ Y)
+        ( compute-extension-type-subuniverse 𝒫)
+    ≃ Σ ( Σ (extension-type l1 X) (λ E → E ＝ Y))
+        ( is-in-subuniverse-extension-type 𝒫 ∘ pr1)
+      by equiv-right-swap-Σ
+    ≃ is-in-subuniverse-extension-type 𝒫 Y
+    by left-unit-law-Σ-is-contr (is-torsorial-Id' Y) (Y , refl)
+
+  is-prop-map-extension-type-extension-type-subuniverse :
+    is-prop-map (extension-type-extension-type-subuniverse 𝒫)
+  is-prop-map-extension-type-extension-type-subuniverse Y =
+    is-prop-equiv
+      ( compute-fiber-extension-type-extension-type-subuniverse Y)
+      ( is-prop-is-in-subuniverse 𝒫 (type-extension-type Y))
+
+  is-emb-extension-type-extension-type-subuniverse :
+    is-emb (extension-type-extension-type-subuniverse 𝒫)
+  is-emb-extension-type-extension-type-subuniverse =
+    is-emb-is-prop-map is-prop-map-extension-type-extension-type-subuniverse
+```
+
+### Characterization of identifications of extensions of types in a subuniverse
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒫 : subuniverse l1 l2) {X : UU l3}
+  where
+
+  equiv-extension-type-subuniverse :
+    extension-type-subuniverse 𝒫 X →
+    extension-type-subuniverse 𝒫 X → UU (l1 ⊔ l3)
+  equiv-extension-type-subuniverse U V =
+    equiv-extension-type
+      ( extension-type-extension-type-subuniverse 𝒫 U)
+      ( extension-type-extension-type-subuniverse 𝒫 V)
+
+  id-equiv-extension-type-subuniverse :
+    (U : extension-type-subuniverse 𝒫 X) → equiv-extension-type-subuniverse U U
+  id-equiv-extension-type-subuniverse U =
+    id-equiv-extension-type (extension-type-extension-type-subuniverse 𝒫 U)
+
+  equiv-eq-extension-type-subuniverse :
+    (U V : extension-type-subuniverse 𝒫 X) →
+    U ＝ V → equiv-extension-type-subuniverse U V
+  equiv-eq-extension-type-subuniverse U V p =
+    equiv-eq-extension-type
+      ( extension-type-extension-type-subuniverse 𝒫 U)
+      ( extension-type-extension-type-subuniverse 𝒫 V)
+      ( ap (extension-type-extension-type-subuniverse 𝒫) p)
+
+  is-equiv-equiv-eq-extension-type-subuniverse :
+    (U V : extension-type-subuniverse 𝒫 X) →
+    is-equiv (equiv-eq-extension-type-subuniverse U V)
+  is-equiv-equiv-eq-extension-type-subuniverse U V =
+    is-equiv-comp
+      ( equiv-eq-extension-type
+        ( extension-type-extension-type-subuniverse 𝒫 U)
+        ( extension-type-extension-type-subuniverse 𝒫 V))
+      ( ap (extension-type-extension-type-subuniverse 𝒫))
+      ( is-emb-extension-type-extension-type-subuniverse 𝒫 U V)
+      ( is-equiv-equiv-eq-extension-type
+        ( extension-type-extension-type-subuniverse 𝒫 U)
+        ( extension-type-extension-type-subuniverse 𝒫 V))
+
+  extensionality-extension-type-subuniverse :
+    (U V : extension-type-subuniverse 𝒫 X) →
+    (U ＝ V) ≃ equiv-extension-type-subuniverse U V
+  extensionality-extension-type-subuniverse U V =
+    equiv-eq-extension-type-subuniverse U V ,
+    is-equiv-equiv-eq-extension-type-subuniverse U V
+
+  eq-equiv-extension-type-subuniverse :
+    (U V : extension-type-subuniverse 𝒫 X) →
+    equiv-extension-type-subuniverse U V → U ＝ V
+  eq-equiv-extension-type-subuniverse U V =
+    map-inv-equiv (extensionality-extension-type-subuniverse U V)
+```
diff --git a/src/foundation/extensions-types.lagda.md b/src/foundation/extensions-types.lagda.md
index 669684f417..7d78a32bdd 100644
--- a/src/foundation/extensions-types.lagda.md
+++ b/src/foundation/extensions-types.lagda.md
@@ -7,7 +7,16 @@ module foundation.extensions-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.commuting-triangles-of-maps
 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.torsorial-type-families
+open import foundation.univalence
 open import foundation.universe-levels
 ```
 
@@ -47,3 +56,86 @@ module _
   inclusion-extension-type : X → type-extension-type
   inclusion-extension-type = pr2 Y
 ```
+
+## Properties
+
+### Characterization of identifications of extensions of types
+
+```agda
+equiv-extension-type :
+  {l1 l2 l3 : Level} {X : UU l1} →
+  extension-type l2 X →
+  extension-type l3 X → UU (l1 ⊔ l2 ⊔ l3)
+equiv-extension-type (Y , f) (Z , g) =
+  Σ (Y ≃ Z) (λ e → coherence-triangle-maps g (map-equiv e) f)
+
+module _
+  {l1 l2 : Level} {X : UU l1}
+  where
+
+  id-equiv-extension-type : (U : extension-type l2 X) → equiv-extension-type U U
+  id-equiv-extension-type U = id-equiv , refl-htpy
+
+  equiv-eq-extension-type :
+    (U V : extension-type l2 X) → U ＝ V → equiv-extension-type U V
+  equiv-eq-extension-type U .U refl = id-equiv-extension-type U
+
+  is-torsorial-equiv-extension-type :
+    (U : extension-type l2 X) → is-torsorial (equiv-extension-type U)
+  is-torsorial-equiv-extension-type U =
+    is-torsorial-Eq-structure
+      ( is-torsorial-equiv (type-extension-type U))
+      ( type-extension-type U , id-equiv)
+      (is-torsorial-htpy' (inclusion-extension-type U))
+
+  is-equiv-equiv-eq-extension-type :
+    (U V : extension-type l2 X) → is-equiv (equiv-eq-extension-type U V)
+  is-equiv-equiv-eq-extension-type U =
+    fundamental-theorem-id
+      ( is-torsorial-equiv-extension-type U)
+      ( equiv-eq-extension-type U)
+
+  extensionality-extension-type :
+    (U V : extension-type l2 X) → (U ＝ V) ≃ equiv-extension-type U V
+  extensionality-extension-type U V =
+    equiv-eq-extension-type U V , is-equiv-equiv-eq-extension-type U V
+
+  eq-equiv-extension-type :
+    (U V : extension-type l2 X) → equiv-extension-type U V → U ＝ V
+  eq-equiv-extension-type U V =
+    map-inv-equiv (extensionality-extension-type U V)
+```
+
+### If an extension is equivalent to an equivalence, then it is an equivalence
+
+```agda
+module _
+  {l1 l2 l3 : Level} {X : UU l1}
+  (U : extension-type l2 X) (V : extension-type l3 X)
+  where
+
+  is-equiv-inclusion-extension-type-equiv :
+    equiv-extension-type U V →
+    is-equiv (inclusion-extension-type V) →
+    is-equiv (inclusion-extension-type U)
+  is-equiv-inclusion-extension-type-equiv (e , H) =
+    is-equiv-top-map-triangle
+      ( inclusion-extension-type V)
+      ( map-equiv e)
+      ( inclusion-extension-type U)
+      ( H)
+      ( is-equiv-map-equiv e)
+
+  is-equiv-inclusion-extension-type-equiv' :
+    equiv-extension-type U V →
+    is-equiv (inclusion-extension-type U) →
+    is-equiv (inclusion-extension-type V)
+  is-equiv-inclusion-extension-type-equiv' (e , H) u =
+    is-equiv-left-map-triangle
+      ( inclusion-extension-type V)
+      ( map-equiv e)
+      ( inclusion-extension-type U)
+      ( H)
+      ( u)
+      ( is-equiv-map-equiv e)
+```
diff --git a/src/foundation/fundamental-theorem-of-identity-types.lagda.md b/src/foundation/fundamental-theorem-of-identity-types.lagda.md
index 9ac5bfc324..38a8adedd0 100644
--- a/src/foundation/fundamental-theorem-of-identity-types.lagda.md
+++ b/src/foundation/fundamental-theorem-of-identity-types.lagda.md
@@ -59,9 +59,9 @@ module _
   abstract
     fundamental-theorem-id :
       is-torsorial B → (f : (x : A) → a ＝ x → B x) → is-fiberwise-equiv f
-    fundamental-theorem-id is-contr-AB f =
+    fundamental-theorem-id is-torsorial-B f =
       is-fiberwise-equiv-is-equiv-tot
-        ( is-equiv-is-contr (tot f) (is-torsorial-Id a) is-contr-AB)
+        ( is-equiv-is-contr (tot f) (is-torsorial-Id a) is-torsorial-B)
 
   abstract
     fundamental-theorem-id' :
@@ -84,8 +84,8 @@ module _
   abstract
     fundamental-theorem-id-J :
       is-torsorial B → is-fiberwise-equiv (ind-Id a (λ x p → B x) b)
-    fundamental-theorem-id-J is-contr-AB =
-      fundamental-theorem-id is-contr-AB (ind-Id a (λ x p → B x) b)
+    fundamental-theorem-id-J is-torsorial-B =
+      fundamental-theorem-id is-torsorial-B (ind-Id a (λ x p → B x) b)
 
   abstract
     fundamental-theorem-id-J' :
diff --git a/src/foundation/global-subuniverses.lagda.md b/src/foundation/global-subuniverses.lagda.md
index e000dc080e..fffb54617f 100644
--- a/src/foundation/global-subuniverses.lagda.md
+++ b/src/foundation/global-subuniverses.lagda.md
@@ -64,9 +64,13 @@ record global-subuniverse (α : Level → Level) : UUω where
       (l : Level) → subuniverse l (α l)
 
     is-closed-under-equiv-global-subuniverse :
-      (l1 l2 : Level) →
+      {l1 l2 : Level} →
       is-closed-under-equiv-subuniverses α subuniverse-global-subuniverse l1 l2
 
+  is-in-global-subuniverse-Prop : {l : Level} → UU l → Prop (α l)
+  is-in-global-subuniverse-Prop {l} X =
+    subuniverse-global-subuniverse l X
+
   is-in-global-subuniverse : {l : Level} → UU l → UU (α l)
   is-in-global-subuniverse {l} X =
     is-in-subuniverse (subuniverse-global-subuniverse l) X
@@ -85,6 +89,12 @@ record global-subuniverse (α : Level → Level) : UUω where
   inclusion-global-subuniverse {l} =
     inclusion-subuniverse (subuniverse-global-subuniverse l)
 
+  is-in-global-subuniverse-inclusion-global-subuniverse :
+    {l : Level} (X : type-global-subuniverse l) →
+    is-in-global-subuniverse (inclusion-global-subuniverse X)
+  is-in-global-subuniverse-inclusion-global-subuniverse {l} =
+    is-in-subuniverse-inclusion-subuniverse (subuniverse-global-subuniverse l)
+
 open global-subuniverse public
 ```
 
diff --git a/src/foundation/maps-in-global-subuniverses.lagda.md b/src/foundation/maps-in-global-subuniverses.lagda.md
index c890a5c258..c3f263ac66 100644
--- a/src/foundation/maps-in-global-subuniverses.lagda.md
+++ b/src/foundation/maps-in-global-subuniverses.lagda.md
@@ -65,7 +65,7 @@ module _
     is-in-global-subuniverse-map 𝒫 (terminal-map A) →
     is-in-global-subuniverse 𝒫 A
   is-in-global-subuniverse-is-in-global-subuniverse-terminal-map H =
-    is-closed-under-equiv-global-subuniverse 𝒫 l1 l1
+    is-closed-under-equiv-global-subuniverse 𝒫
       ( fiber (terminal-map A) star)
       ( A)
       ( equiv-fiber-terminal-map star)
@@ -75,7 +75,7 @@ module _
     is-in-global-subuniverse 𝒫 A →
     is-in-global-subuniverse-map 𝒫 (terminal-map A)
   is-in-global-subuniverse-terminal-map-is-in-global-subuniverse H u =
-    is-closed-under-equiv-global-subuniverse 𝒫 l1 l1
+    is-closed-under-equiv-global-subuniverse 𝒫
       ( A)
       ( fiber (terminal-map A) u)
       ( inv-equiv-fiber-terminal-map u)
@@ -98,7 +98,7 @@ module _
     cartesian-hom-arrow g f →
     is-in-global-subuniverse-map 𝒫 g
   is-in-global-subuniverse-map-base-change F α d =
-    is-closed-under-equiv-global-subuniverse 𝒫 (l1 ⊔ l2) (l3 ⊔ l4)
+    is-closed-under-equiv-global-subuniverse 𝒫
       ( fiber f (map-codomain-cartesian-hom-arrow g f α d))
       ( fiber g d)
       ( inv-equiv (equiv-fibers-cartesian-hom-arrow g f α d))
diff --git a/src/foundation/precomposition-dependent-functions.lagda.md b/src/foundation/precomposition-dependent-functions.lagda.md
index b5156efa46..fef97c901d 100644
--- a/src/foundation/precomposition-dependent-functions.lagda.md
+++ b/src/foundation/precomposition-dependent-functions.lagda.md
@@ -79,27 +79,43 @@ module _
   {g h : (b : B) → C b}
   where
 
-  compute-htpy-eq-ap-precomp-Π :
+  coherence-htpy-eq-ap-precomp-Π :
     coherence-square-maps
       ( ap (precomp-Π f C) {g} {h})
       ( htpy-eq)
       ( htpy-eq)
       ( precomp-Π f (eq-value g h))
-  compute-htpy-eq-ap-precomp-Π refl = refl
+  coherence-htpy-eq-ap-precomp-Π refl = refl
 
-  compute-eq-htpy-ap-precomp-Π :
+  coherence-htpy-eq-ap-precomp-Π' :
+    coherence-square-maps'
+      ( ap (precomp-Π f C) {g} {h})
+      ( htpy-eq)
+      ( htpy-eq)
+      ( precomp-Π f (eq-value g h))
+  coherence-htpy-eq-ap-precomp-Π' = inv-htpy coherence-htpy-eq-ap-precomp-Π
+
+  coherence-eq-htpy-ap-precomp-Π :
     coherence-square-maps
       ( precomp-Π f (eq-value g h))
       ( eq-htpy)
       ( eq-htpy)
       ( ap (precomp-Π f C) {g} {h})
-  compute-eq-htpy-ap-precomp-Π =
+  coherence-eq-htpy-ap-precomp-Π =
     vertical-inv-equiv-coherence-square-maps
       ( ap (precomp-Π f C))
       ( equiv-funext)
       ( equiv-funext)
       ( precomp-Π f (eq-value g h))
-      ( compute-htpy-eq-ap-precomp-Π)
+      ( coherence-htpy-eq-ap-precomp-Π)
+
+  coherence-eq-htpy-ap-precomp-Π' :
+    coherence-square-maps'
+      ( precomp-Π f (eq-value g h))
+      ( eq-htpy)
+      ( eq-htpy)
+      ( ap (precomp-Π f C) {g} {h})
+  coherence-eq-htpy-ap-precomp-Π' = inv-htpy coherence-eq-htpy-ap-precomp-Π
 ```
 
 ### Precomposing functions `Π B C` by `f : A → B` is `k+1`-truncated if and only if precomposing homotopies is `k`-truncated
@@ -118,7 +134,7 @@ is-trunc-map-succ-precomp-Π {k = k} {f = f} {C = C} H =
         ( htpy-eq)
         ( htpy-eq)
         ( precomp-Π f (eq-value g h))
-        ( compute-htpy-eq-ap-precomp-Π f)
+        ( coherence-htpy-eq-ap-precomp-Π f)
         ( funext g h)
         ( funext (g ∘ f) (h ∘ f))
         ( H g h))
diff --git a/src/foundation/precomposition-functions-into-subuniverses.lagda.md b/src/foundation/precomposition-functions-into-subuniverses.lagda.md
index b1d64720ab..8e0a567f55 100644
--- a/src/foundation/precomposition-functions-into-subuniverses.lagda.md
+++ b/src/foundation/precomposition-functions-into-subuniverses.lagda.md
@@ -10,14 +10,15 @@ module foundation.precomposition-functions-into-subuniverses where
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
+open import foundation.precomposition-functions
 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.function-types
+open import foundation-core.homotopies
 open import foundation-core.identity-types
-open import foundation-core.precomposition-functions
 open import foundation-core.propositions
 open import foundation-core.retractions
 open import foundation-core.sections
@@ -28,30 +29,37 @@ open import foundation-core.truncation-levels
 
 </details>
 
-## Theorem
-
-### A map between structured types is an equivalence if precomposition of functions into structured types by that map is an equivalence
+## Definitions
 
 ```agda
 module _
-  {l1 l2 : Level}
-  (α : Level → Level) (P : {l : Level} → UU l → UU (α l))
-  (A : Σ (UU l1) (P {l1})) (B : Σ (UU l2) (P {l2})) (f : pr1 A → pr1 B)
+  {α : Level → Level} (𝒫 : {l : Level} → UU l → UU (α l))
+  {l1 l2 : Level} (A : Σ (UU l1) 𝒫) (B : Σ (UU l2) 𝒫) (f : pr1 A → pr1 B)
   where
 
   universal-property-equiv-structured-type : UUω
   universal-property-equiv-structured-type =
-    {l : Level} (C : Σ (UU l) (P {l})) → is-equiv (precomp f (pr1 C))
+    {l : Level} (C : Σ (UU l) 𝒫) → is-equiv (precomp f (pr1 C))
+```
+
+## Theorem
+
+### A map between structured types is an equivalence if precomposition of functions into structured types by that map is an equivalence
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : {l : Level} → UU l → UU (α l))
+  {l1 l2 : Level} (A : Σ (UU l1) 𝒫) (B : Σ (UU l2) 𝒫) (f : pr1 A → pr1 B)
+  (H : universal-property-equiv-structured-type 𝒫 A B f)
+  where
 
-  map-inv-is-equiv-precomp-structured-type :
-    universal-property-equiv-structured-type → pr1 B → pr1 A
-  map-inv-is-equiv-precomp-structured-type H =
+  map-inv-is-equiv-precomp-structured-type : pr1 B → pr1 A
+  map-inv-is-equiv-precomp-structured-type =
     pr1 (center (is-contr-map-is-equiv (H A) id))
 
   is-section-map-inv-is-equiv-precomp-structured-type :
-    (H : universal-property-equiv-structured-type) →
-    is-section f (map-inv-is-equiv-precomp-structured-type H)
-  is-section-map-inv-is-equiv-precomp-structured-type H =
+    is-section f map-inv-is-equiv-precomp-structured-type
+  is-section-map-inv-is-equiv-precomp-structured-type =
     htpy-eq
       ( ap
         ( pr1)
@@ -59,24 +67,22 @@ module _
           ( is-contr-map-is-equiv (H B) f)
           ( ( f ∘ (pr1 (center (is-contr-map-is-equiv (H A) id)))) ,
             ( ap
-              ( λ (g : pr1 A → pr1 A) → f ∘ g)
+              ( λ g → f ∘ g)
               ( pr2 (center (is-contr-map-is-equiv (H A) id)))))
           ( id , refl)))
 
   is-retraction-map-inv-is-equiv-precomp-structured-type :
-    (H : universal-property-equiv-structured-type) →
-    is-retraction f (map-inv-is-equiv-precomp-structured-type H)
-  is-retraction-map-inv-is-equiv-precomp-structured-type H =
+    is-retraction f map-inv-is-equiv-precomp-structured-type
+  is-retraction-map-inv-is-equiv-precomp-structured-type =
     htpy-eq (pr2 (center (is-contr-map-is-equiv (H A) id)))
 
   abstract
-    is-equiv-is-equiv-precomp-structured-type :
-      universal-property-equiv-structured-type → is-equiv f
-    is-equiv-is-equiv-precomp-structured-type H =
+    is-equiv-is-equiv-precomp-structured-type : is-equiv f
+    is-equiv-is-equiv-precomp-structured-type =
       is-equiv-is-invertible
-        ( map-inv-is-equiv-precomp-structured-type H)
-        ( is-section-map-inv-is-equiv-precomp-structured-type H)
-        ( is-retraction-map-inv-is-equiv-precomp-structured-type H)
+        ( map-inv-is-equiv-precomp-structured-type)
+        ( is-section-map-inv-is-equiv-precomp-structured-type)
+        ( is-retraction-map-inv-is-equiv-precomp-structured-type)
 ```
 
 ## Corollaries
@@ -95,7 +101,7 @@ module _
   is-equiv-is-equiv-precomp-Prop :
     universal-property-equiv-Prop → is-equiv f
   is-equiv-is-equiv-precomp-Prop =
-    is-equiv-is-equiv-precomp-structured-type (λ l → l) is-prop P Q f
+    is-equiv-is-equiv-precomp-structured-type is-prop P Q f
 ```
 
 ### A map between sets is an equivalence if precomposition of functions into sets by that map is an equivalence
@@ -112,7 +118,7 @@ module _
   is-equiv-is-equiv-precomp-Set :
     universal-property-equiv-Set → is-equiv f
   is-equiv-is-equiv-precomp-Set =
-    is-equiv-is-equiv-precomp-structured-type (λ l → l) is-set A B f
+    is-equiv-is-equiv-precomp-structured-type is-set A B f
 ```
 
 ### A map between truncated types is an equivalence if precomposition of functions into truncated types by that map is an equivalence
@@ -132,5 +138,5 @@ module _
   is-equiv-is-equiv-precomp-Truncated-Type :
     universal-property-equiv-Truncated-Type → is-equiv f
   is-equiv-is-equiv-precomp-Truncated-Type =
-    is-equiv-is-equiv-precomp-structured-type (λ l → l) (is-trunc k) A B f
+    is-equiv-is-equiv-precomp-structured-type (is-trunc k) A B f
 ```
diff --git a/src/foundation/precomposition-functions.lagda.md b/src/foundation/precomposition-functions.lagda.md
index b008165dea..9e48f70cfd 100644
--- a/src/foundation/precomposition-functions.lagda.md
+++ b/src/foundation/precomposition-functions.lagda.md
@@ -84,11 +84,19 @@ module _
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
   where
 
-  retraction-section-precomp-domain : section (precomp f X) → retraction f
-  pr1 (retraction-section-precomp-domain s) =
-    map-section (precomp f X) s id
-  pr2 (retraction-section-precomp-domain s) =
-    htpy-eq (is-section-map-section (precomp f X) s id)
+  retraction-map-section-precomp : section (precomp f X) → retraction f
+  retraction-map-section-precomp (s , S) = s id , htpy-eq (S id)
+```
+
+### If `f` has a retraction then `- ∘ f : (Y → X) → (X → X)` has a section
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
+  where
+
+  section-precomp-retraction-map : retraction f → section (precomp f X)
+  section-precomp-retraction-map (r , H) = precomp r X , htpy-precomp H X
 ```
 
 ### Equivalences induce an equivalence from the type of homotopies between two maps to the type of homotopies between their precomposites
@@ -191,28 +199,41 @@ module _
   (f : A → B) {g h : B → C}
   where
 
-  compute-htpy-eq-ap-precomp :
+  coherence-htpy-eq-ap-precomp :
     coherence-square-maps
       ( ap (precomp f C))
       ( htpy-eq)
       ( htpy-eq)
       ( precomp-Π f (eq-value g h))
-  compute-htpy-eq-ap-precomp =
-    compute-htpy-eq-ap-precomp-Π f
+  coherence-htpy-eq-ap-precomp =
+    coherence-htpy-eq-ap-precomp-Π f
+
+  coherence-htpy-eq-ap-precomp' :
+    coherence-square-maps'
+      ( ap (precomp f C))
+      ( htpy-eq)
+      ( htpy-eq)
+      ( precomp-Π f (eq-value g h))
+  coherence-htpy-eq-ap-precomp' =
+    coherence-htpy-eq-ap-precomp-Π' f
 
-  compute-eq-htpy-ap-precomp :
+  coherence-eq-htpy-ap-precomp :
     coherence-square-maps
       ( precomp-Π f (eq-value g h))
       ( eq-htpy)
       ( eq-htpy)
       ( ap (precomp f C))
-  compute-eq-htpy-ap-precomp =
-    vertical-inv-equiv-coherence-square-maps
-      ( ap (precomp f C))
-      ( equiv-funext)
-      ( equiv-funext)
+  coherence-eq-htpy-ap-precomp =
+    coherence-eq-htpy-ap-precomp-Π f
+
+  coherence-eq-htpy-ap-precomp' :
+    coherence-square-maps'
       ( precomp-Π f (eq-value g h))
-      ( compute-htpy-eq-ap-precomp)
+      ( eq-htpy)
+      ( eq-htpy)
+      ( ap (precomp f C))
+  coherence-eq-htpy-ap-precomp' =
+    coherence-eq-htpy-ap-precomp-Π' f
 ```
 
 ### The precomposition map at a dependent pair type
diff --git a/src/foundation/pullback-cones.lagda.md b/src/foundation/pullback-cones.lagda.md
index eb53295e13..f35b29848d 100644
--- a/src/foundation/pullback-cones.lagda.md
+++ b/src/foundation/pullback-cones.lagda.md
@@ -8,6 +8,7 @@ module foundation.pullback-cones where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
 open import foundation.cones-over-cospan-diagrams
 open import foundation.cospan-diagrams
 open import foundation.dependent-pair-types
@@ -18,8 +19,11 @@ open import foundation.homotopies
 open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.multivariable-homotopies
+open import foundation.pullbacks
 open import foundation.standard-pullbacks
 open import foundation.structure-identity-principle
+open import foundation.unit-type
+open import foundation.universal-property-cartesian-product-types
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
@@ -28,7 +32,6 @@ open import foundation-core.contractible-types
 open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
-open import foundation-core.pullbacks
 open import foundation-core.retractions
 open import foundation-core.sections
 open import foundation-core.torsorial-type-families
@@ -226,6 +229,56 @@ id-pullback-cone :
 id-pullback-cone A = ((A , id-cone A) , is-pullback-id-cone A)
 ```
 
+### The identity type pullback cone
+
+```agda
+module _
+  {l : Level} {A : UU l} (x y : A)
+  where
+
+  cospan-diagram-Id : cospan-diagram lzero lzero l
+  cospan-diagram-Id = (unit , unit , A , point x , point y)
+
+  pullback-cone-Id : pullback-cone cospan-diagram-Id l
+  pullback-cone-Id = (((x ＝ y) , cone-Id x y) , is-pullback-Id x y)
+```
+
+### The type of equivalences pullback cone
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  cospan-diagram-equiv : cospan-diagram (l1 ⊔ l2) lzero (l1 ⊔ l2)
+  cospan-diagram-equiv =
+    ( (A → B) × (B → A) × (B → A) ,
+      unit ,
+      (A → A) × (B → B) ,
+      (λ (f , g , h) → h ∘ f , f ∘ g) ,
+      point (id' A , id' B))
+
+  pullback-cone-equiv : pullback-cone cospan-diagram-equiv (l1 ⊔ l2)
+  pullback-cone-equiv = (A ≃ B , cone-equiv) , is-pullback-equiv
+```
+
+### The cartesian product pullback cone
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  cospan-diagram-cartesian-product : cospan-diagram l1 l2 lzero
+  cospan-diagram-cartesian-product =
+    ( A , B , unit , terminal-map A , terminal-map B)
+
+  pullback-cone-cartesian-product :
+    pullback-cone cospan-diagram-cartesian-product (l1 ⊔ l2)
+  pullback-cone-cartesian-product =
+    (A × B , cone-cartesian-product A B) , is-pullback-cartesian-product A B
+```
+
 ## Table of files about pullbacks
 
 The following table lists files that are about pullbacks as a general concept.
diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md
index 7da824f4bb..aa710ea8cd 100644
--- a/src/foundation/pullbacks.lagda.md
+++ b/src/foundation/pullbacks.lagda.md
@@ -9,17 +9,21 @@ open import foundation-core.pullbacks public
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-cubes-of-maps
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.dependent-sums-pullbacks
 open import foundation.descent-equivalences
+open import foundation.equality-cartesian-product-types
+open import foundation.equivalence-extensionality
 open import foundation.equivalences
 open import foundation.function-extensionality
 open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-function-types
 open import foundation.standard-pullbacks
+open import foundation.subtypes
 open import foundation.unit-type
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
@@ -88,6 +92,83 @@ module _
   pr2 (is-pullback-Prop c) = is-prop-is-pullback c
 ```
 
+### The identity type as a pullback
+
+```agda
+module _
+  {l : Level} {A : UU l} (x y : A)
+  where
+
+  cone-Id : cone (point x) (point y) (x ＝ y)
+  cone-Id = terminal-map (x ＝ y) , terminal-map (x ＝ y) , id
+
+  is-pullback-Id : is-pullback (point x) (point y) cone-Id
+  is-pullback-Id =
+    is-equiv-is-invertible
+      coherence-square-standard-pullback
+      refl-htpy
+      refl-htpy
+```
+
+### The type of equivalences as a pullback
+
+The type of equivalences `A ≃ B` can be presented as the following pullback.
+
+```text
+             A ≃ B ----------------------> unit
+               | ⌟                          |
+               |                            |
+               |                            | * ↦ (id , id)
+               |                            |
+               |                            |
+               ∨                            ∨
+  (A → B) × (B → A) × (B → A) ----> (A → A) × (B → B)
+                    (f , g , h) ↦ (h ∘ f , f ∘ g)
+```
+
+This presentation can be found as Proposition 2.18 in {{#cite CORS20}} and
+Corollary 5.1.23 in {{#cite Rij19}}.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  cone-equiv :
+    cone
+      ( λ (f , g , h) → h ∘ f , f ∘ g)
+      ( point (id' A , id' B))
+      ( A ≃ B)
+  cone-equiv =
+      ( λ e →
+        map-equiv e , map-section-map-equiv e , map-retraction-map-equiv e) ,
+      ( terminal-map (A ≃ B)) ,
+      ( λ e →
+        eq-pair
+          ( eq-htpy (is-retraction-map-retraction-map-equiv e))
+          ( eq-htpy (is-section-map-section-map-equiv e)))
+
+  abstract
+    is-pullback-equiv :
+      is-pullback
+        ( λ (f , g , h) → h ∘ f , f ∘ g)
+        ( point (id' A , id' B))
+        ( cone-equiv)
+    is-pullback-equiv =
+      is-equiv-is-invertible
+        ( λ ((f , g , h) , * , H) →
+          f , (g , htpy-eq (pr2 (pair-eq H))) , (h , htpy-eq (pr1 (pair-eq H))))
+        ( λ (_ , * , H) →
+          eq-pair-eq-fiber
+            ( eq-pair-eq-fiber
+              ( ( ap-binary
+                  ( eq-pair)
+                  ( is-retraction-eq-htpy (ap pr1 H))
+                  ( is-retraction-eq-htpy (ap pr2 H))) ∙
+                ( is-section-pair-eq H))))
+        ( λ e → eq-type-subtype is-equiv-Prop refl)
+```
+
 ### In a commuting cube where the front faces are pullbacks, either back face is a pullback iff the other back face is
 
 ```agda
@@ -441,6 +522,10 @@ module _
           ( v))
 ```
 
+## References
+
+{{#bibliography}}
+
 ## Table of files about pullbacks
 
 The following table lists files that are about pullbacks as a general concept.
diff --git a/src/foundation/structure-identity-principle.lagda.md b/src/foundation/structure-identity-principle.lagda.md
index 28faad649b..47915100c2 100644
--- a/src/foundation/structure-identity-principle.lagda.md
+++ b/src/foundation/structure-identity-principle.lagda.md
@@ -23,10 +23,10 @@ open import foundation-core.torsorial-type-families
 ## Idea
 
 [Structure](foundation.structure.md) is presented in type theory by
-[dependent pair types](foundation.dependent-pair-types.md). The **structure
-identity principle** is a way to characterize the
-[identity type](foundation-core.identity-types.md) of a structure, using
-characterizations of the identity types of its components.
+[dependent pair types](foundation.dependent-pair-types.md). The
+{{#concept "structure identity principle" Disambiguation="for types" Agda=structure-identity-principle}}
+is a way to characterize the [identity type](foundation-core.identity-types.md)
+of a structure, using characterizations of the identity types of its components.
 
 ## Lemma
 
@@ -38,14 +38,14 @@ module _
 
   abstract
     is-torsorial-Eq-structure :
-      (is-contr-AC : is-torsorial C) (t : Σ A C) →
+      (is-torsorial-AC : is-torsorial C) (t : Σ A C) →
       is-torsorial (λ y → D (pr1 t) y (pr2 t)) →
       is-torsorial (λ t → Σ (C (pr1 t)) (D (pr1 t) (pr2 t)))
-    is-torsorial-Eq-structure is-contr-AC t is-contr-BD =
+    is-torsorial-Eq-structure is-torsorial-AC t is-torsorial-BD =
       is-contr-equiv
         ( Σ (Σ A C) (λ t → Σ (B (pr1 t)) (λ y → D (pr1 t) y (pr2 t))))
         ( interchange-Σ-Σ D)
-        ( is-contr-Σ is-contr-AC t is-contr-BD)
+        ( is-contr-Σ is-torsorial-AC t is-torsorial-BD)
 ```
 
 ## Theorem
@@ -54,7 +54,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} { A : UU l1} {B : A → UU l2} {Eq-A : A → UU l3}
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {Eq-A : A → UU l3}
   (Eq-B : {x : A} → B x → Eq-A x → UU l4)
   {a : A} {b : B a} (refl-A : Eq-A a) (refl-B : Eq-B b refl-A)
   where
@@ -93,3 +93,10 @@ module _
       ( λ y → is-equiv-map-equiv (g y))
       ( z)
 ```
+
+## External links
+
+- [Structure Identity Principle](https://1lab.dev/1Lab.Univalence.SIP.html) at
+  1lab
+- [structure identity principle](https://ncatlab.org/nlab/show/structure+identity+principle)
+  at $n$Lab
diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md
index 59d60318b5..46a1d7c326 100644
--- a/src/foundation/surjective-maps.lagda.md
+++ b/src/foundation/surjective-maps.lagda.md
@@ -48,7 +48,7 @@ open import foundation-core.torsorial-type-families
 open import foundation-core.truncated-maps
 open import foundation-core.truncation-levels
 
-open import orthogonal-factorization-systems.extensions-of-maps
+open import orthogonal-factorization-systems.extensions-maps
 ```
 
 </details>
diff --git a/src/foundation/unit-type.lagda.md b/src/foundation/unit-type.lagda.md
index ca159a3636..5b832275cd 100644
--- a/src/foundation/unit-type.lagda.md
+++ b/src/foundation/unit-type.lagda.md
@@ -15,9 +15,11 @@ open import foundation.universe-levels
 open import foundation-core.constant-maps
 open import foundation-core.contractible-types
 open import foundation-core.equivalences
+open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
 open import foundation-core.propositions
+open import foundation-core.retractions
 open import foundation-core.sets
 open import foundation-core.truncated-types
 open import foundation-core.truncation-levels
@@ -201,3 +203,14 @@ module _
   pr1 point-injection = point x
   pr2 point-injection = is-injective-point
 ```
+
+### The map `point x` has a retraction for every `x`
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A)
+  where
+
+  retraction-point : retraction (point x)
+  retraction-point = terminal-map A , refl-htpy
+```
diff --git a/src/foundation/universal-property-equivalences.lagda.md b/src/foundation/universal-property-equivalences.lagda.md
index 177b654004..4f4300ef98 100644
--- a/src/foundation/universal-property-equivalences.lagda.md
+++ b/src/foundation/universal-property-equivalences.lagda.md
@@ -97,7 +97,6 @@ module _
       universal-property-equiv f → is-equiv f
     is-equiv-is-equiv-precomp H =
       is-equiv-is-equiv-precomp-structured-type
-        ( λ l → l1 ⊔ l2)
         ( λ X → A → B)
         ( A , f)
         ( B , f)
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index b4d6443ccc..a167d57d4a 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -17,7 +17,7 @@ open import orthogonal-factorization-systems.double-lifts-families-of-elements p
 open import orthogonal-factorization-systems.double-negation-sheaves 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.extensions-maps public
 open import orthogonal-factorization-systems.factorization-operations public
 open import orthogonal-factorization-systems.factorization-operations-function-classes public
 open import orthogonal-factorization-systems.factorization-operations-global-function-classes public
@@ -28,7 +28,9 @@ open import orthogonal-factorization-systems.families-of-types-local-at-maps pub
 open import orthogonal-factorization-systems.fiberwise-orthogonal-maps public
 open import orthogonal-factorization-systems.function-classes public
 open import orthogonal-factorization-systems.functoriality-higher-modalities public
+open import orthogonal-factorization-systems.functoriality-localizations-at-global-subuniverses public
 open import orthogonal-factorization-systems.functoriality-pullback-hom public
+open import orthogonal-factorization-systems.functoriality-reflective-global-subuniverses public
 open import orthogonal-factorization-systems.global-function-classes public
 open import orthogonal-factorization-systems.higher-modalities public
 open import orthogonal-factorization-systems.identity-modality public
@@ -37,7 +39,8 @@ open import orthogonal-factorization-systems.lawvere-tierney-topologies public
 open import orthogonal-factorization-systems.lifting-operations public
 open import orthogonal-factorization-systems.lifting-structures-on-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.lifts-maps public
+open import orthogonal-factorization-systems.localizations-at-global-subuniverses public
 open import orthogonal-factorization-systems.localizations-at-maps public
 open import orthogonal-factorization-systems.localizations-at-subuniverses public
 open import orthogonal-factorization-systems.locally-small-modal-operators public
@@ -55,6 +58,7 @@ open import orthogonal-factorization-systems.orthogonal-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
+open import orthogonal-factorization-systems.reflective-global-subuniverses public
 open import orthogonal-factorization-systems.reflective-modalities public
 open import orthogonal-factorization-systems.reflective-subuniverses public
 open import orthogonal-factorization-systems.regular-cd-structures public
@@ -66,6 +70,7 @@ open import orthogonal-factorization-systems.types-colocal-at-maps public
 open import orthogonal-factorization-systems.types-local-at-maps public
 open import orthogonal-factorization-systems.types-separated-at-maps public
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities public
+open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses public
 open import orthogonal-factorization-systems.wide-function-classes public
 open import orthogonal-factorization-systems.wide-global-function-classes public
 open import orthogonal-factorization-systems.zero-modality 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
index 54b283d49d..4c248d4992 100644
--- a/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md
@@ -90,5 +90,5 @@ module _
 ## 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)
+- [Lifts of maps](orthogonal-factorization-systems.lifts-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
index a577431bf1..c590c46263 100644
--- 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
@@ -296,5 +296,5 @@ module _
 ## 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)
+- [Extensions of maps](orthogonal-factorization-systems.extensions-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
index 54bbaced86..8766921e92 100644
--- a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md
@@ -308,4 +308,4 @@ module _
 ## 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)
+- [Extensions of maps](orthogonal-factorization-systems.extensions-maps.md)
diff --git a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-maps.lagda.md
similarity index 82%
rename from src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
rename to src/orthogonal-factorization-systems/extensions-maps.lagda.md
index 1c04e75a4b..ccdc296bd0 100644
--- a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/extensions-maps.lagda.md
@@ -1,7 +1,7 @@
 # Extensions of maps
 
 ```agda
-module orthogonal-factorization-systems.extensions-of-maps where
+module orthogonal-factorization-systems.extensions-maps where
 ```
 
 <details><summary>Imports</summary>
@@ -9,13 +9,10 @@ module orthogonal-factorization-systems.extensions-of-maps where
 ```agda
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
-open import foundation.contractible-maps
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
-open import foundation.fibers-of-maps
-open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
 open import foundation.functoriality-dependent-pair-types
@@ -25,7 +22,6 @@ open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.monomorphisms
 open import foundation.postcomposition-functions
-open import foundation.precomposition-dependent-functions
 open import foundation.propositions
 open import foundation.sets
 open import foundation.structure-identity-principle
@@ -37,8 +33,6 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.torsorial-type-families
-
-open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
@@ -369,67 +363,34 @@ module _
     is-prop-Π (λ x → is-set-P x (f x) (g (i x)))
 ```
 
-### Every map has a unique extension along `i` if and only if `P` is `i`-local
+## Examples
+
+### Every map is an extension of itself along the identity
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B)
-  {l : Level} (P : B → UU l)
+  {l1 l2 : Level} {A : UU l1} {P : A → UU l2} (f : (x : A) → P x)
   where
 
-  equiv-fiber'-precomp-extension-dependent-type :
-    (f : (x : A) → P (i x)) →
-    fiber' (precomp-Π i P) f ≃ extension-dependent-type i P f
-  equiv-fiber'-precomp-extension-dependent-type f =
-    equiv-tot (λ g → equiv-funext {f = f} {g ∘ i})
-
-  equiv-fiber-precomp-extension-dependent-type :
-    (f : (x : A) → P (i x)) →
-    fiber (precomp-Π i P) f ≃ extension-dependent-type i P f
-  equiv-fiber-precomp-extension-dependent-type f =
-    ( equiv-fiber'-precomp-extension-dependent-type f) ∘e
-    ( equiv-fiber (precomp-Π i P) f)
-
-  equiv-is-contr-extension-dependent-type-is-local-dependent-type :
-    is-local-dependent-type i P ≃
-    ((f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f))
-  equiv-is-contr-extension-dependent-type-is-local-dependent-type =
-    ( equiv-Π-equiv-family
-      ( equiv-is-contr-equiv ∘ equiv-fiber-precomp-extension-dependent-type)) ∘e
-    ( equiv-is-contr-map-is-equiv (precomp-Π i P))
-
-  is-contr-extension-dependent-type-is-local-dependent-type :
-    is-local-dependent-type i P →
-    (f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f)
-  is-contr-extension-dependent-type-is-local-dependent-type =
-    map-equiv equiv-is-contr-extension-dependent-type-is-local-dependent-type
-
-  is-local-dependent-type-is-contr-extension-dependent-type :
-    ((f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f)) →
-    is-local-dependent-type i P
-  is-local-dependent-type-is-contr-extension-dependent-type =
-    map-inv-equiv
-      equiv-is-contr-extension-dependent-type-is-local-dependent-type
-```
-
-## Examples
-
-### Every map is an extension of itself along the identity
+  is-extension-self : is-extension id f f
+  is-extension-self = refl-htpy
 
-```agda
-is-extension-self :
-  {l1 l2 : Level} {A : UU l1} {P : A → UU l2}
-  (f : (x : A) → P x) → 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
-is-extension-along-self :
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  (f : A → B) → is-extension f f id
-is-extension-along-self _ = refl-htpy
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-extension-along-self : is-extension f f id
+  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
@@ -454,5 +415,5 @@ module _
 
 ## See also
 
-- [`orthogonal-factorization-systems.lifts-of-maps`](orthogonal-factorization-systems.lifts-of-maps.md)
+- [`orthogonal-factorization-systems.lifts-maps`](orthogonal-factorization-systems.lifts-maps.md)
   for the dual notion.
diff --git a/src/orthogonal-factorization-systems/functoriality-localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/functoriality-localizations-at-global-subuniverses.lagda.md
new file mode 100644
index 0000000000..84d0582079
--- /dev/null
+++ b/src/orthogonal-factorization-systems/functoriality-localizations-at-global-subuniverses.lagda.md
@@ -0,0 +1,381 @@
+# Functoriality of localizations at global subuniverses
+
+```agda
+module orthogonal-factorization-systems.functoriality-localizations-at-global-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.commuting-squares-of-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.extensions-types-global-subuniverses
+open import foundation.extensions-types-subuniverses
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.global-subuniverses
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.precomposition-functions
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.retracts-of-maps
+open import foundation.retracts-of-types
+open import foundation.subuniverses
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.localizations-at-global-subuniverses
+open import orthogonal-factorization-systems.modal-induction
+open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.modal-subuniverse-induction
+open import orthogonal-factorization-systems.types-local-at-maps
+open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses
+```
+
+</details>
+
+## Idea
+
+Given a [global subuniverse](foundation.global-subuniverses.md) `𝒫`, and two
+`𝒫`-localizations `η_X : X → LX` and `η_Y : Y → LY` then for every map
+`f : X → Y` there is a map `Lf : LX → LY` such that the square
+
+```text
+        f
+  X --------> Y
+  |           |
+  |           |
+  ∨    Lf     ∨
+  LX ------> LY
+```
+
+commutes. This construction preserves identity functions and composition of maps
+
+```text
+  L(g ∘ f) ~ Lg ∘ Lf    and    L(id) ~ id
+```
+
+## Definitions
+
+### The functorial action on maps of types with localizations
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2}
+  (LX : localization-global-subuniverse 𝒫 l3 X)
+  (LY : extension-type-global-subuniverse 𝒫 l4 Y)
+  where
+
+  map-localization-global-subuniverse' :
+    (X → Y) →
+    type-localization-global-subuniverse LX →
+    type-extension-type-global-subuniverse 𝒫 LY
+  map-localization-global-subuniverse' f =
+    map-inv-is-equiv
+      ( up-localization-global-subuniverse LX
+        ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LY))
+      ( inclusion-extension-type-global-subuniverse 𝒫 LY ∘ f)
+
+  eq-naturality-map-localization-global-subuniverse' :
+    (f : X → Y) →
+    map-localization-global-subuniverse' f ∘
+    unit-localization-global-subuniverse LX ＝
+    inclusion-extension-type-global-subuniverse 𝒫 LY ∘
+    f
+  eq-naturality-map-localization-global-subuniverse' f =
+    is-section-map-inv-is-equiv
+      ( up-localization-global-subuniverse LX
+        ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LY))
+      ( inclusion-extension-type-global-subuniverse 𝒫 LY ∘ f)
+
+  naturality-map-localization-global-subuniverse' :
+    (f : X → Y) →
+    coherence-square-maps
+      ( f)
+      ( unit-localization-global-subuniverse LX)
+      ( inclusion-extension-type-global-subuniverse 𝒫 LY)
+      ( map-localization-global-subuniverse' f)
+  naturality-map-localization-global-subuniverse' f =
+    htpy-eq (eq-naturality-map-localization-global-subuniverse' f)
+
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2}
+  (LX : localization-global-subuniverse 𝒫 l3 X)
+  (LY : localization-global-subuniverse 𝒫 l4 Y)
+  where
+
+  map-localization-global-subuniverse :
+    (X → Y) →
+    type-localization-global-subuniverse LX →
+    type-localization-global-subuniverse LY
+  map-localization-global-subuniverse =
+    map-localization-global-subuniverse' 𝒫 LX
+      ( reflection-localization-global-subuniverse LY)
+
+  eq-naturality-map-localization-global-subuniverse :
+    (f : X → Y) →
+    map-localization-global-subuniverse f ∘
+    unit-localization-global-subuniverse LX ＝
+    unit-localization-global-subuniverse LY ∘
+    f
+  eq-naturality-map-localization-global-subuniverse =
+    eq-naturality-map-localization-global-subuniverse' 𝒫 LX
+      ( reflection-localization-global-subuniverse LY)
+
+  naturality-map-localization-global-subuniverse :
+    (f : X → Y) →
+    coherence-square-maps
+      ( f)
+      ( unit-localization-global-subuniverse LX)
+      ( unit-localization-global-subuniverse LY)
+      ( map-localization-global-subuniverse f)
+  naturality-map-localization-global-subuniverse =
+    naturality-map-localization-global-subuniverse' 𝒫 LX
+      ( reflection-localization-global-subuniverse LY)
+```
+
+### The functorial action on maps of types with localizations preserves homotopies
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2}
+  (LX : localization-global-subuniverse 𝒫 l3 X)
+  (LY : extension-type-global-subuniverse 𝒫 l4 Y)
+  where
+
+  abstract
+    preserves-htpy-map-localization-global-subuniverse' :
+      {f g : X → Y} → f ~ g →
+      map-localization-global-subuniverse' 𝒫 LX LY f ~
+      map-localization-global-subuniverse' 𝒫 LX LY g
+    preserves-htpy-map-localization-global-subuniverse' {f} =
+      ind-htpy f
+        ( λ g _ →
+          map-localization-global-subuniverse' 𝒫 LX LY f ~
+          map-localization-global-subuniverse' 𝒫 LX LY g)
+        ( refl-htpy)
+
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2}
+  (LX : localization-global-subuniverse 𝒫 l3 X)
+  (LY : localization-global-subuniverse 𝒫 l4 Y)
+  where
+
+  preserves-htpy-map-localization-global-subuniverse :
+    {f g : X → Y} → f ~ g →
+    map-localization-global-subuniverse 𝒫 LX LY f ~
+    map-localization-global-subuniverse 𝒫 LX LY g
+  preserves-htpy-map-localization-global-subuniverse =
+    preserves-htpy-map-localization-global-subuniverse' 𝒫 LX
+      ( reflection-localization-global-subuniverse LY)
+```
+
+## Properties
+
+### The functorial action on maps of types with localizations preserves identity functions
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 : Level} {X : UU l1}
+  (LX : localization-global-subuniverse 𝒫 l2 X)
+  where
+
+  eq-preserves-id-map-localization-global-subuniverse :
+    map-localization-global-subuniverse 𝒫 LX LX id ＝ id
+  eq-preserves-id-map-localization-global-subuniverse =
+    is-retraction-map-inv-is-equiv
+      ( up-localization-global-subuniverse LX
+        ( type-global-subuniverse-localization-global-subuniverse LX))
+      ( id)
+
+  preserves-id-map-localization-global-subuniverse :
+    map-localization-global-subuniverse 𝒫 LX LX id ~ id
+  preserves-id-map-localization-global-subuniverse =
+    htpy-eq eq-preserves-id-map-localization-global-subuniverse
+```
+
+### The functorial action on maps of types with localizations preserves composition
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {X : UU l1} {Y : UU l2} {Z : UU l3}
+  (LX : localization-global-subuniverse 𝒫 l4 X)
+  (LY : localization-global-subuniverse 𝒫 l5 Y)
+  (LZ : extension-type-global-subuniverse 𝒫 l6 Z)
+  (g : Y → Z) (f : X → Y)
+  where
+
+  eq-preserves-comp-map-localization-global-subuniverse' :
+    map-localization-global-subuniverse' 𝒫 LX LZ (g ∘ f) ＝
+    map-localization-global-subuniverse' 𝒫 LY LZ g ∘
+    map-localization-global-subuniverse 𝒫 LX LY f
+  eq-preserves-comp-map-localization-global-subuniverse' =
+    equational-reasoning
+    map-localization-global-subuniverse' 𝒫 LX LZ (g ∘ f)
+    ＝ ( map-inv-is-equiv
+        ( up-localization-global-subuniverse LX
+          ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LZ))
+        ( map-localization-global-subuniverse' 𝒫 LY LZ g ∘
+          map-localization-global-subuniverse 𝒫 LX LY f ∘
+          unit-localization-global-subuniverse LX))
+    by
+      ap
+        ( map-inv-is-equiv
+          ( up-localization-global-subuniverse LX
+            ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LZ)))
+        ( inv
+          ( ap
+            ( map-localization-global-subuniverse' 𝒫 LY LZ g ∘_)
+            ( eq-naturality-map-localization-global-subuniverse 𝒫 LX LY f) ∙
+            ap
+              ( _∘ f)
+              ( eq-naturality-map-localization-global-subuniverse' 𝒫 LY LZ g)))
+    ＝ ( map-localization-global-subuniverse' 𝒫 LY LZ g ∘
+        map-localization-global-subuniverse 𝒫 LX LY f)
+    by
+      ( is-retraction-map-inv-is-equiv
+        ( up-localization-global-subuniverse LX
+          ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LZ))
+        ( map-localization-global-subuniverse' 𝒫 LY LZ g ∘
+          map-localization-global-subuniverse 𝒫 LX LY f))
+
+  preserves-comp-map-localization-global-subuniverse' :
+    map-localization-global-subuniverse' 𝒫 LX LZ (g ∘ f) ~
+    map-localization-global-subuniverse' 𝒫 LY LZ g ∘
+    map-localization-global-subuniverse 𝒫 LX LY f
+  preserves-comp-map-localization-global-subuniverse' =
+    htpy-eq eq-preserves-comp-map-localization-global-subuniverse'
+
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {X : UU l1} {Y : UU l2} {Z : UU l3}
+  (LX : localization-global-subuniverse 𝒫 l4 X)
+  (LY : localization-global-subuniverse 𝒫 l5 Y)
+  (LZ : localization-global-subuniverse 𝒫 l6 Z)
+  (g : Y → Z) (f : X → Y)
+  where
+
+  eq-preserves-comp-map-localization-global-subuniverse :
+    map-localization-global-subuniverse 𝒫 LX LZ (g ∘ f) ＝
+    map-localization-global-subuniverse 𝒫 LY LZ g ∘
+    map-localization-global-subuniverse 𝒫 LX LY f
+  eq-preserves-comp-map-localization-global-subuniverse =
+    eq-preserves-comp-map-localization-global-subuniverse' 𝒫
+      LX LY (reflection-localization-global-subuniverse LZ) g f
+
+  preserves-comp-map-localization-global-subuniverse :
+    map-localization-global-subuniverse 𝒫 LX LZ (g ∘ f) ~
+    map-localization-global-subuniverse 𝒫 LY LZ g ∘
+    map-localization-global-subuniverse 𝒫 LX LY f
+  preserves-comp-map-localization-global-subuniverse =
+    preserves-comp-map-localization-global-subuniverse' 𝒫
+      LX LY (reflection-localization-global-subuniverse LZ) g f
+```
+
+### Localizations are closed under retracts
+
+**Proof.** Let `X` and `Y` be types with localizations in a global subuniverse
+`𝒫`. Moreover, assume `X` is a retract of `Y` and that `Y ∈ 𝒫`. then applying
+the functoriality of localizations at global subuniverses we have a retract of
+maps
+
+```text
+        i           r
+  X --------> Y --------> X
+  |           |           |
+  |           |           |
+  ∨    Li     ∨    Lr     ∨
+  LX -------> LY ------> LX
+```
+
+since the middle vertical map is an equivalence, so is the outer vertical map.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2}
+  (LX : localization-global-subuniverse 𝒫 l3 X)
+  (LY : localization-global-subuniverse 𝒫 l4 Y)
+  (R : X retract-of Y)
+  where
+
+  inclusion-retract-localization-global-subuniverse :
+    type-localization-global-subuniverse LX →
+    type-localization-global-subuniverse LY
+  inclusion-retract-localization-global-subuniverse =
+    map-localization-global-subuniverse 𝒫 LX LY (inclusion-retract R)
+
+  map-retraction-retract-localization-global-subuniverse :
+    type-localization-global-subuniverse LY →
+    type-localization-global-subuniverse LX
+  map-retraction-retract-localization-global-subuniverse =
+    map-localization-global-subuniverse 𝒫 LY LX (map-retraction-retract R)
+
+  is-retraction-map-retraction-retract-localization-global-subuniverse :
+    is-retraction
+      ( inclusion-retract-localization-global-subuniverse)
+      ( map-retraction-retract-localization-global-subuniverse)
+  is-retraction-map-retraction-retract-localization-global-subuniverse =
+    inv-htpy
+      ( preserves-comp-map-localization-global-subuniverse 𝒫 LX LY LX
+        ( map-retraction-retract R)
+        ( inclusion-retract R)) ∙h
+    preserves-htpy-map-localization-global-subuniverse 𝒫 LX LX
+      ( is-retraction-map-retraction-retract R) ∙h
+    preserves-id-map-localization-global-subuniverse 𝒫 LX
+
+  retraction-retract-localization-global-subuniverse :
+    retraction
+      ( inclusion-retract-localization-global-subuniverse)
+  retraction-retract-localization-global-subuniverse =
+    map-retraction-retract-localization-global-subuniverse ,
+    is-retraction-map-retraction-retract-localization-global-subuniverse
+
+  retract-localization-global-subuniverse :
+    ( type-localization-global-subuniverse LX) retract-of
+    ( type-localization-global-subuniverse LY)
+  retract-localization-global-subuniverse =
+    ( map-localization-global-subuniverse 𝒫 LX LY (inclusion-retract R)) ,
+    ( retraction-retract-localization-global-subuniverse)
+
+  is-in-global-subuniverse-retract-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 Y →
+    is-in-global-subuniverse 𝒫 X
+  is-in-global-subuniverse-retract-localization-global-subuniverse H =
+    is-in-global-subuniverse-is-equiv-unit-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( reflection-localization-global-subuniverse LX)
+      ( up-localization-global-subuniverse LX)
+      ( is-equiv-retract-map-is-equiv'
+        ( unit-localization-global-subuniverse LX)
+        ( unit-localization-global-subuniverse LY)
+        ( R)
+        ( retract-localization-global-subuniverse)
+        ( naturality-map-localization-global-subuniverse 𝒫 LX LY
+          ( inclusion-retract R))
+        ( naturality-map-localization-global-subuniverse 𝒫 LY LX
+          ( map-retraction-retract R))
+        ( is-equiv-unit-is-in-global-subuniverse-universal-property-localization-global-subuniverse
+          ( 𝒫)
+          ( reflection-localization-global-subuniverse LY)
+          ( up-localization-global-subuniverse LY)
+          ( H)))
+```
+
+## References
+
+{{#bibliography}} {{#reference Rij19}} {{#reference CORS20}}
diff --git a/src/orthogonal-factorization-systems/functoriality-reflective-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/functoriality-reflective-global-subuniverses.lagda.md
new file mode 100644
index 0000000000..495d59bdb1
--- /dev/null
+++ b/src/orthogonal-factorization-systems/functoriality-reflective-global-subuniverses.lagda.md
@@ -0,0 +1,274 @@
+# Functoriality of reflective global subuniverses
+
+```agda
+module orthogonal-factorization-systems.functoriality-reflective-global-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.commuting-squares-of-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.extensions-types-global-subuniverses
+open import foundation.extensions-types-subuniverses
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.global-subuniverses
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.precomposition-functions
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.retracts-of-maps
+open import foundation.retracts-of-types
+open import foundation.subuniverses
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.functoriality-localizations-at-global-subuniverses
+open import orthogonal-factorization-systems.localizations-at-global-subuniverses
+open import orthogonal-factorization-systems.modal-induction
+open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.modal-subuniverse-induction
+open import orthogonal-factorization-systems.reflective-global-subuniverses
+open import orthogonal-factorization-systems.types-local-at-maps
+open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses
+```
+
+</details>
+
+## Idea
+
+Given a
+[reflective global subuniverse](orthogonal-factorization-systems.reflective-global-subuniverses.md)
+`𝒫` then for every map `f : X → Y` there is a map `Lf : LX → LY` such that the
+square
+
+```text
+        f
+  X --------> Y
+  |           |
+  |           |
+  ∨    Lf     ∨
+  LX ------> LY
+```
+
+commutes. This construction preserves identity functions and composition of maps
+
+```text
+  L(g ∘ f) ~ Lg ∘ Lf    and    L(id) ~ id
+```
+
+## Definitions
+
+### The functorial action on maps of reflective global subuniverses
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
+  where
+
+  map-reflective-global-subuniverse :
+    (X → Y) →
+    type-reflection-reflective-global-subuniverse 𝒫 X →
+    type-reflection-reflective-global-subuniverse 𝒫 Y
+  map-reflective-global-subuniverse =
+    map-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+
+  eq-naturality-map-reflective-global-subuniverse :
+    (f : X → Y) →
+    map-reflective-global-subuniverse f ∘
+    unit-reflective-global-subuniverse 𝒫 X ＝
+    unit-reflective-global-subuniverse 𝒫 Y ∘
+    f
+  eq-naturality-map-reflective-global-subuniverse =
+    eq-naturality-map-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+
+  naturality-map-reflective-global-subuniverse :
+    (f : X → Y) →
+    coherence-square-maps
+      ( f)
+      ( unit-reflective-global-subuniverse 𝒫 X)
+      ( unit-reflective-global-subuniverse 𝒫 Y)
+      ( map-reflective-global-subuniverse f)
+  naturality-map-reflective-global-subuniverse =
+    naturality-map-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+```
+
+### The functorial action on maps of reflective global subuniverses preserves homotopies
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
+  where
+
+  preserves-htpy-map-reflective-global-subuniverse :
+    {f g : X → Y} → f ~ g →
+    map-reflective-global-subuniverse 𝒫 f ~
+    map-reflective-global-subuniverse 𝒫 g
+  preserves-htpy-map-reflective-global-subuniverse =
+    preserves-htpy-map-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+```
+
+## Properties
+
+### The functorial action on maps of types with localizations preserves identity functions
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 : Level} {X : UU l1}
+  where
+
+  eq-preserves-id-map-reflective-global-subuniverse :
+    map-reflective-global-subuniverse 𝒫 (id' X) ＝ id
+  eq-preserves-id-map-reflective-global-subuniverse =
+    eq-preserves-id-map-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+
+  preserves-id-map-reflective-global-subuniverse :
+    map-reflective-global-subuniverse 𝒫 (id' X) ~ id
+  preserves-id-map-reflective-global-subuniverse =
+    preserves-id-map-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+```
+
+### The functorial action on maps of types with localizations preserves composition
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3}
+  (g : Y → Z) (f : X → Y)
+  where
+
+  eq-preserves-comp-map-reflective-global-subuniverse :
+    map-reflective-global-subuniverse 𝒫 (g ∘ f) ＝
+    map-reflective-global-subuniverse 𝒫 g ∘
+    map-reflective-global-subuniverse 𝒫 f
+  eq-preserves-comp-map-reflective-global-subuniverse =
+    eq-preserves-comp-map-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Z)
+      ( g)
+      ( f)
+
+  preserves-comp-map-reflective-global-subuniverse :
+    map-reflective-global-subuniverse 𝒫 (g ∘ f) ~
+    map-reflective-global-subuniverse 𝒫 g ∘
+    map-reflective-global-subuniverse 𝒫 f
+  preserves-comp-map-reflective-global-subuniverse =
+    preserves-comp-map-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Z)
+      ( g)
+      ( f)
+```
+
+### Reflective global subuniverses are closed under retracts
+
+This is Corollary 5.1.10 in {{#cite Rij19}}.
+
+**Proof.** Let `𝒫` be a reflective global subuniverse and `Y ∈ 𝒫`. Moreover, let
+`X` be a retract of `Y`. then applying the functoriality of the reflective
+subuniverse we have a retract of maps
+
+```text
+        i           r
+  X --------> Y --------> X
+  |           |           |
+  |           |           |
+  ∨    Li     ∨    Lr     ∨
+  LX -------> LY ------> LX
+```
+
+since the middle vertical map is an equivalence, so is the outer vertical map.
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
+  (R : X retract-of Y)
+  where
+
+  inclusion-retract-reflective-global-subuniverse :
+    type-reflection-reflective-global-subuniverse 𝒫 X →
+    type-reflection-reflective-global-subuniverse 𝒫 Y
+  inclusion-retract-reflective-global-subuniverse =
+    map-reflective-global-subuniverse 𝒫 (inclusion-retract R)
+
+  map-retraction-retract-reflective-global-subuniverse :
+    type-reflection-reflective-global-subuniverse 𝒫 Y →
+    type-reflection-reflective-global-subuniverse 𝒫 X
+  map-retraction-retract-reflective-global-subuniverse =
+    map-reflective-global-subuniverse 𝒫 (map-retraction-retract R)
+
+  is-retraction-map-retraction-retract-reflective-global-subuniverse :
+    is-retraction
+      ( inclusion-retract-reflective-global-subuniverse)
+      ( map-retraction-retract-reflective-global-subuniverse)
+  is-retraction-map-retraction-retract-reflective-global-subuniverse =
+    is-retraction-map-retraction-retract-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+      ( R)
+
+  retraction-retract-reflective-global-subuniverse :
+    retraction
+      ( inclusion-retract-reflective-global-subuniverse)
+  retraction-retract-reflective-global-subuniverse =
+    retraction-retract-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+      ( R)
+
+  retract-reflective-global-subuniverse :
+    ( type-reflection-reflective-global-subuniverse 𝒫 X) retract-of
+    ( type-reflection-reflective-global-subuniverse 𝒫 Y)
+  retract-reflective-global-subuniverse =
+    retract-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+      ( R)
+
+  is-in-reflective-global-subuniverse-retract :
+    is-in-reflective-global-subuniverse 𝒫 Y →
+    is-in-reflective-global-subuniverse 𝒫 X
+  is-in-reflective-global-subuniverse-retract =
+    is-in-global-subuniverse-retract-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 X)
+      ( is-reflective-reflective-global-subuniverse 𝒫 Y)
+      ( R)
+```
+
+## References
+
+{{#bibliography}} {{#reference Rij19}} {{#reference CORS20}}
diff --git a/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md b/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md
index 3482e34b6f..cd33ef10d2 100644
--- a/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md
+++ b/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md
@@ -33,8 +33,8 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 open import foundation.whiskering-identifications-concatenation
 
-open import orthogonal-factorization-systems.extensions-of-maps
-open import orthogonal-factorization-systems.lifts-of-maps
+open import orthogonal-factorization-systems.extensions-maps
+open import orthogonal-factorization-systems.lifts-maps
 open import orthogonal-factorization-systems.pullback-hom
 ```
 
diff --git a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
index 51dfe0ed13..be59e74dee 100644
--- a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
@@ -53,7 +53,7 @@ A family of elements equipped with a dependent lift is a
 elements equipped with a lift is a {{#concept "lifted family of elements"}}.
 
 To see how these families relate to
-[lifts of maps](orthogonal-factorization-systems.lifts-of-maps.md), consider the
+[lifts of maps](orthogonal-factorization-systems.lifts-maps.md), consider the
 lifting diagram
 
 ```text
@@ -215,4 +215,4 @@ module _
 ## 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)
+- [Lifts of maps](orthogonal-factorization-systems.lifts-maps.md)
diff --git a/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md b/src/orthogonal-factorization-systems/lifts-maps.lagda.md
similarity index 97%
rename from src/orthogonal-factorization-systems/lifts-of-maps.lagda.md
rename to src/orthogonal-factorization-systems/lifts-maps.lagda.md
index 779ab60222..9d2fe4746b 100644
--- a/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/lifts-maps.lagda.md
@@ -1,7 +1,7 @@
 # Lifts of maps
 
 ```agda
-module orthogonal-factorization-systems.lifts-of-maps where
+module orthogonal-factorization-systems.lifts-maps where
 ```
 
 <details><summary>Imports</summary>
@@ -280,5 +280,5 @@ module _
 
 ## See also
 
-- [`orthogonal-factorization-systems.extensions-of-maps`](orthogonal-factorization-systems.extensions-of-maps.md)
+- [`orthogonal-factorization-systems.extensions-maps`](orthogonal-factorization-systems.extensions-maps.md)
   for the dual notion.
diff --git a/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md
new file mode 100644
index 0000000000..f4ba57ae36
--- /dev/null
+++ b/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md
@@ -0,0 +1,690 @@
+# Localizations at global subuniverses
+
+```agda
+module orthogonal-factorization-systems.localizations-at-global-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.cones-over-cospan-diagrams
+open import foundation.constant-maps
+open import foundation.contractible-types
+open import foundation.cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.extensions-types
+open import foundation.extensions-types-global-subuniverses
+open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.global-subuniverses
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.postcomposition-functions
+open import foundation.precomposition-dependent-functions
+open import foundation.precomposition-functions
+open import foundation.pullback-cones
+open import foundation.pullbacks
+open import foundation.sequential-limits
+open import foundation.singleton-induction
+open import foundation.subuniverses
+open import foundation.type-theoretic-principle-of-choice
+open import foundation.unit-type
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import orthogonal-factorization-systems.orthogonal-maps
+open import orthogonal-factorization-systems.pullback-hom
+open import orthogonal-factorization-systems.types-local-at-maps
+open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses
+```
+
+</details>
+
+## Idea
+
+Let `𝒫` be a [global subuniverse](foundation.global-subuniverses.md). Given a
+type `X`, its
+{{#concept "localization" Disambiguation="at a global subuniverse of types" Agda=localization-global-subuniverse}}
+at `𝒫`, or **`𝒫`-localization**, is a type `LX` in `𝒫` and a map `η : X → LX`
+such that every type in `𝒫` is
+`η`-[local](orthogonal-factorization-systems.types-local-at-maps.md). I.e., for
+every `Z` in `𝒫`, the [precomposition map](foundation-core.function-types.md)
+
+```text
+  - ∘ η : (LX → Z) → (X → Z)
+```
+
+is an [equivalence](foundation-core.equivalences.md). This is referred to as the
+[universal property of localizations](orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses.md).
+
+## Definitions
+
+### The type of localizations of a type at a global subuniverse
+
+```agda
+record
+  localization-global-subuniverse
+    {α : Level → Level} (𝒫 : global-subuniverse α)
+    {l1 : Level} (l2 : Level) (X : UU l1) :
+    UUω
+  where
+
+  constructor make-localization-global-subuniverse
+
+  field
+    reflection-localization-global-subuniverse :
+      extension-type-global-subuniverse 𝒫 l2 X
+
+  extension-type-localization-global-subuniverse :
+    extension-type l2 X
+  extension-type-localization-global-subuniverse =
+    extension-type-extension-type-global-subuniverse 𝒫
+      reflection-localization-global-subuniverse
+
+  type-global-subuniverse-localization-global-subuniverse :
+    type-global-subuniverse 𝒫 l2
+  type-global-subuniverse-localization-global-subuniverse =
+    type-global-subuniverse-extension-type-global-subuniverse 𝒫
+      reflection-localization-global-subuniverse
+
+  type-localization-global-subuniverse : UU l2
+  type-localization-global-subuniverse =
+    type-extension-type-global-subuniverse 𝒫
+      reflection-localization-global-subuniverse
+
+  is-in-global-subuniverse-type-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 type-localization-global-subuniverse
+  is-in-global-subuniverse-type-localization-global-subuniverse =
+    is-in-global-subuniverse-type-extension-type-global-subuniverse 𝒫
+      reflection-localization-global-subuniverse
+
+  unit-localization-global-subuniverse :
+    X → type-localization-global-subuniverse
+  unit-localization-global-subuniverse =
+    inclusion-extension-type-global-subuniverse 𝒫
+      reflection-localization-global-subuniverse
+
+  field
+    up-localization-global-subuniverse :
+      universal-property-localization-global-subuniverse 𝒫 X
+        reflection-localization-global-subuniverse
+
+open localization-global-subuniverse public
+```
+
+## Properties
+
+### Localizations are essentially unique
+
+This is Proposition 5.1.2 in {{#cite Rij19}}.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 : Level} {X : UU l1}
+  (LX : localization-global-subuniverse 𝒫 l2 X)
+  (LX' : localization-global-subuniverse 𝒫 l3 X)
+  where
+
+  essentially-unique-type-localization-global-subuniverse :
+    type-localization-global-subuniverse LX ≃
+    type-localization-global-subuniverse LX'
+  essentially-unique-type-localization-global-subuniverse =
+    essentially-unique-type-universal-property-localization-global-subuniverse 𝒫
+      ( reflection-localization-global-subuniverse LX)
+      ( reflection-localization-global-subuniverse LX')
+      ( up-localization-global-subuniverse LX)
+      ( up-localization-global-subuniverse LX')
+
+  essentially-unique-reflection-localization-global-subuniverse :
+    equiv-extension-type-global-subuniverse 𝒫
+      ( reflection-localization-global-subuniverse LX)
+      ( reflection-localization-global-subuniverse LX')
+  essentially-unique-reflection-localization-global-subuniverse =
+    essentially-unique-extension-type-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( reflection-localization-global-subuniverse LX)
+      ( reflection-localization-global-subuniverse LX')
+      ( up-localization-global-subuniverse LX)
+      ( up-localization-global-subuniverse LX')
+```
+
+### Localizations are unique
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 : Level} {X : UU l1}
+  (LX LX' : localization-global-subuniverse 𝒫 l2 X)
+  where
+
+  unique-type-localization-global-subuniverse :
+    type-localization-global-subuniverse LX ＝
+    type-localization-global-subuniverse LX'
+  unique-type-localization-global-subuniverse =
+    unique-type-universal-property-localization-global-subuniverse 𝒫
+      ( reflection-localization-global-subuniverse LX)
+      ( reflection-localization-global-subuniverse LX')
+      ( up-localization-global-subuniverse LX)
+      ( up-localization-global-subuniverse LX')
+
+  unique-reflection-localization-global-subuniverse :
+    reflection-localization-global-subuniverse LX ＝
+    reflection-localization-global-subuniverse LX'
+  unique-reflection-localization-global-subuniverse =
+    unique-extension-type-universal-property-localization-global-subuniverse 𝒫
+      ( reflection-localization-global-subuniverse LX)
+      ( reflection-localization-global-subuniverse LX')
+      ( up-localization-global-subuniverse LX)
+      ( up-localization-global-subuniverse LX')
+```
+
+### If the unit type has a `𝒫`-localization then it is in `𝒫`
+
+This is Corollary 5.1.4 of {{#cite Rij19}}.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  where
+
+  is-equiv-unit-has-localization-global-subuniverse-unit :
+    {l : Level} (L : localization-global-subuniverse 𝒫 l unit) →
+    is-equiv (unit-localization-global-subuniverse L)
+  is-equiv-unit-has-localization-global-subuniverse-unit L =
+    is-equiv-unit-retraction-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( reflection-localization-global-subuniverse L)
+      ( up-localization-global-subuniverse L)
+      ( retraction-point (unit-localization-global-subuniverse L star))
+
+  is-in-global-subuniverse-has-localization-global-subuniverse-unit :
+    {l : Level} (L : localization-global-subuniverse 𝒫 l unit) →
+    is-in-global-subuniverse 𝒫 unit
+  is-in-global-subuniverse-has-localization-global-subuniverse-unit L =
+    is-in-global-subuniverse-is-equiv-unit-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( reflection-localization-global-subuniverse L)
+      ( up-localization-global-subuniverse L)
+      ( is-equiv-unit-has-localization-global-subuniverse-unit L)
+```
+
+### If a contractible type has a `𝒫`-localization then it is in `𝒫`
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 : Level} {A : UU l1} (H : is-contr A)
+  (LA : localization-global-subuniverse 𝒫 l2 A)
+  where
+
+  is-equiv-unit-has-localization-global-subuniverse-is-contr :
+    is-equiv (unit-localization-global-subuniverse LA)
+  is-equiv-unit-has-localization-global-subuniverse-is-contr =
+    is-equiv-unit-retraction-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( reflection-localization-global-subuniverse LA)
+      ( up-localization-global-subuniverse LA)
+      ( const (type-localization-global-subuniverse LA) (center H) ,
+        contraction H)
+
+  is-in-global-subuniverse-has-localization-global-subuniverse-is-contr :
+    is-in-global-subuniverse 𝒫 A
+  is-in-global-subuniverse-has-localization-global-subuniverse-is-contr =
+    is-in-global-subuniverse-is-equiv-unit-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( reflection-localization-global-subuniverse LA)
+      ( up-localization-global-subuniverse LA)
+      ( is-equiv-unit-has-localization-global-subuniverse-is-contr)
+```
+
+### Dependent sums of dependent types over localizations
+
+Given a localization `η : X → LX` with respect to a global subuniverse `𝒫` and a
+dependent type `P` over `LX`, then if the dependent sum `Σ (l : LX), P l` is in
+`𝒫` the dependent type `P` is `η`-local.
+
+This is stated as Proposition 5.1.5 in {{#cite Rij19}} and as Proposition 2.8 in
+{{#cite CORS20}}.
+
+**Proof.** Consider the following diagram.
+
+```text
+                          - ∘ η
+      (Π (l : LX), P l) --------> (Π (x : X), P (η x))
+             |                             |
+             |                             |
+             |                             |
+             |                             |
+             ∨            - ∘ η            ∨
+  (LX → Σ (l : LX), P l) ------> (X → Σ (l : LX), P l)
+             |                             |
+             |                             |
+     pr1 ∘ - |                             | pr1 ∘ -
+             |                             |
+             ∨            - ∘ η            ∨
+    id ∈ (LX → LX) -------------------> (X → LX)
+```
+
+The bottom horizontal map is an equivalence by the universal property of the
+localization and the top vertical maps are fiber inclusions. Therefore, the
+middle horizontal map is an equivalence and the bottom square is a pullback if
+and only if the the top horizontal map is an equivalence.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 : Level} {X : UU l1}
+  (LX : localization-global-subuniverse 𝒫 l2 X)
+  {P : type-localization-global-subuniverse LX → UU l3}
+  where
+
+  is-local-dependent-type-is-in-global-subuniverse-Σ-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 (Σ (type-localization-global-subuniverse LX) P) →
+    is-local-dependent-type (unit-localization-global-subuniverse LX) P
+  is-local-dependent-type-is-in-global-subuniverse-Σ-localization-global-subuniverse
+    H =
+    is-equiv-target-is-equiv-source-equiv-arrow _ _
+      ( equiv-Π-equiv-family (equiv-fiber-pr1 P) ,
+        equiv-Π-equiv-family
+          ( equiv-fiber-pr1 P ∘ unit-localization-global-subuniverse LX) ,
+        refl-htpy)
+      ( is-orthogonal-fiber-condition-right-map-is-orthogonal-pullback-condition
+        ( unit-localization-global-subuniverse LX)
+        ( pr1 {B = P})
+        ( is-pullback-is-equiv-horizontal-maps _ _
+          ( cone-pullback-hom (unit-localization-global-subuniverse LX) pr1)
+          ( up-localization-global-subuniverse LX
+            ( type-global-subuniverse-localization-global-subuniverse LX))
+          ( up-localization-global-subuniverse LX
+            ( Σ (type-localization-global-subuniverse LX) P , H)))
+        ( id))
+```
+
+> This formalized proof can be made more elegant by formalizing the concept of
+> type families that are orthogonal to maps.
+
+**Alternative proof.** We have an equivalence of arrows
+
+```text
+                                precomp η (Σ LX P)
+             (B → Σ LX P) ------------------------------> (A → Σ LX P)
+                  |                                           |
+                ~ |                                           | ~
+                  ∨                                           ∨
+  Σ (h : B → LX) ((y : B) → P (h y)) --------> Σ (h : A → LX) ((x : A) → P (h x)).
+                  map-Σ _ (precomp η LX) (λ h → precomp-Π η (P ∘ h))
+```
+
+and the functoriality of dependent pair types decomposes as a composite
+
+```text
+  map-Σ _ (precomp η LX) (λ h → precomp-Π η (P ∘ h)) ~
+  map-Σ-map-base _ (precomp η LX) ∘ tot (λ h → precomp-Π η (P ∘ h)).
+```
+
+Since `LX` is `𝒫`-local the map `map-Σ-map-base _ (precomp η LX)` is an
+equivalence. Therefore, `precomp η (Σ LX P)` is an equivalence if and only if
+`λ h → precomp-Π η (P ∘ h)` is a fiberwise equivalence. In particular, if
+`precomp η (Σ LX P)` is an equivalence then `precomp-Π η P` is an equivalence.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 : Level} {X : UU l1}
+  (LX : localization-global-subuniverse 𝒫 l2 X)
+  {P : type-localization-global-subuniverse LX → UU l3}
+  where
+
+  is-local-dependent-type-is-in-global-subuniverse-Σ-localization-global-subuniverse' :
+    is-in-global-subuniverse 𝒫 (Σ (type-localization-global-subuniverse LX) P) →
+    is-local-dependent-type (unit-localization-global-subuniverse LX) P
+  is-local-dependent-type-is-in-global-subuniverse-Σ-localization-global-subuniverse'
+    H =
+    is-fiberwise-equiv-is-equiv-map-Σ
+      ( λ h → (x : X) → P (h x))
+      ( precomp
+        ( unit-localization-global-subuniverse LX)
+        ( type-localization-global-subuniverse LX))
+      ( λ h → precomp-Π (unit-localization-global-subuniverse LX) (P ∘ h))
+      ( up-localization-global-subuniverse LX
+        ( type-global-subuniverse-localization-global-subuniverse LX))
+      ( is-equiv-target-is-equiv-source-equiv-arrow
+        ( precomp
+          ( unit-localization-global-subuniverse LX)
+          ( Σ (type-localization-global-subuniverse LX) P))
+        ( map-Σ
+          ( λ h → (x : X) → P (h x))
+          ( precomp
+            ( unit-localization-global-subuniverse LX)
+            ( type-localization-global-subuniverse LX))
+          ( λ h → precomp-Π (unit-localization-global-subuniverse LX) (P ∘ h)))
+        ( distributive-Π-Σ , distributive-Π-Σ , coherence-precomp-Σ)
+        ( up-localization-global-subuniverse LX
+          ( Σ (type-localization-global-subuniverse LX) P , H)))
+      ( id)
+```
+
+### Dependent products of `𝒫`-types that have a `𝒫`-localization are `𝒫`-types
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
+  (K : (x : A) → is-in-global-subuniverse 𝒫 (B x))
+  (LE : localization-global-subuniverse 𝒫 l3 ((x : A) → B x))
+  where
+
+  is-in-global-subuniverse-Π-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 ((x : A) → B x)
+  is-in-global-subuniverse-Π-localization-global-subuniverse =
+    is-in-global-subuniverse-is-local-type-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( reflection-localization-global-subuniverse LE)
+      ( up-localization-global-subuniverse LE)
+      ( distributive-Π-is-local
+        ( unit-localization-global-subuniverse LE)
+        ( B)
+        ( λ x → up-localization-global-subuniverse LE (B x , K x)))
+```
+
+### Exponentials of `𝒫`-types that have a `𝒫`-localization are `𝒫`-types
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
+  (K : is-in-global-subuniverse 𝒫 B)
+  (LE : localization-global-subuniverse 𝒫 l3 (A → B))
+  where
+
+  is-in-global-subuniverse-exponential-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 (A → B)
+  is-in-global-subuniverse-exponential-localization-global-subuniverse =
+    is-in-global-subuniverse-Π-localization-global-subuniverse 𝒫 (λ _ → K) LE
+```
+
+### Localizations of types of homotopies
+
+Assume given a `𝒫`-localization `η : X → LX` and two maps `f g : LX → Y` where
+`Y ∈ 𝒫`, then the right whiskering map `- ·r η : (g ~ h) → (g ∘ η ~ h ∘ η)` is
+an equivalence.
+
+This is Lemma 5.1.18 in {{#cite Rij19}}.
+
+**Proof.** We have an equivalence of maps
+
+```text
+                ap (- ∘ η)
+        g ＝ h -----------> g ∘ η ＝ h ∘ η
+          |                       |
+  htpy-eq | ~                   ~ | htpy-eq
+          ∨                       ∨
+        g ~ h ------------> g ∘ η ~ h ∘ η
+                  - ·r η
+```
+
+and the map `- ∘ η` is an embedding since `Y` is `η`-local by the universal
+property, hence the top horizontal map is an equivalence and so the bottom map
+is as well.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l3}
+  (LX : localization-global-subuniverse 𝒫 l2 X)
+  (H : is-in-global-subuniverse 𝒫 Y)
+  where
+
+  is-equiv-right-whisker-unit-localization-global-subuniverse :
+    {g h : type-localization-global-subuniverse LX → Y} →
+    is-equiv
+      ( λ H →
+        right-whisker-comp {g = g} {h} H
+          ( unit-localization-global-subuniverse LX))
+  is-equiv-right-whisker-unit-localization-global-subuniverse {g} {h} =
+    is-equiv-target-is-equiv-source-equiv-arrow
+      ( ap (precomp (unit-localization-global-subuniverse LX) Y))
+      ( _·r (unit-localization-global-subuniverse LX))
+      ( equiv-funext ,
+        equiv-funext ,
+        coherence-htpy-eq-ap-precomp' (unit-localization-global-subuniverse LX))
+      (is-emb-is-equiv (up-localization-global-subuniverse LX (Y , H)) g h)
+```
+
+### A type is a `𝒫`-type if it has a `𝒫`-localization and is a pullback of types in `𝒫`
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 l5 : Level}
+  {𝒮 : cospan-diagram l1 l2 l3}
+  (c : pullback-cone 𝒮 l4)
+  (LC : localization-global-subuniverse 𝒫 l5 (domain-pullback-cone 𝒮 c))
+  where
+
+  map-compute-cone-pullback-localization-global-subuniverse :
+    cone
+      ( left-map-cospan-diagram 𝒮)
+      ( right-map-cospan-diagram 𝒮)
+      ( type-localization-global-subuniverse LC) →
+    cone
+      ( left-map-cospan-diagram 𝒮)
+      ( right-map-cospan-diagram 𝒮)
+      ( domain-pullback-cone 𝒮 c)
+  map-compute-cone-pullback-localization-global-subuniverse c' =
+    cone-map
+      ( left-map-cospan-diagram 𝒮)
+      ( right-map-cospan-diagram 𝒮)
+      ( c')
+      ( unit-localization-global-subuniverse LC)
+
+  is-equiv-map-compute-cone-pullback-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) →
+    is-equiv map-compute-cone-pullback-localization-global-subuniverse
+  is-equiv-map-compute-cone-pullback-localization-global-subuniverse x a b =
+    is-equiv-map-Σ _
+      ( up-localization-global-subuniverse LC
+        ( left-type-cospan-diagram 𝒮 , a))
+      ( λ _ →
+        is-equiv-map-Σ _
+          ( up-localization-global-subuniverse LC
+            ( right-type-cospan-diagram 𝒮 , b))
+          ( λ _ →
+            is-equiv-right-whisker-unit-localization-global-subuniverse 𝒫 LC x))
+
+  is-in-global-subuniverse-pullback-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (domain-pullback-cone 𝒮 c)
+  is-in-global-subuniverse-pullback-localization-global-subuniverse x a b =
+    is-in-global-subuniverse-is-local-type-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( reflection-localization-global-subuniverse LC)
+      ( up-localization-global-subuniverse LC)
+      ( is-equiv-source-is-equiv-target-equiv-arrow
+        ( precomp
+          ( unit-localization-global-subuniverse LC)
+          ( domain-pullback-cone 𝒮 c))
+        ( map-compute-cone-pullback-localization-global-subuniverse)
+        ( ( ( cone-map
+              ( left-map-cospan-diagram 𝒮)
+              ( right-map-cospan-diagram 𝒮)
+              ( cone-pullback-cone 𝒮 c)) ,
+            ( up-pullback-cone 𝒮 c (type-localization-global-subuniverse LC))) ,
+          ( ( cone-map
+              ( left-map-cospan-diagram 𝒮)
+              ( right-map-cospan-diagram 𝒮)
+              ( cone-pullback-cone 𝒮 c)) ,
+            ( up-pullback-cone 𝒮 c ( domain-pullback-cone 𝒮 c))) ,
+          ( refl-htpy))
+        ( is-equiv-map-compute-cone-pullback-localization-global-subuniverse
+            ( x)
+            ( a)
+            ( b)))
+```
+
+### Cartesian products of `𝒫`-types that have a `𝒫`-localization are `𝒫`-types
+
+Let `𝒫` be a global subuniverse such that `unit` is a `𝒫`-type. Then if `A` and
+`B` are `𝒫`-types and their cartesian product `A × B` has a `𝒫`-localization,
+then `A × B` is a `𝒫`-type.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  (U : is-in-global-subuniverse 𝒫 unit)
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
+  (H : is-in-global-subuniverse 𝒫 A)
+  (K : is-in-global-subuniverse 𝒫 B)
+  (LI : localization-global-subuniverse 𝒫 l3 (A × B))
+  where
+
+  is-in-global-subuniverse-cartesian-product-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 (A × B)
+  is-in-global-subuniverse-cartesian-product-localization-global-subuniverse =
+    is-in-global-subuniverse-pullback-localization-global-subuniverse 𝒫
+      ( pullback-cone-cartesian-product)
+      ( LI)
+      ( U)
+      ( H)
+      ( K)
+```
+
+### Identity types of `𝒫`-types that have a `𝒫`-localization are `𝒫`-types
+
+Let `𝒫` be a global subuniverse such that `unit` is a `𝒫`-type. Now assume given
+a `𝒫`-type `A` with elements `x` and `y` such that `x ＝ y` has a
+`𝒫`-localization, then `x ＝ y` is a `𝒫`-type.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  (U : is-in-global-subuniverse 𝒫 unit)
+  {l1 l2 : Level} {A : UU l1} {x y : A}
+  (H : is-in-global-subuniverse 𝒫 A)
+  (LI : localization-global-subuniverse 𝒫 l2 (x ＝ y))
+  where
+
+  is-in-global-subuniverse-Id-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 (x ＝ y)
+  is-in-global-subuniverse-Id-localization-global-subuniverse =
+    is-in-global-subuniverse-pullback-localization-global-subuniverse 𝒫
+      ( pullback-cone-Id x y)
+      ( LI)
+      ( H)
+      ( U)
+      ( U)
+```
+
+### Sequential limits of `𝒫`-types that have a `𝒫`-localization are `𝒫`-types
+
+> This remains to be formalized.
+
+### Cartesian products of `𝒫`-localizations
+
+Let `𝒫` be a global subuniverse, then if `η_A : A → LA` and `η_B : B → LB` are
+`𝒫`-localizations such that `LA × LB` is a `𝒫`-type and `𝒫` is closed under
+exponentiating by `LB`, then `η_A × η_B : A × B → LA × LB` is a `𝒫`-localization
+as well.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
+  (LA : localization-global-subuniverse 𝒫 l3 A)
+  (LB : localization-global-subuniverse 𝒫 l4 B)
+  (exp-LB :
+    {l : Level}
+    (Z : type-global-subuniverse 𝒫 l) →
+    is-in-global-subuniverse 𝒫
+      ( type-localization-global-subuniverse LB →
+        inclusion-global-subuniverse 𝒫 Z))
+  (H :
+    is-in-global-subuniverse 𝒫
+      ( type-localization-global-subuniverse LA ×
+        type-localization-global-subuniverse LB))
+  where
+
+  type-cartesian-product-localization-global-subuniverse :
+    UU (l3 ⊔ l4)
+  type-cartesian-product-localization-global-subuniverse =
+    type-localization-global-subuniverse LA ×
+    type-localization-global-subuniverse LB
+
+  unit-cartesian-product-localization-global-subuniverse :
+    A × B → type-cartesian-product-localization-global-subuniverse
+  unit-cartesian-product-localization-global-subuniverse =
+    map-product
+      ( unit-localization-global-subuniverse LA)
+      ( unit-localization-global-subuniverse LB)
+
+  reflection-cartesian-product-localization-global-subuniverse :
+    extension-type-global-subuniverse 𝒫 (l3 ⊔ l4) (A × B)
+  reflection-cartesian-product-localization-global-subuniverse =
+    ( type-cartesian-product-localization-global-subuniverse , H) ,
+    ( unit-cartesian-product-localization-global-subuniverse)
+
+  up-cartesian-product-localization-global-subuniverse :
+    universal-property-localization-global-subuniverse 𝒫 (A × B)
+      ( reflection-cartesian-product-localization-global-subuniverse)
+  up-cartesian-product-localization-global-subuniverse Z =
+    is-equiv-source-is-equiv-target-equiv-arrow
+      ( precomp
+        ( unit-cartesian-product-localization-global-subuniverse)
+        ( inclusion-global-subuniverse 𝒫 Z))
+      ( λ f →
+        ( precomp
+          ( unit-localization-global-subuniverse LB)
+          ( inclusion-global-subuniverse 𝒫 Z)) ∘
+        ( precomp
+          ( unit-localization-global-subuniverse LA)
+          ( type-localization-global-subuniverse LB →
+            inclusion-global-subuniverse 𝒫 Z)
+          ( f)))
+      ( equiv-ev-pair , equiv-ev-pair , refl-htpy)
+      ( is-equiv-comp
+        ( postcomp A
+          ( precomp
+            ( unit-localization-global-subuniverse LB)
+            ( inclusion-global-subuniverse 𝒫 Z)))
+        ( precomp
+          ( unit-localization-global-subuniverse LA)
+          ( type-localization-global-subuniverse LB →
+            inclusion-global-subuniverse 𝒫 Z))
+        ( up-localization-global-subuniverse LA
+          ( ( type-localization-global-subuniverse LB →
+              inclusion-global-subuniverse 𝒫 Z) ,
+            ( exp-LB Z)))
+        ( is-equiv-postcomp-is-equiv
+          ( precomp
+            ( unit-localization-global-subuniverse LB)
+            ( inclusion-global-subuniverse 𝒫 Z))
+          ( up-localization-global-subuniverse LB Z)
+          ( A)))
+
+  cartesian-product-localization-global-subuniverse :
+    localization-global-subuniverse 𝒫 (l3 ⊔ l4) (A × B)
+  reflection-localization-global-subuniverse
+    cartesian-product-localization-global-subuniverse =
+    reflection-cartesian-product-localization-global-subuniverse
+  up-localization-global-subuniverse
+    cartesian-product-localization-global-subuniverse =
+    up-cartesian-product-localization-global-subuniverse
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md
index 4a8aa80c7b..d47b2a74fd 100644
--- a/src/orthogonal-factorization-systems/null-types.lagda.md
+++ b/src/orthogonal-factorization-systems/null-types.lagda.md
@@ -7,6 +7,7 @@ module orthogonal-factorization-systems.null-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.diagonal-maps-of-types
@@ -14,6 +15,8 @@ open import foundation.equivalences
 open import foundation.equivalences-arrows
 open import foundation.fibers-of-maps
 open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.logical-equivalences
@@ -21,9 +24,12 @@ open import foundation.postcomposition-functions
 open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
 open import foundation.propositions
+open import foundation.retractions
 open import foundation.retracts-of-maps
 open import foundation.retracts-of-types
+open import foundation.sections
 open import foundation.type-arithmetic-unit-type
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
 open import foundation.universal-property-equivalences
 open import foundation.universal-property-family-of-fibers-of-maps
@@ -238,3 +244,29 @@ is-null-is-contr {A = A} B is-contr-A =
   is-null-is-local-terminal-map B A
     ( is-local-is-contr (terminal-map B) A is-contr-A)
 ```
+
+### Null types are closed under dependent sums
+
+This is Theorem 2.19 in {{#cite RSS20}}.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {Y : UU l1} {A : UU l2} {B : A → UU l3}
+  (is-null-A : is-null Y A)
+  (is-null-B : (x : A) → is-null Y (B x))
+  where
+
+  is-null-Σ : is-null Y (Σ A B)
+  is-null-Σ =
+    is-equiv-map-equiv
+      ( equivalence-reasoning
+        Σ A B
+        ≃ Σ (Y → A) (λ f → (x : Y) → B (f x))
+        by
+          equiv-Σ
+            ( λ f → (x : Y) → B (f x))
+            ( diagonal-exponential A Y , is-null-A)
+            ( λ x → diagonal-exponential (B x) Y , is-null-B x)
+        ≃ (Y → Σ A B)
+        by inv-distributive-Π-Σ)
+```
diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
index bec501ea4d..ec37ad84de 100644
--- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
@@ -61,8 +61,8 @@ The map `f : A → B` is said to be
 {{#concept "orthogonal" Disambiguation="maps of types" Agda=is-orthogonal}} to
 `g : X → Y` if any of the following equivalent definitions hold
 
-1. Their [pullback-hom](orthogonal-factorization-systems.pullback-hom.md) is an
-   equivalence.
+1. Their [pullback-hom](orthogonal-factorization-systems.pullback-hom.md)
+   `f ⋔ g` is an equivalence.
 
 2. There is a [unique](foundation-core.contractible-types.md)
    [lifting operation](orthogonal-factorization-systems.lifting-operations.md)
@@ -108,6 +108,8 @@ module _
   is-orthogonal : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   is-orthogonal = is-equiv (pullback-hom f g)
 
+  infix 6 _⊥_
+  _⊥_ : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   _⊥_ = is-orthogonal
 
   is-prop-is-orthogonal : is-prop is-orthogonal
@@ -320,6 +322,28 @@ module _
 
 ### Being orthogonal means satisfying the fiber condition for orthogonal maps
 
+**Proof.** The exponential square is a pullback if and only if the induced map
+on fibers of the vertical maps
+
+```text
+  fiber (g ∘ -) h → fiber (g ∘ -) (h ∘ f)
+```
+
+is an equivalence for all `h`, and this map is equivalent to the relevant fiber
+map
+
+```text
+                                      ~
+      (Π (b : B), fiber g (h b)) ----------> fiber (g ∘ -) h
+                  |                                 |
+                  |                                 |
+                  ∨                   ~             ∨
+  (Π (a : A) → (fiber g (h (f a)))) ----> fiber (g ∘ -) (h ∘ f),
+```
+
+hence the fiber condition is satisified if and only if `f` and `g` are
+orthogonal.
+
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
diff --git a/src/orthogonal-factorization-systems/pullback-hom.lagda.md b/src/orthogonal-factorization-systems/pullback-hom.lagda.md
index c905593052..4181ff3a64 100644
--- a/src/orthogonal-factorization-systems/pullback-hom.lagda.md
+++ b/src/orthogonal-factorization-systems/pullback-hom.lagda.md
@@ -524,6 +524,17 @@ module _
 
 ### Computing the fiber map between the vertical maps in the pullback-hom square
 
+We have an equivalence of arrows
+
+```text
+                                      ~
+      (Π (b : B), fiber g (h b)) ----------> fiber (g ∘ -) h
+                  |                                 |
+                  |                                 |
+                  ∨                   ~             ∨
+  (Π (a : A) → (fiber g (h (f a)))) ----> fiber (g ∘ -) (h ∘ f)
+```
+
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
@@ -549,7 +560,7 @@ module _
       ( postcomp A g)
       ( precomp f Y h)
       ( refl)
-      ( compute-eq-htpy-ap-precomp f (pr2 (map-distributive-Π-Σ H)))
+      ( coherence-eq-htpy-ap-precomp f (pr2 (map-distributive-Π-Σ H)))
 ```
 
 ## Table of files about pullbacks
diff --git a/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md
new file mode 100644
index 0000000000..787a963051
--- /dev/null
+++ b/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md
@@ -0,0 +1,477 @@
+# Reflective global subuniverses
+
+```agda
+module orthogonal-factorization-systems.reflective-global-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.cones-over-cospan-diagrams
+open import foundation.contractible-types
+open import foundation.cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.extensions-types-global-subuniverses
+open import foundation.extensions-types-subuniverses
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.global-subuniverses
+open import foundation.identity-types
+open import foundation.precomposition-functions
+open import foundation.propositions
+open import foundation.pullback-cones
+open import foundation.retractions
+open import foundation.subuniverses
+open import foundation.unit-type
+open import foundation.universal-property-pullbacks
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.localizations-at-global-subuniverses
+open import orthogonal-factorization-systems.modal-induction
+open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.modal-subuniverse-induction
+open import orthogonal-factorization-systems.types-local-at-maps
+open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "reflective global subuniverse" Disambiguation="of types" Agda=reflective-global-subuniverse}},
+or **localization**, is a
+[global subuniverse](foundation.global-subuniverses.md) `𝒫` together with a
+reflecting operator `L` on types giving
+[localizations](orthogonal-factorization-systems.localizations-at-global-subuniverses.md)
+at `𝒫`. I.e., for every type `A` there is a type `LA ∈ 𝒫` equipped with a _unit
+map_
+
+```text
+  η : A → LA
+```
+
+satisfying the
+[universal property of localizations](orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses.md).
+This states that every type in `𝒫` is
+[local](orthogonal-factorization-systems.types-local-at-maps.md) at the unit
+`η`. As a consequence, the local types with respect to `L` are precisely the
+types in `𝒫`.
+
+## Definitions
+
+### The predicate on global subuniverses of being reflective
+
+```agda
+is-reflective-global-subuniverse :
+    {α : Level → Level} → (Level → Level) → global-subuniverse α → UUω
+is-reflective-global-subuniverse β 𝒫 =
+  {l : Level} (X : UU l) → localization-global-subuniverse 𝒫 (β l) X
+
+module _
+  {α β : Level → Level}
+  (𝒫 : global-subuniverse α)
+  (H : is-reflective-global-subuniverse β 𝒫)
+  where
+
+  reflection-is-reflective-global-subuniverse :
+    {l : Level} (X : UU l) → extension-type-global-subuniverse 𝒫 (β l) X
+  reflection-is-reflective-global-subuniverse X =
+    reflection-localization-global-subuniverse (H X)
+
+  type-reflection-is-reflective-global-subuniverse :
+    {l : Level} → UU l → UU (β l)
+  type-reflection-is-reflective-global-subuniverse X =
+    type-localization-global-subuniverse (H X)
+
+  is-in-global-subuniverse-type-reflection-is-reflective-global-subuniverse :
+    {l : Level} (X : UU l) →
+    is-in-global-subuniverse 𝒫
+      ( type-reflection-is-reflective-global-subuniverse X)
+  is-in-global-subuniverse-type-reflection-is-reflective-global-subuniverse X =
+    is-in-global-subuniverse-type-localization-global-subuniverse (H X)
+
+  unit-is-reflective-global-subuniverse :
+    {l : Level} (X : UU l) →
+    X → type-reflection-is-reflective-global-subuniverse X
+  unit-is-reflective-global-subuniverse X =
+    unit-localization-global-subuniverse (H X)
+
+  up-localization-is-reflective-global-subuniverse :
+    {l : Level} (X : UU l) →
+    universal-property-localization-global-subuniverse 𝒫 X
+      ( reflection-is-reflective-global-subuniverse X)
+  up-localization-is-reflective-global-subuniverse X =
+    up-localization-global-subuniverse (H X)
+```
+
+### Reflective global subuniverses
+
+```agda
+record
+  reflective-global-subuniverse (α β : Level → Level) : UUω
+  where
+
+  field
+    global-subuniverse-reflective-global-subuniverse :
+      global-subuniverse α
+
+    is-reflective-reflective-global-subuniverse :
+      is-reflective-global-subuniverse β
+        global-subuniverse-reflective-global-subuniverse
+```
+
+```agda
+  subuniverse-reflective-global-subuniverse : (l : Level) → subuniverse l (α l)
+  subuniverse-reflective-global-subuniverse =
+    subuniverse-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+
+  is-closed-under-equiv-reflective-global-subuniverse :
+    {l1 l2 : Level} →
+    is-closed-under-equiv-subuniverses α
+      subuniverse-reflective-global-subuniverse
+      l1
+      l2
+  is-closed-under-equiv-reflective-global-subuniverse =
+    is-closed-under-equiv-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+
+  is-in-reflective-global-subuniverse : {l : Level} → UU l → UU (α l)
+  is-in-reflective-global-subuniverse =
+    is-in-global-subuniverse global-subuniverse-reflective-global-subuniverse
+
+  is-prop-is-in-reflective-global-subuniverse :
+    {l : Level} (X : UU l) → is-prop (is-in-reflective-global-subuniverse X)
+  is-prop-is-in-reflective-global-subuniverse =
+    is-prop-is-in-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+
+  type-reflective-global-subuniverse : (l : Level) → UU (α l ⊔ lsuc l)
+  type-reflective-global-subuniverse =
+    type-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+
+  inclusion-reflective-global-subuniverse :
+    {l : Level} → type-reflective-global-subuniverse l → UU l
+  inclusion-reflective-global-subuniverse =
+    inclusion-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+
+  type-reflection-reflective-global-subuniverse :
+    {l : Level} → UU l → UU (β l)
+  type-reflection-reflective-global-subuniverse =
+    type-reflection-is-reflective-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+      is-reflective-reflective-global-subuniverse
+
+  is-in-global-subuniverse-type-reflection-reflective-global-subuniverse :
+    {l : Level} (X : UU l) →
+    is-in-reflective-global-subuniverse
+      ( type-reflection-reflective-global-subuniverse X)
+  is-in-global-subuniverse-type-reflection-reflective-global-subuniverse =
+    is-in-global-subuniverse-type-reflection-is-reflective-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+      is-reflective-reflective-global-subuniverse
+
+  reflection-reflective-global-subuniverse :
+      {l : Level} (X : UU l) →
+      extension-type-global-subuniverse
+        global-subuniverse-reflective-global-subuniverse
+        ( β l)
+        ( X)
+  reflection-reflective-global-subuniverse =
+    reflection-is-reflective-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+      is-reflective-reflective-global-subuniverse
+
+  unit-reflective-global-subuniverse :
+    {l : Level} (X : UU l) →
+    X → type-reflection-reflective-global-subuniverse X
+  unit-reflective-global-subuniverse =
+    unit-is-reflective-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+      is-reflective-reflective-global-subuniverse
+
+  up-localization-reflective-global-subuniverse :
+    {l : Level} (X : UU l) →
+    universal-property-localization-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+      ( X)
+      ( reflection-reflective-global-subuniverse X)
+  up-localization-reflective-global-subuniverse =
+    up-localization-is-reflective-global-subuniverse
+      global-subuniverse-reflective-global-subuniverse
+      is-reflective-reflective-global-subuniverse
+
+open reflective-global-subuniverse public
+```
+
+## Properties
+
+### A type is in a reflective subuniverse if and only if it is local at reflections
+
+```agda
+module _
+  {α β : Level → Level}
+  (𝒫 : reflective-global-subuniverse α β)
+  where
+
+  is-in-reflective-global-subuniverse-is-local-domain :
+    {l1 : Level} {A : UU l1} →
+    is-local (unit-reflective-global-subuniverse 𝒫 A) A →
+    is-in-reflective-global-subuniverse 𝒫 A
+  is-in-reflective-global-subuniverse-is-local-domain {A = A} =
+    is-in-global-subuniverse-is-local-type-universal-property-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( reflection-reflective-global-subuniverse 𝒫 A)
+      ( up-localization-reflective-global-subuniverse 𝒫 A)
+
+  is-in-reflective-global-subuniverse-is-local :
+    {l1 : Level} {A : UU l1} →
+    ( {l : Level} (X : UU l) →
+      is-local (unit-reflective-global-subuniverse 𝒫 X) A) →
+    is-in-reflective-global-subuniverse 𝒫 A
+  is-in-reflective-global-subuniverse-is-local {A = A} H =
+    is-in-reflective-global-subuniverse-is-local-domain (H A)
+```
+
+### A type `X` is in a reflective subuniverse if and only if the unit is an equivalence at `X`
+
+```agda
+module _
+  {α β : Level → Level}
+  (𝒫 : reflective-global-subuniverse α β)
+  {l : Level} {X : UU l}
+  where
+
+  is-in-reflective-global-subuniverse-is-equiv-unit :
+    is-equiv (unit-reflective-global-subuniverse 𝒫 X) →
+    is-in-reflective-global-subuniverse 𝒫 X
+  is-in-reflective-global-subuniverse-is-equiv-unit =
+    is-in-global-subuniverse-is-equiv-unit-universal-property-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( reflection-reflective-global-subuniverse 𝒫 X)
+      ( up-localization-reflective-global-subuniverse 𝒫 X)
+
+  is-equiv-unit-is-in-reflective-global-subuniverse :
+    is-in-reflective-global-subuniverse 𝒫 X →
+    is-equiv (unit-reflective-global-subuniverse 𝒫 X)
+  is-equiv-unit-is-in-reflective-global-subuniverse =
+    is-equiv-unit-is-in-global-subuniverse-universal-property-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( reflection-reflective-global-subuniverse 𝒫 X)
+      ( up-localization-reflective-global-subuniverse 𝒫 X)
+```
+
+### Reflective global subuniverses contain contractible types
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  where
+
+  is-in-reflective-global-subuniverse-unit :
+    is-in-reflective-global-subuniverse 𝒫 unit
+  is-in-reflective-global-subuniverse-unit =
+    is-in-global-subuniverse-has-localization-global-subuniverse-unit
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-reflective-reflective-global-subuniverse 𝒫 unit)
+
+  is-in-reflective-global-subuniverse-is-contr :
+    {l : Level} {A : UU l} →
+    is-contr A →
+    is-in-reflective-global-subuniverse 𝒫 A
+  is-in-reflective-global-subuniverse-is-contr {A = A} H =
+    is-in-global-subuniverse-has-localization-global-subuniverse-is-contr
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( H)
+      ( is-reflective-reflective-global-subuniverse 𝒫 A)
+```
+
+### Reflective global subuniverses are closed under dependent products
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  is-in-reflective-global-subuniverse-Π :
+    ((x : A) → is-in-reflective-global-subuniverse 𝒫 (B x)) →
+    is-in-reflective-global-subuniverse 𝒫 ((x : A) → B x)
+  is-in-reflective-global-subuniverse-Π H =
+    is-in-global-subuniverse-Π-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( H)
+      ( is-reflective-reflective-global-subuniverse 𝒫 ((x : A) → B x))
+```
+
+### Reflective global subuniverses are closed under exponentials
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  is-in-reflective-global-subuniverse-exponential :
+    is-in-reflective-global-subuniverse 𝒫 B →
+    is-in-reflective-global-subuniverse 𝒫 (A → B)
+  is-in-reflective-global-subuniverse-exponential H =
+    is-in-global-subuniverse-exponential-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( H)
+      ( is-reflective-reflective-global-subuniverse 𝒫 (A → B))
+```
+
+### Reflective global subuniverses are closed under pullbacks
+
+Consider a pullback square
+
+```text
+          q
+    C --------> B
+    | ⌟         |
+  p |           | g
+    ∨           ∨
+    A --------> X
+          f
+```
+
+then if `A`, `B` and `X` are in `𝒫`, then so is `C`.
+
+This is Proposition 5.1.19 in {{#cite Rij19}}.
+
+**Proof.** We have a commuting square
+
+```text
+                  - ∘ η
+       (LC → C) --------> (C → C)
+           |                 |
+           |                 |
+  cone-map |                 | cone-map
+           |                 |
+           ∨                 ∨
+      cone f g LC ····> cone f g C
+```
+
+where the bottom horizontal map is an equivalence by the assumptions that `A`,
+`B` and `X` are `𝒫`-local. The two vertical maps are equivalences by the
+assumption that `C` is a pullback and so the top map must be an equivalence as
+well.
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 l3 l4 : Level}
+  {𝒮 : cospan-diagram l1 l2 l3}
+  (c : pullback-cone 𝒮 l4)
+  where
+
+  is-in-reflective-global-subuniverse-pullback :
+    is-in-reflective-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) →
+    is-in-reflective-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) →
+    is-in-reflective-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) →
+    is-in-reflective-global-subuniverse 𝒫 (domain-pullback-cone 𝒮 c)
+  is-in-reflective-global-subuniverse-pullback =
+    is-in-global-subuniverse-pullback-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( c)
+      ( is-reflective-reflective-global-subuniverse 𝒫
+        ( domain-pullback-cone 𝒮 c))
+```
+
+### Reflective global subuniverses are closed under cartesian product types
+
+This is Corollary 5.1.20 in {{#cite Rij19}}.
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  is-in-reflective-global-subuniverse-cartesian-product :
+    is-in-reflective-global-subuniverse 𝒫 A →
+    is-in-reflective-global-subuniverse 𝒫 B →
+    is-in-reflective-global-subuniverse 𝒫 (A × B)
+  is-in-reflective-global-subuniverse-cartesian-product H K =
+    is-in-global-subuniverse-cartesian-product-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-in-reflective-global-subuniverse-unit 𝒫)
+      ( H)
+      ( K)
+      ( is-reflective-reflective-global-subuniverse 𝒫 (A × B))
+```
+
+### Reflective global subuniverses are closed under identity types
+
+This is Corollary 5.1.21 in {{#cite Rij19}}.
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l : Level} {A : UU l} (x y : A) (H : is-in-reflective-global-subuniverse 𝒫 A)
+  where
+
+  is-in-reflective-global-subuniverse-Id :
+    is-in-reflective-global-subuniverse 𝒫 (x ＝ y)
+  is-in-reflective-global-subuniverse-Id =
+    is-in-global-subuniverse-Id-localization-global-subuniverse
+      ( global-subuniverse-reflective-global-subuniverse 𝒫)
+      ( is-in-reflective-global-subuniverse-unit 𝒫)
+      ( H)
+      ( is-reflective-reflective-global-subuniverse 𝒫 (x ＝ y))
+```
+
+### Reflective global subuniverses are closed under types of equivalences
+
+If `A` and `B` are `𝒫`-types, then the type of equivalences `A ≃ B` is again a
+`𝒫`-type. While this would follow straightforwardly from the above result and
+univalence, we give a proof that is independent of the univalence axiom.
+
+This is Corollary 5.1.23 in {{#cite Rij19}} and Proposition 2.18 in
+{{#cite CORS20}}.
+
+```agda
+module _
+  {α β : Level → Level} (𝒫 : reflective-global-subuniverse α β)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  (H : is-in-reflective-global-subuniverse 𝒫 A)
+  (K : is-in-reflective-global-subuniverse 𝒫 B)
+  where
+
+  is-in-reflective-global-subuniverse-equiv :
+    is-in-reflective-global-subuniverse 𝒫 (A ≃ B)
+  is-in-reflective-global-subuniverse-equiv =
+    is-in-reflective-global-subuniverse-pullback 𝒫
+      pullback-cone-equiv
+      (is-in-reflective-global-subuniverse-cartesian-product 𝒫
+        ( is-in-reflective-global-subuniverse-exponential 𝒫 H)
+        ( is-in-reflective-global-subuniverse-exponential 𝒫 K))
+      (is-in-reflective-global-subuniverse-cartesian-product 𝒫
+        ( is-in-reflective-global-subuniverse-exponential 𝒫 K)
+        ( is-in-reflective-global-subuniverse-cartesian-product 𝒫
+          ( is-in-reflective-global-subuniverse-exponential 𝒫 H)
+          ( is-in-reflective-global-subuniverse-exponential 𝒫 H)))
+      ( is-in-reflective-global-subuniverse-unit 𝒫)
+```
+
+### Reflective global subuniverses are closed under sequential limits
+
+> This remains to be formalized.
+
+## See also
+
+- [Σ-closed reflective subuniverses](orthogonal-factorization-systems.sigma-closed-reflective-subuniverses.md)
+- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md)
+
+## References
+
+{{#bibliography}} {{#reference UF13}} {{#reference RSS20}} {{#reference Rij19}}
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 6b4c1b5c99..1ebbc9e3de 100644
--- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
@@ -9,6 +9,7 @@ module orthogonal-factorization-systems.types-local-at-maps where
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-maps
+open import foundation.commuting-triangles-of-maps
 open import foundation.contractible-maps
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
@@ -16,9 +17,11 @@ open import foundation.dependent-universal-property-equivalences
 open import foundation.empty-types
 open import foundation.equivalences
 open import foundation.families-of-equivalences
+open import foundation.fibers-of-maps
 open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.logical-equivalences
@@ -26,15 +29,19 @@ open import foundation.postcomposition-functions
 open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
 open import foundation.propositions
+open import foundation.retractions
 open import foundation.retracts-of-maps
 open import foundation.retracts-of-types
 open import foundation.sections
+open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-dependent-function-types
 open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
 open import foundation.universal-property-empty-type
 open import foundation.universal-property-equivalences
 open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.extensions-maps
 ```
 
 </details>
@@ -47,7 +54,7 @@ A dependent type `A` over `Y` is said to be
 [precomposition map](foundation-core.function-types.md)
 
 ```text
-  _∘ f : ((y : Y) → A y) → ((x : X) → A (f x))
+  - ∘ f : ((y : Y) → A y) → ((x : X) → A (f x))
 ```
 
 is an [equivalence](foundation-core.equivalences.md).
@@ -103,29 +110,66 @@ module _
 
 ## Properties
 
-### Locality distributes over Π-types
+### Every map has a unique extension along `i` if and only if `P` is `i`-local
 
 ```agda
 module _
-  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  {l : Level} (P : B → UU l)
   where
 
-  distributive-Π-is-local-dependent-type :
-    {l3 l4 : Level} {A : UU l3} (B : A → Y → UU l4) →
-    ((a : A) → is-local-dependent-type f (B a)) →
-    is-local-dependent-type f (λ x → (a : A) → B a x)
-  distributive-Π-is-local-dependent-type B f-loc =
-    is-equiv-map-equiv
-      ( ( equiv-swap-Π) ∘e
-        ( equiv-Π-equiv-family (λ a → precomp-Π f (B a) , (f-loc a))) ∘e
-        ( equiv-swap-Π))
+  equiv-fiber'-precomp-extension-dependent-type :
+    (f : (x : A) → P (i x)) →
+    fiber' (precomp-Π i P) f ≃ extension-dependent-type i P f
+  equiv-fiber'-precomp-extension-dependent-type f =
+    equiv-tot (λ g → equiv-funext {f = f} {g ∘ i})
+
+  equiv-fiber-precomp-extension-dependent-type :
+    (f : (x : A) → P (i x)) →
+    fiber (precomp-Π i P) f ≃ extension-dependent-type i P f
+  equiv-fiber-precomp-extension-dependent-type f =
+    ( equiv-fiber'-precomp-extension-dependent-type f) ∘e
+    ( equiv-fiber (precomp-Π i P) f)
+
+  equiv-is-contr-extension-dependent-type-is-local-dependent-type :
+    is-local-dependent-type i P ≃
+    ((f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f))
+  equiv-is-contr-extension-dependent-type-is-local-dependent-type =
+    ( equiv-Π-equiv-family
+      ( equiv-is-contr-equiv ∘ equiv-fiber-precomp-extension-dependent-type)) ∘e
+    ( equiv-is-contr-map-is-equiv (precomp-Π i P))
+
+  is-contr-extension-dependent-type-is-local-dependent-type :
+    is-local-dependent-type i P →
+    (f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f)
+  is-contr-extension-dependent-type-is-local-dependent-type =
+    map-equiv equiv-is-contr-extension-dependent-type-is-local-dependent-type
+
+  is-local-dependent-type-is-contr-extension-dependent-type :
+    ((f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f)) →
+    is-local-dependent-type i P
+  is-local-dependent-type-is-contr-extension-dependent-type =
+    map-inv-equiv
+      equiv-is-contr-extension-dependent-type-is-local-dependent-type
+```
 
-  distributive-Π-is-local :
-    {l3 l4 : Level} {A : UU l3} (B : A → UU l4) →
-    ((a : A) → is-local f (B a)) →
-    is-local f ((a : A) → B a)
-  distributive-Π-is-local B =
-    distributive-Π-is-local-dependent-type (λ a _ → B a)
+### Every map has a unique extension along `i` if and only if `P` is `i`-local
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  {l : Level} {C : UU l}
+  where
+
+  is-contr-extension-is-local :
+    is-local i C → (f : A → C) → is-contr (extension i f)
+  is-contr-extension-is-local =
+    is-contr-extension-dependent-type-is-local-dependent-type i (λ _ → C)
+
+  is-local-is-contr-extension :
+    ((f : A → C) → is-contr (extension i f)) → is-local i C
+  is-local-is-contr-extension =
+    is-local-dependent-type-is-contr-extension-dependent-type i (λ _ → C)
 ```
 
 ### Local types are closed under equivalences
@@ -185,7 +229,7 @@ module _
       ( refl-htpy)
 ```
 
-### Locality is preserved by homotopies
+### Locality is preserved by homotopies of functions
 
 ```agda
 module _
@@ -288,13 +332,29 @@ module _
   pr1 (is-equiv-is-local-domains' section-precomp-X is-local-Y) =
     section-is-local-domains' section-precomp-X is-local-Y
   pr2 (is-equiv-is-local-domains' section-precomp-X is-local-Y) =
-    retraction-section-precomp-domain f section-precomp-X
+    retraction-map-section-precomp f section-precomp-X
 
   is-equiv-is-local-domains : is-local f X → is-local f Y → is-equiv f
   is-equiv-is-local-domains is-local-X =
     is-equiv-is-local-domains' (pr1 is-local-X)
 ```
 
+### If `f` has a retraction and the codomain of `f` is `f`-local, then `f` is an equivalence
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
+  where
+
+  is-equiv-retraction-is-local-codomain :
+    retraction f → is-local f Y → is-equiv f
+  is-equiv-retraction-is-local-codomain r is-local-Y =
+    section-is-local-domains' f
+      ( section-precomp-retraction-map f r)
+      ( is-local-Y) ,
+    r
+```
+
 ### Propositions are `f`-local if `- ∘ f` has a converse
 
 ```agda
@@ -319,7 +379,7 @@ module _
     is-local-dependent-type-is-prop (λ _ → A) (λ _ → is-prop-A)
 ```
 
-### All type families are local at equivalences
+### All types are local at equivalences
 
 ```agda
 module _
@@ -370,6 +430,96 @@ is-contr-is-local A is-local-A =
     ( universal-property-empty' A)
 ```
 
+### The 3-for-2 property of local types
+
+Given a [commuting triangle](foundation-core.commuting-triangles-of-maps.md) of
+maps
+
+```text
+        f
+   X ------> Y
+    \       /
+   h \     / g
+      \   /
+       ∨ ∨
+        Z,
+```
+
+then if `A` is local at two of the maps then it is local at all three.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3} {A : UU l4}
+  {f : X → Y} {g : Y → Z}
+  where
+
+  is-local-comp : is-local g A → is-local f A → is-local (g ∘ f) A
+  is-local-comp G F = is-equiv-comp (precomp f A) (precomp g A) G F
+
+  is-local-left-map-triangle :
+    {h : X → Z} → coherence-triangle-maps h g f →
+    is-local g A → is-local f A → is-local h A
+  is-local-left-map-triangle {h} K =
+    is-equiv-left-map-triangle
+      ( precomp h A)
+      ( precomp f A)
+      ( precomp g A)
+      ( htpy-precomp K A)
+
+  is-local-right-factor :
+    is-local (g ∘ f) A → is-local g A → is-local f A
+  is-local-right-factor = is-equiv-left-factor (precomp f A) (precomp g A)
+
+  is-local-top-map-triangle :
+    {h : X → Z} → coherence-triangle-maps h g f →
+    is-local h A → is-local g A → is-local f A
+  is-local-top-map-triangle {h} K =
+    is-equiv-right-map-triangle
+      ( precomp h A)
+      ( precomp f A)
+      ( precomp g A)
+      ( htpy-precomp K A)
+
+  is-local-left-factor :
+    is-local f A → is-local (g ∘ f) A → is-local g A
+  is-local-left-factor = is-equiv-right-factor (precomp f A) (precomp g A)
+
+  is-local-right-map-triangle :
+    {h : X → Z} → coherence-triangle-maps h g f →
+    is-local f A → is-local h A → is-local g A
+  is-local-right-map-triangle {h} K =
+    is-equiv-top-map-triangle
+      ( precomp h A)
+      ( precomp f A)
+      ( precomp g A)
+      ( htpy-precomp K A)
+```
+
+### Locality distributes over Π-types
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
+  where
+
+  distributive-Π-is-local-dependent-type :
+    {l3 l4 : Level} {A : UU l3} (B : A → Y → UU l4) →
+    ((a : A) → is-local-dependent-type f (B a)) →
+    is-local-dependent-type f (λ x → (a : A) → B a x)
+  distributive-Π-is-local-dependent-type B f-loc =
+    is-equiv-map-equiv
+      ( ( equiv-swap-Π) ∘e
+        ( equiv-Π-equiv-family (λ a → precomp-Π f (B a) , (f-loc a))) ∘e
+        ( equiv-swap-Π))
+
+  distributive-Π-is-local :
+    {l3 l4 : Level} {A : UU l3} (B : A → UU l4) →
+    ((a : A) → is-local f (B a)) →
+    is-local f ((a : A) → B a)
+  distributive-Π-is-local B =
+    distributive-Π-is-local-dependent-type (λ a _ → B a)
+```
+
 ## See also
 
 - [Local maps](orthogonal-factorization-systems.maps-local-at-maps.md)
diff --git a/src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md
index d47b4396a1..a909c66dac 100644
--- a/src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md
@@ -21,7 +21,7 @@ A type `A` is said to be **separated** with respect to a map `f`, or
 **`f`-separated**, if its [identity types](foundation-core.identity-types.md)
 are [`f`-local](orthogonal-factorization-systems.types-local-at-maps.md).
 
-## Definition
+## Definitions
 
 ```agda
 module _
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
new file mode 100644
index 0000000000..a3c2143af4
--- /dev/null
+++ b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md
@@ -0,0 +1,527 @@
+# The universal property of localizations at global subuniverses
+
+```agda
+module orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.extensions-types
+open import foundation.extensions-types-global-subuniverses
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.global-subuniverses
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.precomposition-functions
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
+open import foundation.subuniverses
+open import foundation.unit-type
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.extensions-maps
+open import orthogonal-factorization-systems.types-local-at-maps
+```
+
+</details>
+
+## Idea
+
+Let `𝒫` be a [global subuniverse](foundation.global-subuniverses.md). Given a
+type `X` we say a type `LX` in `𝒫` [equipped](foundation.structure.md) with a
+unit map `η : X → LX` satisfies the
+{{#concept "universal property of localizations" Disambiguation="at a global universe of types" Agda=universal-property-localization-global-subuniverse}}
+if every type `Z` in `𝒫` is
+`η`-[local](orthogonal-factorization-systems.types-local-at-maps.md). I.e., the
+[precomposition map](foundation-core.function-types.md)
+
+```text
+  - ∘ η : (LX → Z) → (X → Z)
+```
+
+is an [equivalence](foundation-core.equivalences.md).
+
+## Definitions
+
+### The universal property of being a localization at a global subuniverse
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α)
+  (X : UU l1) (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  where
+
+  universal-property-localization-global-subuniverse-Level :
+    (l : Level) → UU (α l ⊔ l1 ⊔ l2 ⊔ lsuc l)
+  universal-property-localization-global-subuniverse-Level l =
+    (Z : type-global-subuniverse 𝒫 l) →
+    is-local
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+      ( inclusion-global-subuniverse 𝒫 Z)
+
+  universal-property-localization-global-subuniverse : UUω
+  universal-property-localization-global-subuniverse =
+    {l : Level} → universal-property-localization-global-subuniverse-Level l
+```
+
+### The recursion principle of localization at a global subuniverse
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α)
+  (X : UU l1) (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  where
+
+  recursion-principle-localization-global-subuniverse-Level :
+    (l : Level) → UU (α l ⊔ l1 ⊔ l2 ⊔ lsuc l)
+  recursion-principle-localization-global-subuniverse-Level l =
+    (Z : type-global-subuniverse 𝒫 l) →
+    section
+      ( precomp
+        ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+        ( inclusion-global-subuniverse 𝒫 Z))
+
+  recursion-principle-localization-global-subuniverse : UUω
+  recursion-principle-localization-global-subuniverse =
+    {l : Level} → recursion-principle-localization-global-subuniverse-Level l
+```
+
+## Properties
+
+### Equivalences satisfy the universal property of localizations
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α)
+  (X : UU l1) (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  where
+
+  universal-property-localization-global-subuniverse-is-equiv :
+    is-equiv (inclusion-extension-type-global-subuniverse 𝒫 LX) →
+    universal-property-localization-global-subuniverse 𝒫 X LX
+  universal-property-localization-global-subuniverse-is-equiv H Z =
+    is-local-is-equiv
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+      ( H)
+      ( inclusion-global-subuniverse 𝒫 Z)
+
+module _
+  {α : Level → Level} {l1 : Level} (𝒫 : global-subuniverse α)
+  (X : type-global-subuniverse 𝒫 l1)
+  where
+
+  universal-property-localization-global-subuniverse-id :
+    universal-property-localization-global-subuniverse 𝒫
+      ( inclusion-global-subuniverse 𝒫 X)
+      ( X , id)
+  universal-property-localization-global-subuniverse-id =
+    universal-property-localization-global-subuniverse-is-equiv 𝒫
+      ( inclusion-global-subuniverse 𝒫 X)
+      ( X , id)
+      ( is-equiv-id)
+```
+
+### Satisfying the universal property of localizations is a property
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α)
+  (X : UU l1) (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  where
+
+  is-prop-universal-property-localization-global-subuniverse-Level :
+    {l : Level} →
+    is-prop (universal-property-localization-global-subuniverse-Level 𝒫 X LX l)
+  is-prop-universal-property-localization-global-subuniverse-Level =
+    is-prop-Π
+      ( λ Z →
+        is-property-is-local
+          ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+          ( inclusion-global-subuniverse 𝒫 Z))
+```
+
+### Localizations are closed under equivalences
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α)
+  (X : UU l1) (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  (H : universal-property-localization-global-subuniverse 𝒫 X LX)
+  where
+
+  equiv-universal-property-localization-global-subuniverse :
+    {l3 : Level} {Y : UU l3}
+    (e : type-extension-type-global-subuniverse 𝒫 LX ≃ Y) →
+    universal-property-localization-global-subuniverse 𝒫 X
+      ( ( Y ,
+          is-closed-under-equiv-global-subuniverse 𝒫
+            ( type-extension-type-global-subuniverse 𝒫 LX)
+            ( Y)
+            ( e)
+            ( is-in-global-subuniverse-type-extension-type-global-subuniverse
+              ( 𝒫)
+              ( LX))) ,
+        ( map-equiv e ∘ inclusion-extension-type-global-subuniverse 𝒫 LX))
+  equiv-universal-property-localization-global-subuniverse e Z =
+    is-local-comp
+      ( is-local-is-equiv _
+        ( is-equiv-map-equiv e)
+        ( inclusion-global-subuniverse 𝒫 Z))
+      ( H Z)
+```
+
+### Localizations are maps with unique extensions
+
+The map `η : X → LX` satisfies the universal property of localizations with
+respect to `𝒫` if and only if every map `f : X → Z` where `Z` is in `𝒫` has a
+unique extension along `η`
+
+```text
+        f
+    X ----> Z
+    |      ∧
+  η |    ⋰
+    ∨  ⋰
+    LX.
+```
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α)
+  (X : UU l1) (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  where
+
+  forward-implication-iff-unique-extensions-universal-property-localization-global-subuniverse :
+    universal-property-localization-global-subuniverse 𝒫 X LX →
+    {l : Level} (Z : type-global-subuniverse 𝒫 l)
+    (f : X → inclusion-global-subuniverse 𝒫 Z) →
+    is-contr (extension (inclusion-extension-type-global-subuniverse 𝒫 LX) f)
+  forward-implication-iff-unique-extensions-universal-property-localization-global-subuniverse
+    H Z =
+    is-contr-extension-is-local
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+      ( H Z)
+
+  backward-implication-iff-unique-extensions-universal-property-localization-global-subuniverse :
+    ( {l : Level} (Z : type-global-subuniverse 𝒫 l)
+      (f : X → inclusion-global-subuniverse 𝒫 Z) →
+      is-contr
+        ( extension (inclusion-extension-type-global-subuniverse 𝒫 LX) f)) →
+    universal-property-localization-global-subuniverse 𝒫 X LX
+  backward-implication-iff-unique-extensions-universal-property-localization-global-subuniverse
+    H Z =
+    is-local-is-contr-extension
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+      ( H Z)
+```
+
+### Localizations are essentially unique
+
+This is Proposition 5.1.2 in {{#cite Rij19}}. We formalize essential uniqueness
+with equivalences of extensions of the type `X`, as the universal property is a
+large proposition.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 : Level} {X : UU l1}
+  (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  (LX' : extension-type-global-subuniverse 𝒫 l3 X)
+  (H : universal-property-localization-global-subuniverse 𝒫 X LX)
+  (H' : universal-property-localization-global-subuniverse 𝒫 X LX')
+  where
+
+  extension-map-essentially-unique-universal-property-localization-global-subuniverse :
+    extension
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX')
+  extension-map-essentially-unique-universal-property-localization-global-subuniverse =
+    center
+      ( forward-implication-iff-unique-extensions-universal-property-localization-global-subuniverse
+        ( 𝒫)
+        ( X)
+        ( LX)
+        ( H)
+        ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LX')
+        ( inclusion-extension-type-global-subuniverse 𝒫 LX'))
+
+  extension-map-inv-essentially-unique-universal-property-localization-global-subuniverse :
+    extension
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX')
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+  extension-map-inv-essentially-unique-universal-property-localization-global-subuniverse =
+    center
+      ( forward-implication-iff-unique-extensions-universal-property-localization-global-subuniverse
+        ( 𝒫)
+        ( X)
+        ( LX')
+        ( H')
+        ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LX)
+        ( inclusion-extension-type-global-subuniverse 𝒫 LX))
+
+  map-essentially-unique-universal-property-localization-global-subuniverse :
+    type-extension-type-global-subuniverse 𝒫 LX →
+    type-extension-type-global-subuniverse 𝒫 LX'
+  map-essentially-unique-universal-property-localization-global-subuniverse =
+    map-extension
+      extension-map-essentially-unique-universal-property-localization-global-subuniverse
+
+  map-inv-essentially-unique-universal-property-localization-global-subuniverse :
+    type-extension-type-global-subuniverse 𝒫 LX' →
+    type-extension-type-global-subuniverse 𝒫 LX
+  map-inv-essentially-unique-universal-property-localization-global-subuniverse =
+    map-extension
+      extension-map-inv-essentially-unique-universal-property-localization-global-subuniverse
+
+  abstract
+    is-section-map-inv-essentially-unique-universal-property-localization-global-subuniverse :
+      is-section
+        map-essentially-unique-universal-property-localization-global-subuniverse
+        map-inv-essentially-unique-universal-property-localization-global-subuniverse
+    is-section-map-inv-essentially-unique-universal-property-localization-global-subuniverse =
+      htpy-eq
+        ( ap
+          ( map-extension)
+          ( eq-is-contr
+            ( forward-implication-iff-unique-extensions-universal-property-localization-global-subuniverse
+              ( 𝒫)
+              ( X)
+              ( LX')
+              ( H')
+              ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LX')
+              ( inclusion-extension-type-global-subuniverse 𝒫 LX'))
+            { map-essentially-unique-universal-property-localization-global-subuniverse ∘
+              map-inv-essentially-unique-universal-property-localization-global-subuniverse ,
+              is-extension-comp-horizontal
+                { f = inclusion-extension-type-global-subuniverse 𝒫 LX'}
+                { inclusion-extension-type-global-subuniverse 𝒫 LX}
+                { inclusion-extension-type-global-subuniverse 𝒫 LX'}
+                { map-inv-essentially-unique-universal-property-localization-global-subuniverse}
+                { map-essentially-unique-universal-property-localization-global-subuniverse}
+                ( is-extension-map-extension
+                    extension-map-inv-essentially-unique-universal-property-localization-global-subuniverse)
+                ( is-extension-map-extension
+                    extension-map-essentially-unique-universal-property-localization-global-subuniverse)}
+            { extension-along-self
+              ( inclusion-extension-type-global-subuniverse 𝒫 LX')}))
+
+  abstract
+    is-retraction-map-inv-essentially-unique-universal-property-localization-global-subuniverse :
+      is-retraction
+        map-essentially-unique-universal-property-localization-global-subuniverse
+        map-inv-essentially-unique-universal-property-localization-global-subuniverse
+    is-retraction-map-inv-essentially-unique-universal-property-localization-global-subuniverse =
+      htpy-eq
+        ( ap
+          ( map-extension)
+          ( eq-is-contr
+            ( forward-implication-iff-unique-extensions-universal-property-localization-global-subuniverse
+              ( 𝒫)
+              ( X)
+              ( LX)
+              ( H)
+              ( type-global-subuniverse-extension-type-global-subuniverse 𝒫 LX)
+              ( inclusion-extension-type-global-subuniverse 𝒫 LX))
+            { map-inv-essentially-unique-universal-property-localization-global-subuniverse ∘
+              map-essentially-unique-universal-property-localization-global-subuniverse ,
+              is-extension-comp-horizontal
+                { f = inclusion-extension-type-global-subuniverse 𝒫 LX}
+                { inclusion-extension-type-global-subuniverse 𝒫 LX'}
+                { inclusion-extension-type-global-subuniverse 𝒫 LX}
+                { map-essentially-unique-universal-property-localization-global-subuniverse}
+                { map-inv-essentially-unique-universal-property-localization-global-subuniverse}
+                ( is-extension-map-extension
+                    extension-map-essentially-unique-universal-property-localization-global-subuniverse)
+                ( is-extension-map-extension
+                    extension-map-inv-essentially-unique-universal-property-localization-global-subuniverse)}
+            { extension-along-self
+              ( inclusion-extension-type-global-subuniverse 𝒫 LX)}))
+
+  is-equiv-map-essentially-unique-universal-property-localization-global-subuniverse :
+    is-equiv
+      map-essentially-unique-universal-property-localization-global-subuniverse
+  is-equiv-map-essentially-unique-universal-property-localization-global-subuniverse =
+    is-equiv-is-invertible
+      map-inv-essentially-unique-universal-property-localization-global-subuniverse
+      is-section-map-inv-essentially-unique-universal-property-localization-global-subuniverse
+      is-retraction-map-inv-essentially-unique-universal-property-localization-global-subuniverse
+
+  essentially-unique-type-universal-property-localization-global-subuniverse :
+    type-extension-type-global-subuniverse 𝒫 LX ≃
+    type-extension-type-global-subuniverse 𝒫 LX'
+  essentially-unique-type-universal-property-localization-global-subuniverse =
+    map-essentially-unique-universal-property-localization-global-subuniverse ,
+    is-equiv-map-essentially-unique-universal-property-localization-global-subuniverse
+
+  essentially-unique-extension-type-universal-property-localization-global-subuniverse :
+    equiv-extension-type-global-subuniverse 𝒫 LX LX'
+  essentially-unique-extension-type-universal-property-localization-global-subuniverse =
+    essentially-unique-type-universal-property-localization-global-subuniverse ,
+    is-extension-map-extension
+      extension-map-essentially-unique-universal-property-localization-global-subuniverse
+```
+
+### Localizations are unique
+
+We formalize uniqueness with equality of extensions of the type `X`, as the
+universal property, that after all is a proposition, is large.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 : Level} {X : UU l1}
+  (LX LX' : extension-type-global-subuniverse 𝒫 l2 X)
+  (H : universal-property-localization-global-subuniverse 𝒫 X LX)
+  (H' : universal-property-localization-global-subuniverse 𝒫 X LX')
+  where
+
+  unique-type-universal-property-localization-global-subuniverse :
+    type-extension-type-global-subuniverse 𝒫 LX ＝
+    type-extension-type-global-subuniverse 𝒫 LX'
+  unique-type-universal-property-localization-global-subuniverse =
+    eq-equiv
+      ( essentially-unique-type-universal-property-localization-global-subuniverse
+        ( 𝒫)
+        ( LX)
+        ( LX')
+        ( H)
+        ( H'))
+
+  unique-extension-type-universal-property-localization-global-subuniverse :
+    LX ＝ LX'
+  unique-extension-type-universal-property-localization-global-subuniverse =
+    eq-equiv-extension-type-global-subuniverse 𝒫 LX LX'
+      ( essentially-unique-extension-type-universal-property-localization-global-subuniverse
+        ( 𝒫)
+        ( LX)
+        ( LX')
+        ( H)
+        ( H'))
+```
+
+### Equivalent conditions for the unit of the localization being an equivalence
+
+Let `η : X → LX` be a localization of `X` at `𝒫`, then the following are
+logically equivalent conditions:
+
+1. The type `X` is contained in `𝒫`.
+2. The map `η` is an equivalence.
+3. The type `X` is local at `η`.
+4. The map `η` has a retraction.
+5. The precomposition map `- ∘ η` has a section at `X`.
+
+This is Proposition 5.1.3 in {{#cite Rij19}}.
+
+#### A type with a `𝒫`-localization is in `𝒫` if and only if the unit is an equivalence
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 : Level} {X : UU l1}
+  (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  (H : universal-property-localization-global-subuniverse 𝒫 X LX)
+  where
+
+  is-in-global-subuniverse-is-equiv-unit-universal-property-localization-global-subuniverse :
+    is-equiv (inclusion-extension-type-global-subuniverse 𝒫 LX) →
+    is-in-global-subuniverse 𝒫 X
+  is-in-global-subuniverse-is-equiv-unit-universal-property-localization-global-subuniverse
+    K =
+    is-closed-under-equiv-global-subuniverse 𝒫
+      ( type-extension-type-global-subuniverse 𝒫 LX)
+      ( X)
+      ( inv-equiv (inclusion-extension-type-global-subuniverse 𝒫 LX , K))
+      ( is-in-global-subuniverse-type-extension-type-global-subuniverse 𝒫 LX)
+
+  is-equiv-unit-is-in-global-subuniverse-universal-property-localization-global-subuniverse :
+    is-in-global-subuniverse 𝒫 X →
+    is-equiv (inclusion-extension-type-global-subuniverse 𝒫 LX)
+  is-equiv-unit-is-in-global-subuniverse-universal-property-localization-global-subuniverse
+    K =
+    is-equiv-inclusion-extension-type-equiv
+      ( extension-type-extension-type-global-subuniverse 𝒫 LX)
+      ( X , id)
+      ( essentially-unique-extension-type-universal-property-localization-global-subuniverse
+        ( 𝒫)
+        ( LX)
+        ( ( X , K) , id)
+        ( H)
+        ( universal-property-localization-global-subuniverse-id 𝒫 (X , K)))
+      ( is-equiv-id)
+```
+
+#### The unit of a `𝒫`-localization is an equivalence if and only if the type is local at the unit
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 : Level} {X : UU l1}
+  (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  (H : universal-property-localization-global-subuniverse 𝒫 X LX)
+  where
+
+  is-equiv-unit-is-local-type-universal-property-localization-global-subuniverse :
+    is-local (inclusion-extension-type-global-subuniverse 𝒫 LX) X →
+    is-equiv (inclusion-extension-type-global-subuniverse 𝒫 LX)
+  is-equiv-unit-is-local-type-universal-property-localization-global-subuniverse
+    K =
+    is-equiv-is-local-domains
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+      ( K)
+      ( H (type-global-subuniverse-extension-type-global-subuniverse 𝒫 LX))
+
+  is-local-type-is-equiv-unit-universal-property-localization-global-subuniverse :
+    is-equiv (inclusion-extension-type-global-subuniverse 𝒫 LX) →
+    is-local (inclusion-extension-type-global-subuniverse 𝒫 LX) X
+  is-local-type-is-equiv-unit-universal-property-localization-global-subuniverse
+    K =
+    H ( X ,
+        is-in-global-subuniverse-is-equiv-unit-universal-property-localization-global-subuniverse
+          𝒫 LX H K)
+
+  is-in-global-subuniverse-is-local-type-universal-property-localization-global-subuniverse :
+    is-local (inclusion-extension-type-global-subuniverse 𝒫 LX) X →
+    is-in-global-subuniverse 𝒫 X
+  is-in-global-subuniverse-is-local-type-universal-property-localization-global-subuniverse
+    K =
+    is-in-global-subuniverse-is-equiv-unit-universal-property-localization-global-subuniverse
+      ( 𝒫)
+      ( LX)
+      ( H)
+      ( is-equiv-unit-is-local-type-universal-property-localization-global-subuniverse
+        ( K))
+```
+
+#### The unit of a `𝒫`-localization is an equivalence if and only if it has a retraction
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 : Level} {X : UU l1}
+  (LX : extension-type-global-subuniverse 𝒫 l2 X)
+  (H : universal-property-localization-global-subuniverse 𝒫 X LX)
+  where
+
+  is-equiv-unit-retraction-universal-property-localization-global-subuniverse :
+    retraction (inclusion-extension-type-global-subuniverse 𝒫 LX) →
+    is-equiv (inclusion-extension-type-global-subuniverse 𝒫 LX)
+  is-equiv-unit-retraction-universal-property-localization-global-subuniverse
+    r =
+    is-equiv-retraction-is-local-codomain
+      ( inclusion-extension-type-global-subuniverse 𝒫 LX)
+      ( r)
+      ( H (type-global-subuniverse-extension-type-global-subuniverse 𝒫 LX))
+```
+
+## References
+
+{{#bibliography}}