diff --git a/src/foundation/contractible-types.lagda.md b/src/foundation/contractible-types.lagda.md
index bfb117148d..34bcad6ead 100644
--- a/src/foundation/contractible-types.lagda.md
+++ b/src/foundation/contractible-types.lagda.md
@@ -23,6 +23,7 @@ open import foundation-core.contractible-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.propositions
 open import foundation-core.subtypes
@@ -197,7 +198,7 @@ module _
       is-equiv-is-invertible
         ( ev-point' (center H))
         ( λ f → eq-htpy (λ x → ap f (contraction H x)))
-        ( λ x → refl)
+        ( refl-htpy)
 
   equiv-diagonal-exponential-is-contr :
     {l : Level} (X : UU l) → is-contr A → X ≃ (A → X)
@@ -205,4 +206,26 @@ module _
     diagonal-exponential X A
   pr2 (equiv-diagonal-exponential-is-contr X H) =
     is-equiv-diagonal-exponential-is-contr H X
+
+  abstract
+    is-equiv-diagonal-exponential-is-contr' :
+      is-contr A →
+      {l : Level} (X : UU l) → is-equiv (diagonal-exponential A X)
+    is-equiv-diagonal-exponential-is-contr' H X =
+      is-equiv-is-invertible
+        ( λ _ → center H)
+        ( λ x → eq-htpy (contraction H ∘ x))
+        ( contraction H)
+
+  equiv-diagonal-exponential-is-contr' :
+    {l : Level} (X : UU l) → is-contr A → A ≃ (X → A)
+  equiv-diagonal-exponential-is-contr' X H =
+    ( diagonal-exponential A X , is-equiv-diagonal-exponential-is-contr' H X)
+
+  abstract
+    is-contr-is-equiv-diagonal-exponential' :
+      ({l : Level} (X : UU l) → is-equiv (diagonal-exponential A X)) →
+      is-contr A
+    is-contr-is-equiv-diagonal-exponential' H =
+      is-contr-is-equiv-self-diagonal-exponential (H A)
 ```
diff --git a/src/foundation/diagonal-maps-of-types.lagda.md b/src/foundation/diagonal-maps-of-types.lagda.md
index b4a0135888..d0651b3b44 100644
--- a/src/foundation/diagonal-maps-of-types.lagda.md
+++ b/src/foundation/diagonal-maps-of-types.lagda.md
@@ -20,6 +20,7 @@ open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.constant-maps
+open import foundation-core.contractible-types
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
@@ -70,7 +71,7 @@ module _
     inv-htpy htpy-diagonal-exponential-Id-ap-diagonal-exponential-htpy-eq
 ```
 
-### Given an element of the exponent the diagonal map is injective
+### If the exponent has an element then the diagonal map is injective
 
 ```agda
 module _
@@ -86,7 +87,7 @@ module _
   pr2 diagonal-exponential-injection = is-injective-diagonal-exponential
 ```
 
-### The action on identifications of an (exponential) diagonal is a diagonal
+### The action on identifications of a diagonal is a diagonal
 
 ```agda
 module _
diff --git a/src/group-theory/invertible-elements-monoids.lagda.md b/src/group-theory/invertible-elements-monoids.lagda.md
index cece924e20..1a27aa4589 100644
--- a/src/group-theory/invertible-elements-monoids.lagda.md
+++ b/src/group-theory/invertible-elements-monoids.lagda.md
@@ -33,7 +33,7 @@ An element `x : M` in a [monoid](group-theory.monoids.md) `M` is said to be
 is said to be **right invertible** if there is an element `y : M` such that
 `xy ＝ e`. The element `x` is said to be
 {{#concept "invertible" WD="invertible element" WDID=Q67474638 Agda=is-invertible-element-Monoid}}
-if it has a two-sided inverse, i.e., if if there is an element `y : M` such that
+if it has a two-sided inverse, i.e., if there is an element `y : M` such that
 `xy = e` and `yx = e`. Left inverses of elements are also called **retractions**
 and right inverses are also called **sections**.
 
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index a2928944db..6a1e039af0 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -13,11 +13,15 @@ open import orthogonal-factorization-systems.anodyne-maps public
 open import orthogonal-factorization-systems.cd-structures public
 open import orthogonal-factorization-systems.cellular-maps public
 open import orthogonal-factorization-systems.closed-modalities public
+open import orthogonal-factorization-systems.connected-maps-at-subuniverses public
+open import orthogonal-factorization-systems.connected-maps-at-subuniverses-over-type public
+open import orthogonal-factorization-systems.connected-types-at-subuniverses public
 open import orthogonal-factorization-systems.continuation-modalities public
 open import orthogonal-factorization-systems.double-lifts-families-of-elements public
 open import orthogonal-factorization-systems.double-negation-sheaves public
 open import orthogonal-factorization-systems.equality-extensions-dependent-maps public
 open import orthogonal-factorization-systems.equality-extensions-maps public
+open import orthogonal-factorization-systems.equivalences-at-subuniverses public
 open import orthogonal-factorization-systems.extensions-dependent-maps public
 open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public
 open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public
diff --git a/src/orthogonal-factorization-systems/connected-maps-at-subuniverses-over-type.lagda.md b/src/orthogonal-factorization-systems/connected-maps-at-subuniverses-over-type.lagda.md
new file mode 100644
index 0000000000..1e5fc15893
--- /dev/null
+++ b/src/orthogonal-factorization-systems/connected-maps-at-subuniverses-over-type.lagda.md
@@ -0,0 +1,128 @@
+# `K`-connected maps over a type, with respect to a subuniverse `K`
+
+```agda
+module orthogonal-factorization-systems.connected-maps-at-subuniverses-over-type where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.structure-identity-principle
+open import foundation.subuniverses
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.torsorial-type-families
+
+open import orthogonal-factorization-systems.connected-maps-at-subuniverses
+```
+
+</details>
+
+## Idea
+
+Given a [subuniverse](foundation.subuniverses.md) `K` we consider the type of
+`K`-[connected maps](orthogonal-factorization-systems.connected-maps-at-subuniverses.md)
+into a type `X`. I.e., the collection of types `A`
+[equipped](foundation.structure.md) with `K`-connected maps from `A` into `X`.
+
+## Definitions
+
+### The type of `K`-connected maps over a type
+
+```agda
+Subuniverse-Connected-Map :
+  {l1 l2 l3 : Level} (l4 : Level) (K : subuniverse l1 l2) (A : UU l3) →
+  UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4)
+Subuniverse-Connected-Map l4 K A = Σ (UU l4) (subuniverse-connected-map K A)
+
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} (f : Subuniverse-Connected-Map l4 K A)
+  where
+
+  type-Subuniverse-Connected-Map : UU l4
+  type-Subuniverse-Connected-Map = pr1 f
+
+  subuniverse-connected-map-Subuniverse-Connected-Map :
+    subuniverse-connected-map K A type-Subuniverse-Connected-Map
+  subuniverse-connected-map-Subuniverse-Connected-Map = pr2 f
+
+  map-Subuniverse-Connected-Map : A → type-Subuniverse-Connected-Map
+  map-Subuniverse-Connected-Map =
+    map-subuniverse-connected-map K
+      ( subuniverse-connected-map-Subuniverse-Connected-Map)
+
+  is-subuniverse-connected-map-Subuniverse-Connected-Map :
+    is-subuniverse-connected-map K map-Subuniverse-Connected-Map
+  is-subuniverse-connected-map-Subuniverse-Connected-Map =
+    is-subuniverse-connected-map-subuniverse-connected-map K
+      ( subuniverse-connected-map-Subuniverse-Connected-Map)
+```
+
+## Properties
+
+### Characterization of equality
+
+```agda
+equiv-Subuniverse-Connected-Map :
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} →
+  (f g : Subuniverse-Connected-Map l4 K A) → UU (l3 ⊔ l4)
+equiv-Subuniverse-Connected-Map K f g =
+  Σ ( type-Subuniverse-Connected-Map K f ≃ type-Subuniverse-Connected-Map K g)
+    ( λ e →
+      map-equiv e ∘ map-Subuniverse-Connected-Map K f ~
+      map-Subuniverse-Connected-Map K g)
+
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3}
+  (f : Subuniverse-Connected-Map l4 K A)
+  where
+
+  id-equiv-Subuniverse-Connected-Map : equiv-Subuniverse-Connected-Map K f f
+  id-equiv-Subuniverse-Connected-Map = (id-equiv , refl-htpy)
+
+  abstract
+    is-torsorial-equiv-Subuniverse-Connected-Map :
+      is-torsorial (equiv-Subuniverse-Connected-Map K f)
+    is-torsorial-equiv-Subuniverse-Connected-Map =
+      is-torsorial-Eq-structure
+        ( is-torsorial-equiv (type-Subuniverse-Connected-Map K f))
+        ( type-Subuniverse-Connected-Map K f , id-equiv)
+        ( is-torsorial-htpy-subuniverse-connected-map K
+          ( subuniverse-connected-map-Subuniverse-Connected-Map K f))
+
+  equiv-eq-Subuniverse-Connected-Map :
+    (g : Subuniverse-Connected-Map l4 K A) →
+    f ＝ g → equiv-Subuniverse-Connected-Map K f g
+  equiv-eq-Subuniverse-Connected-Map .f refl =
+    id-equiv-Subuniverse-Connected-Map
+
+  abstract
+    is-equiv-equiv-eq-Subuniverse-Connected-Map :
+      (g : Subuniverse-Connected-Map l4 K A) →
+      is-equiv (equiv-eq-Subuniverse-Connected-Map g)
+    is-equiv-equiv-eq-Subuniverse-Connected-Map =
+      fundamental-theorem-id
+        ( is-torsorial-equiv-Subuniverse-Connected-Map)
+        ( equiv-eq-Subuniverse-Connected-Map)
+
+  extensionality-Subuniverse-Connected-Map :
+    (g : Subuniverse-Connected-Map l4 K A) →
+    (f ＝ g) ≃ equiv-Subuniverse-Connected-Map K f g
+  extensionality-Subuniverse-Connected-Map g =
+    ( equiv-eq-Subuniverse-Connected-Map g ,
+      is-equiv-equiv-eq-Subuniverse-Connected-Map g)
+
+  eq-equiv-Subuniverse-Connected-Map :
+    (g : Subuniverse-Connected-Map l4 K A) →
+    equiv-Subuniverse-Connected-Map K f g → f ＝ g
+  eq-equiv-Subuniverse-Connected-Map g =
+    map-inv-equiv (extensionality-Subuniverse-Connected-Map g)
+```
diff --git a/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md b/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md
new file mode 100644
index 0000000000..191cb040a6
--- /dev/null
+++ b/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md
@@ -0,0 +1,870 @@
+# `K`-Connected maps, with respect to a subuniverse `K`
+
+```agda
+module orthogonal-factorization-systems.connected-maps-at-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.dependent-universal-property-equivalences
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.function-extensionality
+open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-coproduct-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopy-induction
+open import foundation.inhabited-types
+open import foundation.precomposition-dependent-functions
+open import foundation.precomposition-functions
+open import foundation.propositional-truncations
+open import foundation.retracts-of-maps
+open import foundation.sections
+open import foundation.split-surjective-maps
+open import foundation.subtype-identity-principle
+open import foundation.subuniverses
+open import foundation.surjective-maps
+open import foundation.unit-type
+open import foundation.universal-property-coproduct-types
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universal-property-family-of-fibers-of-maps
+open import foundation.universal-property-unit-type
+open import foundation.universe-levels
+
+open import foundation-core.contractible-maps
+open import foundation-core.embeddings
+open import foundation-core.fibers-of-maps
+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.injective-maps
+open import foundation-core.propositions
+open import foundation-core.subtypes
+open import foundation-core.torsorial-type-families
+
+open import orthogonal-factorization-systems.connected-types-at-subuniverses
+open import orthogonal-factorization-systems.equivalences-at-subuniverses
+open import orthogonal-factorization-systems.extensions-dependent-maps
+open import orthogonal-factorization-systems.localizations-at-subuniverses
+
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.dependent-pullback-property-pushouts
+open import synthetic-homotopy-theory.pushouts
+```
+
+</details>
+
+## Idea
+
+Given a [subuniverse](foundation.subuniverses.md) `K`, a map `f : A → B` is said
+to be
+{{#concept "`K`-connected" Disambiguation="map of types, with respect to a subuniverse" Agda=is-subuniverse-connected-map}}
+if it satisfies the
+{{#concept "universal property" Disambiguation="subuniverse connected map of types"}}
+of `K`-connected maps:
+
+For every `K`-valued family `U` over `B`, the
+[dependent precomposition map](foundation-core.precomposition-dependent-functions.md)
+
+```text
+ - ∘ f : ((b : B) → U b) → ((a : A) → U (f a))
+```
+
+is an [equivalence](foundation-core.equivalences.md).
+
+We give a series of increasingly stronger conditions for a map `f` to be
+`K`-connected. In particular, if `unit ∈ K`, then condition 4 recovers the usual
+definition of a `K`-connected map as in Definition 5.5.1 {{#cite Rij19}}, i.e.,
+as a map whose [fibers](foundation-core.fibers-of-maps.md) have
+[contractible](foundation-core.contractible-types.md)
+`K`-[localizations](orthogonal-factorization-systems.localizations-at-subuniverses.md).
+
+1.  The map `f` is `K`-connected.
+2.  For every `K`-valued family `U` over `B` and every map
+    `u : (x : A) → U (f x)`, the type of
+    [extensions](orthogonal-factorization-systems.extensions-dependent-maps.md)
+    of `u` along `f` is contractible.
+3.  The map `f` is
+    [left orthogonal](orthogonal-factorization-systems.orthogonal-maps.md) to
+    maps `h : C → B` whose fibers are in `K`.
+4.  The [terminal projections](foundation.unit-type.md) of the fibers of `f` are
+    `K`-[equivalences](orthogonal-factorization-systems.equivalences-at-subuniverses.md).
+5.  The fibers of `f` are `K`-connected in the sense that for every `U` in `K`,
+    the [diagonal map](foundation.diagonal-maps-of-types.md)
+    `U → (fiber f y → U)` is an equivalence.
+6.  Every fiber of `f` satisfies the condition that for every `U` in `K` and
+    every function `u : fiber f y → U` there
+    [uniquely exists](foundation.uniqueness-quantification.md) an element
+    `v : U` such that `const v ~ u`.
+7.  The fibers of `f` have `K`-localizations, and for every `y` there
+    [merely exists](foundation.existential-quantification.md) a
+    `u : K(fiber f y)` such that for all `a` and `p : f a ＝ y` we have a
+    [dependent identification](foundation-core.dependent-identifications.md)
+    over `p`
+    ```text
+      u ＝ₚ^[y ↦ K(fiber f y)] (η (f a) (a , refl))
+    ```
+8.  The fibers of `f` have `K`-localizations, and the dependent precomposition
+    map of `f` is [surjective](foundation.surjective-maps.md) at every
+    `K`-valued family `U` over `B`.
+9.  The fibers of `f` have `K`-localizations, and the dependent precomposition
+    map of `f` has a [section](foundation-core.sections.md) at every `K`-valued
+    family `U` over `B`.
+
+If the fibers of `f` have `K`-localizations then these conditions are all
+[equivalent](foundation.logical-equivalences.md). More generally we always have
+that conditions 1-3 are equivalent, conditions 4-6 are equivalent, and
+conditions 7-9 are equivalent.
+
+## Definitions
+
+### The predicate on maps of being `K`-connected
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} {B : UU l4}
+  (f : A → B)
+  where
+
+  is-subuniverse-connected-map-Prop : Prop (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-subuniverse-connected-map-Prop =
+    Π-Prop
+      ( B → type-subuniverse K)
+      ( λ U → is-equiv-Prop (precomp-Π f (pr1 ∘ U)))
+
+  is-subuniverse-connected-map : UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-subuniverse-connected-map =
+    (U : B → type-subuniverse K) → is-equiv (precomp-Π f (pr1 ∘ U))
+
+  is-prop-is-subuniverse-connected-map :
+    is-prop is-subuniverse-connected-map
+  is-prop-is-subuniverse-connected-map =
+    is-prop-type-Prop is-subuniverse-connected-map-Prop
+```
+
+### The type of `K`-connected maps between two types
+
+```agda
+subuniverse-connected-map :
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) →
+  UU l3 → UU l4 → UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+subuniverse-connected-map K A B =
+  type-subtype (is-subuniverse-connected-map-Prop K {A} {B})
+
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} {B : UU l4}
+  where
+
+  map-subuniverse-connected-map : subuniverse-connected-map K A B → A → B
+  map-subuniverse-connected-map =
+    inclusion-subtype (is-subuniverse-connected-map-Prop K)
+
+  is-subuniverse-connected-map-subuniverse-connected-map :
+    (f : subuniverse-connected-map K A B) →
+    is-subuniverse-connected-map K (map-subuniverse-connected-map f)
+  is-subuniverse-connected-map-subuniverse-connected-map =
+    is-in-subtype-inclusion-subtype (is-subuniverse-connected-map-Prop K)
+
+  emb-inclusion-subuniverse-connected-map :
+    subuniverse-connected-map K A B ↪ (A → B)
+  emb-inclusion-subuniverse-connected-map =
+    emb-subtype (is-subuniverse-connected-map-Prop K)
+```
+
+### The extension condition of `K`-connected maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-connected-map-extension-condition :
+    UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-subuniverse-connected-map-extension-condition =
+    (U : B → type-subuniverse K) (u : (x : A) → pr1 (U (f x))) →
+    is-contr (extension-dependent-map f (pr1 ∘ U) u)
+
+  abstract
+    is-prop-is-subuniverse-connected-map-extension-condition :
+      is-prop is-subuniverse-connected-map-extension-condition
+    is-prop-is-subuniverse-connected-map-extension-condition =
+      is-prop-Π (λ U → is-prop-Π (λ u → is-property-is-contr))
+
+  is-subuniverse-connected-map-extension-condition-Prop :
+    Prop (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-subuniverse-connected-map-extension-condition-Prop =
+    ( is-subuniverse-connected-map-extension-condition ,
+      is-prop-is-subuniverse-connected-map-extension-condition)
+```
+
+## Properties
+
+### Equivalent characterizations of `K`-connected maps
+
+#### Extension condition
+
+A map `f : A → B` is `K`-connected if and only if, for every `K`-valued family
+`U` over `B` and every map `u : (x : A) → U (f x)`, the type of dependent
+extensions of `u` along `f` is contractible.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-connected-map-is-subuniverse-connected-map-extension-condition :
+    is-subuniverse-connected-map-extension-condition K f →
+    is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-is-subuniverse-connected-map-extension-condition
+    H U =
+    is-equiv-is-contr-map
+      ( λ u →
+        is-contr-equiv
+          ( extension-dependent-map f (pr1 ∘ U) u)
+          ( compute-extension-fiber-precomp-Π f (pr1 ∘ U) u)
+          ( H U u))
+
+  is-subuniverse-connected-map-extension-condition-is-subuniverse-connected-map :
+    is-subuniverse-connected-map K f →
+    is-subuniverse-connected-map-extension-condition K f
+  is-subuniverse-connected-map-extension-condition-is-subuniverse-connected-map
+    H U u =
+    is-contr-equiv'
+      ( fiber (precomp-Π f (pr1 ∘ U)) u)
+      ( compute-extension-fiber-precomp-Π f (pr1 ∘ U) u)
+      ( is-contr-map-is-equiv (H U) u)
+```
+
+#### Contractible fiber-localization condition
+
+Given a subuniverse `K` then a map `f` is `K`-connected if the fibers are
+`K`-equivalent to contractible types.
+
+**Proof.** We have an equivalence of arrows
+
+```text
+                               ~
+    ((b : B) → unit → U b) --------> ((b : B) → U b)
+               |                            |
+               |                            | precomp-Π f U
+               |                            |
+               ∨               ~            ∨
+  ((b : B) → fiber f b → U b) ---> ((a : A) → U (f a))
+```
+
+where the left-hand map is
+`map-Π (λ b → precomp (terminal-map (fiber f b)) (U b))`, hence if each terminal
+map is a `K`-equivalence then this is an equivalence as well. ∎
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-connected-map-is-subuniverse-equiv-terminal-map-fibers :
+    ((b : B) → is-subuniverse-equiv K (terminal-map (fiber f b))) →
+    is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-is-subuniverse-equiv-terminal-map-fibers H U =
+    is-equiv-target-is-equiv-source-equiv-arrow
+      ( map-Π (λ b → precomp (terminal-map (fiber f b)) (pr1 (U b))))
+      ( precomp-Π f (pr1 ∘ U))
+      ( ( equiv-Π-equiv-family
+          ( λ b → equiv-universal-property-unit (pr1 (U b)))) ,
+        ( equiv-universal-property-family-of-fibers f (pr1 ∘ U)) ,
+        ( refl-htpy))
+      ( is-equiv-map-Π-is-fiberwise-equiv (λ b → H b (U b)))
+```
+
+#### Fiber condition
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-connected-map-is-subuniverse-connected-fibers :
+    ( (b : B) → is-subuniverse-connected K (fiber f b)) →
+    is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-is-subuniverse-connected-fibers H =
+    is-subuniverse-connected-map-is-subuniverse-equiv-terminal-map-fibers K f
+      ( is-subuniverse-equiv-terminal-map-is-subuniverse-connected K ∘ H)
+```
+
+#### Constancy condition on fibers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-connected-map-is-subuniverse-connected-const-condition-fibers :
+    ( (b : B) → is-subuniverse-connected-const-condition K (fiber f b)) →
+    is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-is-subuniverse-connected-const-condition-fibers
+    H =
+    is-subuniverse-connected-map-is-subuniverse-connected-fibers K f
+      ( λ b →
+        is-subuniverse-connected-is-subuniverse-connected-const-condition K
+          ( H b))
+```
+
+#### Section condition
+
+A map is `K`-connected if and only if its dependent precomposition maps admit
+sections and the fibers have `K`-localizations.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  (Kfib : B → UU l3) (η : (b : B) → fiber f b → Kfib b)
+  (is-htpy-injective-precomp-η-Kfib :
+    (b : B) {g h : Kfib b → Kfib b} →
+    precomp (η b) (Kfib b) g ~ precomp (η b) (Kfib b) h → g ~ h)
+  where
+
+  abstract
+    is-contr-subuniverse-localization-fiber-has-section-precomp-Π'' :
+      ( dependent-product-fiber-precomp-Π' f Kfib (λ a → η (f a) (a , refl))) →
+      ((b : B) → is-contr (Kfib b))
+    is-contr-subuniverse-localization-fiber-has-section-precomp-Π'' Fη b =
+        ( pr1 (Fη b) ,
+          is-htpy-injective-precomp-η-Kfib b
+            ( λ where (a , refl) → pr2 (Fη b) (a , refl)))
+
+  abstract
+    is-contr-subuniverse-localization-fiber-has-section-precomp-Π' :
+      fiber (precomp-Π f Kfib) (λ a → η (f a) (a , refl)) →
+      ((b : B) → is-contr (Kfib b))
+    is-contr-subuniverse-localization-fiber-has-section-precomp-Π' (s , H) b =
+      ( s b ,
+        is-htpy-injective-precomp-η-Kfib b (λ where (a , refl) → htpy-eq H a))
+
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  (Kfib : (b : B) → subuniverse-localization K (fiber f b))
+  (s : (U : B → type-subuniverse K) → section (precomp-Π f (pr1 ∘ U)))
+  where
+
+  is-contr-subuniverse-localization-fiber-has-section-precomp-Π :
+    ((b : B) → is-contr (pr1 (Kfib b)))
+  is-contr-subuniverse-localization-fiber-has-section-precomp-Π =
+    is-contr-subuniverse-localization-fiber-has-section-precomp-Π' f
+      ( type-subuniverse-localization K ∘ Kfib)
+      ( unit-subuniverse-localization K ∘ Kfib)
+      ( λ b H →
+        htpy-eq
+          ( is-injective-is-equiv
+            ( is-subuniverse-equiv-unit-subuniverse-localization K (Kfib b)
+              ( type-subuniverse-subuniverse-localization K (Kfib b)))
+            ( eq-htpy H)))
+      ( is-split-surjective-section
+        ( precomp-Π f (type-subuniverse-localization K ∘ Kfib))
+        ( s (type-subuniverse-subuniverse-localization K ∘ Kfib))
+        ( λ a → unit-subuniverse-localization K (Kfib (f a)) (a , refl)))
+
+  is-subuniverse-equiv-terminal-map-fibers-has-section-precomp-Π :
+    (b : B) → is-subuniverse-equiv K (terminal-map (fiber f b))
+  is-subuniverse-equiv-terminal-map-fibers-has-section-precomp-Π b =
+    is-subuniverse-equiv-comp K
+      ( terminal-map (type-subuniverse-localization K (Kfib b)))
+      ( unit-subuniverse-localization K (Kfib b))
+      ( is-subuniverse-equiv-unit-subuniverse-localization K (Kfib b))
+      ( is-subuniverse-equiv-is-equiv K
+        ( terminal-map (type-subuniverse-localization K (Kfib b)))
+        ( is-equiv-terminal-map-is-contr
+          ( is-contr-subuniverse-localization-fiber-has-section-precomp-Π b)))
+
+  is-subuniverse-connected-map-has-section-precomp-Π :
+    is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-has-section-precomp-Π =
+    is-subuniverse-connected-map-is-subuniverse-equiv-terminal-map-fibers K f
+      ( is-subuniverse-equiv-terminal-map-fibers-has-section-precomp-Π)
+```
+
+#### Surjection condition
+
+A map is `K`-connected if its dependent precomposition maps are surjective and
+the fibers have `K`-localizations.
+
+In fact, it suffices that the fibers have `K`-localizations and that for every
+`y` there merely exists a `u : K(fiber f y)` such that for all `a` and
+`p : f a ＝ y` we have a dependent identification over `p`
+
+```text
+  u ＝ₚ^[y ↦ K(fiber f y)] (η (f a) (a , refl)).
+```
+
+This is in turn a slightly weaker condition than inhabitedness of the fiber of
+`precomp-Π f` over the map `a ↦ η (f a) (a , refl)`.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  (Kfib : B → UU l3)
+  (η : (b : B) → fiber f b → Kfib b)
+  (is-htpy-injective-precomp-η-Kfib :
+    (b : B) {g h : Kfib b → Kfib b} →
+    precomp (η b) (Kfib b) g ~ precomp (η b) (Kfib b) h → g ~ h)
+  where
+
+  abstract
+    is-contr-subuniverse-localization-fiber-is-inhabited-family-dependent-product-fiber-precomp-Π' :
+      ( (b : B) →
+        is-inhabited
+          ( family-dependent-product-fiber-precomp-Π' f Kfib
+            ( λ a → η (f a) (a , refl))
+            ( b))) →
+      ((b : B) → is-contr (Kfib b))
+    is-contr-subuniverse-localization-fiber-is-inhabited-family-dependent-product-fiber-precomp-Π'
+      Fη b =
+      rec-trunc-Prop
+        ( is-contr-Prop (Kfib b))
+        ( λ (sb , Hb) →
+          ( sb ,
+            is-htpy-injective-precomp-η-Kfib b
+              ( λ where (a , refl) → Hb (a , refl))))
+        ( Fη b)
+
+  is-contr-subuniverse-localization-fiber-is-inhabited-fiber-precomp-Π :
+    is-inhabited (fiber (precomp-Π f Kfib) (λ a → η (f a) (a , refl))) →
+    ((b : B) → is-contr (Kfib b))
+  is-contr-subuniverse-localization-fiber-is-inhabited-fiber-precomp-Π
+    s b =
+    rec-trunc-Prop
+      ( is-contr-Prop (Kfib b))
+      ( λ s →
+        is-contr-subuniverse-localization-fiber-has-section-precomp-Π'
+          f Kfib η is-htpy-injective-precomp-η-Kfib s b)
+      ( s)
+
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  (Kfib : (b : B) → subuniverse-localization K (fiber f b))
+  where
+
+  is-contr-subuniverse-localization-fiber-is-inhabited-family-dependent-product-fiber-precomp-Π :
+    ( (b : B) →
+      is-inhabited
+        ( family-dependent-product-fiber-precomp-Π' f
+          ( type-subuniverse-localization K ∘ Kfib)
+          ( λ a → unit-subuniverse-localization K (Kfib (f a)) (a , refl))
+          ( b))) →
+    ((b : B) → is-contr (type-subuniverse-localization K (Kfib b)))
+  is-contr-subuniverse-localization-fiber-is-inhabited-family-dependent-product-fiber-precomp-Π =
+    is-contr-subuniverse-localization-fiber-is-inhabited-family-dependent-product-fiber-precomp-Π'
+      ( f)
+      ( type-subuniverse-localization K ∘ Kfib)
+      ( unit-subuniverse-localization K ∘ Kfib)
+      ( λ b H →
+        htpy-eq
+          ( is-injective-is-equiv
+            ( is-subuniverse-equiv-unit-subuniverse-localization K (Kfib b)
+              ( type-subuniverse-subuniverse-localization K (Kfib b)))
+            ( eq-htpy H)))
+
+  is-subuniverse-equiv-terminal-map-fibers-is-inhabited-family-dependent-product-fiber-precomp-Π :
+    ( (b : B) →
+      is-inhabited
+        ( family-dependent-product-fiber-precomp-Π' f
+          ( type-subuniverse-localization K ∘ Kfib)
+          ( λ a → unit-subuniverse-localization K (Kfib (f a)) (a , refl))
+          ( b))) →
+    (b : B) → is-subuniverse-equiv K (terminal-map (fiber f b))
+  is-subuniverse-equiv-terminal-map-fibers-is-inhabited-family-dependent-product-fiber-precomp-Π
+    s b =
+    is-subuniverse-equiv-comp K
+      ( terminal-map (type-subuniverse-localization K (Kfib b)))
+      ( unit-subuniverse-localization K (Kfib b))
+      ( is-subuniverse-equiv-unit-subuniverse-localization K (Kfib b))
+      ( is-subuniverse-equiv-is-equiv K
+        ( terminal-map (type-subuniverse-localization K (Kfib b)))
+        ( is-equiv-terminal-map-is-contr
+          ( is-contr-subuniverse-localization-fiber-is-inhabited-family-dependent-product-fiber-precomp-Π
+            s b)))
+
+  is-subuniverse-connected-map-is-inhabited-family-dependent-product-fiber-precomp-Π :
+    ( (b : B) →
+      is-inhabited
+        ( family-dependent-product-fiber-precomp-Π' f
+          ( type-subuniverse-localization K ∘ Kfib)
+          ( λ a → unit-subuniverse-localization K (Kfib (f a)) (a , refl))
+          ( b))) →
+    is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-is-inhabited-family-dependent-product-fiber-precomp-Π
+    Fη =
+    is-subuniverse-connected-map-is-subuniverse-equiv-terminal-map-fibers K f
+      ( is-subuniverse-equiv-terminal-map-fibers-is-inhabited-family-dependent-product-fiber-precomp-Π
+        ( Fη))
+
+  is-contr-subuniverse-localization-fiber-is-surjective-precomp-Π :
+    ((U : B → type-subuniverse K) → is-surjective (precomp-Π f (pr1 ∘ U))) →
+    ((b : B) → is-contr (pr1 (Kfib b)))
+  is-contr-subuniverse-localization-fiber-is-surjective-precomp-Π H =
+    is-contr-subuniverse-localization-fiber-is-inhabited-fiber-precomp-Π f
+      ( type-subuniverse-localization K ∘ Kfib)
+      ( unit-subuniverse-localization K ∘ Kfib)
+      ( λ b H →
+        htpy-eq
+          ( is-injective-is-equiv
+            ( is-subuniverse-equiv-unit-subuniverse-localization K (Kfib b)
+              ( type-subuniverse-subuniverse-localization K (Kfib b)))
+            ( eq-htpy H)))
+      ( H ( type-subuniverse-subuniverse-localization K ∘ Kfib)
+          ( λ a → unit-subuniverse-localization K (Kfib (f a)) (a , refl)))
+
+  is-subuniverse-equiv-terminal-map-fibers-is-surjective-precomp-Π :
+    ((U : B → type-subuniverse K) → is-surjective (precomp-Π f (pr1 ∘ U))) →
+    (b : B) → is-subuniverse-equiv K (terminal-map (fiber f b))
+  is-subuniverse-equiv-terminal-map-fibers-is-surjective-precomp-Π H b =
+    is-subuniverse-equiv-comp K
+      ( terminal-map (type-subuniverse-localization K (Kfib b)))
+      ( unit-subuniverse-localization K (Kfib b))
+      ( is-subuniverse-equiv-unit-subuniverse-localization K (Kfib b))
+      ( is-subuniverse-equiv-is-equiv K
+        ( terminal-map (type-subuniverse-localization K (Kfib b)))
+        ( is-equiv-terminal-map-is-contr
+          ( is-contr-subuniverse-localization-fiber-is-surjective-precomp-Π
+              H b)))
+
+  is-subuniverse-connected-map-is-surjective-precomp-Π :
+    ((U : B → type-subuniverse K) → is-surjective (precomp-Π f (pr1 ∘ U))) →
+    is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-is-surjective-precomp-Π H =
+    is-subuniverse-connected-map-is-subuniverse-equiv-terminal-map-fibers K f
+      ( is-subuniverse-equiv-terminal-map-fibers-is-surjective-precomp-Π H)
+```
+
+### Characterizing equality of `K`-connected maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} {B : UU l4}
+  where
+
+  htpy-subuniverse-connected-map :
+    (f g : subuniverse-connected-map K A B) → UU (l3 ⊔ l4)
+  htpy-subuniverse-connected-map f g =
+    map-subuniverse-connected-map K f ~ map-subuniverse-connected-map K g
+
+  refl-htpy-subuniverse-connected-map :
+    (f : subuniverse-connected-map K A B) → htpy-subuniverse-connected-map f f
+  refl-htpy-subuniverse-connected-map f = refl-htpy
+
+  abstract
+    is-torsorial-htpy-subuniverse-connected-map :
+      (f : subuniverse-connected-map K A B) →
+      is-torsorial (htpy-subuniverse-connected-map f)
+    is-torsorial-htpy-subuniverse-connected-map f =
+      is-torsorial-Eq-subtype
+        ( is-torsorial-htpy (map-subuniverse-connected-map K f))
+        ( is-prop-is-subuniverse-connected-map K)
+        ( map-subuniverse-connected-map K f)
+        ( refl-htpy-subuniverse-connected-map f)
+        ( is-subuniverse-connected-map-subuniverse-connected-map K f)
+
+  htpy-eq-subuniverse-connected-map :
+    (f g : subuniverse-connected-map K A B) →
+    f ＝ g → htpy-subuniverse-connected-map f g
+  htpy-eq-subuniverse-connected-map f g H = htpy-eq (ap pr1 H)
+
+  abstract
+    is-equiv-htpy-eq-subuniverse-connected-map :
+      (f g : subuniverse-connected-map K A B) →
+      is-equiv (htpy-eq-subuniverse-connected-map f g)
+    is-equiv-htpy-eq-subuniverse-connected-map f =
+      fundamental-theorem-id
+        ( is-torsorial-htpy-subuniverse-connected-map f)
+        ( htpy-eq-subuniverse-connected-map f)
+
+  extensionality-subuniverse-connected-map :
+    (f g : subuniverse-connected-map K A B) →
+    (f ＝ g) ≃ htpy-subuniverse-connected-map f g
+  pr1 (extensionality-subuniverse-connected-map f g) =
+    htpy-eq-subuniverse-connected-map f g
+  pr2 (extensionality-subuniverse-connected-map f g) =
+    is-equiv-htpy-eq-subuniverse-connected-map f g
+
+  eq-htpy-subuniverse-connected-map :
+    (f g : subuniverse-connected-map K A B) →
+    htpy-subuniverse-connected-map f g → (f ＝ g)
+  eq-htpy-subuniverse-connected-map f g =
+    map-inv-equiv (extensionality-subuniverse-connected-map f g)
+```
+
+### All maps are `Contr`-connected
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-Contr-connected-map : is-subuniverse-connected-map (is-contr-Prop {l3}) f
+  is-Contr-connected-map U =
+    is-equiv-is-contr
+      ( precomp-Π f (pr1 ∘ U))
+      ( is-contr-Π (pr2 ∘ U))
+      ( is-contr-Π (pr2 ∘ U ∘ f))
+```
+
+### Equivalences are `K`-connected for any `K`
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} {B : UU l4}
+  where
+
+  is-subuniverse-connected-map-is-equiv :
+    {f : A → B} → is-equiv f → is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-is-equiv H U =
+    is-equiv-precomp-Π-is-equiv H (pr1 ∘ U)
+
+  is-subuniverse-connected-map-equiv :
+    (e : A ≃ B) → is-subuniverse-connected-map K (map-equiv e)
+  is-subuniverse-connected-map-equiv e =
+    is-subuniverse-connected-map-is-equiv (is-equiv-map-equiv e)
+
+  subuniverse-connected-map-equiv :
+    (A ≃ B) → subuniverse-connected-map K A B
+  subuniverse-connected-map-equiv e =
+    ( map-equiv e , is-subuniverse-connected-map-equiv e)
+```
+
+### `K`-connected maps are `K`-equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-equiv-is-subuniverse-connected-map :
+    is-subuniverse-connected-map K f → is-subuniverse-equiv K f
+  is-subuniverse-equiv-is-subuniverse-connected-map F U = F (λ _ → U)
+```
+
+### The composition of two `K`-connected maps is `K`-connected
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {C : UU l5}
+  where
+
+  is-subuniverse-connected-map-comp :
+    {g : B → C} {f : A → B} →
+    is-subuniverse-connected-map K g →
+    is-subuniverse-connected-map K f →
+    is-subuniverse-connected-map K (g ∘ f)
+  is-subuniverse-connected-map-comp {g} {f} G F U =
+    is-equiv-comp
+      ( precomp-Π f (pr1 ∘ U ∘ g))
+      ( precomp-Π g (pr1 ∘ U))
+      ( G U)
+      ( F (U ∘ g))
+
+  comp-subuniverse-connected-map :
+    subuniverse-connected-map K B C →
+    subuniverse-connected-map K A B →
+    subuniverse-connected-map K A C
+  pr1 (comp-subuniverse-connected-map g f) =
+    map-subuniverse-connected-map K g ∘ map-subuniverse-connected-map K f
+  pr2 (comp-subuniverse-connected-map g f) =
+    is-subuniverse-connected-map-comp
+      ( is-subuniverse-connected-map-subuniverse-connected-map K g)
+      ( is-subuniverse-connected-map-subuniverse-connected-map K f)
+```
+
+### Right cancellation of `K`-connected maps
+
+```agda
+is-subuniverse-connected-map-left-factor :
+  {l1 l2 l3 l4 l5 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {C : UU l5}
+  {g : B → C} {h : A → B} →
+  is-subuniverse-connected-map K h →
+  is-subuniverse-connected-map K (g ∘ h) →
+  is-subuniverse-connected-map K g
+is-subuniverse-connected-map-left-factor K {g = g} {h} H GH U =
+  is-equiv-right-factor
+    ( precomp-Π h (pr1 ∘ U ∘ g))
+    ( precomp-Π g (pr1 ∘ U))
+    ( H (U ∘ g))
+    ( GH U)
+```
+
+### `K`-connected maps are closed under cobase change
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} (K : subuniverse l1 l2)
+  {S : UU l3} {A : UU l4} {B : UU l5}
+  (f : S → A) (g : S → B) {X : UU l6} (c : cocone f g X)
+  where
+
+  is-subuniverse-connected-map-cobase-change' :
+    dependent-pullback-property-pushout f g c →
+    is-subuniverse-connected-map K g →
+    is-subuniverse-connected-map K (horizontal-map-cocone f g c)
+  is-subuniverse-connected-map-cobase-change' H G U =
+    is-equiv-vertical-map-is-pullback _ _
+      ( cone-dependent-pullback-property-pushout f g c (pr1 ∘ U))
+      ( G (U ∘ vertical-map-cocone f g c))
+      ( H (pr1 ∘ U))
+
+  is-subuniverse-connected-map-cobase-change :
+    is-pushout f g c →
+    is-subuniverse-connected-map K g →
+    is-subuniverse-connected-map K (horizontal-map-cocone f g c)
+  is-subuniverse-connected-map-cobase-change H =
+    is-subuniverse-connected-map-cobase-change'
+      ( dependent-pullback-property-pushout-is-pushout f g c H)
+```
+
+### `K`-connected maps are closed under retracts of maps
+
+**Proof.** Given a retract of maps
+
+```text
+          i         r
+    A' ------> A ------> A'
+    |          |         |
+  f'|     I    f    R    | f'
+    ∨          ∨         ∨
+    B' ------> B ------> B'
+          i'        r'
+```
+
+with higher coherence `α`, and a `K`-valued family `U` over `B'` there is by
+functoriality an induced retract of dependent precomposition maps
+
+```text
+     Π(A'),(U∘f') <--- Π(A'),(U∘r'∘i'∘f) <--- Π(A),(U∘r'∘f) <--- Π(A'),(U∘f')
+          ∧                                         ∧                 ∧
+          |            α* □ Π(I),(U∘r')             |      Π(R),U     |
+  Π(f'),U |                                    Π(f),(U∘r')            | Π(f'),U
+          |                                         |                 |
+     Π(B'),U <--------- Π(B'),(U∘r'∘i') <----- Π(B),(U∘r') <--- Π(B'),(U),
+```
+
+and since equivalences are closed under retracts of maps, if `f` is
+`K`-connected then so is `f'`. ∎
+
+> This remains to be formalized.
+
+The formalization below takes a shortcut via the fiber condition.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {C : UU l5} {D : UU l6}
+  {f : A → B} {g : C → D} (R : f retract-of-map g)
+  where
+
+  is-subuniverse-connected-map-retract-map' :
+    ((y : D) → is-subuniverse-connected K (fiber g y)) →
+    is-subuniverse-connected-map K f
+  is-subuniverse-connected-map-retract-map' H =
+    is-subuniverse-connected-map-is-subuniverse-connected-fibers K f
+      ( λ b →
+        is-subuniverse-connected-retract K
+          ( retract-fiber-retract-map f g R b)
+          ( H (map-codomain-inclusion-retract-map f g R b)))
+```
+
+### The total map induced by a family of maps is `K`-connected if and only if all maps in the family are `K`-connected
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : A → UU l4} {C : A → UU l5}
+  (f : (x : A) → B x → C x)
+  where
+
+  is-subuniverse-connected-map-tot-is-fiberwise-subuniverse-connected-map :
+    ((x : A) → is-subuniverse-connected-map K (f x)) →
+    is-subuniverse-connected-map K (tot f)
+  is-subuniverse-connected-map-tot-is-fiberwise-subuniverse-connected-map H U =
+    is-equiv-source-is-equiv-target-equiv-arrow
+      ( precomp-Π (tot f) (pr1 ∘ U))
+      ( map-Π (λ i → precomp-Π (f i) (pr1 ∘ U ∘ (i ,_))))
+      ( equiv-ev-pair , equiv-ev-pair , refl-htpy)
+      ( is-equiv-map-Π-is-fiberwise-equiv (λ i → H i (U ∘ (i ,_))))
+```
+
+### Coproducts of `K`-connected maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {A' : UU l5} {B' : UU l6}
+  {f : A → B} {f' : A' → B'}
+  where
+
+  is-subuniverse-connected-map-coproduct :
+    is-subuniverse-connected-map K f →
+    is-subuniverse-connected-map K f' →
+    is-subuniverse-connected-map K (map-coproduct f f')
+  is-subuniverse-connected-map-coproduct F F' U =
+    is-equiv-source-is-equiv-target-equiv-arrow
+      ( precomp-Π (map-coproduct f f') (pr1 ∘ U))
+      ( map-product
+        ( precomp-Π f (pr1 ∘ U ∘ inl))
+        ( precomp-Π f' (pr1 ∘ U ∘ inr)))
+      ( equiv-dependent-universal-property-coproduct
+        ( pr1 ∘ U) ,
+        equiv-dependent-universal-property-coproduct
+          ( pr1 ∘ U ∘ map-coproduct f f') ,
+        refl-htpy)
+      ( is-equiv-map-product _ _ (F (U ∘ inl)) (F' (U ∘ inr)))
+```
+
+### The map on dependent pair types induced by a `K`-connected map is a `K`-equivalence
+
+This requires the added assumption that `K` is closed under exponentiation by
+arbitrary types.
+
+This is a generalization of Lemma 2.27 in {{#cite CORS20}}, since the unit map
+of the $ΣK$-localization is a $ΣK$-equivalence, and $ΣK$-equivalences are in
+particular $K$-connected.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : subuniverse-connected-map K A B)
+  (P : B → UU l1)
+  where
+
+  map-Σ-map-base-subuniverse-connected-map :
+    Σ A (P ∘ map-subuniverse-connected-map K f) → Σ B P
+  map-Σ-map-base-subuniverse-connected-map =
+    map-Σ-map-base (map-subuniverse-connected-map K f) P
+
+  is-subuniverse-equiv-map-Σ-map-base-subuniverse-connected-map :
+    ((V : UU l1) (U : type-subuniverse K) → is-in-subuniverse K (V → pr1 U)) →
+    is-subuniverse-equiv K map-Σ-map-base-subuniverse-connected-map
+  is-subuniverse-equiv-map-Σ-map-base-subuniverse-connected-map H U =
+    is-equiv-source-is-equiv-target-equiv-arrow
+      ( precomp map-Σ-map-base-subuniverse-connected-map (pr1 U))
+      ( precomp-Π (map-subuniverse-connected-map K f) (λ y → (b : P y) → pr1 U))
+      ( equiv-ev-pair , equiv-ev-pair , refl-htpy)
+      ( is-subuniverse-connected-map-subuniverse-connected-map K f
+        ( λ y → ((P y → pr1 U) , H (P y) U)))
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/orthogonal-factorization-systems/connected-types-at-subuniverses.lagda.md b/src/orthogonal-factorization-systems/connected-types-at-subuniverses.lagda.md
new file mode 100644
index 0000000000..85b4d8156b
--- /dev/null
+++ b/src/orthogonal-factorization-systems/connected-types-at-subuniverses.lagda.md
@@ -0,0 +1,290 @@
+# `K`-Connected types, with respect to a subuniverse `K`
+
+```agda
+module orthogonal-factorization-systems.connected-types-at-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.diagonal-maps-of-types
+open import foundation.equivalences
+open import foundation.retracts-of-maps
+open import foundation.retracts-of-types
+open import foundation.subuniverses
+open import foundation.unit-type
+open import foundation.universal-property-unit-type
+open import foundation.universe-levels
+
+open import foundation-core.contractible-maps
+open import foundation-core.embeddings
+open import foundation-core.fibers-of-maps
+open import foundation-core.identity-types
+open import foundation-core.propositions
+open import foundation-core.subtypes
+
+open import orthogonal-factorization-systems.equivalences-at-subuniverses
+```
+
+</details>
+
+## Idea
+
+Given a [subuniverse](foundation.subuniverses.md) `K`, a type `A` is said to be
+{{#concept "`K`-connected" Disambiguation="type, with respect to a subuniverse" Agda=is-subuniverse-connected}}
+if it satisfies the
+{{#concept "universal property" Disambiguation="subuniverse connected types"}}
+of `K`-connected types:
+
+For every `U` in `K`, the [diagonal map](foundation.diagonal-maps-of-types.md)
+
+```text
+ U → (A → U)
+```
+
+is an [equivalence](foundation-core.equivalences.md).
+
+Equivalently, a type is `K`-connected if
+
+1. Its [terminal projection map](foundation.unit-type.md) is a
+   `K`-[equivalence](orthogonal-factorization-systems.equivalences-at-subuniverses.md).
+2. For every `U` in `K` and `u : A → U` there
+   [uniquely exists](foundation.uniqueness-quantification.md) an element `v : U`
+   and a [homotopy](foundation-core.homotopies.md) `const v ~ u`. I.e., every
+   function out of `A` into a `K`-type is uniquely constant.
+
+## Definitions
+
+### The predicate on types of being `K`-connected
+
+```agda
+module _
+  {l1 l2 l3 : Level} (K : subuniverse l1 l2) (A : UU l3)
+  where
+
+  is-subuniverse-connected-Prop : Prop (lsuc l1 ⊔ l2 ⊔ l3)
+  is-subuniverse-connected-Prop =
+    Π-Prop
+      ( type-subuniverse K)
+      ( λ U → is-equiv-Prop (diagonal-exponential (pr1 U) A))
+
+  is-subuniverse-connected : UU (lsuc l1 ⊔ l2 ⊔ l3)
+  is-subuniverse-connected =
+    (U : type-subuniverse K) → is-equiv (diagonal-exponential (pr1 U) A)
+
+  is-prop-is-subuniverse-connected :
+    is-prop is-subuniverse-connected
+  is-prop-is-subuniverse-connected =
+    is-prop-type-Prop is-subuniverse-connected-Prop
+```
+
+### The universe of `K`-connected types
+
+```agda
+subuniverse-connected-type :
+  {l1 l2 : Level} (l3 : Level) (K : subuniverse l1 l2) →
+  UU (lsuc l1 ⊔ l2 ⊔ lsuc l3)
+subuniverse-connected-type l3 K =
+  type-subtype (is-subuniverse-connected-Prop {l3 = l3} K)
+
+module _
+  {l1 l2 l3 : Level} (K : subuniverse l1 l2)
+  where
+
+  type-subuniverse-connected-type : subuniverse-connected-type l3 K → UU l3
+  type-subuniverse-connected-type =
+    inclusion-subtype (is-subuniverse-connected-Prop K)
+
+  is-subuniverse-connected-type-subuniverse-connected-type :
+    (A : subuniverse-connected-type l3 K) →
+    is-subuniverse-connected K (type-subuniverse-connected-type A)
+  is-subuniverse-connected-type-subuniverse-connected-type =
+    is-in-subtype-inclusion-subtype (is-subuniverse-connected-Prop K)
+
+  emb-inclusion-subuniverse-connected-type :
+    subuniverse-connected-type l3 K ↪ UU l3
+  emb-inclusion-subuniverse-connected-type =
+    emb-subtype (is-subuniverse-connected-Prop K)
+```
+
+### The constancy condition of `K`-connected types
+
+```agda
+module _
+  {l1 l2 l3 : Level} (K : subuniverse l1 l2) (A : UU l3)
+  where
+
+  is-subuniverse-connected-const-condition :
+    UU (lsuc l1 ⊔ l2 ⊔ l3)
+  is-subuniverse-connected-const-condition =
+    (U : type-subuniverse K) (u : A → pr1 U) →
+    is-contr (Σ (pr1 U) (λ v → (x : A) → v ＝ u x))
+
+  abstract
+    is-prop-is-subuniverse-connected-const-condition :
+      is-prop is-subuniverse-connected-const-condition
+    is-prop-is-subuniverse-connected-const-condition =
+      is-prop-Π (λ U → is-prop-Π (λ u → is-property-is-contr))
+
+  is-subuniverse-connected-const-condition-Prop :
+    Prop (lsuc l1 ⊔ l2 ⊔ l3)
+  is-subuniverse-connected-const-condition-Prop =
+    ( is-subuniverse-connected-const-condition ,
+      is-prop-is-subuniverse-connected-const-condition)
+```
+
+## Properties
+
+### A type is `K`-connected if and only if the terminal map is a `K`-equivalence
+
+```agda
+module _
+  {l1 l2 l3 : Level} (K : subuniverse l1 l2) {A : UU l3}
+  where
+
+  is-subuniverse-connected-is-subuniverse-equiv-terminal-map :
+    is-subuniverse-equiv K (terminal-map A) →
+    is-subuniverse-connected K A
+  is-subuniverse-connected-is-subuniverse-equiv-terminal-map H U =
+    is-equiv-diagonal-exponential-is-equiv-precomp-terminal-map (H U)
+
+  is-subuniverse-equiv-terminal-map-is-subuniverse-connected :
+    is-subuniverse-connected K A →
+    is-subuniverse-equiv K (terminal-map A)
+  is-subuniverse-equiv-terminal-map-is-subuniverse-connected H U =
+    is-equiv-precomp-terminal-map-is-equiv-diagonal-exponential (H U)
+```
+
+### A type is `K`-connected if and only if it satisfies the constancy condition
+
+```agda
+module _
+  {l1 l2 l3 : Level} (K : subuniverse l1 l2) {A : UU l3}
+  where abstract
+
+  is-subuniverse-connected-is-subuniverse-connected-const-condition :
+    is-subuniverse-connected-const-condition K A →
+    is-subuniverse-connected K A
+  is-subuniverse-connected-is-subuniverse-connected-const-condition H U =
+    is-equiv-is-contr-map
+      ( λ u →
+        is-contr-equiv
+          ( Σ (pr1 U) (λ v → (x : A) → v ＝ u x))
+          ( compute-fiber-diagonal-exponential u)
+          ( H U u))
+
+  is-subuniverse-connected-const-condition-is-subuniverse-connected :
+    is-subuniverse-connected K A →
+    is-subuniverse-connected-const-condition K A
+  is-subuniverse-connected-const-condition-is-subuniverse-connected H U u =
+    is-contr-equiv'
+      ( fiber (diagonal-exponential (pr1 U) A) u)
+      ( compute-fiber-diagonal-exponential u)
+      ( is-contr-map-is-equiv (H U) u)
+```
+
+### All types are `Contr`-connected
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1}
+  where
+
+  is-Contr-connected : is-subuniverse-connected (is-contr-Prop {l2}) A
+  is-Contr-connected U = is-equiv-diagonal-exponential-is-contr' (pr2 U) A
+```
+
+### Contractible types are `K`-connected
+
+```agda
+module _
+  {l1 l2 l3 : Level} (K : subuniverse l1 l2) {A : UU l3}
+  where
+
+  is-subuniverse-connected-is-contr :
+    is-contr A → is-subuniverse-connected K A
+  is-subuniverse-connected-is-contr H U =
+    is-equiv-diagonal-exponential-is-contr H (pr1 U)
+```
+
+### `K`-connected types are closed under retracts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} {B : UU l4}
+  where
+
+  is-subuniverse-connected-retract :
+    A retract-of B →
+    is-subuniverse-connected K B →
+    is-subuniverse-connected K A
+  is-subuniverse-connected-retract R H U =
+    is-equiv-retract-map-is-equiv
+      ( diagonal-exponential (pr1 U) A)
+      ( diagonal-exponential (pr1 U) B)
+      ( retract-map-diagonal-exponential-retract id-retract R)
+      ( H U)
+```
+
+### `K`-connected types are closed under equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} {B : UU l4}
+  where
+
+  is-subuniverse-connected-equiv :
+    A ≃ B →
+    is-subuniverse-connected K B →
+    is-subuniverse-connected K A
+  is-subuniverse-connected-equiv e =
+    is-subuniverse-connected-retract K (retract-equiv e)
+
+  is-subuniverse-connected-equiv' :
+    A ≃ B →
+    is-subuniverse-connected K A →
+    is-subuniverse-connected K B
+  is-subuniverse-connected-equiv' e =
+    is-subuniverse-connected-retract K (retract-inv-equiv e)
+```
+
+### `K`-connected types are closed under `K`-equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} {B : UU l4}
+  where
+
+  is-subuniverse-connected-is-subuniverse-equiv :
+    (f : A → B) → is-subuniverse-equiv K f →
+    is-subuniverse-connected K B → is-subuniverse-connected K A
+  is-subuniverse-connected-is-subuniverse-equiv f F H =
+    is-subuniverse-connected-is-subuniverse-equiv-terminal-map K
+      ( is-subuniverse-equiv-comp K (terminal-map B) f F
+        ( is-subuniverse-equiv-terminal-map-is-subuniverse-connected K H))
+
+  is-subuniverse-connected-is-subuniverse-equiv' :
+    (f : A → B) → is-subuniverse-equiv K f →
+    is-subuniverse-connected K A → is-subuniverse-connected K B
+  is-subuniverse-connected-is-subuniverse-equiv' f F H =
+    is-subuniverse-connected-is-subuniverse-equiv-terminal-map K
+      ( is-subuniverse-equiv-left-factor K (terminal-map B) f
+        ( is-subuniverse-equiv-terminal-map-is-subuniverse-connected K H)
+        ( F))
+
+  is-subuniverse-connected-subuniverse-equiv :
+    subuniverse-equiv K A B →
+    is-subuniverse-connected K B →
+    is-subuniverse-connected K A
+  is-subuniverse-connected-subuniverse-equiv (f , F) =
+    is-subuniverse-connected-is-subuniverse-equiv f F
+
+  is-subuniverse-connected-subuniverse-equiv' :
+    subuniverse-equiv K A B →
+    is-subuniverse-connected K A →
+    is-subuniverse-connected K B
+  is-subuniverse-connected-subuniverse-equiv' (f , F) =
+    is-subuniverse-connected-is-subuniverse-equiv' f F
+```
diff --git a/src/orthogonal-factorization-systems/equivalences-at-subuniverses.lagda.md b/src/orthogonal-factorization-systems/equivalences-at-subuniverses.lagda.md
new file mode 100644
index 0000000000..79ab40f0f2
--- /dev/null
+++ b/src/orthogonal-factorization-systems/equivalences-at-subuniverses.lagda.md
@@ -0,0 +1,374 @@
+# `K`-Equivalences, with respect to a subuniverse `K`
+
+```agda
+module orthogonal-factorization-systems.equivalences-at-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.precomposition-functions
+open import foundation.propositions
+open import foundation.subuniverses
+open import foundation.universal-property-equivalences
+open import foundation.universe-levels
+
+open import foundation-core.contractible-maps
+open import foundation-core.fibers-of-maps
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.retractions
+open import foundation-core.sections
+
+open import orthogonal-factorization-systems.extensions-maps
+```
+
+</details>
+
+## Idea
+
+Given a [subuniverse](foundation.subuniverses.md) `K`, a map `f : A → B` is said
+to be a
+{{#concept "`K`-equivalence" Disambiguation="map of types, with respect to a subuniverse" Agda=is-subuniverse-equiv}}
+if it satisfies the
+{{#concept "universal property" Disambiguation="subuniverse connected map of types"}}
+of `K`-equivalences:
+
+For every `K`-type `U`, the
+[precomposition map](foundation-core.precomposition-functions.md)
+
+```text
+ - ∘ f : (B → U) → (A → U)
+```
+
+is an [equivalence](foundation-core.equivalences.md).
+
+Equivalently, a map `f : A → B` is a `K`-equivalence if
+
+1. For every `U` in `K` and every `u : A → U` has a
+   [unique](foundation-core.contractible-types.md)
+   [extension](orthogonal-factorization-systems.extensions-maps.md) along `f`.
+   I.e., the type of maps `u' : B → U` such that the following triangle
+   [commutes](foundation-core.commuting-triangles-of-maps.md)
+   ```text
+        A
+        |  \
+      f |    \ u
+        |      \
+        ∨   u'   ∨
+        B ------> U
+   ```
+   is contractible.
+
+## Definition
+
+### The predicate on maps of being `K`-equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-equiv : UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-subuniverse-equiv =
+    (U : type-subuniverse K) → is-equiv (precomp f (pr1 U))
+
+  is-prop-is-subuniverse-equiv : is-prop is-subuniverse-equiv
+  is-prop-is-subuniverse-equiv =
+    is-prop-Π (λ U → is-property-is-equiv (precomp f (pr1 U)))
+
+  is-subuniverse-equiv-Prop : Prop (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-subuniverse-equiv-Prop =
+    ( is-subuniverse-equiv , is-prop-is-subuniverse-equiv)
+```
+
+### The type of `K`-equivalences
+
+```agda
+subuniverse-equiv :
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) →
+  UU l3 → UU l4 → UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+subuniverse-equiv K A B = Σ (A → B) (is-subuniverse-equiv K)
+
+module _
+  {l1 l2 l3 l4 : Level}
+  (K : subuniverse l1 l2) {A : UU l3} {B : UU l4}
+  (f : subuniverse-equiv K A B)
+  where
+
+  map-subuniverse-equiv : A → B
+  map-subuniverse-equiv = pr1 f
+
+  is-subuniverse-equiv-subuniverse-equiv :
+    is-subuniverse-equiv K map-subuniverse-equiv
+  is-subuniverse-equiv-subuniverse-equiv = pr2 f
+```
+
+### The extension condition for `K`-equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-equiv-extension-condition : UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-subuniverse-equiv-extension-condition =
+    (U : type-subuniverse K) (u : A → pr1 U) → is-contr (extension-map f u)
+
+  is-prop-is-subuniverse-equiv-extension-condition :
+    is-prop is-subuniverse-equiv-extension-condition
+  is-prop-is-subuniverse-equiv-extension-condition =
+    is-prop-Π (λ U → is-prop-Π (λ u → is-property-is-contr))
+
+  is-subuniverse-equiv-extension-condition-Prop : Prop (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-subuniverse-equiv-extension-condition-Prop =
+    ( is-subuniverse-equiv-extension-condition ,
+      is-prop-is-subuniverse-equiv-extension-condition)
+```
+
+## Properties
+
+### A map is a `K`-equivalence if and only if it satisfies the extension condition
+
+A map `f : A → B` is a `K`-equivalence if and only if, for every `U` in `K` and
+every map `u : A → U`, there is a unique extension of `u` along `f`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where abstract
+
+  is-subuniverse-equiv-is-subuniverse-equiv-extension-condition :
+    is-subuniverse-equiv-extension-condition K f →
+    is-subuniverse-equiv K f
+  is-subuniverse-equiv-is-subuniverse-equiv-extension-condition H U =
+    is-equiv-is-contr-map
+      ( λ u →
+        is-contr-equiv
+          ( extension-map f u)
+          ( compute-extension-fiber-precomp f u)
+          ( H U u))
+
+  is-subuniverse-equiv-extension-condition-is-subuniverse-equiv :
+    is-subuniverse-equiv K f →
+    is-subuniverse-equiv-extension-condition K f
+  is-subuniverse-equiv-extension-condition-is-subuniverse-equiv H U u =
+    is-contr-equiv'
+      ( fiber (precomp f (pr1 U)) u)
+      ( compute-extension-fiber-precomp f u)
+      ( is-contr-map-is-equiv (H U) u)
+```
+
+### Equivalences are `K`-equivalences for all `K`
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} (f : A → B)
+  where
+
+  is-subuniverse-equiv-is-equiv : is-equiv f → is-subuniverse-equiv K f
+  is-subuniverse-equiv-is-equiv H U = is-equiv-precomp-is-equiv f H (pr1 U)
+```
+
+### The identity map is a `K`-equivalence for all `K`
+
+```agda
+is-subuniverse-equiv-id :
+  {l1 l2 l3 : Level} (K : subuniverse l1 l2) {A : UU l3} →
+  is-subuniverse-equiv K (id' A)
+is-subuniverse-equiv-id K = is-subuniverse-equiv-is-equiv K id is-equiv-id
+```
+
+### The `K`-equivalences are closed under homotopies
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {f g : A → B}
+  where
+
+  is-subuniverse-equiv-htpy :
+    f ~ g → is-subuniverse-equiv K g → is-subuniverse-equiv K f
+  is-subuniverse-equiv-htpy H G U =
+    is-equiv-htpy (precomp g (pr1 U)) (htpy-precomp H (pr1 U)) (G U)
+
+  is-subuniverse-equiv-htpy' :
+    f ~ g → is-subuniverse-equiv K f → is-subuniverse-equiv K g
+  is-subuniverse-equiv-htpy' H G U =
+    is-equiv-htpy' (precomp f (pr1 U)) (htpy-precomp H (pr1 U)) (G U)
+```
+
+### The `K`-equivalences are closed under composition
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {C : UU l5}
+  where
+
+  is-subuniverse-equiv-comp :
+    (g : B → C) (f : A → B) →
+    is-subuniverse-equiv K f →
+    is-subuniverse-equiv K g →
+    is-subuniverse-equiv K (g ∘ f)
+  is-subuniverse-equiv-comp g f F G U =
+    is-equiv-comp (precomp f (pr1 U)) (precomp g (pr1 U)) (G U) (F U)
+
+  subuniverse-equiv-comp :
+    subuniverse-equiv K B C →
+    subuniverse-equiv K A B →
+    subuniverse-equiv K A C
+  pr1 (subuniverse-equiv-comp g f) =
+    map-subuniverse-equiv K g ∘ map-subuniverse-equiv K f
+  pr2 (subuniverse-equiv-comp g f) =
+    is-subuniverse-equiv-comp
+      ( map-subuniverse-equiv K g)
+      ( map-subuniverse-equiv K f)
+      ( is-subuniverse-equiv-subuniverse-equiv K f)
+      ( is-subuniverse-equiv-subuniverse-equiv K g)
+```
+
+### The class of `K`-equivalences has the left and right cancellation property
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {C : UU l5}
+  (g : B → C) (f : A → B) (GF : is-subuniverse-equiv K (g ∘ f))
+  where
+
+  is-subuniverse-equiv-left-factor :
+    is-subuniverse-equiv K f → is-subuniverse-equiv K g
+  is-subuniverse-equiv-left-factor F U =
+    is-equiv-right-factor (precomp f (pr1 U)) (precomp g (pr1 U)) (F U) (GF U)
+
+  is-subuniverse-equiv-right-factor :
+    is-subuniverse-equiv K g → is-subuniverse-equiv K f
+  is-subuniverse-equiv-right-factor G U =
+    is-equiv-left-factor (precomp f (pr1 U)) (precomp g (pr1 U)) (GF U) (G U)
+```
+
+### The class of `K`-equivalences satisfies the 3-for-2 property
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {X : UU l5}
+  (f : A → X) (g : B → X) (h : A → B) (p : f ~ g ∘ h)
+  where
+
+  is-subuniverse-equiv-top-map-triangle :
+      is-subuniverse-equiv K g →
+      is-subuniverse-equiv K f →
+      is-subuniverse-equiv K h
+  is-subuniverse-equiv-top-map-triangle G F =
+    is-subuniverse-equiv-right-factor K g h
+      ( is-subuniverse-equiv-htpy' K p F)
+      ( G)
+
+  is-subuniverse-equiv-right-map-triangle :
+    is-subuniverse-equiv K f →
+    is-subuniverse-equiv K h →
+    is-subuniverse-equiv K g
+  is-subuniverse-equiv-right-map-triangle F =
+    is-subuniverse-equiv-left-factor K g h (is-subuniverse-equiv-htpy' K p F)
+
+  is-subuniverse-equiv-left-map-triangle :
+    is-subuniverse-equiv K h →
+    is-subuniverse-equiv K g →
+    is-subuniverse-equiv K f
+  is-subuniverse-equiv-left-map-triangle H G =
+    is-subuniverse-equiv-htpy K p (is-subuniverse-equiv-comp K g h H G)
+```
+
+### Sections of `K`-equivalences are `K`-equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {f : A → B}
+  where
+
+  is-subuniverse-equiv-map-section :
+    (s : section f) →
+    is-subuniverse-equiv K f →
+    is-subuniverse-equiv K (map-section f s)
+  is-subuniverse-equiv-map-section (s , h) =
+    is-subuniverse-equiv-right-factor K f s
+      ( is-subuniverse-equiv-is-equiv K (f ∘ s) (is-equiv-htpy-id h))
+```
+
+### Retractions of `K`-equivalences are `K`-equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {f : A → B}
+  where
+
+  is-subuniverse-equiv-map-retraction :
+    (r : retraction f) →
+    is-subuniverse-equiv K f →
+    is-subuniverse-equiv K (map-retraction f r)
+  is-subuniverse-equiv-map-retraction (r , h) =
+    is-subuniverse-equiv-left-factor K r f
+      ( is-subuniverse-equiv-is-equiv K (r ∘ f) (is-equiv-htpy-id h))
+```
+
+### Composing `K`-equivalences with equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} {B : UU l4} {C : UU l5}
+  where
+
+  is-subuniverse-equiv-is-equiv-is-subuniverse-equiv :
+    (g : B → C) (f : A → B) →
+    is-subuniverse-equiv K g →
+    is-equiv f →
+    is-subuniverse-equiv K (g ∘ f)
+  is-subuniverse-equiv-is-equiv-is-subuniverse-equiv g f eg ef =
+    is-subuniverse-equiv-comp K g f
+      ( is-subuniverse-equiv-is-equiv K f ef)
+      ( eg)
+
+  is-subuniverse-equiv-is-subuniverse-equiv-is-equiv :
+    (g : B → C) (f : A → B) →
+    is-equiv g →
+    is-subuniverse-equiv K f →
+    is-subuniverse-equiv K (g ∘ f)
+  is-subuniverse-equiv-is-subuniverse-equiv-is-equiv g f eg ef =
+    is-subuniverse-equiv-comp K g f
+      ( ef)
+      ( is-subuniverse-equiv-is-equiv K g eg)
+
+  is-subuniverse-equiv-equiv-is-subuniverse-equiv :
+    (g : B → C) (f : A ≃ B) →
+    is-subuniverse-equiv K g →
+    is-subuniverse-equiv K (g ∘ map-equiv f)
+  is-subuniverse-equiv-equiv-is-subuniverse-equiv g (f , ef) eg =
+    is-subuniverse-equiv-is-equiv-is-subuniverse-equiv g f eg ef
+
+  is-subuniverse-equiv-is-subuniverse-equiv-equiv :
+    (g : B ≃ C) (f : A → B) →
+    is-subuniverse-equiv K f →
+    is-subuniverse-equiv K (map-equiv g ∘ f)
+  is-subuniverse-equiv-is-subuniverse-equiv-equiv (g , eg) f ef =
+    is-subuniverse-equiv-is-subuniverse-equiv-is-equiv g f eg ef
+```
+
+## References
+
+- The notion of `K`-equivalence is a generalization of the notion of
+  `L`-equivalence, where `L` is a reflective subuniverse. These were studied in
+  {{#cite CORS20}}.
+
+{{#bibliography}}
diff --git a/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md b/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md
index 1144d685d4..416c112fd3 100644
--- a/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md
@@ -21,7 +21,7 @@ open import orthogonal-factorization-systems.types-local-at-maps
 
 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.types-local-at-maps.md) type `Y`
+`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.
 
@@ -81,8 +81,8 @@ module _
     pr1 is-localization-Y
   pr1 (pr2 (is-subuniverse-localization-is-localization is-localization-Y)) = η
   pr2 (pr2 (is-subuniverse-localization-is-localization is-localization-Y))
-    Z is-local-Z =
-      pr2 is-localization-Y Z is-local-Z
+    (Z , is-local-Z) =
+    pr2 is-localization-Y Z is-local-Z
 ```
 
 It remains to construct a converse.
diff --git a/src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md b/src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md
index c12ced2306..542ea55aa3 100644
--- a/src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md
@@ -12,6 +12,7 @@ open import foundation.dependent-pair-types
 open import foundation.subuniverses
 open import foundation.universe-levels
 
+open import orthogonal-factorization-systems.equivalences-at-subuniverses
 open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
@@ -20,19 +21,30 @@ open import orthogonal-factorization-systems.types-local-at-maps
 ## Idea
 
 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.types-local-at-maps.md). I.e., for
-every `Z` in `P`, the [precomposition map](foundation-core.function-types.md)
+{{#concept "localization" Disambiguation="of a type at a subuniverse" Agda=subuniverse-localization}}
+at `P`, or **`P`-localization**, is a type `Y` in `P` and a `P`-equivalence
+`η : X → Y`, i.e., a map such that for every `Z` in `P` the
+[precomposition map](foundation-core.function-types.md)
 
 ```text
   - ∘ η : (Y → Z) → (X → Z)
 ```
 
-is an [equivalence](foundation-core.equivalences.md).
+is an [equivalence](foundation-core.equivalences.md). In other words, every type
+in `P` is `η`-[local](orthogonal-factorization-systems.types-local-at-maps.md).
 
 ## Definition
 
+### The predicate on a map of being a localization at a subuniverse
+
+```agda
+is-subuniverse-localization-map :
+  {l1 l2 lP : Level} (P : subuniverse l1 lP) {A : UU l2} {PA : UU l1}
+  (η : A → PA) → UU (lsuc l1 ⊔ l2 ⊔ lP)
+is-subuniverse-localization-map P {A} {PA} η =
+  is-in-subuniverse P PA × is-subuniverse-equiv P η
+```
+
 ### The predicate of being a localization at a subuniverse
 
 ```agda
@@ -40,9 +52,7 @@ is-subuniverse-localization :
   {l1 l2 lP : Level} (P : subuniverse l1 lP) →
   UU l2 → UU l1 → UU (lsuc l1 ⊔ l2 ⊔ lP)
 is-subuniverse-localization {l1} {l2} P X Y =
-  ( is-in-subuniverse P Y) ×
-  ( Σ ( X → Y)
-      ( λ η → (Z : UU l1) → is-in-subuniverse P Z → is-local η Z))
+  (is-in-subuniverse P Y) × (subuniverse-equiv P X Y)
 ```
 
 ```agda
@@ -58,8 +68,7 @@ module _
   unit-is-subuniverse-localization = pr1 (pr2 is-localization-Y)
 
   is-local-at-unit-is-in-subuniverse-is-subuniverse-localization :
-    (Z : UU l1) → is-in-subuniverse P Z →
-    is-local unit-is-subuniverse-localization Z
+    (Z : type-subuniverse P) → is-local unit-is-subuniverse-localization (pr1 Z)
   is-local-at-unit-is-in-subuniverse-is-subuniverse-localization =
     pr2 (pr2 is-localization-Y)
 ```
@@ -91,15 +100,19 @@ module _
     is-in-subuniverse-is-subuniverse-localization P
       ( is-subuniverse-localization-subuniverse-localization)
 
+  type-subuniverse-subuniverse-localization : type-subuniverse P
+  type-subuniverse-subuniverse-localization =
+    ( type-subuniverse-localization ,
+      is-in-subuniverse-subuniverse-localization)
+
   unit-subuniverse-localization : X → type-subuniverse-localization
   unit-subuniverse-localization =
     unit-is-subuniverse-localization P
       ( is-subuniverse-localization-subuniverse-localization)
 
-  is-local-at-unit-is-in-subuniverse-subuniverse-localization :
-    (Z : UU l1) →
-    is-in-subuniverse P Z → is-local unit-subuniverse-localization Z
-  is-local-at-unit-is-in-subuniverse-subuniverse-localization =
+  is-subuniverse-equiv-unit-subuniverse-localization :
+    is-subuniverse-equiv P unit-subuniverse-localization
+  is-subuniverse-equiv-unit-subuniverse-localization =
     is-local-at-unit-is-in-subuniverse-is-subuniverse-localization P
       ( is-subuniverse-localization-subuniverse-localization)
 ```
diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
index 41a30148b0..f00277ed1d 100644
--- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
@@ -167,7 +167,7 @@ module _
   pr1 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) =
     unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫
   pr2 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A)))
-    X is-in-subuniverse-X =
+    ( X , is-in-subuniverse-X) =
       is-local-is-in-subuniverse-is-reflective-subuniverse
         𝒫 is-reflective-𝒫 X A is-in-subuniverse-X
 
@@ -186,8 +186,9 @@ module _
     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
-      𝒫 (L B) A is-in-subuniverse-A
+    is-subuniverse-equiv-unit-subuniverse-localization 𝒫
+      ( L B)
+      ( A , is-in-subuniverse-A)
 ```
 
 ## Recursion for reflective subuniverses
diff --git a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
index e84d837cd0..61cd3a03c0 100644
--- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md
@@ -14,6 +14,7 @@ open import foundation.contractible-maps
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.dependent-universal-property-equivalences
+open import foundation.embeddings
 open import foundation.empty-types
 open import foundation.equivalences
 open import foundation.families-of-equivalences
@@ -28,6 +29,7 @@ open import foundation.logical-equivalences
 open import foundation.postcomposition-functions
 open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
+open import foundation.propositional-maps
 open import foundation.propositions
 open import foundation.retractions
 open import foundation.retracts-of-maps
@@ -312,32 +314,42 @@ module _
 
 ### If the domain and codomain of `f` is `f`-local, then `f` is an equivalence
 
+More generally, this is true as soon as the precomposition map of `f` has a
+section at `X` and is an embedding at `Y`.
+
 ```agda
 module _
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
   where
 
-  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) =
+  section-is-epi-at-codomain-section-precomp-domain :
+    section (precomp f X) → is-emb (precomp f Y) → section f
+  pr1 (section-is-epi-at-codomain-section-precomp-domain sX _) =
+    pr1 sX id
+  pr2 (section-is-epi-at-codomain-section-precomp-domain sX eY) =
     htpy-eq
       ( ap
         ( pr1)
-        { ( f ∘ pr1 (section-is-local-domains' section-precomp-X is-local-Y)) ,
-          ( ap (postcomp X f) (pr2 section-precomp-X id))}
+        { f ∘ pr1 sX id , ap (postcomp X f) (pr2 sX id)}
         { id , refl}
-        ( eq-is-contr (is-contr-map-is-equiv is-local-Y f)))
+        ( eq-is-prop (is-prop-map-is-emb eY f)))
+
+  section-is-local-at-codomain-section-precomp-domain :
+    section (precomp f X) → is-local f Y → section f
+  section-is-local-at-codomain-section-precomp-domain sX lY =
+    section-is-epi-at-codomain-section-precomp-domain sX (is-emb-is-equiv lY)
 
-  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-map-section-precomp f section-precomp-X
+  is-equiv-is-epi-at-codomain-section-precomp-domain :
+    section (precomp f X) → is-emb (precomp f Y) → is-equiv f
+  is-equiv-is-epi-at-codomain-section-precomp-domain sX eY =
+    ( section-is-epi-at-codomain-section-precomp-domain sX eY ,
+      retraction-map-section-precomp f sX)
 
   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)
+  is-equiv-is-local-domains lX lY =
+    is-equiv-is-epi-at-codomain-section-precomp-domain
+      ( section-is-equiv lX)
+      ( is-emb-is-equiv lY)
 ```
 
 ### If `f` has a retraction and the codomain of `f` is `f`-local, then `f` is an equivalence
@@ -350,7 +362,7 @@ module _
   is-equiv-retraction-is-local-codomain :
     retraction f → is-local f Y → is-equiv f
   is-equiv-retraction-is-local-codomain r is-local-Y =
-    section-is-local-domains' f
+    section-is-local-at-codomain-section-precomp-domain f
       ( section-precomp-retraction-map f r)
       ( is-local-Y) ,
     r