From 6a4fd252a35c3b3f7a113c9ffc3808674b736b68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?=
 <vojtechstepancik@outlook.com>
Date: Mon, 18 Nov 2024 11:50:06 +0100
Subject: [PATCH 1/3] Fix building the website when a file has only chore
 commits (#1224)

#1223 was a chore PR which added a file. This exposed a bug in our Git
mdbook preprocessor, which filters out chore commits before generating
the "Created by" line.

Now if there are no non-chore commits touching a file, the file is
generated without "Created by".
---
 scripts/preprocessor_git_metadata.py | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/scripts/preprocessor_git_metadata.py b/scripts/preprocessor_git_metadata.py
index 4ae55ce744..0d2a4af12f 100644
--- a/scripts/preprocessor_git_metadata.py
+++ b/scripts/preprocessor_git_metadata.py
@@ -84,12 +84,14 @@ def get_author_element_for_file(filename, include_contributors, contributors):
             'HEAD', '--', filename
         ], capture_output=True, text=True, check=True).stdout.splitlines()
 
-        # Collect authors and sort by number of commits
-        author_names = [
-            author['displayName']
-            for author in sorted_authors_from_raw_shortlog_lines(raw_authors_git_output, contributors)
-        ]
-        attribution_text = f'<p><i>Content created by {format_multiple_authors_attribution(author_names)}.</i></p>'
+        # If all commits to a file are chore commits, then there are no authors
+        if raw_authors_git_output:
+          # Collect authors and sort by number of commits
+          author_names = [
+              author['displayName']
+              for author in sorted_authors_from_raw_shortlog_lines(raw_authors_git_output, contributors)
+          ]
+          attribution_text = f'<p><i>Content created by {format_multiple_authors_attribution(author_names)}.</i></p>'
 
     file_log_output = subprocess.run([
         'git', 'log',

From 5f454d3ae8cb5029bdc075b54cddb1945ab4e1d1 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 19 Nov 2024 18:05:21 +0100
Subject: [PATCH 2/3] Renamings and rewordings OFS (#1188)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

### Summary
- Implement a new naming scheme for files about local and separated
objects at localizations/subuniverses/maps, as discussed with Egbert
privately.
- Improve particular wordings in the OFS namespace.
- Add a partial converse to the lemma `is-trunc-Σ`, computes the fibers
of `map-Σ` and add some coherences between composition and `map-Σ`.
- Add some basic lemmas about local maps.
---
 .../contractible-types.lagda.md               |  18 +++
 ...unctoriality-dependent-pair-types.lagda.md |  95 ++++++++++++++-
 src/foundation-core/propositions.lagda.md     |  19 +++
 src/foundation-core/truncated-types.lagda.md  |  19 +++
 src/foundation.lagda.md                       |   2 +-
 src/foundation/continuations.lagda.md         |   2 +-
 src/foundation/contractible-types.lagda.md    |   8 +-
 .../double-negation-modality.lagda.md         |   4 +
 ...toriality-cartesian-product-types.lagda.md |   2 +-
 src/foundation/global-subuniverses.lagda.md   |  10 +-
 src/foundation/inhabited-types.lagda.md       |  24 ++++
 ...recomposition-dependent-functions.lagda.md |  37 ++++++
 .../precomposition-functions.lagda.md         |  34 ++++++
 ...amental-theorem-of-identity-types.lagda.md |   4 +-
 ... => separated-types-subuniverses.lagda.md} |   4 +-
 ...sal-property-dependent-pair-types.lagda.md |   7 ++
 ...property-family-of-fibers-of-maps.lagda.md |   7 +-
 src/orthogonal-factorization-systems.lagda.md |  12 +-
 .../continuation-modalities.lagda.md          |   2 +-
 .../extensions-of-maps.lagda.md               |   2 +-
 ... families-of-types-local-at-maps.lagda.md} |  16 +--
 .../fiberwise-orthogonal-maps.lagda.md        |   2 +-
 .../global-function-classes.lagda.md          |   5 +-
 .../higher-modalities.lagda.md                |  19 +--
 .../identity-modality.lagda.md                |   2 +-
 ...agda.md => localizations-at-maps.lagda.md} |  12 +-
 ...=> localizations-at-subuniverses.lagda.md} |  12 +-
 ...s.lagda.md => maps-local-at-maps.lagda.md} |  57 +++++++--
 .../null-maps.lagda.md                        |   4 +-
 .../null-types.lagda.md                       |   4 +-
 .../orthogonal-maps.lagda.md                  |   2 +-
 .../raise-modalities.lagda.md                 |   2 +-
 .../reflective-modalities.lagda.md            |   2 +-
 .../reflective-subuniverses.lagda.md          | 115 +++++++++---------
 .../sigma-closed-modalities.lagda.md          |   4 +-
 .../types-colocal-at-maps.lagda.md            |   4 +-
 ....lagda.md => types-local-at-maps.lagda.md} |  44 ++++---
 ...da.md => types-separated-at-maps.lagda.md} |   8 +-
 .../uniquely-eliminating-modalities.lagda.md  |   9 +-
 .../zero-modality.lagda.md                    |   2 +-
 40 files changed, 471 insertions(+), 166 deletions(-)
 rename src/foundation/{separated-types.lagda.md => separated-types-subuniverses.lagda.md} (94%)
 rename src/orthogonal-factorization-systems/{local-families-of-types.lagda.md => families-of-types-local-at-maps.lagda.md} (72%)
 rename src/orthogonal-factorization-systems/{localizations-maps.lagda.md => localizations-at-maps.lagda.md} (84%)
 rename src/orthogonal-factorization-systems/{localizations-subuniverses.lagda.md => localizations-at-subuniverses.lagda.md} (90%)
 rename src/orthogonal-factorization-systems/{local-maps.lagda.md => maps-local-at-maps.lagda.md} (68%)
 rename src/orthogonal-factorization-systems/{local-types.lagda.md => types-local-at-maps.lagda.md} (92%)
 rename src/orthogonal-factorization-systems/{separated-types.lagda.md => types-separated-at-maps.lagda.md} (75%)

diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md
index 5e457cbe84..8b303ff4dd 100644
--- a/src/foundation-core/contractible-types.lagda.md
+++ b/src/foundation-core/contractible-types.lagda.md
@@ -133,6 +133,24 @@ 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:
diff --git a/src/foundation-core/functoriality-dependent-pair-types.lagda.md b/src/foundation-core/functoriality-dependent-pair-types.lagda.md
index 37e73d4330..f3d941d326 100644
--- a/src/foundation-core/functoriality-dependent-pair-types.lagda.md
+++ b/src/foundation-core/functoriality-dependent-pair-types.lagda.md
@@ -7,8 +7,10 @@ module foundation-core.functoriality-dependent-pair-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
@@ -23,7 +25,7 @@ open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.retractions
 open import foundation-core.retracts-of-types
-open import foundation-core.transport-along-identifications
+open import foundation-core.sections
 ```
 
 </details>
@@ -307,6 +309,78 @@ module _
     is-equiv-fiber-map-Σ-map-base-fiber t
 ```
 
+### The fibers of `map-Σ`
+
+We compute the fibers of `map-Σ` first in terms of `fiber'` and then in terms of
+`fiber`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} (D : B → UU l4)
+  (f : A → B) (g : (x : A) → C x → D (f x)) (t : Σ B D)
+  where
+
+  fiber-map-Σ' : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  fiber-map-Σ' =
+    Σ (fiber' f (pr1 t)) (λ s → fiber' (g (pr1 s)) (tr D (pr2 s) (pr2 t)))
+
+  map-fiber-map-Σ' : fiber' (map-Σ D f g) t → fiber-map-Σ'
+  map-fiber-map-Σ' ((a , c) , refl) = (a , refl) , (c , refl)
+
+  map-inv-fiber-map-Σ' : fiber-map-Σ' → fiber' (map-Σ D f g) t
+  map-inv-fiber-map-Σ' ((a , p) , (c , q)) = ((a , c) , eq-pair-Σ p q)
+
+  abstract
+    is-section-map-inv-fiber-map-Σ' :
+      is-section map-fiber-map-Σ' map-inv-fiber-map-Σ'
+    is-section-map-inv-fiber-map-Σ' ((a , refl) , (c , refl)) = refl
+
+  abstract
+    is-retraction-map-inv-fiber-map-Σ' :
+      is-retraction map-fiber-map-Σ' map-inv-fiber-map-Σ'
+    is-retraction-map-inv-fiber-map-Σ' ((a , c) , refl) = refl
+
+  is-equiv-map-fiber-map-Σ' : is-equiv map-fiber-map-Σ'
+  is-equiv-map-fiber-map-Σ' =
+    is-equiv-is-invertible
+      map-inv-fiber-map-Σ'
+      is-section-map-inv-fiber-map-Σ'
+      is-retraction-map-inv-fiber-map-Σ'
+
+  compute-fiber-map-Σ' : fiber' (map-Σ D f g) t ≃ fiber-map-Σ'
+  compute-fiber-map-Σ' = (map-fiber-map-Σ' , is-equiv-map-fiber-map-Σ')
+
+  fiber-map-Σ : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  fiber-map-Σ =
+    Σ (fiber f (pr1 t)) (λ s → fiber (g (pr1 s)) (inv-tr D (pr2 s) (pr2 t)))
+
+  map-fiber-map-Σ : fiber (map-Σ D f g) t → fiber-map-Σ
+  map-fiber-map-Σ ((a , c) , refl) = (a , refl) , (c , refl)
+
+  map-inv-fiber-map-Σ : fiber-map-Σ → fiber (map-Σ D f g) t
+  map-inv-fiber-map-Σ ((a , refl) , c , refl) = ((a , c) , refl)
+
+  abstract
+    is-section-map-inv-fiber-map-Σ :
+      is-section map-fiber-map-Σ map-inv-fiber-map-Σ
+    is-section-map-inv-fiber-map-Σ ((a , refl) , (c , refl)) = refl
+
+  abstract
+    is-retraction-map-inv-fiber-map-Σ :
+      is-retraction map-fiber-map-Σ map-inv-fiber-map-Σ
+    is-retraction-map-inv-fiber-map-Σ ((a , c) , refl) = refl
+
+  is-equiv-map-fiber-map-Σ : is-equiv map-fiber-map-Σ
+  is-equiv-map-fiber-map-Σ =
+    is-equiv-is-invertible
+      map-inv-fiber-map-Σ
+      is-section-map-inv-fiber-map-Σ
+      is-retraction-map-inv-fiber-map-Σ
+
+  compute-fiber-map-Σ : fiber (map-Σ D f g) t ≃ fiber-map-Σ
+  compute-fiber-map-Σ = (map-fiber-map-Σ , is-equiv-map-fiber-map-Σ)
+```
+
 ### If `f : A → B` is a contractible map, then so is `map-Σ-map-base f C`
 
 ```agda
@@ -457,10 +531,27 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
   where
 
-  compute-map-Σ-id : map-Σ B id (λ x → id) ~ id
+  compute-map-Σ-id : map-Σ B id (λ _ → id) ~ id
   compute-map-Σ-id = refl-htpy
 ```
 
+### `map-Σ` preserves composition of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3}
+  {A' : A → UU l4} {B' : B → UU l5} {C' : C → UU l6}
+  {f : A → B} {f' : (x : A) → A' x → B' (f x)}
+  {g : B → C} {g' : (y : B) → B' y → C' (g y)}
+  where
+
+  preserves-comp-map-Σ :
+    map-Σ C' (g ∘ f) (λ x x' → g' (f x) (f' x x')) ~
+    map-Σ C' g g' ∘ map-Σ B' f f'
+  preserves-comp-map-Σ = refl-htpy
+```
+
 ### Computing the action on identifications of `tot`
 
 ```agda
diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md
index 041ce6881d..005680a831 100644
--- a/src/foundation-core/propositions.lagda.md
+++ b/src/foundation-core/propositions.lagda.md
@@ -183,6 +183,25 @@ pr2 (Σ-Prop P Q) =
     ( λ p → is-prop-type-Prop (Q p))
 ```
 
+### If `Σ A B` is a proposition and there is a section `(x : A) → B x` then `A` is a proposition
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (s : (x : A) → B x)
+  where
+
+  is-proof-irrelevant-base-is-proof-irrelevant-Σ' :
+    is-proof-irrelevant (Σ A B) → is-proof-irrelevant A
+  is-proof-irrelevant-base-is-proof-irrelevant-Σ' H a =
+    is-contr-base-is-contr-Σ' A B s (H (a , s a))
+
+  is-prop-base-is-prop-Σ' : is-prop (Σ A B) → is-prop A
+  is-prop-base-is-prop-Σ' H =
+    is-prop-is-proof-irrelevant
+      ( is-proof-irrelevant-base-is-proof-irrelevant-Σ'
+          ( is-proof-irrelevant-is-prop H))
+```
+
 ### Propositions are closed under cartesian product types
 
 ```agda
diff --git a/src/foundation-core/truncated-types.lagda.md b/src/foundation-core/truncated-types.lagda.md
index ef0e87f4a0..fb88b4c3df 100644
--- a/src/foundation-core/truncated-types.lagda.md
+++ b/src/foundation-core/truncated-types.lagda.md
@@ -7,6 +7,7 @@ module foundation-core.truncated-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
@@ -217,6 +218,24 @@ fiber-Truncated-Type A B f b =
   Σ-Truncated-Type A (λ a → Id-Truncated-Type' B (f a) b)
 ```
 
+### Truncatedness of the base of a truncated dependent sum
+
+```agda
+abstract
+  is-trunc-base-is-trunc-Σ' :
+    {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : A → UU l2} →
+    ((x : A) → B x) → is-trunc k (Σ A B) → is-trunc k A
+  is-trunc-base-is-trunc-Σ' {k = neg-two-𝕋} {A} {B} =
+    is-contr-base-is-contr-Σ' A B
+  is-trunc-base-is-trunc-Σ' {k = succ-𝕋 k} s is-trunc-ΣAB x y =
+    is-trunc-base-is-trunc-Σ'
+      ( apd s)
+      ( is-trunc-equiv' k
+        ( (x , s x) ＝ (y , s y))
+        ( equiv-pair-eq-Σ (x , s x) (y , s y))
+        ( is-trunc-ΣAB (x , s x) (y , s y)))
+```
+
 ### Products of truncated types are truncated
 
 ```agda
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 17148ba8de..dbf4204531 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -349,7 +349,7 @@ open import foundation.retractions public
 open import foundation.retracts-of-maps public
 open import foundation.retracts-of-types public
 open import foundation.sections public
-open import foundation.separated-types public
+open import foundation.separated-types-subuniverses public
 open import foundation.sequences public
 open import foundation.sequential-limits public
 open import foundation.set-presented-types public
diff --git a/src/foundation/continuations.lagda.md b/src/foundation/continuations.lagda.md
index 37edfe73e0..853df7969c 100644
--- a/src/foundation/continuations.lagda.md
+++ b/src/foundation/continuations.lagda.md
@@ -35,8 +35,8 @@ 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.local-types
 open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 ```
 
diff --git a/src/foundation/contractible-types.lagda.md b/src/foundation/contractible-types.lagda.md
index 21aa96f701..bfb117148d 100644
--- a/src/foundation/contractible-types.lagda.md
+++ b/src/foundation/contractible-types.lagda.md
@@ -157,11 +157,9 @@ module _
 
   is-contr-Σ-is-prop :
     ((x : A) → is-prop (B x)) → ((x : A) → B x → a ＝ x) → is-contr (Σ A B)
-  pr1 (is-contr-Σ-is-prop p f) = pair a b
-  pr2 (is-contr-Σ-is-prop p f) (pair x y) =
-    eq-type-subtype
-      ( λ x' → pair (B x') (p x'))
-      ( f x y)
+  pr1 (is-contr-Σ-is-prop p f) = a , b
+  pr2 (is-contr-Σ-is-prop p f) (x , y) =
+    eq-type-subtype (λ x' → B x' , p x') (f x y)
 ```
 
 ### The diagonal of contractible types
diff --git a/src/foundation/double-negation-modality.lagda.md b/src/foundation/double-negation-modality.lagda.md
index ab3e6ede25..a3158f9e97 100644
--- a/src/foundation/double-negation-modality.lagda.md
+++ b/src/foundation/double-negation-modality.lagda.md
@@ -16,10 +16,14 @@ open import foundation.propositions
 open import foundation.unit-type
 open import foundation.universe-levels
 
+open import foundation-core.function-types
+open import foundation-core.transport-along-identifications
+
 open import orthogonal-factorization-systems.continuation-modalities
 open import orthogonal-factorization-systems.large-lawvere-tierney-topologies
 open import orthogonal-factorization-systems.lawvere-tierney-topologies
 open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 ```
 
diff --git a/src/foundation/functoriality-cartesian-product-types.lagda.md b/src/foundation/functoriality-cartesian-product-types.lagda.md
index 429e7875e5..08be06910b 100644
--- a/src/foundation/functoriality-cartesian-product-types.lagda.md
+++ b/src/foundation/functoriality-cartesian-product-types.lagda.md
@@ -35,7 +35,7 @@ The **functorial action** of the
 `f : A → B` and `g : C → D` and returns a map
 
 ```text
-  f × g : A × B → C × D`
+  f × g : A × B → C × D
 ```
 
 between the cartesian product types. This functorial action is _bifunctorial_ in
diff --git a/src/foundation/global-subuniverses.lagda.md b/src/foundation/global-subuniverses.lagda.md
index 97fa1d116c..e000dc080e 100644
--- a/src/foundation/global-subuniverses.lagda.md
+++ b/src/foundation/global-subuniverses.lagda.md
@@ -116,7 +116,7 @@ module _
 
 ## Properties
 
-### Global subuniverses are closed under homogenous equivalences
+### Global subuniverses are closed under equivalences between types in a single universe
 
 This is true for any family of subuniverses indexed by universe levels.
 
@@ -126,14 +126,14 @@ module _
   {l : Level} {X Y : UU l}
   where
 
-  is-in-global-subuniverse-homogenous-equiv :
+  is-in-global-subuniverse-equiv-Level :
     X ≃ Y → is-in-global-subuniverse P X → is-in-global-subuniverse P Y
-  is-in-global-subuniverse-homogenous-equiv =
+  is-in-global-subuniverse-equiv-Level =
     is-in-subuniverse-equiv (subuniverse-global-subuniverse P l)
 
-  is-in-global-subuniverse-homogenous-equiv' :
+  is-in-global-subuniverse-equiv-Level' :
     X ≃ Y → is-in-global-subuniverse P Y → is-in-global-subuniverse P X
-  is-in-global-subuniverse-homogenous-equiv' =
+  is-in-global-subuniverse-equiv-Level' =
     is-in-subuniverse-equiv' (subuniverse-global-subuniverse P l)
 ```
 
diff --git a/src/foundation/inhabited-types.lagda.md b/src/foundation/inhabited-types.lagda.md
index 28e0da41c8..93682e4ba5 100644
--- a/src/foundation/inhabited-types.lagda.md
+++ b/src/foundation/inhabited-types.lagda.md
@@ -7,9 +7,11 @@ module foundation.inhabited-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.equality-dependent-function-types
+open import foundation.function-extensionality
 open import foundation.functoriality-propositional-truncation
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.propositional-truncations
@@ -18,6 +20,7 @@ open import foundation.univalence
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
+open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.propositions
 open import foundation-core.torsorial-type-families
@@ -220,6 +223,27 @@ is-contr-is-inhabited-is-prop {A = A} p h =
     ( λ a → a , eq-is-prop' p a)
 ```
 
+### Contractibility of the base of a 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 merely exists 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-Σ :
+      is-inhabited ((x : A) → B x) → is-contr (Σ A B) → is-contr A
+    is-contr-base-is-contr-Σ s is-contr-ΣAB =
+      rec-trunc-Prop
+        ( is-contr-Prop A)
+        ( λ s → is-contr-base-is-contr-Σ' A B s is-contr-ΣAB)
+        ( s)
+```
+
 ## See also
 
 - The notion of _nonempty types_ is treated in
diff --git a/src/foundation/precomposition-dependent-functions.lagda.md b/src/foundation/precomposition-dependent-functions.lagda.md
index 0e1b1294b1..b5156efa46 100644
--- a/src/foundation/precomposition-dependent-functions.lagda.md
+++ b/src/foundation/precomposition-dependent-functions.lagda.md
@@ -10,6 +10,7 @@ open import foundation-core.precomposition-dependent-functions public
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.dependent-universal-property-equivalences
 open import foundation.function-extensionality
 open import foundation.universe-levels
@@ -17,10 +18,12 @@ open import foundation.universe-levels
 open import foundation-core.commuting-squares-of-maps
 open import foundation-core.equivalences
 open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.truncated-maps
 open import foundation-core.truncation-levels
+open import foundation-core.type-theoretic-principle-of-choice
 ```
 
 </details>
@@ -120,3 +123,37 @@ is-trunc-map-succ-precomp-Π {k = k} {f = f} {C = C} H =
         ( funext (g ∘ f) (h ∘ f))
         ( H g h))
 ```
+
+### The dependent precomposition map at a dependent pair type
+
+Given a map `f : X → Y` and a family `B : (y : Y) → A y → 𝒰` we have a
+[commuting square](foundation-core.commuting-squares-of-maps.md)
+
+```text
+                                     precomp-Π f (λ y → Σ (A y) (B y))
+            ((y : Y) → Σ (A y) (B y)) -----------------------------> ((x : X) → Σ (A (f x)) (B (f x)))
+                       |                                                          |
+                     ~ |                                                          | ~
+                       ∨                                                          ∨
+  Σ (a : (y : Y) → A y) ((y : Y) → B y (a y)) --------> Σ (a : (x : X) → A (f x)) ((x : X) → B (f x) (a x)).
+                       map-Σ (precomp-Π f A) (λ a → precomp-Π f (λ y → B y (a y)))
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {X : UU l1} {Y : UU l2} {A : Y → UU l3} {B : (y : Y) → A y → UU l4}
+  {f : X → Y}
+  where
+
+  coherence-precomp-Π-Σ :
+    coherence-square-maps
+      ( precomp-Π f (λ y → Σ (A y) (B y)))
+      ( map-distributive-Π-Σ)
+      ( map-distributive-Π-Σ)
+      ( map-Σ
+        ( λ a → (x : X) → B (f x) (a x))
+        ( precomp-Π f A)
+        ( λ a → precomp-Π f (λ y → B y (a y))))
+  coherence-precomp-Π-Σ = refl-htpy
+```
diff --git a/src/foundation/precomposition-functions.lagda.md b/src/foundation/precomposition-functions.lagda.md
index 720c665b0e..b008165dea 100644
--- a/src/foundation/precomposition-functions.lagda.md
+++ b/src/foundation/precomposition-functions.lagda.md
@@ -26,6 +26,7 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.retractions
+open import foundation-core.type-theoretic-principle-of-choice
 ```
 
 </details>
@@ -213,3 +214,36 @@ module _
       ( precomp-Π f (eq-value g h))
       ( compute-htpy-eq-ap-precomp)
 ```
+
+### The precomposition map at a dependent pair type
+
+Given a map `f : X → Y` and a family `B : A → 𝒰` we have a
+[commuting square](foundation-core.commuting-squares-of-maps.md)
+
+```text
+                                precomp f (Σ A B)
+             (Y → Σ A B) ------------------------------> (X → Σ A B)
+                  |                                           |
+                ~ |                                           | ~
+                  ∨                                           ∨
+  Σ (a : Y → A) ((y : Y) → B (a y)) --------> Σ (a : X → A) ((x : X) → B (a x)).
+                  map-Σ (precomp f A) (λ a → precomp f (B ∘ a))
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {B : A → UU l4}
+  {f : X → Y}
+  where
+
+  coherence-precomp-Σ :
+    coherence-square-maps
+      ( precomp f (Σ A B))
+      ( map-distributive-Π-Σ)
+      ( map-distributive-Π-Σ)
+      ( map-Σ
+        ( λ a → (x : X) → B (a x))
+        ( precomp f A)
+        ( λ a → precomp-Π f (B ∘ a)))
+  coherence-precomp-Σ = coherence-precomp-Π-Σ
+```
diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
index e987a62d6e..14db96e387 100644
--- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
+++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
@@ -26,7 +26,7 @@ open import foundation.inhabited-types
 open import foundation.logical-equivalences
 open import foundation.maps-in-subuniverses
 open import foundation.propositional-truncations
-open import foundation.separated-types
+open import foundation.separated-types-subuniverses
 open import foundation.subuniverses
 open import foundation.surjective-maps
 open import foundation.truncated-maps
@@ -51,7 +51,7 @@ asserts that for any [subuniverse](foundation.subuniverses.md) `P`, and any
    i.e., a family of maps with [fibers](foundation-core.fibers-of-maps.md) in
    `P`.
 2. The [total space](foundation.dependent-pair-types.md) `Σ A B` is
-   [`P`-separated](foundation.separated-types.md), i.e., its
+   [`P`-separated](foundation.separated-types-subuniverses.md), i.e., its
    [identity types](foundation-core.identity-types.md) are in `P`.
 
 In other words, the extended fundamental theorem of
diff --git a/src/foundation/separated-types.lagda.md b/src/foundation/separated-types-subuniverses.lagda.md
similarity index 94%
rename from src/foundation/separated-types.lagda.md
rename to src/foundation/separated-types-subuniverses.lagda.md
index 205ee03495..cc812fa34d 100644
--- a/src/foundation/separated-types.lagda.md
+++ b/src/foundation/separated-types-subuniverses.lagda.md
@@ -1,7 +1,7 @@
-# Separated types
+# Types separated at subuniverses
 
 ```agda
-module foundation.separated-types where
+module foundation.separated-types-subuniverses where
 ```
 
 <details><summary>Imports</summary>
diff --git a/src/foundation/universal-property-dependent-pair-types.lagda.md b/src/foundation/universal-property-dependent-pair-types.lagda.md
index 1d5d970795..54b12615b2 100644
--- a/src/foundation/universal-property-dependent-pair-types.lagda.md
+++ b/src/foundation/universal-property-dependent-pair-types.lagda.md
@@ -15,6 +15,8 @@ open import foundation-core.equivalences
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
+open import foundation-core.retractions
+open import foundation-core.sections
 ```
 
 </details>
@@ -93,3 +95,8 @@ equiv-ev-pair³ {X = X} {Y = Y} {Z = Z} {U = U} {V = V} {W = W} =
     ( equiv-ev-pair)
     ( λ k → equiv-ev-pair²)
 ```
+
+## See also
+
+- For the universal mapping-into property of dependent pair types, see the
+  [type theoretic principle of choice](foundation-core.type-theoretic-principle-of-choice.md)
diff --git a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
index 36da197f0c..a9d2691df4 100644
--- a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
+++ b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
@@ -407,9 +407,10 @@ module _
 ### A type family `C` over `B` satisfies the universal property of the family of fibers of a map `f : A → B` if and only if the constant map `C b → (fiber f b → C b)` is an equivalence for every `b : B`
 
 In other words, the dependent type `C` is
-`f`-[local](orthogonal-factorization-systems.local-types.md) if its fiber over
-`b` is `fiber f b`-[null](orthogonal-factorization-systems.null-types.md) for
-every `b : B`.
+`f`-[local](orthogonal-factorization-systems.types-local-at-maps.md) if its
+fiber over `b` is
+`fiber f b`-[null](orthogonal-factorization-systems.null-types.md) for every
+`b : B`.
 
 This condition simplifies, for example, the proof that
 [connected maps](foundation.connected-maps.md) satisfy a dependent universal
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index fae641f0d6..b4d6443ccc 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -24,6 +24,7 @@ open import orthogonal-factorization-systems.factorization-operations-global-fun
 open import orthogonal-factorization-systems.factorizations-of-maps public
 open import orthogonal-factorization-systems.factorizations-of-maps-function-classes public
 open import orthogonal-factorization-systems.factorizations-of-maps-global-function-classes public
+open import orthogonal-factorization-systems.families-of-types-local-at-maps public
 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
@@ -37,12 +38,10 @@ 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.local-families-of-types public
-open import orthogonal-factorization-systems.local-maps public
-open import orthogonal-factorization-systems.local-types public
-open import orthogonal-factorization-systems.localizations-maps public
-open import orthogonal-factorization-systems.localizations-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
+open import orthogonal-factorization-systems.maps-local-at-maps public
 open import orthogonal-factorization-systems.mere-lifting-properties public
 open import orthogonal-factorization-systems.modal-induction public
 open import orthogonal-factorization-systems.modal-operators public
@@ -59,12 +58,13 @@ open import orthogonal-factorization-systems.raise-modalities 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
-open import orthogonal-factorization-systems.separated-types public
 open import orthogonal-factorization-systems.sigma-closed-modalities public
 open import orthogonal-factorization-systems.sigma-closed-reflective-modalities public
 open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses public
 open import orthogonal-factorization-systems.stable-orthogonal-factorization-systems public
 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.wide-function-classes public
 open import orthogonal-factorization-systems.wide-global-function-classes public
diff --git a/src/orthogonal-factorization-systems/continuation-modalities.lagda.md b/src/orthogonal-factorization-systems/continuation-modalities.lagda.md
index 5d116f266d..0ed70bca76 100644
--- a/src/orthogonal-factorization-systems/continuation-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/continuation-modalities.lagda.md
@@ -29,8 +29,8 @@ open import foundation.universal-property-equivalences
 open import foundation.universe-levels
 
 open import orthogonal-factorization-systems.large-lawvere-tierney-topologies
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 ```
 
diff --git a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
index 02e43793b1..1c04e75a4b 100644
--- a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
@@ -38,7 +38,7 @@ open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.torsorial-type-families
 
-open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
diff --git a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md b/src/orthogonal-factorization-systems/families-of-types-local-at-maps.lagda.md
similarity index 72%
rename from src/orthogonal-factorization-systems/local-families-of-types.lagda.md
rename to src/orthogonal-factorization-systems/families-of-types-local-at-maps.lagda.md
index eb8d398b33..0d79431a42 100644
--- a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md
+++ b/src/orthogonal-factorization-systems/families-of-types-local-at-maps.lagda.md
@@ -1,7 +1,7 @@
-# Local families of types
+# Families of types local at a map
 
 ```agda
-module orthogonal-factorization-systems.local-families-of-types where
+module orthogonal-factorization-systems.families-of-types-local-at-maps where
 ```
 
 <details><summary>Imports</summary>
@@ -13,8 +13,8 @@ open import foundation.precomposition-functions
 open import foundation.propositions
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.orthogonal-maps
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
@@ -22,8 +22,8 @@ open import orthogonal-factorization-systems.orthogonal-maps
 ## Idea
 
 A family of types `B : A → UU l` is said to be
-{{#concept "local" Disambiguation="family of types" Agda=is-local-family}} at
-`f : X → Y`, or **`f`-local**, if every
+{{#concept "local" Disambiguation="family of types at a map" Agda=is-local-family}}
+at a map `f : X → Y`, or **`f`-local**, if every
 [fiber](foundation-core.fibers-of-maps.md) is.
 
 ## Definition
@@ -54,6 +54,6 @@ This remains to be formalized.
 
 ## See also
 
-- [Local maps](orthogonal-factorization-systems.local-maps.md)
-- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md)
-- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md)
+- [Local maps](orthogonal-factorization-systems.maps-local-at-maps.md)
+- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md)
+- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md)
diff --git a/src/orthogonal-factorization-systems/fiberwise-orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/fiberwise-orthogonal-maps.lagda.md
index 0a17ec3748..2cc4966422 100644
--- a/src/orthogonal-factorization-systems/fiberwise-orthogonal-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/fiberwise-orthogonal-maps.lagda.md
@@ -45,10 +45,10 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import orthogonal-factorization-systems.lifting-structures-on-squares
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.null-maps
 open import orthogonal-factorization-systems.orthogonal-maps
 open import orthogonal-factorization-systems.pullback-hom
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
diff --git a/src/orthogonal-factorization-systems/global-function-classes.lagda.md b/src/orthogonal-factorization-systems/global-function-classes.lagda.md
index d400eeea18..b11fa84d13 100644
--- a/src/orthogonal-factorization-systems/global-function-classes.lagda.md
+++ b/src/orthogonal-factorization-systems/global-function-classes.lagda.md
@@ -26,9 +26,10 @@ open import orthogonal-factorization-systems.function-classes
 
 A **global function class** is a global [subtype](foundation.subtypes.md) of
 function types that is closed under composition with
-[equivalences](foundation-core.equivalences.md).
+[equivalences](foundation-core.equivalences.md) between types in arbitrary
+[universes](foundation.universe-levels.md).
 
-Note that composition with homogenous equivalences follows from
+Note that composition with equivalences within a single universe follows from
 [univalence](foundation.univalence.md), so this condition should hold for the
 correct universe polymorphic definition.
 
diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md
index ac69913f80..4ad1fb0f7c 100644
--- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md
@@ -33,22 +33,23 @@ open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 
 ## Idea
 
-A **higher modality** is a _higher mode of logic_ defined in terms of a monadic
+A {{#concept "higher modality" Disambiguation="on types" Agda=higher-modality}}
+is a _higher mode of logic_ defined in terms of an monadic
 [modal operator](orthogonal-factorization-systems.modal-operators.md) `○`
 satisfying a certain induction principle.
 
-The induction principle states that for every type `X` and family
-`P : ○ X → UU`, to define a dependent map `(x' : ○ X) → ○ (P x')` it suffices to
-define it on the image of the modal unit, i.e. `(x : X) → ○ (P (unit-○ x))`.
-Moreover, it satisfies a computation principle stating that when evaluating a
-map defined in this manner on the image of the modal unit, one recovers the
-defining map (propositionally).
+The induction principle states that for every type `X` and family `P : ○ X → 𝒰`,
+to define a dependent map `(x' : ○ X) → ○ (P x')` it suffices to define it on
+the image of the modal unit, i.e. `(x : X) → ○ (P (unit-○ x))`. Moreover, it
+satisfies a computation principle stating that when evaluating a map defined in
+this manner on the image of the modal unit, one recovers the defining map
+(propositionally).
 
 Lastly, higher modalities must also be **identity closed** in the sense that for
 every type `X` the identity types `(x' ＝ y')` are modal for all terms
 `x' y' : ○ X`. In other words, `○ X` is
-[`○`-separated](foundation.separated-types.md). Because of this, higher
-modalities in their most general form only make sense for
+[`○`-separated](foundation.separated-types-subuniverses.md). Because of this,
+(small) higher modalities in their most general form only make sense for
 [locally small modal operators](orthogonal-factorization-systems.locally-small-modal-operators.md).
 
 ## Definition
diff --git a/src/orthogonal-factorization-systems/identity-modality.lagda.md b/src/orthogonal-factorization-systems/identity-modality.lagda.md
index ddd8624de0..34bcadc7b1 100644
--- a/src/orthogonal-factorization-systems/identity-modality.lagda.md
+++ b/src/orthogonal-factorization-systems/identity-modality.lagda.md
@@ -11,8 +11,8 @@ open import foundation.equivalences
 open import foundation.function-types
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 ```
 
diff --git a/src/orthogonal-factorization-systems/localizations-maps.lagda.md b/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md
similarity index 84%
rename from src/orthogonal-factorization-systems/localizations-maps.lagda.md
rename to src/orthogonal-factorization-systems/localizations-at-maps.lagda.md
index 265f973ff8..1144d685d4 100644
--- a/src/orthogonal-factorization-systems/localizations-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md
@@ -1,7 +1,7 @@
 # Localizations at maps
 
 ```agda
-module orthogonal-factorization-systems.localizations-maps where
+module orthogonal-factorization-systems.localizations-at-maps where
 ```
 
 <details><summary>Imports</summary>
@@ -11,8 +11,8 @@ open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
-open import orthogonal-factorization-systems.localizations-subuniverses
+open import orthogonal-factorization-systems.localizations-at-subuniverses
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
@@ -21,9 +21,9 @@ open import orthogonal-factorization-systems.localizations-subuniverses
 
 Let `f` be a map of type `A → B` and let `X` be a type. The **localization** of
 `X` at `f`, or **`f`-localization**, is an
-`f`[-local](orthogonal-factorization-systems.local-types.md) type `Y` together
-with a map `η : X → Y` with the property that every type that is `f`-local is
-also `η`-local.
+`f`[-local](orthogonal-factorization-systems.types-local-at-maps.md) type `Y`
+together with a map `η : X → Y` with the property that every type that is
+`f`-local is also `η`-local.
 
 ## Definition
 
diff --git a/src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md b/src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md
similarity index 90%
rename from src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md
rename to src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md
index 9da1074c37..c12ced2306 100644
--- a/src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md
@@ -1,7 +1,7 @@
 # Localizations at subuniverses
 
 ```agda
-module orthogonal-factorization-systems.localizations-subuniverses where
+module orthogonal-factorization-systems.localizations-at-subuniverses where
 ```
 
 <details><summary>Imports</summary>
@@ -12,7 +12,7 @@ open import foundation.dependent-pair-types
 open import foundation.subuniverses
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
@@ -22,11 +22,11 @@ open import orthogonal-factorization-systems.local-types
 Let `P` be a [subuniverse](foundation.subuniverses.md). Given a type `X`, its
 **localization** at `P`, or **`P`-localization**, is a type `Y` in `P` and a map
 `η : X → Y` such that every type in `P` is
-`η`[-local](orthogonal-factorization-systems.local-types.md). I.e. for every `Z`
-in `P`, the [precomposition map](foundation-core.function-types.md)
+`η`[-local](orthogonal-factorization-systems.types-local-at-maps.md). I.e., for
+every `Z` in `P`, the [precomposition map](foundation-core.function-types.md)
 
 ```text
-  _∘ η : (Y → Z) → (X → Z)
+  - ∘ η : (Y → Z) → (X → Z)
 ```
 
 is an [equivalence](foundation-core.equivalences.md).
@@ -112,7 +112,7 @@ This is Proposition 5.1.2 in _Classifying Types_, and remains to be formalized.
 
 ## See also
 
-- [Localizations at maps](orthogonal-factorization-systems.localizations-maps.md)
+- [Localizations at maps](orthogonal-factorization-systems.localizations-at-maps.md)
 
 ## References
 
diff --git a/src/orthogonal-factorization-systems/local-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
similarity index 68%
rename from src/orthogonal-factorization-systems/local-maps.lagda.md
rename to src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
index f19c0c87ee..ac69503101 100644
--- a/src/orthogonal-factorization-systems/local-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
@@ -1,7 +1,7 @@
-# Local maps
+# Maps local at maps
 
 ```agda
-module orthogonal-factorization-systems.local-maps where
+module orthogonal-factorization-systems.maps-local-at-maps where
 ```
 
 <details><summary>Imports</summary>
@@ -19,20 +19,22 @@ open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.functoriality-fibers-of-maps
+open import foundation.global-subuniverses
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.postcomposition-functions
 open import foundation.precomposition-functions
 open import foundation.propositions
 open import foundation.pullbacks
+open import foundation.retracts-of-maps
 open import foundation.unit-type
 open import foundation.universal-property-family-of-fibers-of-maps
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-families-of-types
-open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.families-of-types-local-at-maps
 open import orthogonal-factorization-systems.orthogonal-maps
 open import orthogonal-factorization-systems.pullback-hom
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
@@ -44,10 +46,7 @@ A map `g : X → Y` is said to be
 `f : A → B`, or
 {{#concept "`f`-local" Disambiguation="maps of types" Agda=is-local-map}}, if
 all its [fibers](foundation-core.fibers-of-maps.md) are
-[`f`-local types](orthogonal-factorization-systems.local-types.md).
-
-Equivalently, the map `g` is `f`-local if and only if `f` is
-[orthogonal](orthogonal-factorization-systems.orthogonal-maps.md) to `g`.
+[`f`-local types](orthogonal-factorization-systems.types-local-at-maps.md).
 
 ## Definition
 
@@ -86,7 +85,7 @@ module _
     is-local-equiv f (equiv-fiber-terminal-map u) H
 ```
 
-### A map is `f`-local if and only if it is `f`-orthogonal
+### A map is `f`-local if it is `f`-orthogonal
 
 ```agda
 module _
@@ -112,9 +111,43 @@ module _
         ( G))
 ```
 
-The converse remains to be formalized.
+### `f`-local maps are closed under base change
+
+Maps local at `f` are closed under base change.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  {f : A → B} {g : C → D} {g' : E → F}
+  where
+
+  is-local-map-base-change :
+    is-local-map f g → cartesian-hom-arrow g' g → is-local-map f g'
+  is-local-map-base-change G α d =
+    is-local-equiv f
+      ( equiv-fibers-cartesian-hom-arrow g' g α d)
+      ( G (map-codomain-cartesian-hom-arrow g' g α d))
+```
+
+### `f`-local maps are closed under retracts
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  {f : A → B} {g : C → D} {g' : E → F}
+  where
+
+  is-local-retract-map :
+    is-local-map f g → g' retract-of-map g → is-local-map f g'
+  is-local-retract-map G R d =
+    is-local-retract
+      ( retract-fiber-retract-map g' g R d)
+      ( G (map-codomain-inclusion-retract-map g' g R d))
+```
 
 ## See also
 
-- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md)
-- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md)
+- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md)
+- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md)
diff --git a/src/orthogonal-factorization-systems/null-maps.lagda.md b/src/orthogonal-factorization-systems/null-maps.lagda.md
index 2863c0ff12..af001e1fc2 100644
--- a/src/orthogonal-factorization-systems/null-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/null-maps.lagda.md
@@ -30,11 +30,11 @@ open import foundation.unit-type
 open import foundation.universal-property-family-of-fibers-of-maps
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-maps
-open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.maps-local-at-maps
 open import orthogonal-factorization-systems.null-families-of-types
 open import orthogonal-factorization-systems.null-types
 open import orthogonal-factorization-systems.orthogonal-maps
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md
index 575cbff8c7..4a8aa80c7b 100644
--- a/src/orthogonal-factorization-systems/null-types.lagda.md
+++ b/src/orthogonal-factorization-systems/null-types.lagda.md
@@ -30,9 +30,9 @@ open import foundation.universal-property-family-of-fibers-of-maps
 open import foundation.universal-property-unit-type
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-maps
-open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.maps-local-at-maps
 open import orthogonal-factorization-systems.orthogonal-maps
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
index 38071154f6..bec501ea4d 100644
--- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
@@ -49,8 +49,8 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import orthogonal-factorization-systems.lifting-structures-on-squares
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.pullback-hom
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
diff --git a/src/orthogonal-factorization-systems/raise-modalities.lagda.md b/src/orthogonal-factorization-systems/raise-modalities.lagda.md
index 2b0597b2fa..1f7569b41d 100644
--- a/src/orthogonal-factorization-systems/raise-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/raise-modalities.lagda.md
@@ -11,8 +11,8 @@ open import foundation.function-types
 open import foundation.raising-universe-levels
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 ```
 
diff --git a/src/orthogonal-factorization-systems/reflective-modalities.lagda.md b/src/orthogonal-factorization-systems/reflective-modalities.lagda.md
index c071673c5f..46c235675f 100644
--- a/src/orthogonal-factorization-systems/reflective-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/reflective-modalities.lagda.md
@@ -40,4 +40,4 @@ reflective-modality l =
 
 ## See also
 
-- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md)
+- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md)
diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
index a4fed1c61f..41a30148b0 100644
--- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
@@ -19,25 +19,28 @@ open import foundation.retractions
 open import foundation.subuniverses
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
-open import orthogonal-factorization-systems.localizations-subuniverses
+open import orthogonal-factorization-systems.localizations-at-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
 ```
 
 </details>
 
 ## Idea
 
-A {{#concept "reflective subuniverse" Agda=reflective-subuniverse}} is a
-[subuniverse](foundation.subuniverses.md) `P` together with a reflecting
-operator `L : 𝒰 → 𝒰` that take values in `P`, and a
-[unit](orthogonal-factorization-systems.modal-operators.md) `A → L A` for all
-types `A` in `𝒰`, with the property that the types in `P` are
-[local](orthogonal-factorization-systems.local-types.md) at the unit for every
-`A`. Hence the local types with respect to `L` are precisely the types in the
-reflective subuniverse.
+A
+{{#concept "reflective subuniverse" Disambiguation="of types" Agda=reflective-subuniverse}},
+or
+{{#concept "localization" Disambiguation="subuniverse" Agda=reflective-subuniverse}},
+is a [subuniverse](foundation.subuniverses.md) `𝒫` together with a reflecting
+operator on the [universe](foundation.universe-levels.md) `L : 𝒰 → 𝒰` that takes
+values in `𝒫`, and a family of unit maps `η : A → LA` for all types `A` in `𝒰`,
+with the property that the types in `𝒫` are
+[local](orthogonal-factorization-systems.types-local-at-maps.md) at the unit for
+every `A`. Hence the local types with respect to `L` are precisely the types in
+the reflective subuniverse.
 
 ## Definitions
 
@@ -45,41 +48,41 @@ reflective subuniverse.
 
 ```agda
 is-reflective-subuniverse :
-  {l1 l2 : Level} (P : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2)
-is-reflective-subuniverse {l1} P =
+  {l1 l2 : Level} (𝒫 : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2)
+is-reflective-subuniverse {l1} 𝒫 =
   Σ ( operator-modality l1 l1)
     ( λ L →
       Σ ( unit-modality L)
-        ( λ unit-L →
-          ( (X : UU l1) → is-in-subuniverse P (L X)) ×
-          ( (X Y : UU l1) → is-in-subuniverse P X → is-local (unit-L {Y}) X)))
+        ( λ η →
+          ( (X : UU l1) → is-in-subuniverse 𝒫 (L X)) ×
+          ( (X Y : UU l1) → is-in-subuniverse 𝒫 X → is-local (η {Y}) X)))
 ```
 
 ```agda
 module _
-  {l1 l2 : Level} (P : subuniverse l1 l2)
-  (is-reflective-P : is-reflective-subuniverse P)
+  {l1 l2 : Level} (𝒫 : subuniverse l1 l2)
+  (is-reflective-𝒫 : is-reflective-subuniverse 𝒫)
   where
 
   operator-is-reflective-subuniverse : operator-modality l1 l1
-  operator-is-reflective-subuniverse = pr1 is-reflective-P
+  operator-is-reflective-subuniverse = pr1 is-reflective-𝒫
 
   unit-is-reflective-subuniverse :
     unit-modality (operator-is-reflective-subuniverse)
-  unit-is-reflective-subuniverse = pr1 (pr2 is-reflective-P)
+  unit-is-reflective-subuniverse = pr1 (pr2 is-reflective-𝒫)
 
   is-in-subuniverse-operator-type-is-reflective-subuniverse :
     (X : UU l1) →
-    is-in-subuniverse P (operator-is-reflective-subuniverse X)
+    is-in-subuniverse 𝒫 (operator-is-reflective-subuniverse X)
   is-in-subuniverse-operator-type-is-reflective-subuniverse =
-    pr1 (pr2 (pr2 is-reflective-P))
+    pr1 (pr2 (pr2 is-reflective-𝒫))
 
   is-local-is-in-subuniverse-is-reflective-subuniverse :
     (X Y : UU l1) →
-    is-in-subuniverse P X →
+    is-in-subuniverse 𝒫 X →
     is-local (unit-is-reflective-subuniverse {Y}) X
   is-local-is-in-subuniverse-is-reflective-subuniverse =
-    pr2 (pr2 (pr2 is-reflective-P))
+    pr2 (pr2 (pr2 is-reflective-𝒫))
 ```
 
 ### The type of reflective subuniverses
@@ -92,11 +95,11 @@ reflective-subuniverse l1 l2 =
 
 ```agda
 module _
-  {l1 l2 : Level} (P : reflective-subuniverse l1 l2)
+  {l1 l2 : Level} (𝒫 : reflective-subuniverse l1 l2)
   where
 
   subuniverse-reflective-subuniverse : subuniverse l1 l2
-  subuniverse-reflective-subuniverse = pr1 P
+  subuniverse-reflective-subuniverse = pr1 𝒫
 
   is-in-reflective-subuniverse : UU l1 → UU l2
   is-in-reflective-subuniverse =
@@ -109,7 +112,7 @@ module _
 
   is-reflective-subuniverse-reflective-subuniverse :
     is-reflective-subuniverse (subuniverse-reflective-subuniverse)
-  is-reflective-subuniverse-reflective-subuniverse = pr2 P
+  is-reflective-subuniverse-reflective-subuniverse = pr2 𝒫
 
   operator-reflective-subuniverse : operator-modality l1 l1
   operator-reflective-subuniverse =
@@ -150,94 +153,94 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (P : subuniverse l1 l2)
-  (is-reflective-P : is-reflective-subuniverse P)
+  {l1 l2 : Level} (𝒫 : subuniverse l1 l2)
+  (is-reflective-𝒫 : is-reflective-subuniverse 𝒫)
   where
 
   has-all-localizations-is-reflective-subuniverse :
-    (A : UU l1) → subuniverse-localization P A
+    (A : UU l1) → subuniverse-localization 𝒫 A
   pr1 (has-all-localizations-is-reflective-subuniverse A) =
-    operator-is-reflective-subuniverse P is-reflective-P A
+    operator-is-reflective-subuniverse 𝒫 is-reflective-𝒫 A
   pr1 (pr2 (has-all-localizations-is-reflective-subuniverse A)) =
     is-in-subuniverse-operator-type-is-reflective-subuniverse
-      P is-reflective-P A
+      𝒫 is-reflective-𝒫 A
   pr1 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) =
-    unit-is-reflective-subuniverse P is-reflective-P
+    unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫
   pr2 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A)))
     X is-in-subuniverse-X =
       is-local-is-in-subuniverse-is-reflective-subuniverse
-        P is-reflective-P X A is-in-subuniverse-X
+        𝒫 is-reflective-𝒫 X A is-in-subuniverse-X
 
 module _
-  {l1 l2 : Level} (P : subuniverse l1 l2)
-  (L : (A : UU l1) → subuniverse-localization P A)
+  {l1 l2 : Level} (𝒫 : subuniverse l1 l2)
+  (L : (A : UU l1) → subuniverse-localization 𝒫 A)
   where
 
   is-reflective-has-all-localizations-subuniverse :
-    is-reflective-subuniverse P
+    is-reflective-subuniverse 𝒫
   pr1 is-reflective-has-all-localizations-subuniverse A =
-    type-subuniverse-localization P (L A)
+    type-subuniverse-localization 𝒫 (L A)
   pr1 (pr2 is-reflective-has-all-localizations-subuniverse) {A} =
-    unit-subuniverse-localization P (L A)
+    unit-subuniverse-localization 𝒫 (L A)
   pr1 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse)) A =
-    is-in-subuniverse-subuniverse-localization P (L A)
+    is-in-subuniverse-subuniverse-localization 𝒫 (L A)
   pr2 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse))
     A B is-in-subuniverse-A =
     is-local-at-unit-is-in-subuniverse-subuniverse-localization
-      P (L B) A is-in-subuniverse-A
+      𝒫 (L B) A is-in-subuniverse-A
 ```
 
 ## Recursion for reflective subuniverses
 
 ```agda
 module _
-  {l1 l2 : Level} (P : subuniverse l1 l2)
-  (is-reflective-P : is-reflective-subuniverse P)
+  {l1 l2 : Level} (𝒫 : subuniverse l1 l2)
+  (is-reflective-𝒫 : is-reflective-subuniverse 𝒫)
   where
 
   rec-modality-is-reflective-subuniverse :
-    rec-modality (unit-is-reflective-subuniverse P is-reflective-P)
+    rec-modality (unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫)
   rec-modality-is-reflective-subuniverse {X} {Y} =
     map-inv-is-equiv
       ( is-local-is-in-subuniverse-is-reflective-subuniverse
-        ( P)
-        ( is-reflective-P)
-        ( operator-is-reflective-subuniverse P is-reflective-P Y)
+        ( 𝒫)
+        ( is-reflective-𝒫)
+        ( operator-is-reflective-subuniverse 𝒫 is-reflective-𝒫 Y)
         ( X)
         ( is-in-subuniverse-operator-type-is-reflective-subuniverse
-          ( P)
-          ( is-reflective-P)
+          ( 𝒫)
+          ( is-reflective-𝒫)
           ( Y)))
 
   map-is-reflective-subuniverse :
     {X Y : UU l1} → (X → Y) →
-    operator-is-reflective-subuniverse P is-reflective-P X →
-    operator-is-reflective-subuniverse P is-reflective-P Y
+    operator-is-reflective-subuniverse 𝒫 is-reflective-𝒫 X →
+    operator-is-reflective-subuniverse 𝒫 is-reflective-𝒫 Y
   map-is-reflective-subuniverse =
     ap-map-rec-modality
-      ( unit-is-reflective-subuniverse P is-reflective-P)
+      ( unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫)
       ( rec-modality-is-reflective-subuniverse)
 
   strong-rec-subuniverse-is-reflective-subuniverse :
     strong-rec-subuniverse-modality
-      ( unit-is-reflective-subuniverse P is-reflective-P)
+      ( unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫)
   strong-rec-subuniverse-is-reflective-subuniverse =
     strong-rec-subuniverse-rec-modality
-      ( unit-is-reflective-subuniverse P is-reflective-P)
+      ( unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫)
       ( rec-modality-is-reflective-subuniverse)
 
   rec-subuniverse-is-reflective-subuniverse :
-    rec-subuniverse-modality (unit-is-reflective-subuniverse P is-reflective-P)
+    rec-subuniverse-modality (unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫)
   rec-subuniverse-is-reflective-subuniverse =
     rec-subuniverse-rec-modality
-      ( unit-is-reflective-subuniverse P is-reflective-P)
+      ( unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫)
       ( rec-modality-is-reflective-subuniverse)
 ```
 
 ## See also
 
 - [Σ-closed reflective subuniverses](orthogonal-factorization-systems.sigma-closed-reflective-subuniverses.md)
-- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md)
+- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md)
 
 ## References
 
diff --git a/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md b/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md
index efb9bfd560..20370cd516 100644
--- a/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md
@@ -21,8 +21,8 @@ open import orthogonal-factorization-systems.modal-operators
 
 A [modal operator](orthogonal-factorization-systems.modal-operators.md) with
 unit is **Σ-closed** if its [subuniverse](foundation.subuniverses.md) of modal
-types is [Σ-closed](foundation.sigma-closed-subuniverses.md). I.e. if `Σ A B` is
-modal whenever `B` is a family of modal types over modal base `A`.
+types is [Σ-closed](foundation.sigma-closed-subuniverses.md). I.e., if `Σ A B`
+is modal whenever `B` is a family of modal types over modal base `A`.
 
 ## Definition
 
diff --git a/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md
index e474f0d6af..7292a82aa0 100644
--- a/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md
@@ -57,8 +57,8 @@ Equivalently, `A` is colocal if
    `f`.
 
 The notion of `f`-colocal types is dual to
-[`f`-local types](orthogonal-factorization-systems.local-types.md), which is a
-type such that the
+[`f`-local types](orthogonal-factorization-systems.types-local-at-maps.md),
+which is a type such that the
 [precomposition map](foundation-core.precomposition-functions.md)
 
 ```text
diff --git a/src/orthogonal-factorization-systems/local-types.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
similarity index 92%
rename from src/orthogonal-factorization-systems/local-types.lagda.md
rename to src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
index 0f957651be..6b4c1b5c99 100644
--- a/src/orthogonal-factorization-systems/local-types.lagda.md
+++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
@@ -1,7 +1,7 @@
-# Local types
+# Types local at maps
 
 ```agda
-module orthogonal-factorization-systems.local-types where
+module orthogonal-factorization-systems.types-local-at-maps where
 ```
 
 <details><summary>Imports</summary>
@@ -56,7 +56,7 @@ We reserve the name `is-local` for when `A` does not vary over `Y`, and specify
 with `is-local-dependent-type` when it does.
 
 Note that a local dependent type is not the same as a
-[local family](orthogonal-factorization-systems.local-families-of-types.md).
+[local family](orthogonal-factorization-systems.families-of-types-local-at-maps.md).
 While a local family is a type family `P` on some other indexing type `A`, such
 that each fiber is local as a nondependent type over `Y`, a local dependent type
 is a local type that additionally may vary over `Y`. Concretely, a local
@@ -165,6 +165,26 @@ module _
   is-local-inv-equiv e = is-local-dependent-type-inv-fam-equiv f (λ _ → e)
 ```
 
+### Local types are closed under retracts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4}
+  {f : X → Y}
+  where
+
+  is-local-retract : A retract-of B → is-local f B → is-local f A
+  is-local-retract R =
+    is-equiv-retract-map-is-equiv'
+      ( precomp f A)
+      ( precomp f B)
+      ( retract-postcomp Y R)
+      ( retract-postcomp X R)
+      ( refl-htpy)
+      ( refl-htpy)
+```
+
 ### Locality is preserved by homotopies
 
 ```agda
@@ -275,7 +295,7 @@ module _
     is-equiv-is-local-domains' (pr1 is-local-X)
 ```
 
-### Propositions are `f`-local if `_∘ f` has a converse
+### Propositions are `f`-local if `- ∘ f` has a converse
 
 ```agda
 module _
@@ -344,20 +364,14 @@ module _
 is-contr-is-local :
   {l : Level} (A : UU l) → is-local (λ (_ : empty) → star) A → is-contr A
 is-contr-is-local A is-local-A =
-  is-contr-is-equiv
+  is-contr-equiv
     ( empty → A)
-    ( λ a _ → a)
-    ( is-equiv-comp
-      ( λ a' _ → a' star)
-      ( λ a _ →
-        map-inv-is-equiv (is-equiv-map-left-unit-law-Π (λ _ → A)) a star)
-      ( is-equiv-map-inv-is-equiv (is-equiv-map-left-unit-law-Π (λ _ → A)))
-      ( is-local-A))
+    ( (precomp (λ _ → star) A , is-local-A) ∘e inv-left-unit-law-Π (λ _ → A))
     ( universal-property-empty' A)
 ```
 
 ## See also
 
-- [Local maps](orthogonal-factorization-systems.local-maps.md)
-- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md)
-- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md)
+- [Local maps](orthogonal-factorization-systems.maps-local-at-maps.md)
+- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md)
+- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md)
diff --git a/src/orthogonal-factorization-systems/separated-types.lagda.md b/src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md
similarity index 75%
rename from src/orthogonal-factorization-systems/separated-types.lagda.md
rename to src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md
index 995088d422..d47b4396a1 100644
--- a/src/orthogonal-factorization-systems/separated-types.lagda.md
+++ b/src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md
@@ -1,7 +1,7 @@
-# Separated types
+# Types separated at maps
 
 ```agda
-module orthogonal-factorization-systems.separated-types where
+module orthogonal-factorization-systems.types-separated-at-maps where
 ```
 
 <details><summary>Imports</summary>
@@ -10,7 +10,7 @@ module orthogonal-factorization-systems.separated-types where
 open import foundation.identity-types
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
@@ -19,7 +19,7 @@ open import orthogonal-factorization-systems.local-types
 
 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.local-types.md).
+are [`f`-local](orthogonal-factorization-systems.types-local-at-maps.md).
 
 ## Definition
 
diff --git a/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md b/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md
index 2857183224..493b2f511f 100644
--- a/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md
@@ -20,8 +20,8 @@ open import foundation.propositions
 open import foundation.univalence
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
 </details>
@@ -31,9 +31,10 @@ open import orthogonal-factorization-systems.modal-operators
 A **uniquely eliminating modality** is a _higher mode of logic_ defined in terms
 of a monadic
 [modal operator](orthogonal-factorization-systems.modal-operators.md) `○`
-satisfying a certain [locality](orthogonal-factorization-systems.local-types.md)
-condition. Namely, that dependent precomposition by the modal unit `unit-○` is
-an equivalence for type families over types in the image of the operator:
+satisfying a certain
+[locality](orthogonal-factorization-systems.types-local-at-maps.md) condition,
+namely that dependent precomposition by the modal unit `unit-○` is an
+equivalence for type families over types in the image of the operator:
 
 ```text
   - ∘ unit-○ : Π (x : ○ X) (○ (P x)) ≃ Π (x : X) (○ (P (unit-○ x)))
diff --git a/src/orthogonal-factorization-systems/zero-modality.lagda.md b/src/orthogonal-factorization-systems/zero-modality.lagda.md
index 855dba60bc..6395eb912e 100644
--- a/src/orthogonal-factorization-systems/zero-modality.lagda.md
+++ b/src/orthogonal-factorization-systems/zero-modality.lagda.md
@@ -10,8 +10,8 @@ module orthogonal-factorization-systems.zero-modality where
 open import foundation.unit-type
 open import foundation.universe-levels
 
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 ```
 

From 76c5d87e9a6c8cd22ef867ca5991e2502b8134dd Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Tue, 19 Nov 2024 12:30:30 -0500
Subject: [PATCH 3/3] Correcting an incorrect definition of discrete relations
 and discrete graphs (#1222)

This PR corrects an incorrect definition.
---
 .../torsorial-type-families.lagda.md          |   4 +-
 src/foundation.lagda.md                       |   3 +-
 .../discrete-binary-relations.lagda.md        |  66 +++++++
 ... => discrete-reflexive-relations.lagda.md} |  52 +++---
 .../functional-correspondences.lagda.md       |  16 +-
 .../torsorial-type-families.lagda.md          |   4 +-
 src/graph-theory.lagda.md                     |   3 +-
 .../discrete-directed-graphs.lagda.md         | 171 ++++++++++++++++++
 src/graph-theory/discrete-graphs.lagda.md     |  78 --------
 .../discrete-reflexive-graphs.lagda.md        | 120 ++++++++++++
 src/graph-theory/reflexive-graphs.lagda.md    |   6 +
 11 files changed, 401 insertions(+), 122 deletions(-)
 create mode 100644 src/foundation/discrete-binary-relations.lagda.md
 rename src/foundation/{discrete-relations.lagda.md => discrete-reflexive-relations.lagda.md} (54%)
 create mode 100644 src/graph-theory/discrete-directed-graphs.lagda.md
 delete mode 100644 src/graph-theory/discrete-graphs.lagda.md
 create mode 100644 src/graph-theory/discrete-reflexive-graphs.lagda.md

diff --git a/src/foundation-core/torsorial-type-families.lagda.md b/src/foundation-core/torsorial-type-families.lagda.md
index 35882429c6..e2dfd083f2 100644
--- a/src/foundation-core/torsorial-type-families.lagda.md
+++ b/src/foundation-core/torsorial-type-families.lagda.md
@@ -99,5 +99,5 @@ module _
 
 ### See also
 
-- [Discrete relations](foundation.discrete-relations.md) are binary torsorial
-  type families.
+- [Discrete reflexive relations](foundation.discrete-reflexive-relations.md) are
+  binary torsorial type families.
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index dbf4204531..3c7bfe2497 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -130,7 +130,8 @@ open import foundation.diagonal-maps-of-types public
 open import foundation.diagonal-span-diagrams public
 open import foundation.diagonals-of-maps public
 open import foundation.diagonals-of-morphisms-arrows public
-open import foundation.discrete-relations public
+open import foundation.discrete-binary-relations public
+open import foundation.discrete-reflexive-relations public
 open import foundation.discrete-relaxed-sigma-decompositions public
 open import foundation.discrete-sigma-decompositions public
 open import foundation.discrete-types public
diff --git a/src/foundation/discrete-binary-relations.lagda.md b/src/foundation/discrete-binary-relations.lagda.md
new file mode 100644
index 0000000000..9edf7ffd3f
--- /dev/null
+++ b/src/foundation/discrete-binary-relations.lagda.md
@@ -0,0 +1,66 @@
+# Discrete binary relations
+
+```agda
+module foundation.discrete-binary-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.empty-types
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [binary relation](foundation.binary-relations.md) `R` on `A` is said to be
+{{#concept "discrete" Disambiguation="binary relation" Agda=is-discrete-Relation}}
+if it does not relate any elements, i.e., if the type `R x y` is empty for all
+`x y : A`. In other words, a binary relation is discrete if and only if it is
+the initial binary relation. This definition ensures that the inclusion of
+[discrete directed graphs](graph-theory.discrete-directed-graphs.md) is a left
+adjoint to the forgetful functor `(V , E) ↦ (V , ∅)`.
+
+The condition of discreteness of binary relations compares to the condition of
+[discreteness](foundation.discrete-reflexive-relations.md) of
+[reflexive relations](foundation.reflexive-relations.md) in the sense that both
+conditions imply initiality. A discrete binary relation is initial becauase it
+is empty, while a discrete reflexive relation is initial because it is
+[torsorial](foundation-core.torsorial-type-families.md) and hence it is an
+[identity system](foundation.identity-systems.md).
+
+**Note:** It is also possible to impose the torsoriality condition on an
+arbitrary binary relation. However, this leads to the concept of
+[functional correspondence](foundation.functional-correspondences.md). That is,
+a binary relation `R` on `A` such that `R x` is torsorial for every `x : A` is
+the graph of a function.
+
+## Definitions
+
+### The predicate on relations of being discrete
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-discrete-prop-Relation : Prop (l1 ⊔ l2)
+  is-discrete-prop-Relation =
+    Π-Prop A (λ x → Π-Prop A (λ y → is-empty-Prop (R x y)))
+
+  is-discrete-Relation : UU (l1 ⊔ l2)
+  is-discrete-Relation = type-Prop is-discrete-prop-Relation
+
+  is-prop-is-discrete-Relation : is-prop is-discrete-Relation
+  is-prop-is-discrete-Relation = is-prop-type-Prop is-discrete-prop-Relation
+```
+
+## See also
+
+- [Discrete reflexive relations](foundation.discrete-reflexive-relations.md)
+- [Discrete directed graphs](graph-theory.discrete-directed-graphs.md)
+- [Discrete-reflexive graphs](graph-theory.discrete-reflexive-graphs.md)
diff --git a/src/foundation/discrete-relations.lagda.md b/src/foundation/discrete-reflexive-relations.lagda.md
similarity index 54%
rename from src/foundation/discrete-relations.lagda.md
rename to src/foundation/discrete-reflexive-relations.lagda.md
index 1a6535940b..236e380874 100644
--- a/src/foundation/discrete-relations.lagda.md
+++ b/src/foundation/discrete-reflexive-relations.lagda.md
@@ -1,7 +1,7 @@
-# Discrete relations
+# Discrete reflexive relations
 
 ```agda
-module foundation.discrete-relations where
+module foundation.discrete-reflexive-relations where
 ```
 
 <details><summary>Imports</summary>
@@ -22,15 +22,15 @@ open import foundation-core.propositions
 
 ## Idea
 
-A [relation](foundation.binary-relations.md) `R` on `A` is said to be
-{{#concept "discrete" Disambiguation="binary relations valued in types" Agda=is-discrete-Relation}}
+A [reflexive relation](foundation.binary-relations.md) `R` on `A` is said to be
+{{#concept "discrete" Disambiguation="reflexive relations valued in types" Agda=is-discrete-Reflexive-Relation}}
 if, for every element `x : A`, the type family `R x` is
 [torsorial](foundation-core.torsorial-type-families.md). In other words, the
 [dependent sum](foundation.dependent-pair-types.md) `Σ (y : A), (R x y)` is
-[contractible](foundation-core.contractible-types.md) for every `x`. The
-{{#concept "standard discrete relation" Disambiguation="binary relations valued in types"}}
-on a type `X` is the relation defined by
-[identifications](foundation-core.identity-types.md),
+[contractible](foundation-core.contractible-types.md) for every `x`.
+
+The {{#concept "standard discrete reflexive relation"}} on a type `X` is the
+relation defined by [identifications](foundation-core.identity-types.md),
 
 ```text
   R x y := (x ＝ y).
@@ -38,25 +38,6 @@ on a type `X` is the relation defined by
 
 ## Definitions
 
-### The predicate on relations of being discrete
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
-  where
-
-  is-discrete-prop-Relation : Prop (l1 ⊔ l2)
-  is-discrete-prop-Relation = Π-Prop A (λ x → is-torsorial-Prop (R x))
-
-  is-discrete-Relation : UU (l1 ⊔ l2)
-  is-discrete-Relation =
-    type-Prop is-discrete-prop-Relation
-
-  is-prop-is-discrete-Relation : is-prop is-discrete-Relation
-  is-prop-is-discrete-Relation =
-    is-prop-type-Prop is-discrete-prop-Relation
-```
-
 ### The predicate on reflexive relations of being discrete
 
 ```agda
@@ -66,7 +47,7 @@ module _
 
   is-discrete-prop-Reflexive-Relation : Prop (l1 ⊔ l2)
   is-discrete-prop-Reflexive-Relation =
-    is-discrete-prop-Relation (rel-Reflexive-Relation R)
+    Π-Prop A (λ a → is-torsorial-Prop (rel-Reflexive-Relation R a))
 
   is-discrete-Reflexive-Relation : UU (l1 ⊔ l2)
   is-discrete-Reflexive-Relation =
@@ -78,13 +59,22 @@ module _
     is-prop-type-Prop is-discrete-prop-Reflexive-Relation
 ```
 
-### The standard discrete relation on a type
+## Properties
+
+### The identity relation is discrete
 
 ```agda
 module _
   {l : Level} (A : UU l)
   where
 
-  is-discrete-Id-Relation : is-discrete-Relation (Id {A = A})
-  is-discrete-Id-Relation = is-torsorial-Id
+  is-discrete-Id-Reflexive-Relation :
+    is-discrete-Reflexive-Relation (Id-Reflexive-Relation A)
+  is-discrete-Id-Reflexive-Relation = is-torsorial-Id
 ```
+
+## See also
+
+- [Discrete binary relations](foundation.discrete-binary-relations.md)
+- [Discrete directed graphs](graph-theory.discrete-directed-graphs.md)
+- [Discrete reflexive graphs](graph-theory.discrete-reflexive-graphs.md)
diff --git a/src/foundation/functional-correspondences.lagda.md b/src/foundation/functional-correspondences.lagda.md
index a615239cd0..ed5998a661 100644
--- a/src/foundation/functional-correspondences.lagda.md
+++ b/src/foundation/functional-correspondences.lagda.md
@@ -14,6 +14,7 @@ open import foundation.equality-dependent-function-types
 open import foundation.function-extensionality
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.subtype-identity-principle
+open import foundation.torsorial-type-families
 open import foundation.univalence
 open import foundation.universe-levels
 
@@ -21,18 +22,19 @@ open import foundation-core.equivalences
 open import foundation-core.identity-types
 open import foundation-core.propositions
 open import foundation-core.subtypes
-open import foundation-core.torsorial-type-families
 ```
 
 </details>
 
 ## Idea
 
-A functional dependent correspondence is a dependent binary correspondence
-`C : Π (a : A) → B a → 𝒰` from a type `A` to a type family `B` over `A` such
-that for every `a : A` the type `Σ (b : B a), C a b` is contractible. The type
-of dependent functions from `A` to `B` is equivalent to the type of functional
-dependent correspondences.
+A
+{{#concept "functional (dependent) correspondence" Agda=is-functional-correspondence}}
+is a dependent binary correspondence `C : Π (a : A) → B a → 𝒰` from a type `A`
+to a type family `B` over `A` such that for every `a : A` the type family
+`C a : B a → Type` is [torsorial](foundation-core.torsorial-type-families.md).
+The type of dependent functions from `A` to `B` is equivalent to the type of
+functional dependent correspondences.
 
 ## Definition
 
@@ -41,7 +43,7 @@ is-functional-correspondence-Prop :
   {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (a : A) → B a → UU l3) →
   Prop (l1 ⊔ l2 ⊔ l3)
 is-functional-correspondence-Prop {A = A} {B} C =
-  Π-Prop A (λ x → is-contr-Prop (Σ (B x) (C x)))
+  Π-Prop A (λ x → is-torsorial-Prop (C x))
 
 is-functional-correspondence :
   {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (a : A) → B a → UU l3) →
diff --git a/src/foundation/torsorial-type-families.lagda.md b/src/foundation/torsorial-type-families.lagda.md
index db72746fb4..0929568e83 100644
--- a/src/foundation/torsorial-type-families.lagda.md
+++ b/src/foundation/torsorial-type-families.lagda.md
@@ -113,5 +113,5 @@ module _
 
 ### See also
 
-- [Discrete relations](foundation.discrete-relations.md) are binary torsorial
-  type families.
+- [Discrete reflexive relations](foundation.discrete-reflexive-relations.md) are
+  binary torsorial type families.
diff --git a/src/graph-theory.lagda.md b/src/graph-theory.lagda.md
index 9ac8fd5589..4355ecf1c8 100644
--- a/src/graph-theory.lagda.md
+++ b/src/graph-theory.lagda.md
@@ -15,7 +15,8 @@ open import graph-theory.connected-undirected-graphs public
 open import graph-theory.cycles-undirected-graphs public
 open import graph-theory.directed-graph-structures-on-standard-finite-sets public
 open import graph-theory.directed-graphs public
-open import graph-theory.discrete-graphs public
+open import graph-theory.discrete-directed-graphs public
+open import graph-theory.discrete-reflexive-graphs public
 open import graph-theory.displayed-large-reflexive-graphs public
 open import graph-theory.edge-coloured-undirected-graphs public
 open import graph-theory.embeddings-directed-graphs public
diff --git a/src/graph-theory/discrete-directed-graphs.lagda.md b/src/graph-theory/discrete-directed-graphs.lagda.md
new file mode 100644
index 0000000000..c3ff8a436b
--- /dev/null
+++ b/src/graph-theory/discrete-directed-graphs.lagda.md
@@ -0,0 +1,171 @@
+# Discrete directed graphs
+
+```agda
+module graph-theory.discrete-directed-graphs where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.discrete-binary-relations
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.homotopies
+open import foundation.retractions
+open import foundation.sections
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.propositions
+open import foundation-core.torsorial-type-families
+
+open import graph-theory.directed-graphs
+open import graph-theory.morphisms-directed-graphs
+open import graph-theory.reflexive-graphs
+```
+
+</details>
+
+## Idea
+
+A [directed graph](graph-theory.directed-graphs.md) `G ≐ (V , E)` is said to be
+{{#concept "discrete" Disambiguation="directed graph" Agda=is-discrete-Directed-Graph}}
+if it has no edges. In other words, a directed graph is discrete if it is of the
+form `Δ A`, where `Δ` is the left adjoint to the forgetful functor `(V , E) ↦ V`
+from directed graphs to types.
+
+Recall that [reflexive graphs](graph-theory.reflexive-graphs.md) are said to be
+discrete if the edge relation is
+[torsorial](foundation-core.torsorial-type-families.md). The condition that a
+directed graph is discrete compares to the condition that a reflexive graph is
+discrete in the sense that in both cases discreteness implies initiality of the
+edge relation: The empty relation is the initial relation, while the identity
+relation is the initial reflexive relation.
+
+One may wonder if the torsoriality condition of discreteness shouldn't directly
+carry over to the discreteness condition on directed graphs. Indeed, an earlier
+implementation of discreteness in agda-unimath had this faulty definition.
+However, this leads to examples that are not typically considered discrete.
+Consider, for example, the directed graph with `V := ℕ` the
+[natural numbers](elementary-number-theory.natural-numbers.md) and
+`E m n := (m + 1 ＝ n)` as in
+
+```text
+  0 ---> 1 ---> 2 ---> ⋯.
+```
+
+This directed graph satisfies the condition that the type family `E m` is
+torsorial for every `m : ℕ`, simply because `E` is a
+[functional correspondence](foundation.functional-correspondences.md). However,
+this graph is not considered discrete since it relates distinct vertices.
+
+## Definitions
+
+### The predicate on graphs of being discrete
+
+```agda
+module _
+  {l1 l2 : Level} (G : Directed-Graph l1 l2)
+  where
+
+  is-discrete-prop-Directed-Graph : Prop (l1 ⊔ l2)
+  is-discrete-prop-Directed-Graph =
+    is-discrete-prop-Relation (edge-Directed-Graph G)
+
+  is-discrete-Directed-Graph : UU (l1 ⊔ l2)
+  is-discrete-Directed-Graph =
+    is-discrete-Relation (edge-Directed-Graph G)
+
+  is-prop-is-discrete-Directed-Graph :
+    is-prop is-discrete-Directed-Graph
+  is-prop-is-discrete-Directed-Graph =
+    is-prop-is-discrete-Relation (edge-Directed-Graph G)
+```
+
+### The standard discrete directed graph
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  discrete-Directed-Graph : Directed-Graph l lzero
+  pr1 discrete-Directed-Graph = A
+  pr2 discrete-Directed-Graph x y = empty
+```
+
+## Properties
+
+### Morphisms from a standard discrete directed graph are maps into vertices
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (G : Directed-Graph l1 l2)
+  where
+
+  ev-hom-discrete-Directed-Graph :
+    hom-Directed-Graph (discrete-Directed-Graph A) G →
+    A → vertex-Directed-Graph G
+  ev-hom-discrete-Directed-Graph =
+    vertex-hom-Directed-Graph (discrete-Directed-Graph _) G
+
+  map-inv-ev-hom-discrete-Directed-Graph :
+    (A → vertex-Directed-Graph G) →
+    hom-Directed-Graph (discrete-Directed-Graph A) G
+  pr1 (map-inv-ev-hom-discrete-Directed-Graph f) = f
+  pr2 (map-inv-ev-hom-discrete-Directed-Graph f) x y ()
+
+  is-section-map-inv-ev-hom-discrete-Directed-Graph :
+    is-section
+      ( ev-hom-discrete-Directed-Graph)
+      ( map-inv-ev-hom-discrete-Directed-Graph)
+  is-section-map-inv-ev-hom-discrete-Directed-Graph f = refl
+
+  htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph :
+    (f : hom-Directed-Graph (discrete-Directed-Graph A) G) →
+    htpy-hom-Directed-Graph
+      ( discrete-Directed-Graph A)
+      ( G)
+      ( map-inv-ev-hom-discrete-Directed-Graph
+        ( ev-hom-discrete-Directed-Graph f))
+      ( f)
+  pr1 (htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f) =
+    refl-htpy
+  pr2 (htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f) x y ()
+
+  is-retraction-map-inv-ev-hom-discrete-Directed-Graph :
+    is-retraction
+      ( ev-hom-discrete-Directed-Graph)
+      ( map-inv-ev-hom-discrete-Directed-Graph)
+  is-retraction-map-inv-ev-hom-discrete-Directed-Graph f =
+    eq-htpy-hom-Directed-Graph
+      ( discrete-Directed-Graph A)
+      ( G)
+      ( map-inv-ev-hom-discrete-Directed-Graph
+        ( ev-hom-discrete-Directed-Graph f))
+      ( f)
+      ( htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f)
+
+  abstract
+    is-equiv-ev-hom-discrete-Directed-Graph :
+      is-equiv ev-hom-discrete-Directed-Graph
+    is-equiv-ev-hom-discrete-Directed-Graph =
+      is-equiv-is-invertible
+        map-inv-ev-hom-discrete-Directed-Graph
+        is-section-map-inv-ev-hom-discrete-Directed-Graph
+        is-retraction-map-inv-ev-hom-discrete-Directed-Graph
+
+  ev-equiv-hom-discrete-Directed-Graph :
+    hom-Directed-Graph (discrete-Directed-Graph A) G ≃
+    (A → vertex-Directed-Graph G)
+  pr1 ev-equiv-hom-discrete-Directed-Graph =
+    ev-hom-discrete-Directed-Graph
+  pr2 ev-equiv-hom-discrete-Directed-Graph =
+    is-equiv-ev-hom-discrete-Directed-Graph
+```
+
+## See also
+
+- [Discrete reflexive graphs](graph-theory.discrete-reflexive-graphs.md)
diff --git a/src/graph-theory/discrete-graphs.lagda.md b/src/graph-theory/discrete-graphs.lagda.md
deleted file mode 100644
index 4e5a0b8a2a..0000000000
--- a/src/graph-theory/discrete-graphs.lagda.md
+++ /dev/null
@@ -1,78 +0,0 @@
-# Discrete graphs
-
-```agda
-module graph-theory.discrete-graphs where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.contractible-types
-open import foundation.dependent-pair-types
-open import foundation.discrete-relations
-open import foundation.universe-levels
-
-open import foundation-core.identity-types
-open import foundation-core.propositions
-open import foundation-core.torsorial-type-families
-
-open import graph-theory.directed-graphs
-open import graph-theory.reflexive-graphs
-```
-
-</details>
-
-## Idea
-
-A [directed graph](graph-theory.directed-graphs.md) `G ≐ (V , E)` is said to be
-{{#concept "discrete" Disambiguation="graph" Agda=is-discrete-Graph}} if, for
-every vertex `x : V`, the type family of edges with source `x`, `E x`, is
-[torsorial](foundation-core.torsorial-type-families.md). In other words, if the
-[dependent sum](foundation.dependent-pair-types.md) `Σ (y : V), (E x y)` is
-[contractible](foundation-core.contractible-types.md) for every `x`. The
-{{#concept "standard discrete graph"}} associated to a type `X` is the graph
-whose vertices are elements of `X`, and edges are
-[identifications](foundation-core.identity-types.md),
-
-```text
-  E x y := (x ＝ y).
-```
-
-## Definitions
-
-### The predicate on graphs of being discrete
-
-```agda
-module _
-  {l1 l2 : Level} (G : Directed-Graph l1 l2)
-  where
-
-  is-discrete-prop-Graph : Prop (l1 ⊔ l2)
-  is-discrete-prop-Graph = is-discrete-prop-Relation (edge-Directed-Graph G)
-
-  is-discrete-Graph : UU (l1 ⊔ l2)
-  is-discrete-Graph = type-Prop is-discrete-prop-Graph
-
-  is-prop-is-discrete-Graph : is-prop is-discrete-Graph
-  is-prop-is-discrete-Graph = is-prop-type-Prop is-discrete-prop-Graph
-```
-
-### The predicate on reflexive graphs of being discrete
-
-```agda
-module _
-  {l1 l2 : Level} (G : Reflexive-Graph l1 l2)
-  where
-
-  is-discrete-prop-Reflexive-Graph : Prop (l1 ⊔ l2)
-  is-discrete-prop-Reflexive-Graph =
-    is-discrete-prop-Graph (graph-Reflexive-Graph G)
-
-  is-discrete-Reflexive-Graph : UU (l1 ⊔ l2)
-  is-discrete-Reflexive-Graph =
-    type-Prop is-discrete-prop-Reflexive-Graph
-
-  is-prop-is-discrete-Reflexive-Graph : is-prop is-discrete-Reflexive-Graph
-  is-prop-is-discrete-Reflexive-Graph =
-    is-prop-type-Prop is-discrete-prop-Reflexive-Graph
-```
diff --git a/src/graph-theory/discrete-reflexive-graphs.lagda.md b/src/graph-theory/discrete-reflexive-graphs.lagda.md
new file mode 100644
index 0000000000..845ca50851
--- /dev/null
+++ b/src/graph-theory/discrete-reflexive-graphs.lagda.md
@@ -0,0 +1,120 @@
+# Discrete reflexive graphs
+
+```agda
+module graph-theory.discrete-reflexive-graphs where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.discrete-reflexive-relations
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.propositions
+open import foundation-core.torsorial-type-families
+
+open import graph-theory.directed-graphs
+open import graph-theory.reflexive-graphs
+```
+
+</details>
+
+## Idea
+
+A [reflexive graph](graph-theory.reflexive-graphs.md) `G ≐ (V , E , r)` is said
+to be
+{{#concept "discrete" Disambiguation="reflexive graph" Agda=is-discrete-Reflexive-Graph}}
+if, for every vertex `x : V`, the type family of edges with source `x`, `E x`,
+is [torsorial](foundation-core.torsorial-type-families.md). In other words, if
+the [dependent sum](foundation.dependent-pair-types.md) `Σ (y : V), (E x y)` is
+[contractible](foundation-core.contractible-types.md) for every `x`. The
+{{#concept "standard discrete graph"}} associated to a type `X` is the reflexive
+graph whose vertices are elements of `X`, and edges are
+[identifications](foundation-core.identity-types.md),
+
+```text
+  E x y := (x ＝ y).
+```
+
+For any type `A` there is a
+{{#concept "standard discrete reflexive graph" Agda=standard-Discrete-Reflexive-Graph}}
+`Δ A`, which is defined by
+
+```text
+  (Δ A)₀ := A
+  (Δ A)₁ := Id A
+  refl (Δ A) := refl
+```
+
+Since torsorial type families are
+[identity systems](foundation.identity-systems.md), it follows that a reflexive
+graph is discrete precisely when its edge relation is initial. In other words,
+the inclusion of the discrete reflexive graphs into the reflexive graphs
+satisfies the universal property of being left adjoint to the forgetful functor
+`G ↦ Δ G₀`, mapping a reflexive graph to the standard discrete graph on its type
+of vertices.
+
+## Definitions
+
+### The predicate on reflexive graphs of being discrete
+
+```agda
+module _
+  {l1 l2 : Level} (G : Reflexive-Graph l1 l2)
+  where
+
+  is-discrete-prop-Reflexive-Graph : Prop (l1 ⊔ l2)
+  is-discrete-prop-Reflexive-Graph =
+    is-discrete-prop-Reflexive-Relation
+      ( edge-reflexive-relation-Reflexive-Graph G)
+
+  is-discrete-Reflexive-Graph : UU (l1 ⊔ l2)
+  is-discrete-Reflexive-Graph =
+    type-Prop is-discrete-prop-Reflexive-Graph
+
+  is-prop-is-discrete-Reflexive-Graph : is-prop is-discrete-Reflexive-Graph
+  is-prop-is-discrete-Reflexive-Graph =
+    is-prop-type-Prop is-discrete-prop-Reflexive-Graph
+```
+
+### Discrete reflexive graphs
+
+```agda
+module _
+  (l1 l2 : Level)
+  where
+
+  Discrete-Reflexive-Graph : UU (lsuc l1 ⊔ lsuc l2)
+  Discrete-Reflexive-Graph =
+    Σ (Reflexive-Graph l1 l2) is-discrete-Reflexive-Graph
+```
+
+### The standard discrete reflexive graph
+
+```agda
+module _
+  {l1 : Level} (A : UU l1)
+  where
+
+  discrete-Reflexive-Graph : Reflexive-Graph l1 l1
+  pr1 discrete-Reflexive-Graph = A
+  pr1 (pr2 discrete-Reflexive-Graph) = Id
+  pr2 (pr2 discrete-Reflexive-Graph) a = refl
+
+  is-discrete-discrete-Reflexive-Graph :
+    is-discrete-Reflexive-Graph discrete-Reflexive-Graph
+  is-discrete-discrete-Reflexive-Graph =
+    is-torsorial-Id
+
+  standard-Discrete-Reflexive-Graph :
+    Discrete-Reflexive-Graph l1 l1
+  pr1 standard-Discrete-Reflexive-Graph = discrete-Reflexive-Graph
+  pr2 standard-Discrete-Reflexive-Graph = is-discrete-discrete-Reflexive-Graph
+```
+
+## See also
+
+- [Discrete directed graphs](graph-theory.discrete-directed-graphs.md)
diff --git a/src/graph-theory/reflexive-graphs.lagda.md b/src/graph-theory/reflexive-graphs.lagda.md
index 76f15912ae..a64a9e16cf 100644
--- a/src/graph-theory/reflexive-graphs.lagda.md
+++ b/src/graph-theory/reflexive-graphs.lagda.md
@@ -8,6 +8,7 @@ module graph-theory.reflexive-graphs where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.reflexive-relations
 open import foundation.universe-levels
 
 open import graph-theory.directed-graphs
@@ -41,6 +42,11 @@ module _
   refl-Reflexive-Graph : (x : vertex-Reflexive-Graph) → edge-Reflexive-Graph x x
   refl-Reflexive-Graph = pr2 (pr2 G)
 
+  edge-reflexive-relation-Reflexive-Graph :
+    Reflexive-Relation l2 vertex-Reflexive-Graph
+  pr1 edge-reflexive-relation-Reflexive-Graph = edge-Reflexive-Graph
+  pr2 edge-reflexive-relation-Reflexive-Graph = refl-Reflexive-Graph
+
   graph-Reflexive-Graph : Directed-Graph l1 l2
   graph-Reflexive-Graph = vertex-Reflexive-Graph , edge-Reflexive-Graph
 ```