diff --git a/src/foundation-core/truncated-maps.lagda.md b/src/foundation-core/truncated-maps.lagda.md
index 068c7c04d2..720b4c6286 100644
--- a/src/foundation-core/truncated-maps.lagda.md
+++ b/src/foundation-core/truncated-maps.lagda.md
@@ -10,10 +10,12 @@ module foundation-core.truncated-maps where
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-fibers-of-maps
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 
 open import foundation-core.commuting-squares-of-maps
 open import foundation-core.contractible-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
@@ -112,23 +114,37 @@ module _
   where
 
   abstract
-    is-trunc-map-is-trunc-map-ap :
+    is-trunc-map-succ-is-trunc-map-ap :
       ((x y : A) → is-trunc-map k (ap f {x} {y})) → is-trunc-map (succ-𝕋 k) f
-    is-trunc-map-is-trunc-map-ap is-trunc-map-ap-f b (pair x p) (pair x' p') =
+    is-trunc-map-succ-is-trunc-map-ap is-trunc-map-ap-f b (x , p) (x' , p') =
       is-trunc-equiv k
-        ( fiber (ap f) (p ∙ (inv p')))
-        ( equiv-fiber-ap-eq-fiber f (pair x p) (pair x' p'))
-        ( is-trunc-map-ap-f x x' (p ∙ (inv p')))
+        ( fiber (ap f) (p ∙ inv p'))
+        ( equiv-fiber-ap-eq-fiber f (x , p) (x' , p'))
+        ( is-trunc-map-ap-f x x' (p ∙ inv p'))
 
   abstract
-    is-trunc-map-ap-is-trunc-map :
+    is-trunc-map-ap-is-trunc-map-succ :
       is-trunc-map (succ-𝕋 k) f → (x y : A) → is-trunc-map k (ap f {x} {y})
-    is-trunc-map-ap-is-trunc-map is-trunc-map-f x y p =
+    is-trunc-map-ap-is-trunc-map-succ is-trunc-map-f x y p =
       is-trunc-is-equiv' k
-        ( pair x p ＝ pair y refl)
+        ( (x , p) ＝ (y , refl))
         ( eq-fiber-fiber-ap f x y p)
         ( is-equiv-eq-fiber-fiber-ap f x y p)
-        ( is-trunc-map-f (f y) (pair x p) (pair y refl))
+        ( is-trunc-map-f (f y) (x , p) (y , refl))
+```
+
+### The action on identifications of a `k`-truncated map is also `k`-truncated
+
+```agda
+module _
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  abstract
+    is-trunc-map-ap-is-trunc-map :
+      is-trunc-map k f → (x y : A) → is-trunc-map k (ap f {x} {y})
+    is-trunc-map-ap-is-trunc-map H =
+      is-trunc-map-ap-is-trunc-map-succ k f (is-trunc-map-succ-is-trunc-map k H)
 ```
 
 ### The domain of any `k`-truncated map into a `k+1`-truncated type is `k+1`-truncated
@@ -146,7 +162,7 @@ is-trunc-is-trunc-map-into-is-trunc
     ( k)
     ( ap f)
     ( is-trunc-B (f a) (f a'))
-    ( is-trunc-map-ap-is-trunc-map k f is-trunc-map-f a a')
+    ( is-trunc-map-ap-is-trunc-map-succ k f is-trunc-map-f a a')
 ```
 
 ### A family of types is a family of `k`-truncated types if and only of the projection map is `k`-truncated
@@ -274,7 +290,7 @@ abstract
         ( map-compute-fiber-comp g h (g b))
         ( is-equiv-map-compute-fiber-comp g h (g b))
         ( is-trunc-map-htpy k (inv-htpy H) is-trunc-f (g b)))
-      ( pair b refl)
+      ( b , refl)
 ```
 
 ### If a composite `g ∘ h` and its left factor `g` are truncated maps, then its right factor `h` is a truncated map
@@ -305,3 +321,21 @@ module _
       ( is-trunc-map-comp k i g M
         ( is-trunc-map-is-equiv k K))
 ```
+
+### If the domain is contractible and the codomain is `k+1`-truncated then the map is `k`-truncated
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  is-trunc-map-is-trunc-succ-codomain-is-contr-domain :
+    is-contr A →
+    is-trunc (succ-𝕋 k) B →
+    is-trunc-map k f
+  is-trunc-map-is-trunc-succ-codomain-is-contr-domain c tB u =
+    is-trunc-equiv k
+      ( f (center c) ＝ u)
+      ( left-unit-law-Σ-is-contr c (center c))
+      ( tB (f (center c)) u)
+```
diff --git a/src/foundation/0-connected-types.lagda.md b/src/foundation/0-connected-types.lagda.md
index 756f782225..a9f50ba0fe 100644
--- a/src/foundation/0-connected-types.lagda.md
+++ b/src/foundation/0-connected-types.lagda.md
@@ -1,4 +1,4 @@
-# `0`-Connected types
+# 0-Connected types
 
 ```agda
 module foundation.0-connected-types where
@@ -10,12 +10,17 @@ module foundation.0-connected-types where
 open import foundation.action-on-identifications-functions
 open import foundation.constant-maps
 open import foundation.contractible-types
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equality-coproduct-types
+open import foundation.evaluation-functions
 open import foundation.fiber-inclusions
 open import foundation.functoriality-set-truncation
 open import foundation.images
 open import foundation.inhabited-types
 open import foundation.mere-equality
+open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.set-truncations
 open import foundation.sets
@@ -56,7 +61,13 @@ is-0-connected A = type-Prop (is-0-connected-Prop A)
 
 is-prop-is-0-connected : {l : Level} (A : UU l) → is-prop (is-0-connected A)
 is-prop-is-0-connected A = is-prop-type-Prop (is-0-connected-Prop A)
+```
+
+## Properties
 
+### 0-connected types are inhabited
+
+```agda
 abstract
   is-inhabited-is-0-connected :
     {l : Level} {A : UU l} → is-0-connected A → is-inhabited A
@@ -65,13 +76,21 @@ abstract
       ( center C)
       ( set-Prop (trunc-Prop A))
       ( unit-trunc-Prop)
+```
+
+### Elements of 0-connected types are all merely equal
 
+```agda
 abstract
   mere-eq-is-0-connected :
     {l : Level} {A : UU l} → is-0-connected A → all-elements-merely-equal A
   mere-eq-is-0-connected {A = A} H x y =
     apply-effectiveness-unit-trunc-Set (eq-is-contr H)
+```
+
+### A type is 0-connected if it is inhabited and all elements are merely equal
 
+```agda
 abstract
   is-0-connected-mere-eq :
     {l : Level} {A : UU l} (a : A) →
@@ -91,17 +110,22 @@ abstract
     apply-universal-property-trunc-Prop H
       ( is-0-connected-Prop _)
       ( λ a → is-0-connected-mere-eq a (K a))
+```
 
-is-0-connected-is-surjective-point :
-  {l1 : Level} {A : UU l1} (a : A) →
-  is-surjective (point a) → is-0-connected A
-is-0-connected-is-surjective-point a H =
-  is-0-connected-mere-eq a
-    ( λ x →
-      apply-universal-property-trunc-Prop
-        ( H x)
-        ( mere-eq-Prop a x)
-        ( λ u → unit-trunc-Prop (pr2 u)))
+### A type is 0-connected iff any point inclusion is surjective
+
+```agda
+abstract
+  is-0-connected-is-surjective-point :
+    {l1 : Level} {A : UU l1} (a : A) →
+    is-surjective (point a) → is-0-connected A
+  is-0-connected-is-surjective-point a H =
+    is-0-connected-mere-eq a
+      ( λ x →
+        apply-universal-property-trunc-Prop
+          ( H x)
+          ( mere-eq-Prop a x)
+          ( λ u → unit-trunc-Prop (pr2 u)))
 
 abstract
   is-surjective-point-is-0-connected :
@@ -112,21 +136,29 @@ abstract
       ( mere-eq-is-0-connected H a x)
       ( trunc-Prop (fiber (point a) x))
       ( λ where refl → unit-trunc-Prop (star , refl))
+```
+
+### If `A` is 0-connected and `B` is `k+1`-truncated then every evaluation map `(A → B) → B` is `k`-truncated
 
-is-trunc-map-ev-point-is-connected :
+```agda
+is-trunc-map-ev-is-connected :
   {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (a : A) →
   is-0-connected A → is-trunc (succ-𝕋 k) B →
-  is-trunc-map k (ev-point' a {B})
-is-trunc-map-ev-point-is-connected k {A} {B} a H K =
+  is-trunc-map k (ev-function B a)
+is-trunc-map-ev-is-connected k {A} {B} a H K =
   is-trunc-map-comp k
-    ( ev-point' star {B})
+    ( ev-function B star)
     ( precomp (point a) B)
     ( is-trunc-map-is-equiv k
       ( universal-property-contr-is-contr star is-contr-unit B))
     ( is-trunc-map-precomp-Π-is-surjective k
       ( is-surjective-point-is-0-connected a H)
       ( λ _ → (B , K)))
+```
+
+### The dependent universal property of 0-connected types
 
+```agda
 equiv-dependent-universal-property-is-0-connected :
   {l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
   ( {l : Level} (P : A → Prop l) →
@@ -143,7 +175,11 @@ apply-dependent-universal-property-is-0-connected :
   {l : Level} (P : A → Prop l) → type-Prop (P a) → (x : A) → type-Prop (P x)
 apply-dependent-universal-property-is-0-connected a H P =
   map-inv-equiv (equiv-dependent-universal-property-is-0-connected a H P)
+```
+
+### A type `A` is 0-connected if and only if every fiber inclusion `B a → Σ A B` is surjective
 
+```agda
 abstract
   is-surjective-fiber-inclusion :
     {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
@@ -172,7 +208,11 @@ abstract
     is-0-connected A
   is-0-connected-is-surjective-fiber-inclusion a H =
     is-0-connected-mere-eq a (mere-eq-is-surjective-fiber-inclusion a H)
+```
+
+### 0-connected types are closed under equivalences
 
+```agda
 is-0-connected-equiv :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} →
   (A ≃ B) → is-0-connected B → is-0-connected A
@@ -184,7 +224,7 @@ is-0-connected-equiv' :
 is-0-connected-equiv' e = is-0-connected-equiv (inv-equiv e)
 ```
 
-### `0`-connected types are closed under cartesian products
+### 0-connected types are closed under cartesian products
 
 ```agda
 module _
@@ -200,7 +240,7 @@ module _
       ( is-contr-product p1 p2)
 ```
 
-### The unit type is `0`-connected
+### The unit type is 0-connected
 
 ```agda
 abstract
@@ -209,7 +249,7 @@ abstract
     is-contr-equiv' unit equiv-unit-trunc-unit-Set is-contr-unit
 ```
 
-### A contractible type is `0`-connected
+### Contractible types are 0-connected
 
 ```agda
 is-0-connected-is-contr :
@@ -219,43 +259,94 @@ is-0-connected-is-contr X p =
   is-contr-equiv X (inv-equiv (equiv-unit-trunc-Set (X , is-set-is-contr p))) p
 ```
 
-### The image of a function with a `0`-connected domain is `0`-connected
+### The image of a function with a 0-connected domain is 0-connected
 
 ```agda
-abstract
-  is-0-connected-im-is-0-connected-domain :
-    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
-    is-0-connected A → is-0-connected (im f)
-  is-0-connected-im-is-0-connected-domain {A = A} {B} f C =
-    apply-universal-property-trunc-Prop
-      ( is-inhabited-is-0-connected C)
-      ( is-contr-Prop _)
-      ( λ a →
-        is-contr-equiv'
-          ( im (map-trunc-Set f))
-          ( equiv-trunc-im-Set f)
-          ( is-contr-im
-            ( trunc-Set B)
-            ( unit-trunc-Set a)
-            ( apply-dependent-universal-property-trunc-Set'
-              ( λ x →
-                set-Prop
-                  ( Id-Prop
-                    ( trunc-Set B)
-                    ( map-trunc-Set f x)
-                    ( map-trunc-Set f (unit-trunc-Set a))))
-              ( λ a' →
-                apply-universal-property-trunc-Prop
-                  ( mere-eq-is-0-connected C a' a)
-                  ( Id-Prop
-                    ( trunc-Set B)
-                    ( map-trunc-Set f (unit-trunc-Set a'))
-                    ( map-trunc-Set f (unit-trunc-Set a)))
-                  ( λ where refl → refl)))))
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
 
-abstract
-  is-0-connected-im-point' :
-    {l1 : Level} {A : UU l1} (f : unit → A) → is-0-connected (im f)
-  is-0-connected-im-point' f =
-    is-0-connected-im-is-0-connected-domain f is-0-connected-unit
+  abstract
+    is-contr-im-map-trunc-Set-is-0-connected-domain' :
+      A → all-elements-merely-equal A → is-contr (im (map-trunc-Set f))
+    is-contr-im-map-trunc-Set-is-0-connected-domain' a C =
+      is-contr-im
+        ( trunc-Set B)
+        ( unit-trunc-Set a)
+        ( apply-dependent-universal-property-trunc-Set'
+          ( λ x →
+            set-Prop
+              ( Id-Prop
+                ( trunc-Set B)
+                ( map-trunc-Set f x)
+                ( map-trunc-Set f (unit-trunc-Set a))))
+          ( λ a' →
+            apply-universal-property-trunc-Prop
+              ( C a' a)
+              ( Id-Prop
+                ( trunc-Set B)
+                ( map-trunc-Set f (unit-trunc-Set a'))
+                ( map-trunc-Set f (unit-trunc-Set a)))
+              ( λ where refl → refl)))
+
+  abstract
+    is-0-connected-im-is-0-connected-domain' :
+      A → all-elements-merely-equal A → is-0-connected (im f)
+    is-0-connected-im-is-0-connected-domain' a C =
+      is-contr-equiv'
+        ( im (map-trunc-Set f))
+        ( equiv-trunc-im-Set f)
+        ( is-contr-im-map-trunc-Set-is-0-connected-domain' a C)
+
+  abstract
+    is-0-connected-im-is-0-connected-domain :
+      is-0-connected A → is-0-connected (im f)
+    is-0-connected-im-is-0-connected-domain C =
+      apply-universal-property-trunc-Prop
+        ( is-inhabited-is-0-connected C)
+        ( is-contr-Prop _)
+        ( λ a →
+          is-0-connected-im-is-0-connected-domain' a (mere-eq-is-0-connected C))
+```
+
+### The image of a point is 0-connected
+
+```agda
+module _
+  {l1 : Level} {A : UU l1}
+  where
+
+  abstract
+    is-0-connected-im-point' : (f : unit → A) → is-0-connected (im f)
+    is-0-connected-im-point' f =
+      is-0-connected-im-is-0-connected-domain f is-0-connected-unit
+
+  abstract
+    is-0-connected-im-point : (a : A) → is-0-connected (im (point a))
+    is-0-connected-im-point a = is-0-connected-im-point' (point a)
+```
+
+### Coproducts of inhabited types are not 0-connected
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  abstract
+    is-not-0-connected-coproduct-has-element :
+      A → B → ¬ is-0-connected (A + B)
+    is-not-0-connected-coproduct-has-element a b H =
+      apply-universal-property-trunc-Prop
+        ( mere-eq-is-0-connected H (inl a) (inr b))
+        ( empty-Prop)
+        ( is-empty-eq-coproduct-inl-inr a b)
+
+  abstract
+    is-not-0-connected-coproduct-is-inhabited :
+      is-inhabited A → is-inhabited B → ¬ is-0-connected (A + B)
+    is-not-0-connected-coproduct-is-inhabited |a| |b| =
+      apply-twice-universal-property-trunc-Prop |a| |b|
+        ( neg-type-Prop (is-0-connected (A + B)))
+        ( is-not-0-connected-coproduct-has-element)
 ```
diff --git a/src/foundation/connected-maps.lagda.md b/src/foundation/connected-maps.lagda.md
index 414edbd171..7613972118 100644
--- a/src/foundation/connected-maps.lagda.md
+++ b/src/foundation/connected-maps.lagda.md
@@ -7,6 +7,7 @@ module foundation.connected-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.connected-types
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
@@ -41,9 +42,12 @@ open import foundation-core.truncated-maps
 
 ## Idea
 
-A map is said to be **`k`-connected** if its
-[fibers](foundation-core.fibers-of-maps.md) are
-[`k`-connected types](foundation.connected-types.md).
+A map is said to be
+{{#concept "`k`-connected" Disambiguation="map of types" Agda=is-connected-map Agda=connected-map}}
+if its [fibers](foundation-core.fibers-of-maps.md) are
+`k`-[connected types](foundation.connected-types.md). In other words, if their
+`k`-[truncations](foundation.truncations.md) are
+[contractible](foundation-core.contractible-types.md).
 
 ## Definitions
 
@@ -85,43 +89,6 @@ module _
 
   emb-inclusion-connected-map : connected-map k A B ↪ (A → B)
   emb-inclusion-connected-map = emb-subtype (is-connected-map-Prop k)
-
-  htpy-connected-map : (f g : connected-map k A B) → UU (l1 ⊔ l2)
-  htpy-connected-map f g = (map-connected-map f) ~ (map-connected-map g)
-
-  refl-htpy-connected-map : (f : connected-map k A B) → htpy-connected-map f f
-  refl-htpy-connected-map f = refl-htpy
-
-  is-torsorial-htpy-connected-map :
-    (f : connected-map k A B) → is-torsorial (htpy-connected-map f)
-  is-torsorial-htpy-connected-map f =
-    is-torsorial-Eq-subtype
-      ( is-torsorial-htpy (map-connected-map f))
-      ( is-prop-is-connected-map k)
-      ( map-connected-map f)
-      ( refl-htpy-connected-map f)
-      ( is-connected-map-connected-map f)
-
-  htpy-eq-connected-map :
-    (f g : connected-map k A B) → f ＝ g → htpy-connected-map f g
-  htpy-eq-connected-map f .f refl = refl-htpy-connected-map f
-
-  is-equiv-htpy-eq-connected-map :
-    (f g : connected-map k A B) → is-equiv (htpy-eq-connected-map f g)
-  is-equiv-htpy-eq-connected-map f =
-    fundamental-theorem-id
-      ( is-torsorial-htpy-connected-map f)
-      ( htpy-eq-connected-map f)
-
-  extensionality-connected-map :
-    (f g : connected-map k A B) → (f ＝ g) ≃ htpy-connected-map f g
-  pr1 (extensionality-connected-map f g) = htpy-eq-connected-map f g
-  pr2 (extensionality-connected-map f g) = is-equiv-htpy-eq-connected-map f g
-
-  eq-htpy-connected-map :
-    (f g : connected-map k A B) → htpy-connected-map f g → (f ＝ g)
-  eq-htpy-connected-map f g =
-    map-inv-equiv (extensionality-connected-map f g)
 ```
 
 ### The type of connected maps into a type
@@ -193,6 +160,51 @@ module _
 
 ## Properties
 
+### Characterizing equality of `k`-connected maps
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2}
+  where
+
+  htpy-connected-map : (f g : connected-map k A B) → UU (l1 ⊔ l2)
+  htpy-connected-map f g = (map-connected-map f) ~ (map-connected-map g)
+
+  refl-htpy-connected-map : (f : connected-map k A B) → htpy-connected-map f f
+  refl-htpy-connected-map f = refl-htpy
+
+  is-torsorial-htpy-connected-map :
+    (f : connected-map k A B) → is-torsorial (htpy-connected-map f)
+  is-torsorial-htpy-connected-map f =
+    is-torsorial-Eq-subtype
+      ( is-torsorial-htpy (map-connected-map f))
+      ( is-prop-is-connected-map k)
+      ( map-connected-map f)
+      ( refl-htpy-connected-map f)
+      ( is-connected-map-connected-map f)
+
+  htpy-eq-connected-map :
+    (f g : connected-map k A B) → f ＝ g → htpy-connected-map f g
+  htpy-eq-connected-map f g H = htpy-eq (ap pr1 H)
+
+  is-equiv-htpy-eq-connected-map :
+    (f g : connected-map k A B) → is-equiv (htpy-eq-connected-map f g)
+  is-equiv-htpy-eq-connected-map f =
+    fundamental-theorem-id
+      ( is-torsorial-htpy-connected-map f)
+      ( htpy-eq-connected-map f)
+
+  extensionality-connected-map :
+    (f g : connected-map k A B) → (f ＝ g) ≃ htpy-connected-map f g
+  pr1 (extensionality-connected-map f g) = htpy-eq-connected-map f g
+  pr2 (extensionality-connected-map f g) = is-equiv-htpy-eq-connected-map f g
+
+  eq-htpy-connected-map :
+    (f g : connected-map k A B) → htpy-connected-map f g → (f ＝ g)
+  eq-htpy-connected-map f g =
+    map-inv-equiv (extensionality-connected-map f g)
+```
+
 ### All maps are `(-2)`-connected
 
 ```agda
@@ -204,6 +216,24 @@ module _
   is-neg-two-connected-map b = is-neg-two-connected (fiber f b)
 ```
 
+### Connected maps are closed under homotopies
+
+```agda
+module _
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f g : A → B}
+  where
+
+  is-connected-map-htpy :
+    (f ~ g) → is-connected-map k g → is-connected-map k f
+  is-connected-map-htpy H G x =
+    is-connected-equiv (inv-equiv-fiber-htpy H x) (G x)
+
+  is-connected-map-htpy' :
+    (f ~ g) → is-connected-map k f → is-connected-map k g
+  is-connected-map-htpy' H F x =
+    is-connected-equiv (equiv-fiber-htpy H x) (F x)
+```
+
 ### Equivalences are `k`-connected for any `k`
 
 ```agda
@@ -227,6 +257,22 @@ module _
   pr2 (connected-map-equiv e) = is-connected-map-equiv e
 ```
 
+### The identity map is `k`-connected for every `k`
+
+```agda
+is-connected-map-id :
+  {l : Level} {k : 𝕋} {A : UU l} → is-connected-map k (id' A)
+is-connected-map-id = is-connected-map-equiv id-equiv
+
+is-connected-map-htpy-id :
+  {l : Level} {k : 𝕋} {A : UU l} {f : A → A} → f ~ id → is-connected-map k f
+is-connected-map-htpy-id H = is-connected-map-htpy _ H is-connected-map-id
+
+is-connected-map-htpy-id' :
+  {l : Level} {k : 𝕋} {A : UU l} {f : A → A} → id ~ f → is-connected-map k f
+is-connected-map-htpy-id' H = is-connected-map-htpy' _ H is-connected-map-id
+```
+
 ### A `(k+1)`-connected map is `k`-connected
 
 ```agda
@@ -300,6 +346,24 @@ module _
     is-connected-equiv (inv-compute-fiber-tot f (x , y)) (H (x , y))
 ```
 
+### A map is an equivalence if it is `k`-connected and `k`-truncated
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  is-contr-map-is-connected-map-is-trunc-map :
+    is-trunc-map k f → is-connected-map k f → is-contr-map f
+  is-contr-map-is-connected-map-is-trunc-map H K x =
+    is-contr-is-connected-is-trunc (H x) (K x)
+
+  is-equiv-is-connected-map-is-trunc-map :
+    is-trunc-map k f → is-connected-map k f → is-equiv f
+  is-equiv-is-connected-map-is-trunc-map H K =
+    is-equiv-is-contr-map (is-contr-map-is-connected-map-is-trunc-map H K)
+```
+
 ### Dependent universal property for connected maps
 
 ```agda
@@ -419,7 +483,7 @@ module _
       contraction-is-connected-map-dependent-universal-property-connected-map b
 ```
 
-### The map `unit-trunc {k}` is `k`-connected
+### The unit map of the `k`-truncation is `k`-connected
 
 ```agda
 module _
diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md
index 06cf448eef..75ef75f011 100644
--- a/src/foundation/connected-types.lagda.md
+++ b/src/foundation/connected-types.lagda.md
@@ -27,6 +27,7 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.precomposition-functions
 open import foundation-core.retracts-of-types
+open import foundation-core.truncated-maps
 open import foundation-core.truncated-types
 open import foundation-core.truncation-levels
 ```
@@ -35,7 +36,10 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-A type is said to be **`k`-connected** if its `k`-truncation is contractible.
+A type is said to be
+{{#concept "`k`-connected" Disambiguation="type" Agda=is-connected Agda=Connected-Type}}
+if its `k`-[truncation](foundation.truncations.md) is
+[contractible](foundation-core.contractible-types.md).
 
 ## Definition
 
@@ -152,9 +156,7 @@ module _
   where
 
   is-connected-retract-of :
-    A retract-of B →
-    is-connected k B →
-    is-connected k A
+    A retract-of B → is-connected k B → is-connected k A
   is-connected-retract-of R =
     is-contr-retract-of (type-trunc k B) (retract-of-trunc-retract-of R)
 ```
@@ -172,6 +174,18 @@ module _
       ( λ B → is-equiv-diagonal-exponential-is-contr H (type-Truncated-Type B))
 ```
 
+### A type that is `k`-connected and `k`-truncated is contractible
+
+```agda
+module _
+  {l1 : Level} {k : 𝕋} {A : UU l1}
+  where
+
+  is-contr-is-connected-is-trunc : is-trunc k A → is-connected k A → is-contr A
+  is-contr-is-connected-is-trunc H =
+    is-contr-equiv (type-trunc k A) (equiv-unit-trunc (A , H))
+```
+
 ### A type that is `(k+1)`-connected is `k`-connected
 
 ```agda
@@ -186,42 +200,6 @@ is-connected-is-connected-succ-𝕋 k H =
         ( H))
 ```
 
-### The total space of a family of `k`-connected types over a `k`-connected type is `k`-connected
-
-```agda
-is-connected-Σ :
-  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} →
-  is-connected k A → ((x : A) → is-connected k (B x)) →
-  is-connected k (Σ A B)
-is-connected-Σ k H K =
-  is-contr-equiv _ (equiv-trunc k (equiv-pr1 K) ∘e equiv-trunc-Σ k) H
-```
-
-### If the total space of a family of `k`-connected types is `k`-connected so is the base
-
-**Proof.** We compute
-
-```text
-  ║Σ (x : A), B x║ₖ ≃ ║Σ (x : A), ║B x║ₖ║ₖ by equiv-trunc-Σ
-                    ≃ ║Σ (x : A), 1 ║ₖ      by k-connectedness of B
-                    ≃ ║A║ₖ                  by the right unit law of Σ
-```
-
-and so, in particular, if the total space is `k`-connected so is the base. □
-
-```agda
-is-connected-base :
-  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} →
-  ((x : A) → is-connected k (B x)) → is-connected k (Σ A B) → is-connected k A
-is-connected-base k {A} {B} K =
-  is-contr-equiv'
-    ( type-trunc k (Σ A B))
-    ( equivalence-reasoning
-      type-trunc k (Σ A B)
-      ≃ type-trunc k (Σ A (type-trunc k ∘ B)) by equiv-trunc-Σ k
-      ≃ type-trunc k A by equiv-trunc k (right-unit-law-Σ-is-contr K))
-```
-
 ### An inhabited type `A` is `k + 1`-connected if and only if its identity types are `k`-connected
 
 ```agda
@@ -271,3 +249,53 @@ module _
                 ( λ where refl → refl)
                 ( center (K a x)))))
 ```
+
+### The total space of a family of `k`-connected types over a `k`-connected type is `k`-connected
+
+```agda
+is-connected-Σ :
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} →
+  is-connected k A → ((x : A) → is-connected k (B x)) →
+  is-connected k (Σ A B)
+is-connected-Σ k H K =
+  is-contr-equiv _ (equiv-trunc k (equiv-pr1 K) ∘e equiv-trunc-Σ k) H
+```
+
+### If the total space of a family of `k`-connected types is `k`-connected so is the base
+
+**Proof.** We compute
+
+```text
+  ║Σ (x : A), B x║ₖ ≃ ║Σ (x : A), ║B x║ₖ║ₖ by equiv-trunc-Σ
+                    ≃ ║Σ (x : A), 1 ║ₖ      by k-connectedness of B
+                    ≃ ║A║ₖ                  by the right unit law of Σ
+```
+
+and so, in particular, if the total space is `k`-connected then so is the base.
+∎
+
+```agda
+is-connected-base :
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} →
+  ((x : A) → is-connected k (B x)) → is-connected k (Σ A B) → is-connected k A
+is-connected-base k {A} {B} K =
+  is-contr-equiv'
+    ( type-trunc k (Σ A B))
+    ( equivalence-reasoning
+      type-trunc k (Σ A B)
+      ≃ type-trunc k (Σ A (type-trunc k ∘ B)) by equiv-trunc-Σ k
+      ≃ type-trunc k A by equiv-trunc k (right-unit-law-Σ-is-contr K))
+```
+
+### If the domain of `f` is `k+1`-connected, then the `k+1`-truncation of `f` is `k`-truncated
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-trunc-map-trunc-succ-is-succ-connected-domain :
+    is-connected (succ-𝕋 k) A → is-trunc-map k (map-trunc (succ-𝕋 k) f)
+  is-trunc-map-trunc-succ-is-succ-connected-domain c =
+    is-trunc-map-is-trunc-succ-codomain-is-contr-domain c is-trunc-type-trunc
+```
diff --git a/src/foundation/diagonals-of-maps.lagda.md b/src/foundation/diagonals-of-maps.lagda.md
index a965e62bc4..8454997692 100644
--- a/src/foundation/diagonals-of-maps.lagda.md
+++ b/src/foundation/diagonals-of-maps.lagda.md
@@ -88,7 +88,7 @@ abstract
     is-trunc-is-equiv k (fiber (ap f) p)
       ( fiber-ap-fiber-diagonal-map f (triple x y p))
       ( is-equiv-fiber-ap-fiber-diagonal-map f (triple x y p))
-      ( is-trunc-map-ap-is-trunc-map k f is-trunc-f x y p)
+      ( is-trunc-map-ap-is-trunc-map-succ k f is-trunc-f x y p)
 
 abstract
   is-trunc-map-is-trunc-diagonal-map :
diff --git a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
index e5ff5b16a5..bec1d7a0cf 100644
--- a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
+++ b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
@@ -187,7 +187,7 @@ module _
   is-equiv-diagonal-into-fibers-precomp-is-epimorphism-Truncated-Type :
     is-epimorphism-Truncated-Type k f →
     {l : Level} (X : Truncated-Type l k) →
-    is-equiv (diagonal-into-fibers-precomp f (type-Truncated-Type X))
+    is-equiv (diagonal-into-fibers-precomp f)
   is-equiv-diagonal-into-fibers-precomp-is-epimorphism-Truncated-Type e X =
     is-equiv-map-section-family
       ( λ g → g , refl)
@@ -202,11 +202,10 @@ module _
     is-equiv (diagonal-into-cocone f (type-Truncated-Type X))
   is-equiv-diagonal-into-cocone-is-epimorphism-Truncated-Type e X =
     is-equiv-comp
-      ( map-equiv (compute-total-fiber-precomp f (type-Truncated-Type X)))
-      ( diagonal-into-fibers-precomp f (type-Truncated-Type X))
+      ( map-equiv (compute-total-fiber-precomp f))
+      ( diagonal-into-fibers-precomp f)
       ( is-equiv-diagonal-into-fibers-precomp-is-epimorphism-Truncated-Type e X)
-      ( is-equiv-map-equiv
-        ( compute-total-fiber-precomp f (type-Truncated-Type X)))
+      ( is-equiv-map-equiv (compute-total-fiber-precomp f))
 
   is-equiv-horizontal-map-cocone-is-epimorphism-Truncated-Type :
     is-epimorphism-Truncated-Type k f →
@@ -241,7 +240,7 @@ module _
         is-contr-equiv
           ( Σ ( B → (type-Truncated-Type X))
               ( λ h → coherence-square-maps f f h g))
-          ( compute-fiber-precomp f (type-Truncated-Type X) g)
+          ( compute-fiber-precomp f g)
           ( is-contr-is-equiv-pr1 (h X) g))
 
   is-epimorphism-is-equiv-vertical-map-cocone-Truncated-Type :
diff --git a/src/foundation/epimorphisms.lagda.md b/src/foundation/epimorphisms.lagda.md
index b7c5bb9ab4..3c78e79e8f 100644
--- a/src/foundation/epimorphisms.lagda.md
+++ b/src/foundation/epimorphisms.lagda.md
@@ -84,7 +84,7 @@ module _
   where
 
   is-equiv-diagonal-into-fibers-precomp-is-epimorphism :
-    is-epimorphism f → is-equiv (diagonal-into-fibers-precomp f X)
+    is-epimorphism f → is-equiv (diagonal-into-fibers-precomp f)
   is-equiv-diagonal-into-fibers-precomp-is-epimorphism e =
     is-equiv-map-section-family
       ( λ g → (g , refl))
@@ -102,10 +102,10 @@ module _
     universal-property-pushout f f (cocone-codiagonal-map f)
   universal-property-pushout-is-epimorphism e X =
     is-equiv-comp
-      ( map-equiv (compute-total-fiber-precomp f X))
-      ( diagonal-into-fibers-precomp f X)
+      ( map-equiv (compute-total-fiber-precomp f))
+      ( diagonal-into-fibers-precomp f)
       ( is-equiv-diagonal-into-fibers-precomp-is-epimorphism f X e)
-      ( is-equiv-map-equiv (compute-total-fiber-precomp f X))
+      ( is-equiv-map-equiv (compute-total-fiber-precomp f))
 ```
 
 If the map `f : A → B` is epi, then its codiagonal is an equivalence.
@@ -142,7 +142,7 @@ If the map `f : A → B` is epi, then its codiagonal is an equivalence.
       ( λ g →
         is-contr-equiv
           ( Σ (B → X) (λ h → coherence-square-maps f f h g))
-          ( compute-fiber-precomp f X g)
+          ( compute-fiber-precomp f g)
           ( is-contr-fam-is-equiv-map-section-family
             ( λ h →
               ( vertical-map-cocone f f
diff --git a/src/foundation/faithful-maps.lagda.md b/src/foundation/faithful-maps.lagda.md
index 0e523f08b3..341c52fb7a 100644
--- a/src/foundation/faithful-maps.lagda.md
+++ b/src/foundation/faithful-maps.lagda.md
@@ -107,12 +107,12 @@ module _
 
   is-0-map-is-faithful : is-faithful f → is-0-map f
   is-0-map-is-faithful H =
-    is-trunc-map-is-trunc-map-ap neg-one-𝕋 f
+    is-trunc-map-succ-is-trunc-map-ap neg-one-𝕋 f
       ( λ x y → is-prop-map-is-emb (H x y))
 
   is-faithful-is-0-map : is-0-map f → is-faithful f
   is-faithful-is-0-map H x y =
-    is-emb-is-prop-map (is-trunc-map-ap-is-trunc-map neg-one-𝕋 f H x y)
+    is-emb-is-prop-map (is-trunc-map-ap-is-trunc-map-succ neg-one-𝕋 f H x y)
 ```
 
 ## Properties
diff --git a/src/foundation/functoriality-dependent-function-types.lagda.md b/src/foundation/functoriality-dependent-function-types.lagda.md
index 9fc8e6c98c..cc9c75b565 100644
--- a/src/foundation/functoriality-dependent-function-types.lagda.md
+++ b/src/foundation/functoriality-dependent-function-types.lagda.md
@@ -49,9 +49,9 @@ first argument, and covariantly in its second argument.
 
 ```agda
 module _
-  { l1 l2 l3 l4 : Level}
-  { A' : UU l1} {B' : A' → UU l2} {A : UU l3} (B : A → UU l4)
-  ( e : A' ≃ A) (f : (a' : A') → B' a' ≃ B (map-equiv e a'))
+  {l1 l2 l3 l4 : Level}
+  {A' : UU l1} {B' : A' → UU l2} {A : UU l3} (B : A → UU l4)
+  (e : A' ≃ A) (f : (a' : A') → B' a' ≃ B (map-equiv e a'))
   where
 
   map-equiv-Π : ((a' : A') → B' a') → ((a : A) → B a)
@@ -85,16 +85,21 @@ module _
                 ( is-section-map-inv-is-equiv (is-equiv-map-equiv e) a))))
 
   equiv-Π : ((a' : A') → B' a') ≃ ((a : A) → B a)
-  pr1 equiv-Π = map-equiv-Π
-  pr2 equiv-Π = is-equiv-map-equiv-Π
+  equiv-Π = (map-equiv-Π , is-equiv-map-equiv-Π)
 ```
 
 #### Computing `map-equiv-Π`
 
 ```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A' : UU l1} {B' : A' → UU l2} {A : UU l3} (B : A → UU l4)
+  (e : A' ≃ A) (f : (a' : A') → B' a' ≃ B (map-equiv e a'))
+  where
+
   compute-map-equiv-Π :
     (h : (a' : A') → B' a') (a' : A') →
-    map-equiv-Π h (map-equiv e a') ＝ map-equiv (f a') (h a')
+    map-equiv-Π B e f h (map-equiv e a') ＝ map-equiv (f a') (h a')
   compute-map-equiv-Π h a' =
     ( ap
       ( λ t →
@@ -112,8 +117,8 @@ module _
     α x refl = refl
 
 id-map-equiv-Π :
-  { l1 l2 : Level} {A : UU l1} (B : A → UU l2) →
-  ( map-equiv-Π B (id-equiv {A = A}) (λ a → id-equiv {A = B a})) ~ id
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) →
+  map-equiv-Π B (id-equiv {A = A}) (λ a → id-equiv {A = B a}) ~ id
 id-map-equiv-Π B h = eq-htpy (compute-map-equiv-Π B id-equiv (λ _ → id-equiv) h)
 ```
 
@@ -121,16 +126,14 @@ id-map-equiv-Π B h = eq-htpy (compute-map-equiv-Π B id-equiv (λ _ → id-equi
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {A : UU l1}
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
   where
 
   equiv-htpy-map-Π-fam-equiv :
-    { B : A → UU l2} {C : A → UU l3} →
-    ( e : fam-equiv B C) (f g : (a : A) → B a) →
-    ( f ~ g) ≃ (map-Π (map-fam-equiv e) f ~ map-Π (map-fam-equiv e) g)
+    (e : fam-equiv B C) (f g : (a : A) → B a) →
+    (f ~ g) ≃ (map-Π (map-fam-equiv e) f ~ map-Π (map-fam-equiv e) g)
   equiv-htpy-map-Π-fam-equiv e f g =
-    equiv-Π-equiv-family
-      ( λ a → equiv-ap (e a) (f a) (g a))
+    equiv-Π-equiv-family (λ a → equiv-ap (e a) (f a) (g a))
 ```
 
 ### Families of truncated maps induce truncated maps on dependent function types
@@ -164,118 +167,110 @@ module _
 ### A family of truncated maps over any map induces a truncated map on dependent function types
 
 ```agda
-is-trunc-map-map-Π-is-trunc-map' :
-  (k : 𝕋) {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-  {J : UU l4} (α : J → I) (f : (i : I) → A i → B i) →
-  ((i : I) → is-trunc-map k (f i)) → is-trunc-map k (map-Π' α f)
-is-trunc-map-map-Π-is-trunc-map' k {J = J} α f H h =
-  is-trunc-equiv' k
-    ( (j : J) → fiber (f (α j)) (h j))
-    ( compute-fiber-map-Π' α f h)
-    ( is-trunc-Π k (λ j → H (α j) (h j)))
-
-is-trunc-map-is-trunc-map-map-Π' :
-  (k : 𝕋) {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-  (f : (i : I) → A i → B i) →
-  ({l : Level} {J : UU l} (α : J → I) → is-trunc-map k (map-Π' α f)) →
-  (i : I) → is-trunc-map k (f i)
-is-trunc-map-is-trunc-map-map-Π' k {A = A} {B} f H i b =
-  is-trunc-equiv' k
-    ( fiber (map-Π (λ _ → f i)) (point b))
-    ( equiv-Σ
-      ( λ a → f i a ＝ b)
-      ( equiv-universal-property-unit (A i))
-      ( λ h → equiv-ap
-        ( equiv-universal-property-unit (B i))
-        ( map-Π (λ _ → f i) h)
-        ( point b)))
-    ( H (λ _ → i) (point b))
-
-is-emb-map-Π-is-emb' :
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3} →
-  {J : UU l4} (α : J → I) (f : (i : I) → A i → B i) →
-  ((i : I) → is-emb (f i)) → is-emb (map-Π' α f)
-is-emb-map-Π-is-emb' α f H =
-  is-emb-is-prop-map
-    ( is-trunc-map-map-Π-is-trunc-map' neg-one-𝕋 α f
-      ( λ i → is-prop-map-is-emb (H i)))
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
+  where
+
+  is-trunc-map-map-Π' :
+    (k : 𝕋) {l4 : Level} {J : UU l4} (α : J → I) (f : (i : I) → A i → B i) →
+    ((i : I) → is-trunc-map k (f i)) → is-trunc-map k (map-Π' α f)
+  is-trunc-map-map-Π' k {J = J} α f H h =
+    is-trunc-equiv' k
+      ( (j : J) → fiber (f (α j)) (h j))
+      ( compute-fiber-map-Π' α f h)
+      ( is-trunc-Π k (λ j → H (α j) (h j)))
+
+  is-trunc-map-is-trunc-map-map-Π' :
+    (k : 𝕋) (f : (i : I) → A i → B i) →
+    ({l : Level} {J : UU l} (α : J → I) → is-trunc-map k (map-Π' α f)) →
+    (i : I) → is-trunc-map k (f i)
+  is-trunc-map-is-trunc-map-map-Π' k f H i b =
+    is-trunc-equiv' k
+      ( fiber (map-Π (λ _ → f i)) (point b))
+      ( equiv-Σ
+        ( λ a → f i a ＝ b)
+        ( equiv-universal-property-unit (A i))
+        ( λ h →
+          equiv-ap
+            ( equiv-universal-property-unit (B i))
+            ( map-Π (λ _ → f i) h)
+            ( point b)))
+      ( H (λ _ → i) (point b))
+
+  is-emb-map-Π' :
+    {l4 : Level} {J : UU l4} (α : J → I) (f : (i : I) → A i → B i) →
+    ((i : I) → is-emb (f i)) → is-emb (map-Π' α f)
+  is-emb-map-Π' α f H =
+    is-emb-is-prop-map
+      ( is-trunc-map-map-Π' neg-one-𝕋 α f (λ i → is-prop-map-is-emb (H i)))
+```
+
+### The action on homotopies of equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A' : UU l1} (B' : A' → UU l2) {A : UU l3} (B : A → UU l4)
+  where
+
+  HTPY-map-equiv-Π :
+    (e e' : A' ≃ A) → htpy-equiv e e' → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  HTPY-map-equiv-Π e e' H =
+    (f : (a' : A') → B' a' ≃ B (map-equiv e a')) →
+    (f' : (a' : A') → B' a' ≃ B (map-equiv e' a')) →
+    (K : (a' : A') → tr B (H a') ∘ map-equiv (f a') ~ map-equiv (f' a')) →
+    map-equiv-Π B e f ~ map-equiv-Π B e' f'
+
+  htpy-map-equiv-Π-refl-htpy :
+    (e : A' ≃ A) → HTPY-map-equiv-Π e e (refl-htpy-equiv e)
+  htpy-map-equiv-Π-refl-htpy e f f' K =
+    ( htpy-map-Π
+      ( λ a →
+        ( tr B (is-section-map-inv-is-equiv (is-equiv-map-equiv e) a)) ·l
+        ( K (map-inv-is-equiv (is-equiv-map-equiv e) a)))) ·r
+    ( precomp-Π (map-inv-is-equiv (is-equiv-map-equiv e)) B')
+
+  abstract
+    htpy-map-equiv-Π :
+      (e e' : A' ≃ A) (H : htpy-equiv e e') → HTPY-map-equiv-Π e e' H
+    htpy-map-equiv-Π e =
+      ind-htpy-equiv e
+        ( HTPY-map-equiv-Π e)
+        ( htpy-map-equiv-Π-refl-htpy e)
+
+    compute-htpy-map-equiv-Π :
+      (e : A' ≃ A) →
+      htpy-map-equiv-Π e e (refl-htpy-equiv e) ＝ htpy-map-equiv-Π-refl-htpy e
+    compute-htpy-map-equiv-Π e =
+      compute-ind-htpy-equiv e
+        ( HTPY-map-equiv-Π e)
+        ( htpy-map-equiv-Π-refl-htpy e)
 ```
 
-###
+### The action on automorphisms
 
 ```agda
-HTPY-map-equiv-Π :
-  { l1 l2 l3 l4 : Level}
-  { A' : UU l1} (B' : A' → UU l2) {A : UU l3} (B : A → UU l4)
-  ( e e' : A' ≃ A) (H : htpy-equiv e e') →
-  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-HTPY-map-equiv-Π {A' = A'} B' {A} B e e' H =
-  ( f : (a' : A') → B' a' ≃ B (map-equiv e a')) →
-  ( f' : (a' : A') → B' a' ≃ B (map-equiv e' a')) →
-  ( K : (a' : A') →
-        ((tr B (H a')) ∘ (map-equiv (f a'))) ~ (map-equiv (f' a'))) →
-  ( map-equiv-Π B e f) ~ (map-equiv-Π B e' f')
-
-htpy-map-equiv-Π-refl-htpy :
-  { l1 l2 l3 l4 : Level}
-  { A' : UU l1} {B' : A' → UU l2} {A : UU l3} (B : A → UU l4)
-  ( e : A' ≃ A) →
-  HTPY-map-equiv-Π B' B e e (refl-htpy-equiv e)
-htpy-map-equiv-Π-refl-htpy {B' = B'} B e f f' K =
-  ( htpy-map-Π
-    ( λ a →
-      ( tr B (is-section-map-inv-is-equiv (is-equiv-map-equiv e) a)) ·l
-      ( K (map-inv-is-equiv (is-equiv-map-equiv e) a)))) ·r
-  ( precomp-Π (map-inv-is-equiv (is-equiv-map-equiv e)) B')
-
-abstract
-  htpy-map-equiv-Π :
-    { l1 l2 l3 l4 : Level}
-    { A' : UU l1} {B' : A' → UU l2} {A : UU l3} (B : A → UU l4)
-    ( e e' : A' ≃ A) (H : htpy-equiv e e') →
-    HTPY-map-equiv-Π B' B e e' H
-  htpy-map-equiv-Π {B' = B'} B e e' H f f' K =
-    ind-htpy-equiv e
-      ( HTPY-map-equiv-Π B' B e)
-      ( htpy-map-equiv-Π-refl-htpy B e)
-      e' H f f' K
-
-  compute-htpy-map-equiv-Π :
-    { l1 l2 l3 l4 : Level}
-    { A' : UU l1} {B' : A' → UU l2} {A : UU l3} (B : A → UU l4)
-    ( e : A' ≃ A) →
-    ( htpy-map-equiv-Π {B' = B'} B e e (refl-htpy-equiv e)) ＝
-    ( ( htpy-map-equiv-Π-refl-htpy B e))
-  compute-htpy-map-equiv-Π {B' = B'} B e =
-    compute-ind-htpy-equiv e
-      ( HTPY-map-equiv-Π B' B e)
-      ( htpy-map-equiv-Π-refl-htpy B e)
-
-map-automorphism-Π :
-  { l1 l2 : Level} {A : UU l1} {B : A → UU l2}
-  ( e : A ≃ A) (f : (a : A) → B a ≃ B (map-equiv e a)) →
-  ( (a : A) → B a) → ((a : A) → B a)
-map-automorphism-Π {B = B} e f =
-  ( map-Π (λ a → (map-inv-is-equiv (is-equiv-map-equiv (f a))))) ∘
-  ( precomp-Π (map-equiv e) B)
-
-abstract
-  is-equiv-map-automorphism-Π :
-    { l1 l2 : Level} {A : UU l1} {B : A → UU l2}
-    ( e : A ≃ A) (f : (a : A) → B a ≃ B (map-equiv e a)) →
-    is-equiv (map-automorphism-Π e f)
-  is-equiv-map-automorphism-Π {B = B} e f =
-    is-equiv-comp _ _
-      ( is-equiv-precomp-Π-is-equiv (is-equiv-map-equiv e) B)
-      ( is-equiv-map-Π-is-fiberwise-equiv
-        ( λ a → is-equiv-map-inv-is-equiv (is-equiv-map-equiv (f a))))
-
-automorphism-Π :
-  { l1 l2 : Level} {A : UU l1} {B : A → UU l2}
-  ( e : A ≃ A) (f : (a : A) → B a ≃ B (map-equiv e a)) →
-  ( (a : A) → B a) ≃ ((a : A) → B a)
-pr1 (automorphism-Π e f) = map-automorphism-Π e f
-pr2 (automorphism-Π e f) = is-equiv-map-automorphism-Π e f
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  (e : A ≃ A) (f : (a : A) → B a ≃ B (map-equiv e a))
+  where
+
+  map-automorphism-Π : ((a : A) → B a) → ((a : A) → B a)
+  map-automorphism-Π =
+    ( map-Π (λ a → (map-inv-is-equiv (is-equiv-map-equiv (f a))))) ∘
+    ( precomp-Π (map-equiv e) B)
+
+  abstract
+    is-equiv-map-automorphism-Π :
+      is-equiv map-automorphism-Π
+    is-equiv-map-automorphism-Π =
+      is-equiv-comp _ _
+        ( is-equiv-precomp-Π-is-equiv (is-equiv-map-equiv e) B)
+        ( is-equiv-map-Π-is-fiberwise-equiv
+          ( λ a → is-equiv-map-inv-is-equiv (is-equiv-map-equiv (f a))))
+
+  automorphism-Π : ((a : A) → B a) ≃ ((a : A) → B a)
+  automorphism-Π = (map-automorphism-Π , is-equiv-map-automorphism-Π)
 ```
 
 ### Families of retracts induce retracts of dependent function types
diff --git a/src/foundation/functoriality-function-types.lagda.md b/src/foundation/functoriality-function-types.lagda.md
index a86808a6d2..7797a47622 100644
--- a/src/foundation/functoriality-function-types.lagda.md
+++ b/src/foundation/functoriality-function-types.lagda.md
@@ -71,10 +71,7 @@ module _
     is-trunc-map k f →
     {l3 : Level} (A : UU l3) → is-trunc-map k (postcomp A f)
   is-trunc-map-postcomp-is-trunc-map is-trunc-f A =
-    is-trunc-map-map-Π-is-trunc-map' k
-      ( terminal-map A)
-      ( point f)
-      ( point is-trunc-f)
+    is-trunc-map-map-Π' k (terminal-map A) (point f) (point is-trunc-f)
 
   is-trunc-map-is-trunc-map-postcomp :
     ({l3 : Level} (A : UU l3) → is-trunc-map k (postcomp A f)) →
diff --git a/src/foundation/mere-path-cosplit-maps.lagda.md b/src/foundation/mere-path-cosplit-maps.lagda.md
index 94523eeebc..a32550ef06 100644
--- a/src/foundation/mere-path-cosplit-maps.lagda.md
+++ b/src/foundation/mere-path-cosplit-maps.lagda.md
@@ -106,7 +106,7 @@ is-mere-path-cosplit-is-trunc neg-two-𝕋 is-trunc-f =
   unit-trunc-Prop (retraction-is-contr-map is-trunc-f)
 is-mere-path-cosplit-is-trunc (succ-𝕋 k) {f = f} is-trunc-f x y =
   is-mere-path-cosplit-is-trunc k
-    ( is-trunc-map-ap-is-trunc-map k f is-trunc-f x y)
+    ( is-trunc-map-ap-is-trunc-map-succ k f is-trunc-f x y)
 ```
 
 ### If a map is `k`-path-cosplit then it is merely `k+1`-path-cosplit
diff --git a/src/foundation/morphisms-arrows.lagda.md b/src/foundation/morphisms-arrows.lagda.md
index 7abfa99887..0c53c53eb7 100644
--- a/src/foundation/morphisms-arrows.lagda.md
+++ b/src/foundation/morphisms-arrows.lagda.md
@@ -10,16 +10,17 @@ module foundation.morphisms-arrows where
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
+open import foundation.homotopies
 open import foundation.postcomposition-functions
 open import foundation.precomposition-functions
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.commuting-squares-of-maps
+open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-function-types
 open import foundation-core.functoriality-dependent-pair-types
-open import foundation-core.homotopies
 open import foundation-core.identity-types
 ```
 
@@ -74,6 +75,44 @@ module _
   coh-hom-arrow = pr2 ∘ pr2
 ```
 
+```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
+
+  coherence-hom-arrow' : (A → X) → (B → Y) → UU (l1 ⊔ l4)
+  coherence-hom-arrow' i = coherence-square-maps' i f g
+
+  hom-arrow' : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-arrow' = Σ (A → X) (λ i → Σ (B → Y) (coherence-hom-arrow' i))
+
+  map-domain-hom-arrow' : hom-arrow' → A → X
+  map-domain-hom-arrow' = pr1
+
+  map-codomain-hom-arrow' : hom-arrow' → B → Y
+  map-codomain-hom-arrow' = pr1 ∘ pr2
+
+  coh-hom-arrow' :
+    (h : hom-arrow') →
+    coherence-hom-arrow' (map-domain-hom-arrow' h) (map-codomain-hom-arrow' h)
+  coh-hom-arrow' = pr2 ∘ pr2
+
+  equiv-hom-arrow-hom-arrow' : hom-arrow' ≃ hom-arrow f g
+  equiv-hom-arrow-hom-arrow' =
+    equiv-tot (λ i → equiv-tot (λ j → equiv-inv-htpy (g ∘ i) (j ∘ f)))
+
+  equiv-hom-arrow'-hom-arrow : hom-arrow f g ≃ hom-arrow'
+  equiv-hom-arrow'-hom-arrow =
+    equiv-tot (λ i → equiv-tot (λ j → equiv-inv-htpy (j ∘ f) (g ∘ i)))
+
+  hom-arrow-hom-arrow' : hom-arrow' → hom-arrow f g
+  hom-arrow-hom-arrow' = map-equiv equiv-hom-arrow-hom-arrow'
+
+  hom-arrow'-hom-arrow : hom-arrow f g → hom-arrow'
+  hom-arrow'-hom-arrow = map-equiv equiv-hom-arrow'-hom-arrow
+```
+
 ## Operations
 
 ### The identity morphism of arrows
@@ -94,11 +133,14 @@ where the homotopy `id ∘ f ~ f ∘ id` is the reflexivity homotopy.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
   where
 
-  id-hom-arrow : hom-arrow f f
-  id-hom-arrow = (id , id , refl-htpy)
+  id-hom-arrow' : (f : A → B) → hom-arrow f f
+  id-hom-arrow' f = (id , id , refl-htpy)
+
+  id-hom-arrow : {f : A → B} → hom-arrow f f
+  id-hom-arrow {f} = id-hom-arrow' f
 ```
 
 ### Composition of morphisms of arrows
@@ -165,12 +207,48 @@ module _
       ( coh-hom-arrow g h b)
 
   comp-hom-arrow : hom-arrow f h
-  pr1 comp-hom-arrow =
-    map-domain-comp-hom-arrow
-  pr1 (pr2 comp-hom-arrow) =
-    map-codomain-comp-hom-arrow
-  pr2 (pr2 comp-hom-arrow) =
-    coh-comp-hom-arrow
+  comp-hom-arrow =
+    ( map-domain-comp-hom-arrow ,
+      map-codomain-comp-hom-arrow ,
+      coh-comp-hom-arrow)
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
+  (f : A → B) (g : X → Y) (h : U → V) (b : hom-arrow' g h) (a : hom-arrow' f g)
+  where
+
+  map-domain-comp-hom-arrow' : A → U
+  map-domain-comp-hom-arrow' =
+    map-domain-hom-arrow' g h b ∘ map-domain-hom-arrow' f g a
+
+  map-codomain-comp-hom-arrow' : B → V
+  map-codomain-comp-hom-arrow' =
+    map-codomain-hom-arrow' g h b ∘ map-codomain-hom-arrow' f g a
+
+  coh-comp-hom-arrow' :
+    coherence-hom-arrow' f h
+      ( map-domain-comp-hom-arrow')
+      ( map-codomain-comp-hom-arrow')
+  coh-comp-hom-arrow' =
+    pasting-horizontal-coherence-square-maps'
+      ( map-domain-hom-arrow' f g a)
+      ( map-domain-hom-arrow' g h b)
+      ( f)
+      ( g)
+      ( h)
+      ( map-codomain-hom-arrow' f g a)
+      ( map-codomain-hom-arrow' g h b)
+      ( coh-hom-arrow' f g a)
+      ( coh-hom-arrow' g h b)
+
+  comp-hom-arrow' : hom-arrow' f h
+  comp-hom-arrow' =
+    ( map-domain-comp-hom-arrow' ,
+      map-codomain-comp-hom-arrow' ,
+      coh-comp-hom-arrow')
 ```
 
 ### Transposing morphisms of arrows
diff --git a/src/foundation/path-cosplit-maps.lagda.md b/src/foundation/path-cosplit-maps.lagda.md
index 6e8f984ada..dbb0e02eff 100644
--- a/src/foundation/path-cosplit-maps.lagda.md
+++ b/src/foundation/path-cosplit-maps.lagda.md
@@ -170,7 +170,8 @@ is-path-cosplit-is-trunc :
 is-path-cosplit-is-trunc neg-two-𝕋 is-trunc-f =
   retraction-is-contr-map is-trunc-f
 is-path-cosplit-is-trunc (succ-𝕋 k) {f = f} is-trunc-f x y =
-  is-path-cosplit-is-trunc k (is-trunc-map-ap-is-trunc-map k f is-trunc-f x y)
+  is-path-cosplit-is-trunc k
+    ( is-trunc-map-ap-is-trunc-map-succ k f is-trunc-f x y)
 ```
 
 ### If a map is `k`-path-cosplit then it is `k+1`-path-cosplit
diff --git a/src/foundation/precomposition-dependent-functions.lagda.md b/src/foundation/precomposition-dependent-functions.lagda.md
index fef97c901d..d1bcc3dbb4 100644
--- a/src/foundation/precomposition-dependent-functions.lagda.md
+++ b/src/foundation/precomposition-dependent-functions.lagda.md
@@ -10,13 +10,20 @@ open import foundation-core.precomposition-dependent-functions public
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.dependent-homotopies
+open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
 open import foundation.dependent-universal-property-equivalences
 open import foundation.function-extensionality
+open import foundation.sections
+open import foundation.transport-along-homotopies
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.commuting-squares-of-maps
+open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.equivalences
+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
@@ -30,6 +37,104 @@ open import foundation-core.type-theoretic-principle-of-choice
 
 ## Properties
 
+### Computations of the fibers of `precomp-Π`
+
+The fiber of `- ∘ f : ((b : B) → U b) → ((a : A) → U (f a))` at
+`g ∘ f : (b : B) → U b` is equivalent to the type of maps `h : (b : B) → U b`
+equipped with a homotopy witnessing that the square
+
+```text
+        f
+    A -----> B
+    |        |
+  f |        | h
+    ∨        ∨
+    B ---> U ∘ f
+        g
+```
+
+commutes.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (U : B → UU l3)
+  where
+
+  compute-extension-fiber-precomp-Π' :
+    (g : (a : A) → U (f a)) →
+    fiber (precomp-Π f U) g ≃
+    Σ ((b : B) → U b) (λ h → (a : A) → (h ∘ f) a ＝ g a)
+  compute-extension-fiber-precomp-Π' g =
+    equiv-tot (λ h → equiv-funext)
+
+  compute-extension-fiber-precomp-Π :
+    (g : (a : A) → U (f a)) →
+    fiber (precomp-Π f U) g ≃ Σ ((b : B) → U b) (λ h → g ~ h ∘ f)
+  compute-extension-fiber-precomp-Π g =
+    equiv-tot (λ h → equiv-funext) ∘e equiv-fiber (precomp-Π f U) g
+
+  compute-fiber-precomp-Π :
+    (g : (b : B) → U b) →
+    fiber (precomp-Π f U) (g ∘ f) ≃ Σ ((b : B) → U b) (λ h → g ∘ f ~ h ∘ f)
+  compute-fiber-precomp-Π g =
+    compute-extension-fiber-precomp-Π (g ∘ f)
+
+  compute-total-fiber-precomp-Π :
+    Σ ((b : B) → U b) (λ g → fiber (precomp-Π f U) (g ∘ f)) ≃
+    Σ ((b : B) → U b) (λ u → Σ ((b : B) → U b) (λ v → u ∘ f ~ v ∘ f))
+  compute-total-fiber-precomp-Π = equiv-tot compute-fiber-precomp-Π
+
+  diagonal-into-fibers-precomp-Π :
+    ((b : B) → U b) → Σ ((b : B) → U b) (λ g → fiber (precomp-Π f U) (g ∘ f))
+  diagonal-into-fibers-precomp-Π = map-section-family (λ g → (g , refl))
+```
+
+- In
+  [`foundation.universal-property-family-of-fibers-of-maps`](foundation.universal-property-family-of-fibers-of-maps.md)
+  we compute the fiber family of dependent precomposition maps as a dependent
+  product
+  ```text
+    dependent-product-characterization-fiber-precomp-Π :
+      fiber (precomp-Π f U) g ≃
+      ( (b : B) →
+        Σ (u : U b),
+          (((a , p) : fiber f b) → dependent-identification U p (g a) u)).
+  ```
+
+### The action of dependent precomposition on homotopies
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
+  {f g : A → B} (H : f ~ g) (C : B → UU l3) (h : (y : B) → C y)
+  where
+
+  eq-htpy-precomp-Π : (λ x → tr C (H x) (precomp-Π f C h x)) ＝ precomp-Π g C h
+  eq-htpy-precomp-Π = eq-htpy (htpy-htpy-precomp-Π H C h)
+
+  htpy-precomp-Π :
+    dependent-identification
+      ( λ v → (a : A) → C (v a))
+      ( eq-htpy H)
+      ( precomp-Π f C h)
+      ( precomp-Π g C h)
+  htpy-precomp-Π =
+    compute-tr-htpy (λ _ → C) H (precomp-Π f C h) ∙ eq-htpy-precomp-Π
+
+  eq-htpy-precomp-Π' :
+    precomp-Π f C h ＝ (λ x → inv-tr C (H x) (precomp-Π g C h x))
+  eq-htpy-precomp-Π' = eq-htpy (htpy-htpy-precomp-Π' H C h)
+
+  htpy-precomp-Π' :
+    dependent-identification'
+      ( λ v → (a : A) → C (v a))
+      ( eq-htpy H)
+      ( precomp-Π f C h)
+      ( precomp-Π g C h)
+  htpy-precomp-Π' =
+    eq-htpy-precomp-Π' ∙ inv (compute-inv-tr-htpy (λ _ → C) H (precomp-Π g C h))
+```
+
 ### Equivalences induce an equivalence from the type of homotopies between two dependent functions to the type of homotopies between their precomposites
 
 ```agda
@@ -127,7 +232,7 @@ is-trunc-map-succ-precomp-Π :
   ((g h : (b : B) → C b) → is-trunc-map k (precomp-Π f (eq-value g h))) →
   is-trunc-map (succ-𝕋 k) (precomp-Π f C)
 is-trunc-map-succ-precomp-Π {k = k} {f = f} {C = C} H =
-  is-trunc-map-is-trunc-map-ap k (precomp-Π f C)
+  is-trunc-map-succ-is-trunc-map-ap k (precomp-Π f C)
     ( λ g h →
       is-trunc-map-top-is-trunc-map-bottom-is-equiv k
         ( ap (precomp-Π f C))
diff --git a/src/foundation/precomposition-functions.lagda.md b/src/foundation/precomposition-functions.lagda.md
index 9e48f70cfd..51c0079846 100644
--- a/src/foundation/precomposition-functions.lagda.md
+++ b/src/foundation/precomposition-functions.lagda.md
@@ -131,25 +131,25 @@ commutes.
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (X : UU l3)
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) {X : UU l3}
   where
 
-  compute-coherence-triangle-fiber-precomp' :
+  compute-extension-fiber-precomp' :
     (g : A → X) →
     fiber (precomp f X) g ≃ Σ (B → X) (λ h → coherence-triangle-maps' g h f)
-  compute-coherence-triangle-fiber-precomp' g = equiv-tot (λ _ → equiv-funext)
+  compute-extension-fiber-precomp' g = equiv-tot (λ _ → equiv-funext)
 
-  compute-coherence-triangle-fiber-precomp :
+  compute-extension-fiber-precomp :
     (g : A → X) →
     fiber (precomp f X) g ≃ Σ (B → X) (λ h → coherence-triangle-maps g h f)
-  compute-coherence-triangle-fiber-precomp g =
+  compute-extension-fiber-precomp g =
     equiv-tot (λ _ → equiv-funext) ∘e equiv-fiber (precomp f X) g
 
   compute-fiber-precomp :
     (g : B → X) →
     fiber (precomp f X) (g ∘ f) ≃
     Σ (B → X) (λ h → coherence-square-maps f f h g)
-  compute-fiber-precomp g = compute-coherence-triangle-fiber-precomp (g ∘ f)
+  compute-fiber-precomp g = compute-extension-fiber-precomp (g ∘ f)
 
   compute-total-fiber-precomp :
     Σ (B → X) (λ g → fiber (precomp f X) (g ∘ f)) ≃
diff --git a/src/foundation/transport-along-homotopies.lagda.md b/src/foundation/transport-along-homotopies.lagda.md
index 577c47c512..890a38d330 100644
--- a/src/foundation/transport-along-homotopies.lagda.md
+++ b/src/foundation/transport-along-homotopies.lagda.md
@@ -11,11 +11,11 @@ open import foundation.action-on-identifications-functions
 open import foundation.function-extensionality
 open import foundation.homotopy-induction
 open import foundation.transport-along-higher-identifications
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.homotopies
 open import foundation-core.identity-types
-open import foundation-core.transport-along-identifications
 ```
 
 </details>
@@ -41,6 +41,10 @@ module _
     (f ~ g) → ((x : A) → C x (f x)) → ((x : A) → C x (g x))
   tr-htpy H f' x = tr (C x) (H x) (f' x)
 
+  inv-tr-htpy :
+    (f ~ g) → ((x : A) → C x (g x)) → ((x : A) → C x (f x))
+  inv-tr-htpy H f' x = inv-tr (C x) (H x) (f' x)
+
   tr-htpy² :
     {H K : f ~ g} (L : H ~ K) (f' : (x : A) → C x (f x)) →
     tr-htpy H f' ~ tr-htpy K f'
@@ -82,3 +86,37 @@ module _
         ( λ _ → statement-compute-tr-htpy)
         ( base-case-compute-tr-htpy)
 ```
+
+### Inverse transport along a homotopy `H` is homotopic to inverse transport along the identification `eq-htpy H`
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3)
+  where
+
+  statement-compute-inv-tr-htpy :
+    {f g : (x : A) → B x} (H : f ~ g) → UU (l1 ⊔ l3)
+  statement-compute-inv-tr-htpy H =
+    inv-tr (λ u → (x : A) → C x (u x)) (eq-htpy H) ~ inv-tr-htpy C H
+
+  base-case-compute-inv-tr-htpy :
+    {f : (x : A) → B x} → statement-compute-inv-tr-htpy (refl-htpy' f)
+  base-case-compute-inv-tr-htpy =
+    htpy-eq (ap (inv-tr (λ u → (x : A) → C x (u x))) (eq-htpy-refl-htpy _))
+
+  abstract
+    compute-inv-tr-htpy :
+      {f g : (x : A) → B x} (H : f ~ g) → statement-compute-inv-tr-htpy H
+    compute-inv-tr-htpy {f} =
+      ind-htpy f
+        ( λ _ → statement-compute-inv-tr-htpy)
+        ( base-case-compute-inv-tr-htpy)
+
+    compute-inv-tr-htpy-refl-htpy :
+      {f : (x : A) → B x} →
+      compute-inv-tr-htpy (refl-htpy' f) ＝ base-case-compute-inv-tr-htpy
+    compute-inv-tr-htpy-refl-htpy {f} =
+      compute-ind-htpy f
+        ( λ _ → statement-compute-inv-tr-htpy)
+        ( base-case-compute-inv-tr-htpy)
+```
diff --git a/src/foundation/truncation-equivalences.lagda.md b/src/foundation/truncation-equivalences.lagda.md
index 5462a0bf32..da39546ed6 100644
--- a/src/foundation/truncation-equivalences.lagda.md
+++ b/src/foundation/truncation-equivalences.lagda.md
@@ -29,9 +29,12 @@ 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.precomposition-dependent-functions
 open import foundation-core.precomposition-functions
+open import foundation-core.retractions
 open import foundation-core.sections
 open import foundation-core.transport-along-identifications
+open import foundation-core.truncated-maps
 open import foundation-core.truncated-types
 open import foundation-core.truncation-levels
 ```
@@ -67,6 +70,14 @@ module _
   is-truncation-equivalence-truncation-equivalence :
     is-truncation-equivalence k map-truncation-equivalence
   is-truncation-equivalence-truncation-equivalence = pr2 f
+
+  map-trunc-truncation-equivalence : type-trunc k A → type-trunc k B
+  map-trunc-truncation-equivalence = map-trunc k map-truncation-equivalence
+
+  equiv-trunc-truncation-equivalence : type-trunc k A ≃ type-trunc k B
+  equiv-trunc-truncation-equivalence =
+    ( map-trunc-truncation-equivalence ,
+      is-truncation-equivalence-truncation-equivalence)
 ```
 
 ## Properties
@@ -123,7 +134,7 @@ is-truncation-equivalence-is-equiv-precomp k {A} {B} f H =
         ( H _ X))
 ```
 
-### An equivalence is a `k`-equivalence for all `k`
+### Equivalences are `k`-equivalences for all `k`
 
 ```agda
 module _
@@ -135,6 +146,32 @@ module _
   is-truncation-equivalence-is-equiv e = is-equiv-map-equiv-trunc k (f , e)
 ```
 
+### The identity map is a `k`-equivalence for all `k`
+
+```agda
+is-truncation-equivalence-id :
+  {l : Level} {k : 𝕋} {A : UU l} → is-truncation-equivalence k (id' A)
+is-truncation-equivalence-id = is-truncation-equivalence-is-equiv id is-equiv-id
+```
+
+### The `k`-equivalences are closed under homotopies
+
+```agda
+module _
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f g : A → B}
+  where
+
+  is-truncation-equivalence-htpy :
+    f ~ g → is-truncation-equivalence k g → is-truncation-equivalence k f
+  is-truncation-equivalence-htpy H =
+    is-equiv-htpy (map-trunc k g) (htpy-trunc H)
+
+  is-truncation-equivalence-htpy' :
+    f ~ g → is-truncation-equivalence k f → is-truncation-equivalence k g
+  is-truncation-equivalence-htpy' H =
+    is-equiv-htpy' (map-trunc k f) (htpy-trunc H)
+```
+
 ### Every `k`-connected map is a `k`-equivalence
 
 ```agda
@@ -164,7 +201,7 @@ module _
   is-truncation-equivalence-comp g f ef eg =
     is-equiv-htpy
       ( map-trunc k g ∘ map-trunc k f)
-        ( preserves-comp-map-trunc k g f)
+      ( preserves-comp-map-trunc k g f)
       ( is-equiv-comp (map-trunc k g) (map-trunc k f) ef eg)
 
   truncation-equivalence-comp :
@@ -191,14 +228,14 @@ module _
 
   is-truncation-equivalence-left-factor :
     is-truncation-equivalence k f → is-truncation-equivalence k g
-  is-truncation-equivalence-left-factor ef =
+  is-truncation-equivalence-left-factor =
     is-equiv-left-factor
       ( map-trunc k g)
       ( map-trunc k f)
-      ( is-equiv-htpy
+      ( is-equiv-htpy'
         ( map-trunc k (g ∘ f))
-        ( inv-htpy (preserves-comp-map-trunc k g f)) e)
-      ( ef)
+        ( preserves-comp-map-trunc k g f)
+        ( e))
 
   is-truncation-equivalence-right-factor :
     is-truncation-equivalence k g → is-truncation-equivalence k f
@@ -207,12 +244,44 @@ module _
       ( map-trunc k g)
       ( map-trunc k f)
       ( eg)
-      ( is-equiv-htpy
+      ( is-equiv-htpy'
         ( map-trunc k (g ∘ f))
-        ( inv-htpy (preserves-comp-map-trunc k g f))
+        ( preserves-comp-map-trunc k g f)
         ( e))
 ```
 
+### Sections of `k`-equivalences are `k`-equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  is-truncation-equivalence-map-section :
+    (k : 𝕋) (s : section f) →
+    is-truncation-equivalence k f →
+    is-truncation-equivalence k (map-section f s)
+  is-truncation-equivalence-map-section k (s , h) =
+    is-truncation-equivalence-right-factor f s
+      ( is-truncation-equivalence-is-equiv (f ∘ s) (is-equiv-htpy-id h))
+```
+
+### Retractions of `k`-equivalences are `k`-equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  is-truncation-equivalence-map-retraction :
+    (k : 𝕋) (r : retraction f) →
+    is-truncation-equivalence k f →
+    is-truncation-equivalence k (map-retraction f r)
+  is-truncation-equivalence-map-retraction k (r , h) =
+    is-truncation-equivalence-left-factor r f
+      ( is-truncation-equivalence-is-equiv (r ∘ f) (is-equiv-htpy-id h))
+```
+
 ### Composing `k`-equivalences with equivalences
 
 ```agda
@@ -244,27 +313,44 @@ module _
     (g : B → C) (f : A ≃ B) →
     is-truncation-equivalence k g →
     is-truncation-equivalence k (g ∘ map-equiv f)
-  is-truncation-equivalence-equiv-is-truncation-equivalence g f eg =
-    is-truncation-equivalence-is-equiv-is-truncation-equivalence g
-      ( map-equiv f)
-      ( eg)
-      ( is-equiv-map-equiv f)
+  is-truncation-equivalence-equiv-is-truncation-equivalence g (f , ef) eg =
+    is-truncation-equivalence-is-equiv-is-truncation-equivalence g f eg ef
 
   is-truncation-equivalence-is-truncation-equivalence-equiv :
     (g : B ≃ C) (f : A → B) →
     is-truncation-equivalence k f →
     is-truncation-equivalence k (map-equiv g ∘ f)
-  is-truncation-equivalence-is-truncation-equivalence-equiv g f ef =
-    is-truncation-equivalence-is-truncation-equivalence-is-equiv
-      ( map-equiv g)
-      ( f)
-      ( is-equiv-map-equiv g)
-      ( ef)
+  is-truncation-equivalence-is-truncation-equivalence-equiv (g , eg) f ef =
+    is-truncation-equivalence-is-truncation-equivalence-is-equiv g f eg ef
 ```
 
 ### The map on dependent pair types induced by the unit of the `(k+1)`-truncation is a `k`-equivalence
 
-This is an instance of Lemma 2.27 in {{#cite CORS20}} listed below.
+This is an instance of Lemma 2.27 in {{#cite CORS20}}.
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋}
+  {X : UU l1} (P : type-trunc k X → UU l2)
+  where
+
+  map-Σ-map-base-unit-trunc' :
+    Σ X (P ∘ unit-trunc) → Σ (type-trunc k X) P
+  map-Σ-map-base-unit-trunc' = map-Σ-map-base unit-trunc P
+
+  is-truncation-equivalence-map-Σ-map-base-unit-trunc' :
+    is-truncation-equivalence k map-Σ-map-base-unit-trunc'
+  is-truncation-equivalence-map-Σ-map-base-unit-trunc' =
+    is-truncation-equivalence-is-equiv-precomp k
+      ( map-Σ-map-base-unit-trunc')
+      ( λ l (Y , TY) →
+        is-equiv-equiv
+          ( equiv-ev-pair)
+          ( equiv-ev-pair)
+          ( refl-htpy)
+          ( dependent-universal-property-trunc
+            ( λ t → ((P t → Y) , is-trunc-function-type k TY))))
+```
 
 ```agda
 module _
@@ -281,32 +367,33 @@ module _
   is-truncation-equivalence-map-Σ-map-base-unit-trunc =
     is-truncation-equivalence-is-equiv-precomp k
       ( map-Σ-map-base-unit-trunc)
-      ( λ l X →
+      ( λ l (Y , TY) →
         is-equiv-equiv
+          {f = precomp (λ x → unit-trunc (pr1 x) , pr2 x) Y}
+          {g = precomp-Π unit-trunc (λ |x| → (b : P |x|) → Y)}
           ( equiv-ev-pair)
           ( equiv-ev-pair)
           ( refl-htpy)
           ( dependent-universal-property-trunc
             ( λ t →
-              ( ( P t → type-Truncated-Type X) ,
+              ( ( P t → Y) ,
                 ( is-trunc-succ-is-trunc k
-                  ( is-trunc-function-type k
-                    ( is-trunc-type-Truncated-Type X)))))))
+                  ( is-trunc-function-type k TY))))))
 ```
 
-### There is an `k`-equivalence between the fiber of a map and the fiber of its `(k+1)`-truncation
+### There is a `k`-equivalence between the fiber of a map and the fiber of its `(k+1)`-truncation
 
 This is an instance of Corollary 2.29 in {{#cite CORS20}}.
 
 We consider the following composition of maps
 
 ```text
-   fiber f b = Σ A (λ a → f a = b)
-             → Σ A (λ a → ║f a ＝ b║)
-             ≃ Σ A (λ a → |f a| = |b|)
-             ≃ Σ A (λ a → ║f║ |a| = |b|)
-             → Σ ║A║ (λ t → ║f║ t = |b|)
-             = fiber ║f║ |b|
+  fiber f b = Σ A (λ a → f a = b)
+            → Σ A (λ a → ║f a ＝ b║)
+            ≃ Σ A (λ a → |f a| = |b|)
+            ≃ Σ A (λ a → ║f║ |a| = |b|)
+            → Σ ║A║ (λ t → ║f║ t = |b|)
+            = fiber ║f║ |b|
 ```
 
 where the first and last maps are `k`-equivalences.
@@ -327,36 +414,45 @@ module _
         ( map-effectiveness-trunc k (f a) b) ∘
         ( unit-trunc)))
 
-  is-truncation-equivalence-fiber-map-trunc-fiber :
-    is-truncation-equivalence k fiber-map-trunc-fiber
-  is-truncation-equivalence-fiber-map-trunc-fiber =
-    is-truncation-equivalence-comp
-      ( map-Σ-map-base-unit-trunc
-        ( λ t → map-trunc (succ-𝕋 k) f t ＝ unit-trunc b))
-      ( tot
-        ( λ a →
-          ( concat (naturality-unit-trunc (succ-𝕋 k) f a) (unit-trunc b)) ∘
-          ( map-effectiveness-trunc k (f a) b) ∘
-          ( unit-trunc)))
-      ( is-truncation-equivalence-is-truncation-equivalence-equiv
-        ( equiv-tot
+  abstract
+    is-truncation-equivalence-fiber-map-trunc-fiber :
+      is-truncation-equivalence k fiber-map-trunc-fiber
+    is-truncation-equivalence-fiber-map-trunc-fiber =
+      is-truncation-equivalence-comp
+        ( map-Σ-map-base-unit-trunc
+          ( λ t → map-trunc (succ-𝕋 k) f t ＝ unit-trunc b))
+        ( tot
           ( λ a →
-            ( equiv-concat
-              ( naturality-unit-trunc (succ-𝕋 k) f a)
-              ( unit-trunc b)) ∘e
-            ( effectiveness-trunc k (f a) b)))
-        ( λ (a , p) → a , unit-trunc p)
-        ( is-equiv-map-equiv (equiv-trunc-Σ k)))
-      ( is-truncation-equivalence-map-Σ-map-base-unit-trunc
-        ( λ t → map-trunc (succ-𝕋 k) f t ＝ unit-trunc b))
+            ( concat (naturality-unit-trunc (succ-𝕋 k) f a) (unit-trunc b)) ∘
+            ( map-effectiveness-trunc k (f a) b) ∘
+            ( unit-trunc)))
+        ( is-truncation-equivalence-is-truncation-equivalence-equiv
+          ( equiv-tot
+            ( λ a →
+              ( equiv-concat
+                ( naturality-unit-trunc (succ-𝕋 k) f a)
+                ( unit-trunc b)) ∘e
+              ( effectiveness-trunc k (f a) b)))
+          ( λ (a , p) → a , unit-trunc p)
+          ( is-equiv-map-equiv (equiv-trunc-Σ k)))
+        ( is-truncation-equivalence-map-Σ-map-base-unit-trunc
+          ( λ t → map-trunc (succ-𝕋 k) f t ＝ unit-trunc b))
 
   truncation-equivalence-fiber-map-trunc-fiber :
     truncation-equivalence k
       ( fiber f b)
       ( fiber (map-trunc (succ-𝕋 k) f) (unit-trunc b))
-  pr1 truncation-equivalence-fiber-map-trunc-fiber = fiber-map-trunc-fiber
+  pr1 truncation-equivalence-fiber-map-trunc-fiber =
+    fiber-map-trunc-fiber
   pr2 truncation-equivalence-fiber-map-trunc-fiber =
     is-truncation-equivalence-fiber-map-trunc-fiber
+
+  equiv-trunc-fiber-map-trunc-fiber :
+    type-trunc k (fiber f b) ≃
+    type-trunc k (fiber (map-trunc (succ-𝕋 k) f) (unit-trunc b))
+  equiv-trunc-fiber-map-trunc-fiber =
+    equiv-trunc-truncation-equivalence k
+      ( truncation-equivalence-fiber-map-trunc-fiber)
 ```
 
 ### Being `k`-connected is invariant under `k`-equivalences
@@ -372,12 +468,25 @@ module _
   is-connected-is-truncation-equivalence-is-connected f e =
     is-contr-equiv (type-trunc k B) (map-trunc k f , e)
 
+  is-connected-is-truncation-equivalence-is-connected' :
+    (f : A → B) → is-truncation-equivalence k f →
+    is-connected k A → is-connected k B
+  is-connected-is-truncation-equivalence-is-connected' f e =
+    is-contr-equiv' (type-trunc k A) (map-trunc k f , e)
+
   is-connected-truncation-equivalence-is-connected :
     truncation-equivalence k A B → is-connected k B → is-connected k A
   is-connected-truncation-equivalence-is-connected f =
     is-connected-is-truncation-equivalence-is-connected
       ( map-truncation-equivalence k f)
       ( is-truncation-equivalence-truncation-equivalence k f)
+
+  is-connected-truncation-equivalence-is-connected' :
+    truncation-equivalence k A B → is-connected k A → is-connected k B
+  is-connected-truncation-equivalence-is-connected' f =
+    is-connected-is-truncation-equivalence-is-connected'
+      ( map-truncation-equivalence k f)
+      ( is-truncation-equivalence-truncation-equivalence k f)
 ```
 
 ### Every `(k+1)`-equivalence is `k`-connected
@@ -394,57 +503,75 @@ module _
   is-connected-map-is-succ-truncation-equivalence e b =
     is-connected-truncation-equivalence-is-connected
       ( truncation-equivalence-fiber-map-trunc-fiber f b)
-      ( is-connected-is-contr k (is-contr-map-is-equiv e (unit-trunc b)))
+      ( is-connected-map-is-equiv e (unit-trunc b))
+```
+
+### A map is `k`-connected if and only if its `k+1`-truncation is
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  is-connected-map-trunc-succ-is-succ-connected-domain :
+    is-connected-map k f →
+    is-connected-map k (map-trunc (succ-𝕋 k) f)
+  is-connected-map-trunc-succ-is-succ-connected-domain cf t =
+    apply-universal-property-trunc-Prop
+      ( is-surjective-unit-trunc-succ t)
+      ( is-connected-Prop k (fiber (map-trunc (succ-𝕋 k) f) t))
+      ( λ (b , p) →
+        tr
+          ( λ s → is-connected k (fiber (map-trunc (succ-𝕋 k) f) s))
+          ( p)
+          ( is-connected-truncation-equivalence-is-connected'
+            ( truncation-equivalence-fiber-map-trunc-fiber f b)
+            ( cf b)))
+
+  is-connected-map-is-connected-map-trunc-succ :
+    is-connected-map k (map-trunc (succ-𝕋 k) f) →
+    is-connected-map k f
+  is-connected-map-is-connected-map-trunc-succ cf' b =
+    is-connected-truncation-equivalence-is-connected
+      ( truncation-equivalence-fiber-map-trunc-fiber f b)
+      ( cf' (unit-trunc b))
 ```
 
 ### The codomain of a `k`-connected map is `(k+1)`-connected if its domain is `(k+1)`-connected
 
 This follows part of the proof of Proposition 2.31 in {{#cite CORS20}}.
 
+**Proof.** Let $f : A → B$ be a $k$-connected map on a $k+1$-connected domain.
+To show that the codomain is $k+1$-connected it is enough to show that $f$ is a
+$k+1$-equivalence, in other words, that $║f║ₖ₊₁$ is an equivalence. By previous
+computations we know that $║f║ₖ₊₁$ is $k$-truncated since the domain is
+$k+1$-connected, and that $║f║ₖ₊₁$ is $k$-connected since $f$ is $k$-connected,
+so we are done. ∎
+
 ```agda
 module _
   {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
   where
 
-  is-trunc-fiber-map-trunc-is-succ-connected :
-    is-connected (succ-𝕋 k) A →
-    (b : B) →
-    is-trunc k (fiber (map-trunc (succ-𝕋 k) f) (unit-trunc b))
-  is-trunc-fiber-map-trunc-is-succ-connected c b =
-    is-trunc-equiv k
-      ( map-trunc (succ-𝕋 k) f (center c) ＝ unit-trunc b)
-      ( left-unit-law-Σ-is-contr c (center c))
-      ( is-trunc-type-trunc (map-trunc (succ-𝕋 k) f (center c)) (unit-trunc b))
-
-  is-succ-connected-is-connected-map-is-succ-connected :
+  is-truncation-equivalence-succ-is-succ-connected-domain-is-connected-map :
+    is-connected-map k f →
     is-connected (succ-𝕋 k) A →
+    is-truncation-equivalence (succ-𝕋 k) f
+  is-truncation-equivalence-succ-is-succ-connected-domain-is-connected-map
+    cf cA =
+    is-equiv-is-connected-map-is-trunc-map
+      ( is-trunc-map-trunc-succ-is-succ-connected-domain f cA)
+      ( is-connected-map-trunc-succ-is-succ-connected-domain cf)
+
+  is-succ-connected-codomain-is-succ-connected-domain-is-connected-map :
     is-connected-map k f →
+    is-connected (succ-𝕋 k) A →
     is-connected (succ-𝕋 k) B
-  is-succ-connected-is-connected-map-is-succ-connected cA cf =
-    is-contr-is-equiv'
-      ( type-trunc (succ-𝕋 k) A)
-      ( map-trunc (succ-𝕋 k) f)
-      ( is-equiv-is-contr-map
-        ( λ t →
-          apply-universal-property-trunc-Prop
-            ( is-surjective-is-truncation
-              ( trunc (succ-𝕋 k) B)
-              ( is-truncation-trunc)
-              ( t))
-            ( is-contr-Prop (fiber (map-trunc (succ-𝕋 k) f) t))
-            ( λ (b , p) →
-              tr
-                ( λ s → is-contr (fiber (map-trunc (succ-𝕋 k) f) s))
-                ( p)
-                ( is-contr-equiv'
-                  ( type-trunc k (fiber f b))
-                  ( ( inv-equiv
-                      ( equiv-unit-trunc
-                        ( fiber (map-trunc (succ-𝕋 k) f) (unit-trunc b) ,
-                          is-trunc-fiber-map-trunc-is-succ-connected cA b))) ∘e
-                    ( map-trunc k (fiber-map-trunc-fiber f b) ,
-                      is-truncation-equivalence-fiber-map-trunc-fiber f b))
-                  ( cf b)))))
+  is-succ-connected-codomain-is-succ-connected-domain-is-connected-map cf cA =
+    is-connected-is-truncation-equivalence-is-connected' f
+      ( is-truncation-equivalence-succ-is-succ-connected-domain-is-connected-map
+        ( cf)
+        ( cA))
       ( cA)
 ```
 
@@ -452,39 +579,100 @@ module _
 
 This is an instance of Proposition 2.31 in {{#cite CORS20}}.
 
+**Proof.** If $g$ is $(k+1)$-connected then by the cancellation property of
+$(k+1)$-equivalences, $f$ is a $k+1$-equivalence, and so in particular
+$k$-connected.
+
+Conversely, assume $f$ is $k$-connected. We want to show that the fibers of $g$
+are $k+1$-connected, so let $c$ be an element of the codomain of $g$. The fibers
+of the composite $g ∘ f$ compute as
+
+$$
+  \operatorname{fiber}_{g\circ f}(c) ≃
+  \sum_{(b , p) : \operatorname{fiber}_{g}(c)}{\operatorname{fiber}_{f}(b)}.
+$$
+
+By the previous lemma, since $\operatorname{fiber}_{g\circ f}(c)$ is
+$k+1$-connected, $\operatorname{fiber}_{g}(c)$ is $k+1$-connected if the first
+projection map of this type is $k$-connected, and its fibers compute to the
+fibers of $f$. ∎
+
 ```agda
 module _
   {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {C : UU l3}
   (g : B → C) (f : A → B) (cgf : is-connected-map (succ-𝕋 k) (g ∘ f))
   where
 
+  is-succ-truncation-equivalence-right-factor-is-succ-connected-map-left-factor :
+    is-connected-map (succ-𝕋 k) g → is-truncation-equivalence (succ-𝕋 k) f
+  is-succ-truncation-equivalence-right-factor-is-succ-connected-map-left-factor
+    cg =
+    is-truncation-equivalence-right-factor g f
+      ( is-truncation-equivalence-is-connected-map (g ∘ f) cgf)
+      ( is-truncation-equivalence-is-connected-map g cg)
+
   is-connected-map-right-factor-is-succ-connected-map-left-factor :
     is-connected-map (succ-𝕋 k) g → is-connected-map k f
   is-connected-map-right-factor-is-succ-connected-map-left-factor cg =
     is-connected-map-is-succ-truncation-equivalence f
-      ( is-truncation-equivalence-right-factor g f
-        ( is-truncation-equivalence-is-connected-map (g ∘ f) cgf)
-        ( is-truncation-equivalence-is-connected-map g cg))
+      ( is-succ-truncation-equivalence-right-factor-is-succ-connected-map-left-factor
+        ( cg))
 
   is-connected-map-right-factor-is-succ-connected-map-right-factor :
     is-connected-map k f → is-connected-map (succ-𝕋 k) g
   is-connected-map-right-factor-is-succ-connected-map-right-factor cf c =
-    is-succ-connected-is-connected-map-is-succ-connected
+    is-succ-connected-codomain-is-succ-connected-domain-is-connected-map
       ( pr1)
-      ( is-connected-equiv' (compute-fiber-comp g f c) (cgf c))
       ( λ p →
         is-connected-equiv
           ( equiv-fiber-pr1 (fiber f ∘ pr1) p)
           ( cf (pr1 p)))
+      ( is-connected-equiv' (compute-fiber-comp g f c) (cgf c))
+```
+
+As a corollary, if $g ∘ f$ is $(k + 1)$-connected for some $g$, and $f$ is
+$k$-connected, then $f$ is a $k+1$-equivalence.
+
+```agda
+  is-succ-truncation-equiv-is-succ-connected-comp :
+    is-connected-map k f → is-truncation-equivalence (succ-𝕋 k) f
+  is-succ-truncation-equiv-is-succ-connected-comp cf =
+    is-succ-truncation-equivalence-right-factor-is-succ-connected-map-left-factor
+    ( is-connected-map-right-factor-is-succ-connected-map-right-factor cf)
 ```
 
 ### A `k`-equivalence with a section is `k`-connected
 
+**Proof.** If $k ≐ -2$ notice that every map is $-2$-connected. So let
+$k ≐ n + 1$ for some truncation level $n$ and let $f$ be our $k$-equivalence
+with a section $s$. By assumption, we have a commuting triangle of maps
+
+```text
+        A
+      ∧   \
+   s /     \ f
+    /       ∨
+  B ======== B.
+```
+
+By the previous lemma, since the identity map is $k$-connected, it thus suffices
+to show that $s$ is $n$-connected. But by the cancellation property of
+$n+1$-equivalences $s$ is an $n+1$-equivalence and $n+1$-equivalences are in
+particular $n$-connected. ∎
+
 ```agda
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
   where
 
+  is-connected-map-section-is-truncation-equivalence-succ :
+    (k : 𝕋) (s : section f) →
+    is-truncation-equivalence (succ-𝕋 k) f →
+    is-connected-map k (map-section f s)
+  is-connected-map-section-is-truncation-equivalence-succ k (s , h) e =
+    is-connected-map-is-succ-truncation-equivalence s
+      ( is-truncation-equivalence-map-section (succ-𝕋 k) (s , h) e)
+
   is-connected-map-is-truncation-equivalence-section :
     (k : 𝕋) →
     section f → is-truncation-equivalence k f → is-connected-map k f
@@ -492,21 +680,17 @@ module _
     is-neg-two-connected-map f
   is-connected-map-is-truncation-equivalence-section (succ-𝕋 k) (s , h) e =
     is-connected-map-right-factor-is-succ-connected-map-right-factor f s
-      ( is-connected-map-is-equiv (is-equiv-htpy id h is-equiv-id))
-      ( is-connected-map-is-succ-truncation-equivalence s
-        ( is-truncation-equivalence-right-factor f s
-          ( is-truncation-equivalence-is-equiv
-            ( f ∘ s)
-            ( is-equiv-htpy id h is-equiv-id))
-          ( e)))
+      ( is-connected-map-htpy-id h)
+      ( is-connected-map-section-is-truncation-equivalence-succ k (s , h) e)
 ```
 
 ## References
 
 - The notion of `k`-equivalence is a special case of the notion of
-  `L`-equivalence, where `L` is a reflective subuniverse. They were studied in
-  the paper {{#cite CORS20}}.
-- The class of `k`-equivalences is left orthogonal to the class of `k`-étale
-  maps. This was shown in {{#cite CR21}}.
+  `L`-equivalence, where `L` is a reflective subuniverse. These were studied in
+  {{#cite CORS20}}.
+- The class of `k`-equivalences is
+  [left orthogonal](orthogonal-factorization-systems.orthogonal-maps.md) to the
+  class of `k`-étale maps. This was shown in {{#cite CR21}}.
 
 {{#bibliography}}
diff --git a/src/foundation/truncations.lagda.md b/src/foundation/truncations.lagda.md
index ed07abee14..df07a9a146 100644
--- a/src/foundation/truncations.lagda.md
+++ b/src/foundation/truncations.lagda.md
@@ -27,6 +27,8 @@ open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.propositions
+open import foundation-core.retractions
+open import foundation-core.sections
 open import foundation-core.torsorial-type-families
 open import foundation-core.truncation-levels
 open import foundation-core.universal-property-truncation
@@ -313,26 +315,27 @@ module _
   map-inv-unit-trunc = map-universal-property-trunc A id
 
   is-retraction-map-inv-unit-trunc :
-    ( map-inv-unit-trunc ∘ unit-trunc) ~ id
+    is-retraction unit-trunc map-inv-unit-trunc
   is-retraction-map-inv-unit-trunc = triangle-universal-property-trunc A id
 
-  is-section-map-inv-unit-trunc :
-    ( unit-trunc ∘ map-inv-unit-trunc) ~ id
-  is-section-map-inv-unit-trunc =
-    htpy-eq
-      ( pr1
-        ( pair-eq-Σ
-          ( eq-is-prop'
-            ( is-trunc-succ-is-trunc
-              ( neg-two-𝕋)
-              ( universal-property-trunc
-                ( k)
-                ( type-Truncated-Type A)
-                ( trunc k (type-Truncated-Type A))
-                ( unit-trunc)))
-            ( unit-trunc ∘ map-inv-unit-trunc ,
-              unit-trunc ·l is-retraction-map-inv-unit-trunc)
-            ( id , refl-htpy))))
+  abstract
+    is-section-map-inv-unit-trunc :
+      is-section unit-trunc map-inv-unit-trunc
+    is-section-map-inv-unit-trunc =
+      htpy-eq
+        ( pr1
+          ( pair-eq-Σ
+            ( eq-is-prop'
+              ( is-trunc-succ-is-trunc
+                ( neg-two-𝕋)
+                ( universal-property-trunc
+                  ( k)
+                  ( type-Truncated-Type A)
+                  ( trunc k (type-Truncated-Type A))
+                  ( unit-trunc)))
+              ( unit-trunc ∘ map-inv-unit-trunc ,
+                unit-trunc ·l is-retraction-map-inv-unit-trunc)
+              ( id , refl-htpy))))
 
   is-equiv-unit-trunc : is-equiv unit-trunc
   is-equiv-unit-trunc =
@@ -343,8 +346,18 @@ module _
 
   equiv-unit-trunc :
     type-Truncated-Type A ≃ type-trunc k (type-Truncated-Type A)
-  pr1 equiv-unit-trunc = unit-trunc
-  pr2 equiv-unit-trunc = is-equiv-unit-trunc
+  equiv-unit-trunc = (unit-trunc , is-equiv-unit-trunc)
+
+  is-equiv-map-inv-unit-trunc : is-equiv map-inv-unit-trunc
+  is-equiv-map-inv-unit-trunc =
+    is-equiv-is-invertible
+      unit-trunc
+      is-retraction-map-inv-unit-trunc
+      is-section-map-inv-unit-trunc
+
+  inv-equiv-unit-trunc :
+    type-trunc k (type-Truncated-Type A) ≃ type-Truncated-Type A
+  inv-equiv-unit-trunc = (map-inv-unit-trunc , is-equiv-map-inv-unit-trunc)
 ```
 
 ### A contractible type is equivalent to its `k`-truncation
diff --git a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
index a9d2691df4..8c4000e1bd 100644
--- a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
+++ b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
@@ -12,12 +12,17 @@ open import foundation.dependent-pair-types
 open import foundation.diagonal-maps-of-types
 open import foundation.families-of-equivalences
 open import foundation.function-extensionality
+open import foundation.precomposition-dependent-functions
+open import foundation.precomposition-functions
 open import foundation.subtype-identity-principle
+open import foundation.type-theoretic-principle-of-choice
+open import foundation.universal-property-dependent-pair-types
 open import foundation.universe-levels
 
 open import foundation-core.constant-maps
 open import foundation-core.contractible-maps
 open import foundation-core.contractible-types
+open import foundation-core.dependent-identifications
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
@@ -25,7 +30,6 @@ open import foundation-core.functoriality-dependent-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.precomposition-dependent-functions
 open import foundation-core.retractions
 open import foundation-core.sections
 
@@ -144,6 +148,10 @@ module _
   lift-family-of-elements-fiber : lift-family-of-elements (fiber f) f
   pr1 (lift-family-of-elements-fiber a) = a
   pr2 (lift-family-of-elements-fiber a) = refl
+
+  lift-family-of-elements-fiber' : lift-family-of-elements (fiber' f) f
+  pr1 (lift-family-of-elements-fiber' a) = a
+  pr2 (lift-family-of-elements-fiber' a) = refl
 ```
 
 ## Properties
@@ -152,58 +160,60 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  (C : (y : B) (z : fiber f y) → UU l3)
   where
 
-  module _
-    {l3 : Level} (C : (y : B) (z : fiber f y) → UU l3)
-    where
-
-    ev-lift-family-of-elements-fiber :
-      ((y : B) (z : fiber f y) → C y z) → ((x : A) → C (f x) (x , refl))
-    ev-lift-family-of-elements-fiber =
-      ev-double-lift-family-of-elements (lift-family-of-elements-fiber f)
-
-    extend-lift-family-of-elements-fiber :
-      ((x : A) → C (f x) (x , refl)) → ((y : B) (z : fiber f y) → C y z)
-    extend-lift-family-of-elements-fiber h .(f x) (x , refl) = h x
+  ev-lift-family-of-elements-fiber :
+    ((y : B) (z : fiber f y) → C y z) → ((x : A) → C (f x) (x , refl))
+  ev-lift-family-of-elements-fiber =
+    ev-double-lift-family-of-elements (lift-family-of-elements-fiber f)
 
-    is-section-extend-lift-family-of-elements-fiber :
-      is-section
-        ( ev-lift-family-of-elements-fiber)
-        ( extend-lift-family-of-elements-fiber)
-    is-section-extend-lift-family-of-elements-fiber h = refl
+  extend-lift-family-of-elements-fiber :
+    ((x : A) → C (f x) (x , refl)) → ((y : B) (z : fiber f y) → C y z)
+  extend-lift-family-of-elements-fiber h .(f x) (x , refl) = h x
 
-    is-retraction-extend-lift-family-of-elements-fiber' :
-      (h : (y : B) (z : fiber f y) → C y z) (y : B) →
-      extend-lift-family-of-elements-fiber
-        ( ev-lift-family-of-elements-fiber h)
-        ( y) ~
-      h y
-    is-retraction-extend-lift-family-of-elements-fiber' h .(f z) (z , refl) =
-      refl
+  is-section-extend-lift-family-of-elements-fiber :
+    is-section
+      ( ev-lift-family-of-elements-fiber)
+      ( extend-lift-family-of-elements-fiber)
+  is-section-extend-lift-family-of-elements-fiber h = refl
+
+  htpy-is-retraction-extend-lift-family-of-elements-fiber :
+    (h : (y : B) (z : fiber f y) → C y z) (y : B) →
+    extend-lift-family-of-elements-fiber
+      ( ev-lift-family-of-elements-fiber h)
+      ( y) ~
+    h y
+  htpy-is-retraction-extend-lift-family-of-elements-fiber h .(f z) (z , refl) =
+    refl
 
+  abstract
     is-retraction-extend-lift-family-of-elements-fiber :
       is-retraction
         ( ev-lift-family-of-elements-fiber)
         ( extend-lift-family-of-elements-fiber)
     is-retraction-extend-lift-family-of-elements-fiber h =
-      eq-htpy (eq-htpy ∘ is-retraction-extend-lift-family-of-elements-fiber' h)
+      eq-htpy
+        ( eq-htpy ∘ htpy-is-retraction-extend-lift-family-of-elements-fiber h)
 
-    is-equiv-extend-lift-family-of-elements-fiber :
-      is-equiv extend-lift-family-of-elements-fiber
-    is-equiv-extend-lift-family-of-elements-fiber =
-      is-equiv-is-invertible
-        ( ev-lift-family-of-elements-fiber)
-        ( is-retraction-extend-lift-family-of-elements-fiber)
-        ( is-section-extend-lift-family-of-elements-fiber)
+  is-equiv-extend-lift-family-of-elements-fiber :
+    is-equiv extend-lift-family-of-elements-fiber
+  is-equiv-extend-lift-family-of-elements-fiber =
+    is-equiv-is-invertible
+      ( ev-lift-family-of-elements-fiber)
+      ( is-retraction-extend-lift-family-of-elements-fiber)
+      ( is-section-extend-lift-family-of-elements-fiber)
+
+  inv-equiv-dependent-universal-property-family-of-fibers :
+    ((x : A) → C (f x) (x , refl)) ≃ ((y : B) (z : fiber f y) → C y z)
+  inv-equiv-dependent-universal-property-family-of-fibers =
+    ( extend-lift-family-of-elements-fiber ,
+      is-equiv-extend-lift-family-of-elements-fiber)
 
-    inv-equiv-dependent-universal-property-family-of-fibers :
-      ((x : A) → C (f x) (x , refl)) ≃ ((y : B) (z : fiber f y) → C y z)
-    pr1 inv-equiv-dependent-universal-property-family-of-fibers =
-      extend-lift-family-of-elements-fiber
-    pr2 inv-equiv-dependent-universal-property-family-of-fibers =
-      is-equiv-extend-lift-family-of-elements-fiber
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
 
   dependent-universal-property-family-of-fibers-fiber :
     dependent-universal-property-family-of-fibers
@@ -211,18 +221,95 @@ module _
       ( lift-family-of-elements-fiber f)
   dependent-universal-property-family-of-fibers-fiber C =
     is-equiv-is-invertible
-      ( extend-lift-family-of-elements-fiber C)
-      ( is-section-extend-lift-family-of-elements-fiber C)
-      ( is-retraction-extend-lift-family-of-elements-fiber C)
+      ( extend-lift-family-of-elements-fiber f C)
+      ( is-section-extend-lift-family-of-elements-fiber f C)
+      ( is-retraction-extend-lift-family-of-elements-fiber f C)
 
   equiv-dependent-universal-property-family-of-fibers :
     {l3 : Level} (C : (y : B) (z : fiber f y) → UU l3) →
     ((y : B) (z : fiber f y) → C y z) ≃
     ((x : A) → C (f x) (x , refl))
-  pr1 (equiv-dependent-universal-property-family-of-fibers C) =
-    ev-lift-family-of-elements-fiber C
-  pr2 (equiv-dependent-universal-property-family-of-fibers C) =
-    dependent-universal-property-family-of-fibers-fiber C
+  equiv-dependent-universal-property-family-of-fibers C =
+    ( ev-lift-family-of-elements-fiber f C ,
+      dependent-universal-property-family-of-fibers-fiber C)
+```
+
+### The variant family of fibers of a map satisfies the dependent universal property of the family of fibers of a map
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  (C : (y : B) (z : fiber' f y) → UU l3)
+  where
+
+  ev-lift-family-of-elements-fiber' :
+    ((y : B) (z : fiber' f y) → C y z) → ((x : A) → C (f x) (x , refl))
+  ev-lift-family-of-elements-fiber' =
+    ev-double-lift-family-of-elements (lift-family-of-elements-fiber' f)
+
+  extend-lift-family-of-elements-fiber' :
+    ((x : A) → C (f x) (x , refl)) → ((y : B) (z : fiber' f y) → C y z)
+  extend-lift-family-of-elements-fiber' h .(f x) (x , refl) = h x
+
+  is-section-extend-lift-family-of-elements-fiber' :
+    is-section
+      ( ev-lift-family-of-elements-fiber')
+      ( extend-lift-family-of-elements-fiber')
+  is-section-extend-lift-family-of-elements-fiber' h = refl
+
+  htpy-is-retraction-extend-lift-family-of-elements-fiber' :
+    (h : (y : B) (z : fiber' f y) → C y z) (y : B) →
+    extend-lift-family-of-elements-fiber'
+      ( ev-lift-family-of-elements-fiber' h)
+      ( y) ~
+    h y
+  htpy-is-retraction-extend-lift-family-of-elements-fiber' h .(f z) (z , refl) =
+    refl
+
+  abstract
+    is-retraction-extend-lift-family-of-elements-fiber' :
+      is-retraction
+        ( ev-lift-family-of-elements-fiber')
+        ( extend-lift-family-of-elements-fiber')
+    is-retraction-extend-lift-family-of-elements-fiber' h =
+      eq-htpy
+        ( eq-htpy ∘ htpy-is-retraction-extend-lift-family-of-elements-fiber' h)
+
+  is-equiv-extend-lift-family-of-elements-fiber' :
+    is-equiv extend-lift-family-of-elements-fiber'
+  is-equiv-extend-lift-family-of-elements-fiber' =
+    is-equiv-is-invertible
+      ( ev-lift-family-of-elements-fiber')
+      ( is-retraction-extend-lift-family-of-elements-fiber')
+      ( is-section-extend-lift-family-of-elements-fiber')
+
+  inv-equiv-dependent-universal-property-family-of-fibers' :
+    ((x : A) → C (f x) (x , refl)) ≃ ((y : B) (z : fiber' f y) → C y z)
+  inv-equiv-dependent-universal-property-family-of-fibers' =
+    ( extend-lift-family-of-elements-fiber' ,
+      is-equiv-extend-lift-family-of-elements-fiber')
+
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  dependent-universal-property-family-of-fibers-fiber' :
+    dependent-universal-property-family-of-fibers
+      ( fiber' f)
+      ( lift-family-of-elements-fiber' f)
+  dependent-universal-property-family-of-fibers-fiber' C =
+    is-equiv-is-invertible
+      ( extend-lift-family-of-elements-fiber' f C)
+      ( is-section-extend-lift-family-of-elements-fiber' f C)
+      ( is-retraction-extend-lift-family-of-elements-fiber' f C)
+
+  equiv-dependent-universal-property-family-of-fibers' :
+    {l3 : Level} (C : (y : B) (z : fiber' f y) → UU l3) →
+    ((y : B) (z : fiber' f y) → C y z) ≃
+    ((x : A) → C (f x) (x , refl))
+  equiv-dependent-universal-property-family-of-fibers' C =
+    ( ev-lift-family-of-elements-fiber' f C ,
+      dependent-universal-property-family-of-fibers-fiber' C)
 ```
 
 ### The family of fibers of a map satisfies the universal property of the family of fibers of a map
@@ -431,3 +518,193 @@ module _
       ( is-equiv-map-Π-is-fiberwise-equiv H)
       ( universal-property-family-of-fibers-fiber f C)
 ```
+
+### Computing the fibers of precomposition dependent functions as dependent products
+
+We give four equivalences for the fibers of precomposition dependent functions
+as dependent products:
+
+```text
+  fiber (precomp-Π f U) g
+    ≃ (b : B) → Σ (u : U b), ((a , p) : fiber  f b) → g a ＝ₚᵁ u
+    ≃ (b : B) → Σ (u : U b), ((a , p) : fiber' f b) → u ＝ₚᵁ g a
+    ≃ (b : B) → Σ (u : U b), (a : A) (p : f a ＝ b) → g a ＝ₚᵁ u
+    ≃ (b : B) → Σ (u : U b), (a : A) (p : b ＝ f a) → u ＝ₚᵁ g a
+```
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (U : B → UU l3)
+  (g : (a : A) → U (f a))
+  where
+
+  family-dependent-product-fiber-precomp-Π : B → UU (l1 ⊔ l2 ⊔ l3)
+  family-dependent-product-fiber-precomp-Π b =
+    Σ (U b) (λ u → ((a , p) : fiber f b) → dependent-identification U p (g a) u)
+
+  dependent-product-fiber-precomp-Π : UU (l1 ⊔ l2 ⊔ l3)
+  dependent-product-fiber-precomp-Π =
+    (b : B) → family-dependent-product-fiber-precomp-Π b
+
+  dependent-product-characterization-fiber-precomp-Π :
+    fiber (precomp-Π f U) g ≃ dependent-product-fiber-precomp-Π
+  dependent-product-characterization-fiber-precomp-Π =
+    equivalence-reasoning
+      fiber (precomp-Π f U) g
+      ≃ Σ ((b : B) → U b) (λ h → (a : A) → g a ＝ (h ∘ f) a)
+        by compute-extension-fiber-precomp-Π f U g
+      ≃ Σ ( (b : B) → U b)
+          ( λ h → (b : B) ((a , p) : fiber f b) →
+            dependent-identification U p (g a) (h b))
+        by
+          equiv-tot
+            ( λ h →
+              inv-equiv-dependent-universal-property-family-of-fibers f
+                ( λ y (a , p) → dependent-identification U p (g a) (h y)))
+      ≃ ( (b : B) →
+          Σ ( U b)
+            ( λ u →
+              ((a , p) : fiber f b) → dependent-identification U p (g a) u))
+        by inv-distributive-Π-Σ
+
+  family-fiber-dependent-product-curry-precomp-Π : B → UU (l1 ⊔ l2 ⊔ l3)
+  family-fiber-dependent-product-curry-precomp-Π b =
+    Σ ( U b)
+      ( λ u → (a : A) (p : f a ＝ b) → dependent-identification U p (g a) u)
+
+  fiber-dependent-product-curry-precomp-Π : UU (l1 ⊔ l2 ⊔ l3)
+  fiber-dependent-product-curry-precomp-Π =
+    (b : B) → family-fiber-dependent-product-curry-precomp-Π b
+
+  curried-dependent-product-characterization-fiber-precomp-Π :
+    fiber (precomp-Π f U) g ≃ fiber-dependent-product-curry-precomp-Π
+  curried-dependent-product-characterization-fiber-precomp-Π =
+    ( equiv-Π-equiv-family (λ b → equiv-tot (λ u → equiv-ev-pair))) ∘e
+    ( dependent-product-characterization-fiber-precomp-Π)
+
+  family-dependent-product-fiber-precomp-Π' : B → UU (l1 ⊔ l2 ⊔ l3)
+  family-dependent-product-fiber-precomp-Π' b =
+    Σ ( U b)
+      ( λ u → ((a , p) : fiber' f b) → dependent-identification U p u (g a))
+
+  dependent-product-fiber-precomp-Π' : UU (l1 ⊔ l2 ⊔ l3)
+  dependent-product-fiber-precomp-Π' =
+    (b : B) → family-dependent-product-fiber-precomp-Π' b
+
+  dependent-product-characterization-fiber-precomp-Π' :
+    fiber (precomp-Π f U) g ≃ dependent-product-fiber-precomp-Π'
+  dependent-product-characterization-fiber-precomp-Π' =
+    equivalence-reasoning
+      fiber (precomp-Π f U) g
+      ≃ Σ ((b : B) → U b) (λ h → (a : A) → (h ∘ f) a ＝ g a)
+        by compute-extension-fiber-precomp-Π' f U g
+      ≃ Σ ( (b : B) → U b)
+          ( λ h → (b : B) ((a , p) : fiber' f b) →
+            dependent-identification U p (h b) (g a))
+        by
+          equiv-tot
+            ( λ h →
+              inv-equiv-dependent-universal-property-family-of-fibers' f
+                ( λ y (a , p) → dependent-identification U p (h y) (g a)))
+      ≃ ( (b : B) →
+          Σ ( U b)
+            ( λ u →
+              ((a , p) : fiber' f b) → dependent-identification U p u (g a)))
+        by inv-distributive-Π-Σ
+
+  family-fiber-dependent-product-curry-precomp-Π' : B → UU (l1 ⊔ l2 ⊔ l3)
+  family-fiber-dependent-product-curry-precomp-Π' b =
+    Σ (U b) (λ u → (a : A) (p : b ＝ f a) → dependent-identification U p u (g a))
+
+  fiber-dependent-product-curry-precomp-Π' : UU (l1 ⊔ l2 ⊔ l3)
+  fiber-dependent-product-curry-precomp-Π' =
+    (b : B) → family-fiber-dependent-product-curry-precomp-Π' b
+
+  curried-dependent-product-characterization-fiber-precomp-Π' :
+    fiber (precomp-Π f U) g ≃ fiber-dependent-product-curry-precomp-Π'
+  curried-dependent-product-characterization-fiber-precomp-Π' =
+    ( equiv-Π-equiv-family (λ b → equiv-tot (λ u → equiv-ev-pair))) ∘e
+    ( dependent-product-characterization-fiber-precomp-Π')
+```
+
+### Fibers of precomposition functions as dependent products
+
+We give four equivalences for the fibers of precomposition functions as
+dependent products:
+
+```text
+  fiber (precomp f U) g
+    ≃ (b : B) → Σ (u : U), ((a , p) : fiber  f b) → g a ＝ u
+    ≃ (b : B) → Σ (u : U), ((a , p) : fiber' f b) → u ＝ g a
+    ≃ (b : B) → Σ (u : U), (a : A) → f a ＝ b → g a ＝ u
+    ≃ (b : B) → Σ (u : U), (a : A) → b ＝ f a → u ＝ g a
+```
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) {U : UU l3}
+  (g : A → U)
+  where
+
+  family-dependent-product-fiber-precomp : B → UU (l1 ⊔ l2 ⊔ l3)
+  family-dependent-product-fiber-precomp b =
+    Σ U (λ u → ((a , _) : fiber f b) → g a ＝ u)
+
+  dependent-product-fiber-precomp : UU (l1 ⊔ l2 ⊔ l3)
+  dependent-product-fiber-precomp =
+    (b : B) → family-dependent-product-fiber-precomp b
+
+  dependent-product-characterization-fiber-precomp :
+    fiber (precomp f U) g ≃ dependent-product-fiber-precomp
+  dependent-product-characterization-fiber-precomp =
+    equivalence-reasoning
+      fiber (precomp f U) g
+      ≃ Σ (B → U) (λ h → (a : A) → g a ＝ (h ∘ f) a)
+        by compute-extension-fiber-precomp f g
+      ≃ Σ ( B → U)
+          ( λ h → (b : B) ((a , _) : fiber f b) → g a ＝ h b)
+        by
+          equiv-tot
+            ( λ h →
+              inv-equiv-dependent-universal-property-family-of-fibers f
+                ( λ y (a , _) → (g a ＝ h y)))
+      ≃ ( (b : B) → Σ U (λ u → ((a , _) : fiber f b) → g a ＝ u))
+        by inv-distributive-Π-Σ
+
+  curried-dependent-product-characterization-fiber-precomp :
+    fiber (precomp f U) g ≃ ((b : B) → Σ U (λ u → (a : A) → f a ＝ b → g a ＝ u))
+  curried-dependent-product-characterization-fiber-precomp =
+    ( equiv-Π-equiv-family (λ b → equiv-tot (λ u → equiv-ev-pair))) ∘e
+    ( dependent-product-characterization-fiber-precomp)
+
+  family-dependent-product-fiber-precomp' : B → UU (l1 ⊔ l2 ⊔ l3)
+  family-dependent-product-fiber-precomp' b =
+    Σ U (λ u → ((a , _) : fiber' f b) → u ＝ g a)
+
+  dependent-product-fiber-precomp' : UU (l1 ⊔ l2 ⊔ l3)
+  dependent-product-fiber-precomp' =
+    (b : B) → family-dependent-product-fiber-precomp' b
+
+  dependent-product-characterization-fiber-precomp' :
+    fiber (precomp f U) g ≃ dependent-product-fiber-precomp'
+  dependent-product-characterization-fiber-precomp' =
+    equivalence-reasoning
+      fiber (precomp f U) g
+      ≃ Σ (B → U) (λ h → (h ∘ f) ~ g)
+        by compute-extension-fiber-precomp' f g
+      ≃ Σ ( B → U)
+          ( λ h → (b : B) ((a , _) : fiber' f b) → h b ＝ g a)
+        by
+          equiv-tot
+            ( λ h →
+              inv-equiv-dependent-universal-property-family-of-fibers' f
+                ( λ y (a , _) → (h y ＝ g a)))
+      ≃ ( (b : B) → Σ U (λ u → ((a , _) : fiber' f b) → u ＝ g a))
+        by inv-distributive-Π-Σ
+
+  curried-dependent-product-characterization-fiber-precomp' :
+    fiber (precomp f U) g ≃ ((b : B) → Σ U (λ u → (a : A) → b ＝ f a → u ＝ g a))
+  curried-dependent-product-characterization-fiber-precomp' =
+    ( equiv-Π-equiv-family (λ b → equiv-tot (λ u → equiv-ev-pair))) ∘e
+    ( dependent-product-characterization-fiber-precomp')
+```
diff --git a/src/foundation/universal-property-truncation.lagda.md b/src/foundation/universal-property-truncation.lagda.md
index 3d261465a4..8b3b3cf9c3 100644
--- a/src/foundation/universal-property-truncation.lagda.md
+++ b/src/foundation/universal-property-truncation.lagda.md
@@ -16,6 +16,7 @@ open import foundation.function-extensionality
 open import foundation.identity-types
 open import foundation.propositional-truncations
 open import foundation.surjective-maps
+open import foundation.truncations
 open import foundation.type-arithmetic-dependent-function-types
 open import foundation.universal-property-dependent-pair-types
 open import foundation.universal-property-identity-types
@@ -60,14 +61,14 @@ module _
           ( Σ (type-Truncated-Type C) (λ z → g x ＝ z))
           ( equiv-tot
             ( λ z →
-              ( ( equiv-ev-refl' x) ∘e
-                ( equiv-Π-equiv-family
-                  ( λ x' →
-                    equiv-is-truncation
-                      ( Id-Truncated-Type B (f x') (f x))
-                      ( ap f)
-                      ( K x' x)
-                      ( Id-Truncated-Type C (g x') z)))) ∘e
+              ( equiv-ev-refl' x) ∘e
+              ( equiv-Π-equiv-family
+                ( λ x' →
+                  equiv-is-truncation
+                    ( Id-Truncated-Type B (f x') (f x))
+                    ( ap f)
+                    ( K x' x)
+                    ( Id-Truncated-Type C (g x') z))) ∘e
               ( equiv-ev-pair)))
           ( is-torsorial-Id (g x)))
 
@@ -82,11 +83,10 @@ module _
               ( λ z → (t : fiber f y) → (g (pr1 t) ＝ z)))
           ( ( equiv-tot
               ( λ h →
-                ( ( ( inv-equiv (equiv-funext)) ∘e
-                    ( equiv-Π-equiv-family
-                      ( λ x →
-                        equiv-inv (g x) (h (f x)) ∘e equiv-ev-refl (f x)))) ∘e
-                  ( equiv-swap-Π)) ∘e
+                ( equiv-eq-htpy) ∘e
+                ( equiv-Π-equiv-family
+                  ( λ x → equiv-inv (g x) (h (f x)) ∘e equiv-ev-refl (f x))) ∘e
+                ( equiv-swap-Π) ∘e
                 ( equiv-Π-equiv-family (λ x → equiv-ev-pair)))) ∘e
             ( distributive-Π-Σ))
           ( is-contr-Π
@@ -103,5 +103,10 @@ module _
     map-inv-is-equiv
       ( dependent-universal-property-truncation-is-truncation B f H
         ( λ y → truncated-type-trunc-Prop k (fiber f y)))
-      ( λ x → unit-trunc-Prop (pair x refl))
+      ( λ x → unit-trunc-Prop (x , refl))
+
+is-surjective-unit-trunc-succ :
+  {l : Level} {k : 𝕋} {A : UU l} → is-surjective (unit-trunc {k = succ-𝕋 k} {A})
+is-surjective-unit-trunc-succ {k = k} {A} =
+  is-surjective-is-truncation (trunc (succ-𝕋 k) A) is-truncation-trunc
 ```
diff --git a/src/foundation/universal-property-unit-type.lagda.md b/src/foundation/universal-property-unit-type.lagda.md
index ca15e0b392..8579a1bb27 100644
--- a/src/foundation/universal-property-unit-type.lagda.md
+++ b/src/foundation/universal-property-unit-type.lagda.md
@@ -18,7 +18,10 @@ open import foundation-core.constant-maps
 open import foundation-core.contractible-types
 open import foundation-core.equivalences
 open import foundation-core.homotopies
+open import foundation-core.identity-types
 open import foundation-core.precomposition-functions
+open import foundation-core.retractions
+open import foundation-core.sections
 ```
 
 </details>
@@ -41,7 +44,7 @@ ev-star P f = f star
 
 ev-star' :
   {l : Level} (Y : UU l) → (unit → Y) → Y
-ev-star' Y = ev-star (λ t → Y)
+ev-star' Y = ev-star (λ _ → Y)
 
 abstract
   dependent-universal-property-unit :
@@ -55,20 +58,35 @@ pr1 (equiv-dependent-universal-property-unit P) = ev-star P
 pr2 (equiv-dependent-universal-property-unit P) =
   dependent-universal-property-unit P
 
-abstract
-  universal-property-unit :
-    {l : Level} (Y : UU l) → is-equiv (ev-star' Y)
-  universal-property-unit Y = dependent-universal-property-unit (λ t → Y)
+module _
+  {l : Level} (Y : UU l)
+  where
+
+  is-section-const-unit : is-section (ev-star' Y) (const unit)
+  is-section-const-unit = refl-htpy
+
+  is-retraction-const-unit : is-retraction (ev-star' Y) (const unit)
+  is-retraction-const-unit = refl-htpy
+
+  universal-property-unit : is-equiv (ev-star' Y)
+  universal-property-unit =
+    is-equiv-is-invertible
+      ( const unit)
+      ( is-section-const-unit)
+      ( is-retraction-const-unit)
+
+  equiv-universal-property-unit : (unit → Y) ≃ Y
+  equiv-universal-property-unit = (ev-star' Y , universal-property-unit)
 
-equiv-universal-property-unit :
-  {l : Level} (Y : UU l) → (unit → Y) ≃ Y
-pr1 (equiv-universal-property-unit Y) = ev-star' Y
-pr2 (equiv-universal-property-unit Y) = universal-property-unit Y
+  is-equiv-const-unit : is-equiv (const unit)
+  is-equiv-const-unit =
+    is-equiv-is-invertible
+      ( ev-star' Y)
+      ( is-retraction-const-unit)
+      ( is-section-const-unit)
 
-inv-equiv-universal-property-unit :
-  {l : Level} (Y : UU l) → Y ≃ (unit → Y)
-inv-equiv-universal-property-unit Y =
-  inv-equiv (equiv-universal-property-unit Y)
+  inv-equiv-universal-property-unit : Y ≃ (unit → Y)
+  inv-equiv-universal-property-unit = (const unit , is-equiv-const-unit)
 
 abstract
   is-equiv-point-is-contr :
@@ -123,3 +141,21 @@ abstract
       ( universal-property-unit-is-equiv-point x is-equiv-point Y)
       ( refl-htpy)
 ```
+
+### Precomposition with the terminal map is an equivalence if and only if the diagonal exponential is
+
+```agda
+is-equiv-precomp-terminal-map-is-equiv-diagonal-exponential :
+  {l1 l2 : Level} {X : UU l1} {U : UU l2} →
+  is-equiv (diagonal-exponential U X) →
+  is-equiv (precomp (terminal-map X) U)
+is-equiv-precomp-terminal-map-is-equiv-diagonal-exponential H =
+  is-equiv-left-factor _ _ H (is-equiv-const-unit _)
+
+is-equiv-diagonal-exponential-is-equiv-precomp-terminal-map :
+  {l1 l2 : Level} {X : UU l1} {U : UU l2} →
+  is-equiv (precomp (terminal-map X) U) →
+  is-equiv (diagonal-exponential U X)
+is-equiv-diagonal-exponential-is-equiv-precomp-terminal-map H =
+  is-equiv-comp _ _ (is-equiv-const-unit _) H
+```
diff --git a/src/group-theory/homomorphisms-concrete-groups.lagda.md b/src/group-theory/homomorphisms-concrete-groups.lagda.md
index 4b12ff6251..2283144a3f 100644
--- a/src/group-theory/homomorphisms-concrete-groups.lagda.md
+++ b/src/group-theory/homomorphisms-concrete-groups.lagda.md
@@ -34,7 +34,7 @@ module _
 
   is-set-hom-Concrete-Group : is-set hom-Concrete-Group
   is-set-hom-Concrete-Group =
-    is-trunc-map-ev-point-is-connected
+    is-trunc-map-ev-is-connected
       ( zero-𝕋)
       ( shape-Concrete-Group G)
       ( is-0-connected-classifying-type-Concrete-Group G)
diff --git a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
index bb4ecc695f..1a47382283 100644
--- a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
@@ -306,7 +306,7 @@ module _
       ( ap (map-pointed-map f))
       ( is-trunc-map-is-equiv k
         ( is-equiv-tr-type-Ω (preserves-point-pointed-map f)))
-      ( is-trunc-map-ap-is-trunc-map k
+      ( is-trunc-map-ap-is-trunc-map-succ k
         ( map-pointed-map f)
         ( H)
         ( point-Pointed-Type A)
diff --git a/src/trees/morphisms-polynomial-endofunctors.lagda.md b/src/trees/morphisms-polynomial-endofunctors.lagda.md
index a30bed6f20..85cd8ee091 100644
--- a/src/trees/morphisms-polynomial-endofunctors.lagda.md
+++ b/src/trees/morphisms-polynomial-endofunctors.lagda.md
@@ -350,9 +350,8 @@ module _
         by
         equiv-tot
           ( λ (a , p) →
-            compute-coherence-triangle-fiber-precomp'
+            compute-extension-fiber-precomp'
               ( α₁ a)
-              ( X)
               ( inv-tr (λ c' → Q₁ c' → X) p x))
       ≃ Σ ( fiber α₀ c)
           ( λ (a , p) →