diff --git a/src/foundation-core/retracts-of-types.lagda.md b/src/foundation-core/retracts-of-types.lagda.md
index 8811b4a08c..41e3177933 100644
--- a/src/foundation-core/retracts-of-types.lagda.md
+++ b/src/foundation-core/retracts-of-types.lagda.md
@@ -14,6 +14,7 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.function-types
+open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.postcomposition-functions
 open import foundation-core.precomposition-functions
@@ -168,6 +169,17 @@ module _
     eq-htpy (is-retraction-map-retraction-retract R ·r h)
 ```
 
+### Every type is a retract of itself
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  id-retract : A retract-of A
+  id-retract = (id , id , refl-htpy)
+```
+
 ### Composition of retracts
 
 ```agda
diff --git a/src/foundation/constant-maps.lagda.md b/src/foundation/constant-maps.lagda.md
index 50092a9456..ee108c5882 100644
--- a/src/foundation/constant-maps.lagda.md
+++ b/src/foundation/constant-maps.lagda.md
@@ -15,11 +15,20 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.faithful-maps
 open import foundation.function-extensionality
+open import foundation.functoriality-dependent-pair-types
+open import foundation.morphisms-arrows
+open import foundation.postcomposition-functions
+open import foundation.retracts-of-maps
+open import foundation.retracts-of-types
+open import foundation.transposition-identifications-along-equivalences
 open import foundation.type-arithmetic-unit-type
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.1-types
+open import foundation-core.commuting-squares-of-maps
 open import foundation-core.contractible-maps
 open import foundation-core.embeddings
 open import foundation-core.equivalences
@@ -55,6 +64,14 @@ module _
   compute-action-htpy-function-const c H = ap-const c (eq-htpy H)
 ```
 
+### Computing the fibers of point inclusions
+
+```agda
+compute-fiber-point :
+  {l : Level} {A : UU l} (x y : A) → fiber (point x) y ≃ (x ＝ y)
+compute-fiber-point x y = left-unit-law-product
+```
+
 ### A type is `k+1`-truncated if and only if all point inclusions are `k`-truncated maps
 
 ```agda
@@ -62,9 +79,6 @@ module _
   {l : Level} {A : UU l}
   where
 
-  compute-fiber-point : (x y : A) → fiber (point x) y ≃ (x ＝ y)
-  compute-fiber-point x y = left-unit-law-product
-
   abstract
     is-trunc-map-point-is-trunc :
       (k : 𝕋) → is-trunc (succ-𝕋 k) A →
diff --git a/src/foundation/diagonal-maps-of-types.lagda.md b/src/foundation/diagonal-maps-of-types.lagda.md
index e21cd71a53..b4a0135888 100644
--- a/src/foundation/diagonal-maps-of-types.lagda.md
+++ b/src/foundation/diagonal-maps-of-types.lagda.md
@@ -11,6 +11,11 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.function-extensionality
+open import foundation.functoriality-dependent-pair-types
+open import foundation.morphisms-arrows
+open import foundation.postcomposition-functions
+open import foundation.retracts-of-types
+open import foundation.transposition-identifications-along-equivalences
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
@@ -80,3 +85,36 @@ module _
   pr1 diagonal-exponential-injection = diagonal-exponential A B
   pr2 diagonal-exponential-injection = is-injective-diagonal-exponential
 ```
+
+### The action on identifications of an (exponential) diagonal is a diagonal
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) {B : UU l2} (x y : B)
+  where
+
+  compute-htpy-eq-ap-diagonal-exponential :
+    htpy-eq ∘ ap (diagonal-exponential B A) ~ diagonal-exponential (x ＝ y) A
+  compute-htpy-eq-ap-diagonal-exponential refl = refl
+
+  inv-compute-htpy-eq-ap-diagonal-exponential :
+    diagonal-exponential (x ＝ y) A ~ htpy-eq ∘ ap (diagonal-exponential B A)
+  inv-compute-htpy-eq-ap-diagonal-exponential =
+    inv-htpy compute-htpy-eq-ap-diagonal-exponential
+
+  compute-eq-htpy-ap-diagonal-exponential :
+    ap (diagonal-exponential B A) ~ eq-htpy ∘ diagonal-exponential (x ＝ y) A
+  compute-eq-htpy-ap-diagonal-exponential p =
+    map-eq-transpose-equiv
+      ( equiv-funext)
+      ( compute-htpy-eq-ap-diagonal-exponential p)
+```
+
+### Computing the fibers of diagonal maps
+
+```agda
+compute-fiber-diagonal-exponential :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
+  fiber (diagonal-exponential B A) f ≃ Σ B (λ b → (x : A) → b ＝ f x)
+compute-fiber-diagonal-exponential f = equiv-tot (λ _ → equiv-funext)
+```
diff --git a/src/foundation/retracts-of-maps.lagda.md b/src/foundation/retracts-of-maps.lagda.md
index d79a6ea065..14878fae2f 100644
--- a/src/foundation/retracts-of-maps.lagda.md
+++ b/src/foundation/retracts-of-maps.lagda.md
@@ -11,9 +11,11 @@ open import foundation.action-on-identifications-functions
 open import foundation.commuting-prisms-of-maps
 open import foundation.commuting-triangles-of-morphisms-arrows
 open import foundation.dependent-pair-types
+open import foundation.diagonal-maps-of-types
 open import foundation.function-extensionality
 open import foundation.functoriality-fibers-of-maps
 open import foundation.homotopies-morphisms-arrows
+open import foundation.homotopy-algebra
 open import foundation.morphisms-arrows
 open import foundation.postcomposition-functions
 open import foundation.precomposition-functions
@@ -21,6 +23,7 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.commuting-squares-of-maps
+open import foundation-core.constant-maps
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
@@ -904,6 +907,75 @@ module _
   pr2 retract-map-postcomp-retract-map = retraction-postcomp-retract-map
 ```
 
+### If `A` is a retract of `B` and `S` is a retract of `T` then `diagonal-exponential A S` is a retract of `diagonal-exponential B T`
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {S : UU l3} {T : UU l4}
+  (R : A retract-of B) (Q : S retract-of T)
+  where
+
+  inclusion-diagonal-exponential-retract :
+    hom-arrow (diagonal-exponential A S) (diagonal-exponential B T)
+  inclusion-diagonal-exponential-retract =
+    ( inclusion-retract R ,
+      precomp (map-retraction-retract Q) B ∘ postcomp S (inclusion-retract R) ,
+      refl-htpy)
+
+  hom-retraction-diagonal-exponential-retract :
+    hom-arrow (diagonal-exponential B T) (diagonal-exponential A S)
+  hom-retraction-diagonal-exponential-retract =
+    ( map-retraction-retract R ,
+      postcomp S (map-retraction-retract R) ∘ precomp (inclusion-retract Q) B ,
+      refl-htpy)
+
+  coh-retract-map-diagonal-exponential-retract :
+    coherence-retract-map
+      ( diagonal-exponential A S)
+      ( diagonal-exponential B T)
+      ( inclusion-diagonal-exponential-retract)
+      ( hom-retraction-diagonal-exponential-retract)
+      ( is-retraction-map-retraction-retract R)
+      ( horizontal-concat-htpy
+        ( htpy-postcomp S (is-retraction-map-retraction-retract R))
+        ( htpy-precomp (is-retraction-map-retraction-retract Q) A))
+  coh-retract-map-diagonal-exponential-retract x =
+    ( compute-eq-htpy-ap-diagonal-exponential S
+      ( map-retraction-retract R (inclusion-retract R x))
+      ( x)
+      ( is-retraction-map-retraction-retract R x)) ∙
+    ( ap
+      ( λ p →
+        ( ap (λ f a → map-retraction-retract R (inclusion-retract R (f a))) p) ∙
+        ( eq-htpy (λ _ → is-retraction-map-retraction-retract R x)))
+      ( inv
+        ( ( ap
+            ( eq-htpy)
+            ( eq-htpy (ap-const x ·r is-retraction-map-retraction-retract Q))) ∙
+          ( eq-htpy-refl-htpy (diagonal-exponential A S x))))) ∙
+      ( inv right-unit)
+
+  is-retraction-hom-retraction-diagonal-exponential-retract :
+    is-retraction-hom-arrow
+      ( diagonal-exponential A S)
+      ( diagonal-exponential B T)
+      ( inclusion-diagonal-exponential-retract)
+      ( hom-retraction-diagonal-exponential-retract)
+  is-retraction-hom-retraction-diagonal-exponential-retract =
+    ( ( is-retraction-map-retraction-retract R) ,
+      ( horizontal-concat-htpy
+        ( htpy-postcomp S (is-retraction-map-retraction-retract R))
+        ( htpy-precomp (is-retraction-map-retraction-retract Q) A)) ,
+      ( coh-retract-map-diagonal-exponential-retract))
+
+  retract-map-diagonal-exponential-retract :
+    (diagonal-exponential A S) retract-of-map (diagonal-exponential B T)
+  retract-map-diagonal-exponential-retract =
+    ( inclusion-diagonal-exponential-retract ,
+      hom-retraction-diagonal-exponential-retract ,
+      is-retraction-hom-retraction-diagonal-exponential-retract)
+```
+
 ## References
 
 {{#bibliography}} {{#reference UF13}}
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index 0a15faea26..95c940b7c6 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -42,6 +42,8 @@ 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
 open import orthogonal-factorization-systems.modal-subuniverse-induction public
+open import orthogonal-factorization-systems.null-families-of-types public
+open import orthogonal-factorization-systems.null-maps public
 open import orthogonal-factorization-systems.null-types public
 open import orthogonal-factorization-systems.open-modalities public
 open import orthogonal-factorization-systems.orthogonal-factorization-systems public
diff --git a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md b/src/orthogonal-factorization-systems/local-families-of-types.lagda.md
index 18f7cb3737..eb8d398b33 100644
--- a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md
+++ b/src/orthogonal-factorization-systems/local-families-of-types.lagda.md
@@ -23,15 +23,15 @@ open import orthogonal-factorization-systems.orthogonal-maps
 
 A family of types `B : A → UU l` is said to be
 {{#concept "local" Disambiguation="family of types" Agda=is-local-family}} at
-`f : Y → X`, or **`f`-local**, if every
+`f : X → Y`, or **`f`-local**, if every
 [fiber](foundation-core.fibers-of-maps.md) is.
 
 ## Definition
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {Y : UU l1} {X : UU l2}
-  (f : Y → X) {A : UU l3} (B : A → UU l4)
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2}
+  (f : X → Y) {A : UU l3} (B : A → UU l4)
   where
 
   is-local-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
diff --git a/src/orthogonal-factorization-systems/local-maps.lagda.md b/src/orthogonal-factorization-systems/local-maps.lagda.md
index 5703f6ba16..f19c0c87ee 100644
--- a/src/orthogonal-factorization-systems/local-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/local-maps.lagda.md
@@ -7,34 +7,54 @@ module orthogonal-factorization-systems.local-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.cartesian-morphisms-arrows
+open import foundation.cones-over-cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
 open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-fibers-of-maps
+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.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.orthogonal-maps
+open import orthogonal-factorization-systems.pullback-hom
 ```
 
 </details>
 
 ## Idea
 
-A map `g : A → B` is said to be
+A map `g : X → Y` is said to be
 {{#concept "local" Disambiguation="maps of types" Agda=is-local-map}} at
-`f : Y → X`, or
+`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`.
+
 ## Definition
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {Y : UU l1} {X : UU l2} {A : UU l3} {B : UU l4}
-  (f : Y → X) (g : A → B)
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
   where
 
   is-local-map : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
@@ -51,17 +71,17 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {Y : UU l1} {X : UU l2} {B : UU l3}
-  (f : Y → X)
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {Y : UU l3}
+  (f : A → B)
   where
 
   is-local-is-local-terminal-map :
-    is-local-map f (terminal-map B) → is-local f B
+    is-local-map f (terminal-map Y) → is-local f Y
   is-local-is-local-terminal-map H =
     is-local-equiv f (inv-equiv-fiber-terminal-map star) (H star)
 
   is-local-terminal-map-is-local :
-    is-local f B → is-local-map f (terminal-map B)
+    is-local f Y → is-local-map f (terminal-map Y)
   is-local-terminal-map-is-local H u =
     is-local-equiv f (equiv-fiber-terminal-map u) H
 ```
@@ -70,8 +90,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level}
-  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {X' : UU l5} {Y' : UU l6}
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
   (f : A → B) (g : X → Y)
   where
 
diff --git a/src/orthogonal-factorization-systems/local-types.lagda.md b/src/orthogonal-factorization-systems/local-types.lagda.md
index 38b13c18ae..0f957651be 100644
--- a/src/orthogonal-factorization-systems/local-types.lagda.md
+++ b/src/orthogonal-factorization-systems/local-types.lagda.md
@@ -41,25 +41,36 @@ open import foundation.universe-levels
 
 ## Idea
 
-A dependent type `A` over `X` is said to be **local at** `f : Y → X`, or
-**`f`-local**, if the [precomposition map](foundation-core.function-types.md)
+A dependent type `A` over `Y` is said to be
+{{#concept "local at" Disambiguation="map of types"}} `f : X → Y`, or
+{{#concept "`f`-local" Disambiguation="map of types"}} , if the
+[precomposition map](foundation-core.function-types.md)
 
 ```text
-  _∘ f : ((x : X) → A x) → ((y : Y) → A (f y))
+  _∘ f : ((y : Y) → A y) → ((x : X) → A (f x))
 ```
 
 is an [equivalence](foundation-core.equivalences.md).
 
-We reserve the name `is-local` for when `A` does not vary over `X`, and specify
+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).
+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
+dependent type `A` may be understood as a family of types such that for every
+`y : Y`, `A y` is
+`fiber f y`-[null](orthogonal-factorization-systems.null-types.md).
+
 ## Definition
 
 ### Local dependent types
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) (A : X → UU l3)
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (f : X → Y) (A : Y → UU l3)
   where
 
   is-local-dependent-type : UU (l1 ⊔ l2 ⊔ l3)
@@ -77,7 +88,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) (A : UU l3)
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (f : X → Y) (A : UU l3)
   where
 
   is-local : UU (l1 ⊔ l2 ⊔ l3)
@@ -92,15 +103,15 @@ module _
 
 ## Properties
 
-### Being local distributes over Π-types
+### Locality distributes over Π-types
 
 ```agda
 module _
-  {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
   where
 
   distributive-Π-is-local-dependent-type :
-    {l3 l4 : Level} {A : UU l3} (B : A → X → UU l4) →
+    {l3 l4 : Level} {A : UU l3} (B : A → Y → UU l4) →
     ((a : A) → is-local-dependent-type f (B a)) →
     is-local-dependent-type f (λ x → (a : A) → B a x)
   distributive-Π-is-local-dependent-type B f-loc =
@@ -122,8 +133,8 @@ module _
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
-  {Y : UU l1} {X : UU l2} {A : X → UU l3} {B : X → UU l4}
-  (f : Y → X)
+  {X : UU l1} {Y : UU l2} {A : Y → UU l3} {B : Y → UU l4}
+  (f : X → Y)
   where
 
   is-local-dependent-type-fam-equiv :
@@ -143,8 +154,8 @@ module _
 
 module _
   {l1 l2 l3 l4 : Level}
-  {Y : UU l1} {X : UU l2} {A : UU l3} {B : UU l4}
-  (f : Y → X)
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4}
+  (f : X → Y)
   where
 
   is-local-equiv : A ≃ B → is-local f B → is-local f A
@@ -158,7 +169,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {Y : UU l1} {X : UU l2} {A : UU l3} {f f' : Y → X}
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {f f' : X → Y}
   where
 
   is-local-htpy : (H : f ~ f') → is-local f' A → is-local f A
@@ -227,7 +238,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
   where
 
   is-equiv-is-local : ({l : Level} (A : UU l) → is-local f A) → is-equiv f
@@ -238,43 +249,43 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
   where
 
-  section-is-local-domains' : section (precomp f Y) → is-local f X → section f
-  pr1 (section-is-local-domains' section-precomp-Y is-local-X) =
-    pr1 section-precomp-Y id
-  pr2 (section-is-local-domains' section-precomp-Y is-local-X) =
+  section-is-local-domains' : section (precomp f X) → is-local f Y → section f
+  pr1 (section-is-local-domains' section-precomp-X is-local-Y) =
+    pr1 section-precomp-X id
+  pr2 (section-is-local-domains' section-precomp-X is-local-Y) =
     htpy-eq
       ( ap
         ( pr1)
-        { ( f ∘ pr1 (section-is-local-domains' section-precomp-Y is-local-X)) ,
-          ( ap (postcomp Y f) (pr2 section-precomp-Y id))}
+        { ( f ∘ pr1 (section-is-local-domains' section-precomp-X is-local-Y)) ,
+          ( ap (postcomp X f) (pr2 section-precomp-X id))}
         { id , refl}
-        ( eq-is-contr (is-contr-map-is-equiv is-local-X f)))
+        ( eq-is-contr (is-contr-map-is-equiv is-local-Y f)))
 
-  is-equiv-is-local-domains' : section (precomp f Y) → is-local f X → is-equiv f
-  pr1 (is-equiv-is-local-domains' section-precomp-Y is-local-X) =
-    section-is-local-domains' section-precomp-Y is-local-X
-  pr2 (is-equiv-is-local-domains' section-precomp-Y is-local-X) =
-    retraction-section-precomp-domain f section-precomp-Y
+  is-equiv-is-local-domains' : section (precomp f X) → is-local f Y → is-equiv f
+  pr1 (is-equiv-is-local-domains' section-precomp-X is-local-Y) =
+    section-is-local-domains' section-precomp-X is-local-Y
+  pr2 (is-equiv-is-local-domains' section-precomp-X is-local-Y) =
+    retraction-section-precomp-domain f section-precomp-X
 
-  is-equiv-is-local-domains : is-local f Y → is-local f X → is-equiv f
-  is-equiv-is-local-domains is-local-Y =
-    is-equiv-is-local-domains' (pr1 is-local-Y)
+  is-equiv-is-local-domains : is-local f X → is-local f Y → is-equiv f
+  is-equiv-is-local-domains is-local-X =
+    is-equiv-is-local-domains' (pr1 is-local-X)
 ```
 
 ### Propositions are `f`-local if `_∘ f` has a converse
 
 ```agda
 module _
-  {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
   where
 
   is-local-dependent-type-is-prop :
-    {l : Level} (A : X → UU l) →
-    ((x : X) → is-prop (A x)) →
-    (((y : Y) → A (f y)) → ((x : X) → A x)) →
+    {l : Level} (A : Y → UU l) →
+    ((y : Y) → is-prop (A y)) →
+    (((x : X) → A (f x)) → ((y : Y) → A y)) →
     is-local-dependent-type f A
   is-local-dependent-type-is-prop A is-prop-A =
     is-equiv-has-converse-is-prop
@@ -283,22 +294,20 @@ module _
 
   is-local-is-prop :
     {l : Level} (A : UU l) →
-    is-prop A → ((Y → A) → (X → A)) → is-local f A
+    is-prop A → ((X → A) → (Y → A)) → is-local f A
   is-local-is-prop A is-prop-A =
     is-local-dependent-type-is-prop (λ _ → A) (λ _ → is-prop-A)
 ```
 
-## Examples
-
 ### All type families are local at equivalences
 
 ```agda
 module _
-  {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
   where
 
   is-local-dependent-type-is-equiv :
-    is-equiv f → {l : Level} (A : X → UU l) → is-local-dependent-type f A
+    is-equiv f → {l : Level} (A : Y → UU l) → is-local-dependent-type f A
   is-local-dependent-type-is-equiv is-equiv-f =
     is-equiv-precomp-Π-is-equiv is-equiv-f
 
@@ -311,12 +320,12 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
   where
 
   is-local-dependent-type-is-contr :
-    {l : Level} (A : X → UU l) →
-    ((x : X) → is-contr (A x)) → is-local-dependent-type f A
+    {l : Level} (A : Y → UU l) →
+    ((y : Y) → is-contr (A y)) → is-local-dependent-type f A
   is-local-dependent-type-is-contr A is-contr-A =
     is-equiv-is-contr
       ( precomp-Π f A)
diff --git a/src/orthogonal-factorization-systems/null-families-of-types.lagda.md b/src/orthogonal-factorization-systems/null-families-of-types.lagda.md
new file mode 100644
index 0000000000..9a6dfa29eb
--- /dev/null
+++ b/src/orthogonal-factorization-systems/null-families-of-types.lagda.md
@@ -0,0 +1,123 @@
+# Null families of types
+
+```agda
+module orthogonal-factorization-systems.null-families-of-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.precomposition-functions
+open import foundation.propositions
+open import foundation.retracts-of-types
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.null-types
+open import orthogonal-factorization-systems.orthogonal-maps
+```
+
+</details>
+
+## Idea
+
+A family of types `B : A → UU l` is said to be
+{{#concept "null" Disambiguation="family of types" Agda=is-null-family}} at `Y`,
+or **`Y`-null**, if every fiber is. I.e., if the
+[diagonal map](foundation.diagonal-maps-of-types.md)
+
+```text
+  Δ : B x → (Y → B x)
+```
+
+is an [equivalence](foundation-core.equivalences.md) for every `x` in `A`.
+
+## Definitions
+
+### `Y`-null families of types
+
+```agda
+module _
+  {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} (B : A → UU l3)
+  where
+
+  is-null-family : UU (l1 ⊔ l2 ⊔ l3)
+  is-null-family = (x : A) → is-null Y (B x)
+
+  is-property-is-null-family : is-prop is-null-family
+  is-property-is-null-family =
+    is-prop-Π (λ x → is-prop-is-null Y (B x))
+
+  is-null-family-Prop : Prop (l1 ⊔ l2 ⊔ l3)
+  is-null-family-Prop = (is-null-family , is-property-is-null-family)
+```
+
+## Properties
+
+### Closure under equivalences
+
+If `C` is `Y`-null and we have equivalences `X ≃ Y` and `(x : A) → B x ≃ C x`,
+then `B` is `X`-null.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {B : A → UU l4}
+  where
+
+  is-null-family-equiv :
+    {l5 : Level} {C : A → UU l5} →
+    X ≃ Y → ((x : A) → B x ≃ C x) →
+    is-null-family Y C → is-null-family X B
+  is-null-family-equiv e f H x = is-null-equiv e (f x) (H x)
+
+  is-null-family-equiv-exponent :
+    (e : X ≃ Y) → is-null-family Y B → is-null-family X B
+  is-null-family-equiv-exponent e H x = is-null-equiv-exponent e (H x)
+
+module _
+  {l1 l2 l3 l4 : Level} {Y : UU l1} {A : UU l2} {B : A → UU l3} {C : A → UU l4}
+  where
+
+  is-null-family-equiv-family :
+    ((x : A) → B x ≃ C x) → is-null-family Y C → is-null-family Y B
+  is-null-family-equiv-family f H x = is-null-equiv-base (f x) (H x)
+```
+
+### Closure under retracts
+
+If `C` is `Y`-null and `X` is a retract of `Y` and `B x` is a retract of `C x`
+for all `x`, then `B` is `X`-null.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : A → UU l4} {C : A → UU l5}
+  where
+
+  is-null-family-retract :
+    X retract-of Y → ((x : A) → (B x) retract-of (C x)) →
+    is-null-family Y C → is-null-family X B
+  is-null-family-retract e f H x = is-null-retract e (f x) (H x)
+
+module _
+  {l1 l2 l3 l4 : Level} {Y : UU l1} {A : UU l2} {B : A → UU l3} {C : A → UU l4}
+  where
+
+  is-null-family-retract-family :
+    ((x : A) → (B x) retract-of (C x)) → is-null-family Y C → is-null-family Y B
+  is-null-family-retract-family f H x = is-null-retract-base (f x) (H x)
+
+module _
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {B : A → UU l4}
+  where
+
+  is-null-family-retract-exponent :
+    X retract-of Y → is-null-family Y B → is-null-family X B
+  is-null-family-retract-exponent e H x = is-null-retract-exponent e (H x)
+```
+
+## See also
+
+- In [`null-maps`](orthogonal-factorization-systems.null-maps.md) we show that a
+  type family is `Y`-null if and only if its total space projection is.
diff --git a/src/orthogonal-factorization-systems/null-maps.lagda.md b/src/orthogonal-factorization-systems/null-maps.lagda.md
new file mode 100644
index 0000000000..2863c0ff12
--- /dev/null
+++ b/src/orthogonal-factorization-systems/null-maps.lagda.md
@@ -0,0 +1,280 @@
+# Null maps
+
+```agda
+module orthogonal-factorization-systems.null-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cones-over-cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.diagonal-maps-of-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.families-of-equivalences
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-fibers-of-maps
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.morphisms-arrows
+open import foundation.postcomposition-functions
+open import foundation.precomposition-functions
+open import foundation.propositions
+open import foundation.pullbacks
+open import foundation.type-arithmetic-unit-type
+open import foundation.type-theoretic-principle-of-choice
+open import foundation.unit-type
+open import foundation.universal-property-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.null-families-of-types
+open import orthogonal-factorization-systems.null-types
+open import orthogonal-factorization-systems.orthogonal-maps
+```
+
+</details>
+
+## Idea
+
+A map `f : A → B` is said to be
+{{#concept "null" Disambiguation="function at a type" Agda=is-null-map}} at `Y`,
+or {{#concept "`Y`-null" Disambiguation="function at a type" Agda=is-null-map}}
+if its [fibers](foundation-core.fibers-of-maps.md) are
+`Y`-[null](orthogonal-factorization-systems.null-types.md), or equivalently, if
+the square
+
+```text
+         Δ
+    A ------> (Y → A)
+    |            |
+  f |            | f ∘ -
+    ∨            ∨
+    B ------> (Y → B)
+         Δ
+```
+
+is a [pullback](foundation-core.pullbacks.md).
+
+## Definitions
+
+### The fiber condition for `Y`-null maps
+
+```agda
+module _
+  {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} {B : UU l3} (f : A → B)
+  where
+
+  is-null-map : UU (l1 ⊔ l2 ⊔ l3)
+  is-null-map = is-null-family Y (fiber f)
+
+  is-property-is-null-map : is-prop is-null-map
+  is-property-is-null-map = is-property-is-null-family Y (fiber f)
+
+  is-null-map-Prop : Prop (l1 ⊔ l2 ⊔ l3)
+  is-null-map-Prop = (is-null-map , is-property-is-null-map)
+```
+
+### The pullback condition for `Y`-null maps
+
+```agda
+module _
+  {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} {B : UU l3} (f : A → B)
+  where
+
+  cone-is-null-map-pullback-condition :
+    cone (diagonal-exponential B Y) (postcomp Y f) A
+  cone-is-null-map-pullback-condition =
+    (f , diagonal-exponential A Y , refl-htpy)
+
+  is-null-map-pullback-condition : UU (l1 ⊔ l2 ⊔ l3)
+  is-null-map-pullback-condition =
+    is-pullback
+      ( diagonal-exponential B Y)
+      ( postcomp Y f)
+      ( cone-is-null-map-pullback-condition)
+
+  is-prop-is-null-map-pullback-condition :
+    is-prop is-null-map-pullback-condition
+  is-prop-is-null-map-pullback-condition =
+    is-prop-is-pullback
+      ( diagonal-exponential B Y)
+      ( postcomp Y f)
+      ( cone-is-null-map-pullback-condition)
+```
+
+## Properties
+
+### A type family is `Y`-null if and only if its total space projection is
+
+```agda
+module _
+  {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} (B : A → UU l3)
+  where
+
+  is-null-family-is-null-map-pr1 :
+    is-null-map Y (pr1 {B = B}) → is-null-family Y B
+  is-null-family-is-null-map-pr1 =
+    is-null-family-equiv-family (inv-equiv-fiber-pr1 B)
+
+  is-null-map-pr1-is-null-family :
+    is-null-family Y B → is-null-map Y (pr1 {B = B})
+  is-null-map-pr1-is-null-family =
+    is-null-family-equiv-family (equiv-fiber-pr1 B)
+```
+
+### The pullback and fiber condition for `Y`-null maps are equivalent
+
+```agda
+module _
+  {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} {B : UU l3} (f : A → B)
+  where
+
+  abstract
+    compute-map-fiber-vertical-map-cone-is-null-map-pullback-condition :
+      (b : B) →
+      equiv-arrow
+        ( map-fiber-vertical-map-cone
+          ( diagonal-exponential B Y)
+          ( postcomp Y f)
+          ( cone-is-null-map-pullback-condition Y f)
+          ( b))
+        ( diagonal-exponential (fiber f b) Y)
+    compute-map-fiber-vertical-map-cone-is-null-map-pullback-condition b =
+      ( id-equiv ,
+        inv-compute-Π-fiber-postcomp Y f (diagonal-exponential B Y b) ,
+        ( λ where (x , refl) → refl))
+
+  is-null-map-pullback-condition-is-null-map :
+    is-null-map Y f → is-null-map-pullback-condition Y f
+  is-null-map-pullback-condition-is-null-map H =
+    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone
+      ( diagonal-exponential B Y)
+      ( postcomp Y f)
+      ( cone-is-null-map-pullback-condition Y f)
+      ( λ b →
+        is-equiv-source-is-equiv-target-equiv-arrow
+          ( map-fiber-vertical-map-cone
+            ( diagonal-exponential B Y)
+            ( postcomp Y f)
+            ( cone-is-null-map-pullback-condition Y f)
+            ( b))
+          ( diagonal-exponential (fiber f b) Y)
+          ( compute-map-fiber-vertical-map-cone-is-null-map-pullback-condition
+            ( b))
+          ( H b))
+
+  is-null-map-is-null-map-pullback-condition :
+    is-null-map-pullback-condition Y f → is-null-map Y f
+  is-null-map-is-null-map-pullback-condition H b =
+    is-equiv-target-is-equiv-source-equiv-arrow
+      ( map-fiber-vertical-map-cone
+        ( diagonal-exponential B Y)
+        ( postcomp Y f)
+        ( cone-is-null-map-pullback-condition Y f)
+        ( b))
+      ( diagonal-exponential (fiber f b) Y)
+      ( compute-map-fiber-vertical-map-cone-is-null-map-pullback-condition b)
+      ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+        ( diagonal-exponential B Y)
+        ( postcomp Y f)
+        ( cone-is-null-map-pullback-condition Y f)
+        ( H)
+        ( b))
+```
+
+### A map is `Y`-null if and only if it is local at the terminal projection `Y → unit`
+
+```agda
+module _
+  {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} {B : UU l3} (f : A → B)
+  where
+
+  is-local-terminal-map-is-null-map :
+    is-null-map Y f → is-local-map (terminal-map Y) f
+  is-local-terminal-map-is-null-map H x =
+    is-local-terminal-map-is-null Y (fiber f x) (H x)
+
+  is-null-map-is-local-terminal-map :
+    is-local-map (terminal-map Y) f → is-null-map Y f
+  is-null-map-is-local-terminal-map H x =
+    is-null-is-local-terminal-map Y (fiber f x) (H x)
+
+  equiv-is-local-terminal-map-is-null-map :
+    is-null-map Y f ≃ is-local-map (terminal-map Y) f
+  equiv-is-local-terminal-map-is-null-map =
+    equiv-iff-is-prop
+      ( is-property-is-null-map Y f)
+      ( is-property-is-local-map (terminal-map Y) f)
+      ( is-local-terminal-map-is-null-map)
+      ( is-null-map-is-local-terminal-map)
+
+  equiv-is-null-map-is-local-terminal-map :
+    is-local-map (terminal-map Y) f ≃ is-null-map Y f
+  equiv-is-null-map-is-local-terminal-map =
+    inv-equiv equiv-is-local-terminal-map-is-null-map
+```
+
+### A map is `Y`-null if and only if the terminal projection of `Y` is orthogonal to `f`
+
+```agda
+module _
+  {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} {B : UU l3} (f : A → B)
+  where
+
+  is-null-map-is-orthogonal-fiber-condition-terminal-map :
+    is-orthogonal-fiber-condition-right-map (terminal-map Y) f →
+    is-null-map Y f
+  is-null-map-is-orthogonal-fiber-condition-terminal-map H b =
+    is-equiv-target-is-equiv-source-equiv-arrow
+      ( precomp (terminal-map Y) (fiber f b))
+      ( diagonal-exponential (fiber f b) Y)
+      ( left-unit-law-function-type (fiber f b) , id-equiv , refl-htpy)
+      ( H (point b))
+
+  is-orthogonal-fiber-condition-terminal-map-is-null-map :
+    is-null-map Y f →
+    is-orthogonal-fiber-condition-right-map (terminal-map Y) f
+  is-orthogonal-fiber-condition-terminal-map-is-null-map H b =
+    is-equiv-source-is-equiv-target-equiv-arrow
+      ( precomp (terminal-map Y) (fiber f (b star)))
+      ( diagonal-exponential (fiber f (b star)) Y)
+      ( left-unit-law-function-type (fiber f (b star)) , id-equiv , refl-htpy)
+      ( H (b star))
+
+  is-null-map-is-orthogonal-pullback-condition-terminal-map :
+    is-orthogonal-pullback-condition (terminal-map Y) f → is-null-map Y f
+  is-null-map-is-orthogonal-pullback-condition-terminal-map H =
+    is-null-map-is-orthogonal-fiber-condition-terminal-map
+      ( is-orthogonal-fiber-condition-right-map-is-orthogonal-pullback-condition
+        ( terminal-map Y)
+        ( f)
+        ( H))
+
+  is-orthogonal-pullback-condition-terminal-map-is-null-map :
+    is-null-map Y f → is-orthogonal-pullback-condition (terminal-map Y) f
+  is-orthogonal-pullback-condition-terminal-map-is-null-map H =
+    is-orthogonal-pullback-condition-is-orthogonal-fiber-condition-right-map
+      ( terminal-map Y)
+      ( f)
+      ( is-orthogonal-fiber-condition-terminal-map-is-null-map H)
+
+  is-null-map-is-orthogonal-terminal-map :
+    is-orthogonal (terminal-map Y) f → is-null-map Y f
+  is-null-map-is-orthogonal-terminal-map H =
+    is-null-map-is-orthogonal-fiber-condition-terminal-map
+      ( is-orthogonal-fiber-condition-right-map-is-orthogonal
+        ( terminal-map Y)
+        ( f)
+        ( H))
+
+  is-orthogonal-terminal-map-is-null-map :
+    is-null-map Y f → is-orthogonal (terminal-map Y) f
+  is-orthogonal-terminal-map-is-null-map H =
+    is-orthogonal-is-orthogonal-fiber-condition-right-map (terminal-map Y) f
+      ( is-orthogonal-fiber-condition-terminal-map-is-null-map H)
+```
diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md
index 23642b80f1..6e50e36ba6 100644
--- a/src/orthogonal-factorization-systems/null-types.lagda.md
+++ b/src/orthogonal-factorization-systems/null-types.lagda.md
@@ -7,36 +7,53 @@ module orthogonal-factorization-systems.null-types where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.constant-maps
 open import foundation.dependent-pair-types
 open import foundation.diagonal-maps-of-types
 open import foundation.equivalences
+open import foundation.equivalences-arrows
 open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.homotopies
+open import foundation.identity-types
 open import foundation.logical-equivalences
+open import foundation.postcomposition-functions
+open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
 open import foundation.propositions
+open import foundation.retracts-of-maps
+open import foundation.retracts-of-types
 open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
+open import foundation.universal-property-equivalences
 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.orthogonal-maps
 ```
 
 </details>
 
 ## Idea
 
-A type `A` is said to be **null at** `Y`, or **`Y`-null**, if the diagonal map
+A type `A` is said to be
+{{#concept "null at" Disambiguation="type" Agda=is-null}} `Y`, or
+{{#concept "`Y`-null" Disambiguation="type" Agda=is-null}}, if the
+[diagonal map](foundation.diagonal-maps-of-types.md)
 
 ```text
   Δ : A → (Y → A)
 ```
 
-is an equivalence. The idea is that _`A` observes the type `Y` to be
-contractible_.
+is an [equivalence](foundation-core.equivalences.md). The idea is that `A`
+"observes" the type `Y` to be
+[contractible](foundation-core.contractible-types.md).
 
-## Definition
+## Definitions
+
+### The predicate on a type of being `Y`-null
 
 ```agda
 module _
@@ -56,6 +73,78 @@ module _
 
 ## Properties
 
+### Closure under equivalences
+
+If `B` is `Y`-null and we have equivalences `X ≃ Y` and `A ≃ B`, then `A` is
+`X`-null.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4}
+  where
+
+  is-null-equiv : (e : X ≃ Y) (f : A ≃ B) → is-null Y B → is-null X A
+  is-null-equiv e f H =
+    is-equiv-htpy-equiv
+      ( equiv-precomp e A ∘e equiv-postcomp Y (inv-equiv f) ∘e (_ , H) ∘e f)
+      ( λ x → eq-htpy (λ _ → inv (is-retraction-map-inv-equiv f x)))
+
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {A : UU l3}
+  where
+
+  is-null-equiv-exponent : (e : X ≃ Y) → is-null Y A → is-null X A
+  is-null-equiv-exponent e H =
+    is-equiv-comp
+      ( precomp (map-equiv e) A)
+      ( diagonal-exponential A Y)
+      ( H)
+      ( is-equiv-precomp-equiv e A)
+
+module _
+  {l1 l2 l3 : Level} {Y : UU l1} {A : UU l2} {B : UU l3}
+  where
+
+  is-null-equiv-base : (f : A ≃ B) → is-null Y B → is-null Y A
+  is-null-equiv-base f H =
+    is-equiv-htpy-equiv
+      ( equiv-postcomp Y (inv-equiv f) ∘e (_ , H) ∘e f)
+      ( λ b → eq-htpy (λ _ → inv (is-retraction-map-inv-equiv f b)))
+```
+
+### Closure under retracts
+
+If `B` is `Y`-null and `X` is a retract of `Y` and `A` is a retract of `B`, then
+`A` is `X`-null.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4}
+  where
+
+  is-null-retract :
+    X retract-of Y → A retract-of B → is-null Y B → is-null X A
+  is-null-retract e f =
+    is-equiv-retract-map-is-equiv
+      ( diagonal-exponential A X)
+      ( diagonal-exponential B Y)
+      ( retract-map-diagonal-exponential-retract f e)
+
+module _
+  {l1 l2 l3 : Level} {Y : UU l1} {A : UU l2} {B : UU l3}
+  where
+
+  is-null-retract-base : A retract-of B → is-null Y B → is-null Y A
+  is-null-retract-base = is-null-retract id-retract
+
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {A : UU l3}
+  where
+
+  is-null-retract-exponent : X retract-of Y → is-null Y A → is-null X A
+  is-null-retract-exponent e = is-null-retract e id-retract
+```
+
 ### A type is `Y`-null if and only if it is local at the terminal projection `Y → unit`
 
 ```agda
@@ -63,30 +152,63 @@ module _
   {l1 l2 : Level} (Y : UU l1) (A : UU l2)
   where
 
-  is-local-is-null : is-null Y A → is-local (λ y → star) A
-  is-local-is-null =
+  is-local-terminal-map-is-null : is-null Y A → is-local (terminal-map Y) A
+  is-local-terminal-map-is-null =
     is-equiv-comp
       ( diagonal-exponential A Y)
       ( map-left-unit-law-function-type A)
       ( is-equiv-map-left-unit-law-function-type A)
 
-  is-null-is-local : is-local (λ y → star) A → is-null Y A
-  is-null-is-local =
+  is-null-is-local-terminal-map : is-local (terminal-map Y) A → is-null Y A
+  is-null-is-local-terminal-map =
     is-equiv-comp
-      ( precomp (λ y → star) A)
+      ( precomp (terminal-map Y) A)
       ( map-inv-left-unit-law-function-type A)
       ( is-equiv-map-inv-left-unit-law-function-type A)
 
-  equiv-is-local-is-null : is-null Y A ≃ is-local (λ y → star) A
-  equiv-is-local-is-null =
+  equiv-is-local-terminal-map-is-null :
+    is-null Y A ≃ is-local (terminal-map Y) A
+  equiv-is-local-terminal-map-is-null =
     equiv-iff-is-prop
       ( is-property-is-equiv (diagonal-exponential A Y))
-      ( is-property-is-equiv (precomp (λ y → star) A))
-      ( is-local-is-null)
-      ( is-null-is-local)
+      ( is-property-is-equiv (precomp (terminal-map Y) A))
+      ( is-local-terminal-map-is-null)
+      ( is-null-is-local-terminal-map)
+
+  equiv-is-null-is-local-terminal-map :
+    is-local (terminal-map Y) A ≃ is-null Y A
+  equiv-is-null-is-local-terminal-map =
+    inv-equiv equiv-is-local-terminal-map-is-null
+```
+
+### A type is `Y`-null if and only if the terminal projection of `Y` is orthogonal to the terminal projection of `A`
+
+```agda
+module _
+  {l1 l2 : Level} {Y : UU l1} {A : UU l2}
+  where
 
-  equiv-is-null-is-local : is-local (λ y → star) A ≃ is-null Y A
-  equiv-is-null-is-local = inv-equiv equiv-is-local-is-null
+  is-null-is-orthogonal-terminal-maps :
+    is-orthogonal (terminal-map Y) (terminal-map A) → is-null Y A
+  is-null-is-orthogonal-terminal-maps H =
+    is-null-is-local-terminal-map Y A
+      ( is-local-is-orthogonal-terminal-map (terminal-map Y) H)
+
+  is-orthogonal-terminal-maps-is-null :
+    is-null Y A → is-orthogonal (terminal-map Y) (terminal-map A)
+  is-orthogonal-terminal-maps-is-null H =
+    is-orthogonal-is-orthogonal-fiber-condition-right-map
+      ( terminal-map Y)
+      ( terminal-map A)
+      ( λ _ →
+        is-equiv-source-is-equiv-target-equiv-arrow
+          ( precomp (terminal-map Y) (fiber (terminal-map A) star))
+          ( diagonal-exponential A Y)
+          ( ( equiv-fiber-terminal-map star) ∘e
+            ( equiv-universal-property-unit (fiber (terminal-map A) star)) ,
+            ( equiv-postcomp Y (equiv-fiber-terminal-map star)) ,
+            ( refl-htpy))
+          ( H))
 ```
 
 ### A type is `f`-local if it is null at every fiber of `f`
diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
index b00240504a..1f47496951 100644
--- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
@@ -19,6 +19,7 @@ open import foundation.dependent-pair-types
 open import foundation.dependent-products-pullbacks
 open import foundation.dependent-sums-pullbacks
 open import foundation.equivalences
+open import foundation.equivalences-arrows
 open import foundation.fibered-maps
 open import foundation.fibers-of-maps
 open import foundation.function-extensionality
@@ -26,15 +27,18 @@ open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-fibers-of-maps
 open import foundation.homotopies
 open import foundation.morphisms-arrows
 open import foundation.postcomposition-functions
 open import foundation.postcomposition-pullbacks
+open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
 open import foundation.products-pullbacks
 open import foundation.propositions
 open import foundation.pullbacks
 open import foundation.type-arithmetic-dependent-function-types
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
 open import foundation.universal-property-cartesian-product-types
 open import foundation.universal-property-coproduct-types
@@ -64,7 +68,7 @@ The map `f : A → B` is said to be
    [lifting operation](orthogonal-factorization-systems.lifting-operations.md)
    between `f` and `g`.
 
-3. The following is a [pullback](foundation.pullbacks.md) square:
+3. The following is a [pullback](foundation-core.pullbacks.md) square:
 
    ```text
                 - ∘ f
@@ -76,7 +80,15 @@ The map `f : A → B` is said to be
                 - ∘ f
    ```
 
-4. The [fibers](foundation-core.fibers-of-maps.md) of `g` are
+4. The induced dependent precomposition map
+
+   ```text
+     - ∘ f : ((x : B) → fiber g (h x)) --> ((x : A) → fiber g (h (f x)))
+   ```
+
+   is an equivalence for every `h : B → Y`.
+
+5. The [fibers](foundation-core.fibers-of-maps.md) of `g` are
    [`f`-local](orthogonal-factorization-systems.local-types.md), i.e., `g` is an
    [`f`-local map](orthogonal-factorization-systems.local-maps.md).
 
@@ -188,6 +200,38 @@ module _
       ( cone-pullback-hom f g)
 ```
 
+### The fiber condition for orthogonal maps
+
+The maps `f` and `g` are orthogonal if and only if the induced family of maps on
+fibers
+
+```text
+                           (- ∘ f)
+   ((x : B) → fiber g (h x)) --> ((x : A) → fiber g (h (f x)))
+                      |               |
+                      |               |
+                      ∨    (- ∘ f)    ∨
+                   (B → X) ------> (A → X)
+                      |               |
+              (g ∘ -) |               | (g ∘ -)
+                      ∨    (- ∘ f)    ∨
+               h ∈ (B → Y) ------> (A → Y)
+```
+
+is an equivalence for every `h : B → Y`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
+  where
+
+  is-orthogonal-fiber-condition-right-map : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-orthogonal-fiber-condition-right-map =
+    (h : B → Y) → is-equiv (precomp-Π f (fiber g ∘ h))
+```
+
 ## Properties
 
 ### Being orthogonal means that the type of lifting squares is contractible
@@ -278,6 +322,68 @@ module _
         ( H))
 ```
 
+### Being orthogonal means satisfying the fiber condition for orthogonal maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
+  where
+
+  is-orthogonal-fiber-condition-right-map-is-orthogonal-pullback-condition :
+    is-orthogonal-pullback-condition f g →
+    is-orthogonal-fiber-condition-right-map f g
+  is-orthogonal-fiber-condition-right-map-is-orthogonal-pullback-condition H h =
+    is-equiv-source-is-equiv-target-equiv-arrow
+      ( precomp-Π f (fiber g ∘ h))
+      ( map-fiber-vertical-map-cone
+        ( precomp f Y)
+        ( postcomp A g)
+        ( cone-pullback-hom f g)
+        ( h))
+      ( compute-map-fiber-vertical-pullback-hom f g h)
+      ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+        ( precomp f Y)
+        ( postcomp A g)
+        ( cone-pullback-hom f g)
+        ( H)
+        ( h))
+
+  is-orthogonal-fiber-condition-right-map-is-orthogonal :
+    is-orthogonal f g →
+    is-orthogonal-fiber-condition-right-map f g
+  is-orthogonal-fiber-condition-right-map-is-orthogonal H =
+    is-orthogonal-fiber-condition-right-map-is-orthogonal-pullback-condition
+      ( is-orthogonal-pullback-condition-is-orthogonal f g H)
+
+  is-orthogonal-pullback-condition-is-orthogonal-fiber-condition-right-map :
+    is-orthogonal-fiber-condition-right-map f g →
+    is-orthogonal-pullback-condition f g
+  is-orthogonal-pullback-condition-is-orthogonal-fiber-condition-right-map H =
+    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone
+      ( precomp f Y)
+      ( postcomp A g)
+      ( cone-pullback-hom f g)
+      ( λ h →
+        is-equiv-target-is-equiv-source-equiv-arrow
+          ( precomp-Π f (fiber g ∘ h))
+          ( map-fiber-vertical-map-cone
+            ( precomp f Y)
+            ( postcomp A g)
+            ( cone-pullback-hom f g)
+            ( h))
+          ( compute-map-fiber-vertical-pullback-hom f g h)
+          ( H h))
+
+  is-orthogonal-is-orthogonal-fiber-condition-right-map :
+    is-orthogonal-fiber-condition-right-map f g →
+    is-orthogonal f g
+  is-orthogonal-is-orthogonal-fiber-condition-right-map H =
+    is-orthogonal-is-orthogonal-pullback-condition f g
+      ( is-orthogonal-pullback-condition-is-orthogonal-fiber-condition-right-map
+        ( H))
+```
+
 ### Orthogonality is preserved by homotopies
 
 ```agda
@@ -988,7 +1094,7 @@ module _
         ( is-orthogonal-pullback-condition-is-orthogonal f g G))
 ```
 
-### A type is `f`-local if and only if the terminal map is `f`-orthogonal
+### A type is `f`-local if and only if its terminal map is `f`-orthogonal
 
 **Proof (forward direction):** If the terminal map is right orthogonal to `f`,
 that means we have a pullback square