From 5e15f6bd114f7d0de5f4a91c47919c5f65ba3690 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 5 Nov 2023 17:38:56 +0100
Subject: [PATCH] Retracts of maps (#900)

---
 .../commuting-squares-of-maps.lagda.md        |  14 +-
 .../equality-dependent-pair-types.lagda.md    |   9 +-
 src/foundation-core/fibers-of-maps.lagda.md   |  29 +-
 src/foundation-core/identity-types.lagda.md   |  22 +-
 src/foundation-core/retractions.lagda.md      |  22 +-
 .../commuting-squares-of-homotopies.lagda.md  |   8 +-
 ...muting-squares-of-identifications.lagda.md |   2 +-
 .../equality-fibers-of-maps.lagda.md          |  52 +-
 src/foundation/fibered-maps.lagda.md          |  17 +-
 src/foundation/fibers-of-maps.lagda.md        |   5 +-
 .../functoriality-fibers-of-maps.lagda.md     |  77 ++-
 src/foundation/retractions.lagda.md           |   5 +-
 src/foundation/sequential-limits.lagda.md     |   6 +-
 src/orthogonal-factorization-systems.lagda.md |   1 +
 .../retracts-of-maps.lagda.md                 | 524 ++++++++++++++++++
 ...cocones-under-sequential-diagrams.lagda.md |   4 +-
 .../morphisms-sequential-diagrams.lagda.md    |   4 +-
 17 files changed, 700 insertions(+), 101 deletions(-)
 create mode 100644 src/orthogonal-factorization-systems/retracts-of-maps.lagda.md

diff --git a/src/foundation-core/commuting-squares-of-maps.lagda.md b/src/foundation-core/commuting-squares-of-maps.lagda.md
index de050e312c..ab4d844e0a 100644
--- a/src/foundation-core/commuting-squares-of-maps.lagda.md
+++ b/src/foundation-core/commuting-squares-of-maps.lagda.md
@@ -35,12 +35,16 @@ is said to commute if there is a homotopy between both composites.
 ## Definitions
 
 ```agda
-coherence-square-maps :
+module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
-  (top : C → B) (left : C → A) (right : B → X) (bottom : A → X) →
-  UU (l3 ⊔ l4)
-coherence-square-maps top left right bottom =
-  bottom ∘ left ~ right ∘ top
+  (top : C → B) (left : C → A) (right : B → X) (bottom : A → X)
+  where
+
+  coherence-square-maps : UU (l3 ⊔ l4)
+  coherence-square-maps = bottom ∘ left ~ right ∘ top
+
+  coherence-square-maps' : UU (l3 ⊔ l4)
+  coherence-square-maps' = right ∘ top ~ bottom ∘ left
 ```
 
 ## Properties
diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md
index 9cf8a462d2..2fbbc0134c 100644
--- a/src/foundation-core/equality-dependent-pair-types.lagda.md
+++ b/src/foundation-core/equality-dependent-pair-types.lagda.md
@@ -72,9 +72,12 @@ module _
     {x : A} {s t : B x} → s ＝ t → (x , s) ＝ (x , t)
   eq-pair-eq-pr2 {x} = ap {B = Σ A B} (pair x)
 
+  ap-pr1-eq-pair-eq-pr2 :
+    {x : A} {s t : B x} (p : s ＝ t) → ap pr1 (eq-pair-eq-pr2 p) ＝ refl
+  ap-pr1-eq-pair-eq-pr2 refl = refl
+
   is-retraction-pair-eq-Σ :
-    (s t : Σ A B) →
-    ((pair-eq-Σ {s} {t}) ∘ (eq-pair-Σ' {s} {t})) ~ id {A = Eq-Σ s t}
+    (s t : Σ A B) → pair-eq-Σ {s} {t} ∘ eq-pair-Σ' {s} {t} ~ id {A = Eq-Σ s t}
   is-retraction-pair-eq-Σ (pair x y) (pair .x .y) (pair refl refl) = refl
 
   is-section-pair-eq-Σ :
@@ -104,7 +107,7 @@ module _
   equiv-pair-eq-Σ s t = pair pair-eq-Σ (is-equiv-pair-eq-Σ s t)
 
   η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t
-  η-pair t = eq-pair-Σ refl refl
+  η-pair t = refl
 
   eq-base-eq-pair : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t)
   eq-base-eq-pair p = pr1 (pair-eq-Σ p)
diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md
index 255a9c8c24..1cf60c7926 100644
--- a/src/foundation-core/fibers-of-maps.lagda.md
+++ b/src/foundation-core/fibers-of-maps.lagda.md
@@ -53,7 +53,7 @@ module _
   where
 
   Eq-fiber : fiber f b → fiber f b → UU (l1 ⊔ l2)
-  Eq-fiber s t = Σ (pr1 s ＝ pr1 t) (λ α → ((ap f α) ∙ (pr2 t)) ＝ (pr2 s))
+  Eq-fiber s t = Σ (pr1 s ＝ pr1 t) (λ α → ap f α ∙ pr2 t ＝ pr2 s)
 
   refl-Eq-fiber : (s : fiber f b) → Eq-fiber s s
   pr1 (refl-Eq-fiber s) = refl
@@ -66,16 +66,15 @@ module _
   eq-Eq-fiber-uncurry (refl , refl) = refl
 
   eq-Eq-fiber :
-    {s t : fiber f b} (α : pr1 s ＝ pr1 t) →
-    ((ap f α) ∙ (pr2 t)) ＝ pr2 s → s ＝ t
+    {s t : fiber f b} (α : pr1 s ＝ pr1 t) → ap f α ∙ pr2 t ＝ pr2 s → s ＝ t
   eq-Eq-fiber α β = eq-Eq-fiber-uncurry (α , β)
 
   is-section-eq-Eq-fiber :
-    {s t : fiber f b} → (Eq-eq-fiber {s} {t} ∘ eq-Eq-fiber-uncurry {s} {t}) ~ id
+    {s t : fiber f b} → Eq-eq-fiber {s} {t} ∘ eq-Eq-fiber-uncurry {s} {t} ~ id
   is-section-eq-Eq-fiber (refl , refl) = refl
 
   is-retraction-eq-Eq-fiber :
-    {s t : fiber f b} → (eq-Eq-fiber-uncurry {s} {t} ∘ Eq-eq-fiber {s} {t}) ~ id
+    {s t : fiber f b} → eq-Eq-fiber-uncurry {s} {t} ∘ Eq-eq-fiber {s} {t} ~ id
   is-retraction-eq-Eq-fiber refl = refl
 
   abstract
@@ -112,7 +111,7 @@ module _
   where
 
   Eq-fiber' : fiber' f b → fiber' f b → UU (l1 ⊔ l2)
-  Eq-fiber' s t = Σ (pr1 s ＝ pr1 t) (λ α → (pr2 t ＝ ((pr2 s) ∙ (ap f α))))
+  Eq-fiber' s t = Σ (pr1 s ＝ pr1 t) (λ α → pr2 t ＝ pr2 s ∙ ap f α)
 
   refl-Eq-fiber' : (s : fiber' f b) → Eq-fiber' s s
   pr1 (refl-Eq-fiber' s) = refl
@@ -126,18 +125,17 @@ module _
     ap (pair x) (inv right-unit)
 
   eq-Eq-fiber' :
-    {s t : fiber' f b} (α : pr1 s ＝ pr1 t) →
-    (pr2 t) ＝ ((pr2 s) ∙ (ap f α)) → s ＝ t
+    {s t : fiber' f b} (α : pr1 s ＝ pr1 t) → pr2 t ＝ pr2 s ∙ ap f α → s ＝ t
   eq-Eq-fiber' α β = eq-Eq-fiber-uncurry' (α , β)
 
   is-section-eq-Eq-fiber' :
     {s t : fiber' f b} →
-    (Eq-eq-fiber' {s} {t} ∘ eq-Eq-fiber-uncurry' {s} {t}) ~ id
+    Eq-eq-fiber' {s} {t} ∘ eq-Eq-fiber-uncurry' {s} {t} ~ id
   is-section-eq-Eq-fiber' {x , refl} (refl , refl) = refl
 
   is-retraction-eq-Eq-fiber' :
     {s t : fiber' f b} →
-    (eq-Eq-fiber-uncurry' {s} {t} ∘ Eq-eq-fiber' {s} {t}) ~ id
+    eq-Eq-fiber-uncurry' {s} {t} ∘ Eq-eq-fiber' {s} {t} ~ id
   is-retraction-eq-Eq-fiber' {x , refl} refl = refl
 
   abstract
@@ -182,11 +180,10 @@ module _
   pr1 (map-inv-equiv-fiber (x , refl)) = x
   pr2 (map-inv-equiv-fiber (x , refl)) = refl
 
-  is-section-map-inv-equiv-fiber : (map-equiv-fiber ∘ map-inv-equiv-fiber) ~ id
+  is-section-map-inv-equiv-fiber : map-equiv-fiber ∘ map-inv-equiv-fiber ~ id
   is-section-map-inv-equiv-fiber (x , refl) = refl
 
-  is-retraction-map-inv-equiv-fiber :
-    (map-inv-equiv-fiber ∘ map-equiv-fiber) ~ id
+  is-retraction-map-inv-equiv-fiber : map-inv-equiv-fiber ∘ map-equiv-fiber ~ id
   is-retraction-map-inv-equiv-fiber (x , refl) = refl
 
   is-equiv-map-equiv-fiber : is-equiv map-equiv-fiber
@@ -315,13 +312,11 @@ module _
   inv-map-compute-fiber-comp :
     Σ (fiber g x) (λ t → fiber h (pr1 t)) → fiber (g ∘ h) x
   pr1 (inv-map-compute-fiber-comp t) = pr1 (pr2 t)
-  pr2 (inv-map-compute-fiber-comp t) =
-    ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t)
+  pr2 (inv-map-compute-fiber-comp t) = ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t)
 
   is-section-inv-map-compute-fiber-comp :
     (map-compute-fiber-comp ∘ inv-map-compute-fiber-comp) ~ id
-  is-section-inv-map-compute-fiber-comp
-    ((.(h a) , refl) , (a , refl)) = refl
+  is-section-inv-map-compute-fiber-comp ((.(h a) , refl) , (a , refl)) = refl
 
   is-retraction-inv-map-compute-fiber-comp :
     (inv-map-compute-fiber-comp ∘ map-compute-fiber-comp) ~ id
diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md
index 236c8d76ea..6583fc23e9 100644
--- a/src/foundation-core/identity-types.lagda.md
+++ b/src/foundation-core/identity-types.lagda.md
@@ -156,15 +156,19 @@ module _
 ### Transposing inverses
 
 ```agda
-left-transpose-eq-concat :
-  {l : Level} {A : UU l} {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z)
-  (r : x ＝ z) → ((p ∙ q) ＝ r) → q ＝ ((inv p) ∙ r)
-left-transpose-eq-concat refl q r s = s
-
-right-transpose-eq-concat :
-  {l : Level} {A : UU l} {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z)
-  (r : x ＝ z) → ((p ∙ q) ＝ r) → p ＝ (r ∙ (inv q))
-right-transpose-eq-concat p refl r s = ((inv right-unit) ∙ s) ∙ (inv right-unit)
+module _
+  {l : Level} {A : UU l} {x y : A}
+  where
+
+  left-transpose-eq-concat :
+    (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
+    p ∙ q ＝ r → q ＝ inv p ∙ r
+  left-transpose-eq-concat refl q r s = s
+
+  right-transpose-eq-concat :
+    (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
+    p ∙ q ＝ r → p ＝ r ∙ inv q
+  right-transpose-eq-concat p refl r s = (inv right-unit ∙ s) ∙ inv right-unit
 ```
 
 The fact that `left-transpose-eq-concat` and `right-transpose-eq-concat` are
diff --git a/src/foundation-core/retractions.lagda.md b/src/foundation-core/retractions.lagda.md
index 051bdea2a5..b852838a58 100644
--- a/src/foundation-core/retractions.lagda.md
+++ b/src/foundation-core/retractions.lagda.md
@@ -26,7 +26,9 @@ A **retraction** is a map that has a right inverse, i.e. a section. Thus,
 homotopic to the identity at `A`. Moreover, in this case we say that `A` _is a
 retract of_ `B`.
 
-## Definition
+## Definitions
+
+### The type of retractions
 
 ```agda
 module _
@@ -40,11 +42,14 @@ module _
   map-retraction f = pr1
 
   is-retraction-map-retraction :
-    (f : A → B) (r : retraction f) → (map-retraction f r ∘ f) ~ id
+    (f : A → B) (r : retraction f) → map-retraction f r ∘ f ~ id
   is-retraction-map-retraction f = pr2
+```
 
-_retract-of_ :
-  {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
+### Retracts of a type
+
+```agda
+_retract-of_ : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
 A retract-of B = Σ (A → B) retraction
 
 module _
@@ -58,13 +63,12 @@ module _
     (R : A retract-of B) → retraction (section-retract-of R)
   retraction-section-retract-of = pr2
 
-  retraction-retract-of : (A retract-of B) → B → A
+  retraction-retract-of : A retract-of B → B → A
   retraction-retract-of R = pr1 (retraction-section-retract-of R)
 
-  is-retraction-retraction-retract-of :
-    (R : A retract-of B) →
-    (retraction-retract-of R ∘ section-retract-of R) ~ id
-  is-retraction-retraction-retract-of R = pr2 (retraction-section-retract-of R)
+  is-retract-retract-of :
+    (R : A retract-of B) → retraction-retract-of R ∘ section-retract-of R ~ id
+  is-retract-retract-of R = pr2 (retraction-section-retract-of R)
 ```
 
 ## Properties
diff --git a/src/foundation/commuting-squares-of-homotopies.lagda.md b/src/foundation/commuting-squares-of-homotopies.lagda.md
index c14f9bbf33..a6459cf3fa 100644
--- a/src/foundation/commuting-squares-of-homotopies.lagda.md
+++ b/src/foundation/commuting-squares-of-homotopies.lagda.md
@@ -24,11 +24,11 @@ A square of [homotopies](foundation-core.homotopies.md)
       |         |
  left |         | right
       v         v
-      z ------> i
+      h ------> i
         bottom
 ```
 
-is said to **commute** if there is a homotopy `left ∙h bottom ~ top ∙h right`.
+is said to **commute** if there is a homotopy `left ∙h bottom ~ top ∙h right `.
 Such a homotopy is called a **coherence** of the square.
 
 ## Definition
@@ -39,7 +39,7 @@ module _
   where
 
   coherence-square-homotopies :
-    (left : f ~ h) (bottom : h ~ i) (top : f ~ g) (right : g ~ i) → UU (l1 ⊔ l2)
-  coherence-square-homotopies left bottom top right =
+    (top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) → UU (l1 ⊔ l2)
+  coherence-square-homotopies top left right bottom =
     left ∙h bottom ~ top ∙h right
 ```
diff --git a/src/foundation/commuting-squares-of-identifications.lagda.md b/src/foundation/commuting-squares-of-identifications.lagda.md
index 77c150f49c..0c716a303b 100644
--- a/src/foundation/commuting-squares-of-identifications.lagda.md
+++ b/src/foundation/commuting-squares-of-identifications.lagda.md
@@ -45,7 +45,7 @@ module _
   coherence-square-identifications :
     (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) → UU l
   coherence-square-identifications top left right bottom =
-    (left ∙ bottom) ＝ (top ∙ right)
+    left ∙ bottom ＝ top ∙ right
 ```
 
 ## Operations
diff --git a/src/foundation/equality-fibers-of-maps.lagda.md b/src/foundation/equality-fibers-of-maps.lagda.md
index c4ccf1aa1a..8c075e0f97 100644
--- a/src/foundation/equality-fibers-of-maps.lagda.md
+++ b/src/foundation/equality-fibers-of-maps.lagda.md
@@ -37,7 +37,7 @@ For any map `f : A → B` any `b : B` and any `x y : fiber f b`, there is an
 equivalence
 
 ```text
-(x ＝ y) ≃ fiber (ap f) ((pr2 x) ∙ (inv (pr2 y)))
+(x ＝ y) ≃ fiber (ap f) (pr2 x ∙ inv (pr2 y))
 ```
 
 ### Proof
@@ -48,19 +48,16 @@ module _
   where
 
   fiber-ap-eq-fiber-fiberwise :
-    (s t : fiber f b) (p : (pr1 s) ＝ (pr1 t)) →
-    ((tr (λ (a : A) → (f a) ＝ b) p (pr2 s)) ＝ (pr2 t)) →
-    (ap f p ＝ ((pr2 s) ∙ (inv (pr2 t))))
-  fiber-ap-eq-fiber-fiberwise (pair .x' p) (pair x' refl) refl =
-    inv ∘ (concat right-unit refl)
+    (s t : fiber f b) (p : pr1 s ＝ pr1 t) →
+    tr (λ (a : A) → f a ＝ b) p (pr2 s) ＝ pr2 t →
+    ap f p ＝ pr2 s ∙ inv (pr2 t)
+  fiber-ap-eq-fiber-fiberwise (.x' , p) (x' , refl) refl =
+    inv ∘ concat right-unit refl
 
   abstract
     is-fiberwise-equiv-fiber-ap-eq-fiber-fiberwise :
       (s t : fiber f b) → is-fiberwise-equiv (fiber-ap-eq-fiber-fiberwise s t)
-    is-fiberwise-equiv-fiber-ap-eq-fiber-fiberwise
-      ( pair x y)
-      ( pair .x refl)
-      ( refl) =
+    is-fiberwise-equiv-fiber-ap-eq-fiber-fiberwise (x , y) (.x , refl) refl =
       is-equiv-comp
         ( inv)
         ( concat right-unit refl)
@@ -69,15 +66,15 @@ module _
 
   fiber-ap-eq-fiber :
     (s t : fiber f b) → s ＝ t →
-    fiber (ap f {x = pr1 s} {y = pr1 t}) ((pr2 s) ∙ (inv (pr2 t)))
+    fiber (ap f {x = pr1 s} {y = pr1 t}) (pr2 s ∙ inv (pr2 t))
   pr1 (fiber-ap-eq-fiber s .s refl) = refl
   pr2 (fiber-ap-eq-fiber s .s refl) = inv (right-inv (pr2 s))
 
   triangle-fiber-ap-eq-fiber :
     (s t : fiber f b) →
-    ( fiber-ap-eq-fiber s t) ~
-    ( (tot (fiber-ap-eq-fiber-fiberwise s t)) ∘ (pair-eq-Σ {s = s} {t}))
-  triangle-fiber-ap-eq-fiber (pair x refl) .(pair x refl) refl = refl
+    fiber-ap-eq-fiber s t ~
+    tot (fiber-ap-eq-fiber-fiberwise s t) ∘ pair-eq-Σ {s = s} {t}
+  triangle-fiber-ap-eq-fiber (x , refl) .(x , refl) refl = refl
 
   abstract
     is-equiv-fiber-ap-eq-fiber :
@@ -94,28 +91,41 @@ module _
 
   equiv-fiber-ap-eq-fiber :
     (s t : fiber f b) →
-    (s ＝ t) ≃ fiber (ap f {x = pr1 s} {y = pr1 t}) ((pr2 s) ∙ (inv (pr2 t)))
+    (s ＝ t) ≃ fiber (ap f {x = pr1 s} {y = pr1 t}) (pr2 s ∙ inv (pr2 t))
   pr1 (equiv-fiber-ap-eq-fiber s t) = fiber-ap-eq-fiber s t
   pr2 (equiv-fiber-ap-eq-fiber s t) = is-equiv-fiber-ap-eq-fiber s t
 
+  map-inv-fiber-ap-eq-fiber :
+    (s t : fiber f b) →
+    fiber (ap f {x = pr1 s} {y = pr1 t}) (pr2 s ∙ inv (pr2 t)) →
+    s ＝ t
+  map-inv-fiber-ap-eq-fiber (x , refl) (.x , p) (refl , u) =
+    eq-pair-eq-pr2 (ap inv u ∙ inv-inv p)
+
+  ap-pr1-map-inv-fiber-ap-eq-fiber :
+    (s t : fiber f b) →
+    (v : fiber (ap f {x = pr1 s} {y = pr1 t}) (pr2 s ∙ inv (pr2 t))) →
+    ap pr1 (map-inv-fiber-ap-eq-fiber s t v) ＝ pr1 v
+  ap-pr1-map-inv-fiber-ap-eq-fiber (x , refl) (.x , p) (refl , u) =
+    ap-pr1-eq-pair-eq-pr2 (ap inv u ∙ inv-inv p)
+
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (x y : A)
   where
 
   eq-fiber-fiber-ap :
-    (q : f x ＝ f y) → (pair x q) ＝ (pair y refl) → fiber (ap f {x} {y}) q
+    (q : f x ＝ f y) → (x , q) ＝ (y , refl) → fiber (ap f {x} {y}) q
   eq-fiber-fiber-ap q =
-    ( tr (fiber (ap f)) right-unit) ∘
-    ( fiber-ap-eq-fiber f (pair x q) (pair y refl))
+    tr (fiber (ap f)) right-unit ∘ fiber-ap-eq-fiber f (x , q) (y , refl)
 
   abstract
     is-equiv-eq-fiber-fiber-ap :
-      (q : (f x) ＝ (f y)) → is-equiv (eq-fiber-fiber-ap q)
+      (q : (f x) ＝ f y) → is-equiv (eq-fiber-fiber-ap q)
     is-equiv-eq-fiber-fiber-ap q =
       is-equiv-comp
         ( tr (fiber (ap f)) right-unit)
-        ( fiber-ap-eq-fiber f (pair x q) (pair y refl))
-        ( is-equiv-fiber-ap-eq-fiber f (pair x q) (pair y refl))
+        ( fiber-ap-eq-fiber f (x , q) (y , refl))
+        ( is-equiv-fiber-ap-eq-fiber f (x , q) (y , refl))
         ( is-equiv-tr (fiber (ap f)) right-unit)
 ```
 
diff --git a/src/foundation/fibered-maps.lagda.md b/src/foundation/fibered-maps.lagda.md
index 63a17a6c56..89c8df666d 100644
--- a/src/foundation/fibered-maps.lagda.md
+++ b/src/foundation/fibered-maps.lagda.md
@@ -51,10 +51,10 @@ Consider a diagram of the form
        i
 ```
 
-A fibered map from `f` to `g` over `i` is a map `h : A → B` such that the square
-`(i ∘ f) ~ (g ∘ h)` commutes.
+A **fibered map** from `f` to `g` over `i` is a map `h : A → B` such that the
+square `i ∘ f ~ g ∘ h` [commutes](foundation-core.commuting-squares-of-maps.md).
 
-## Definition
+## Definitions
 
 ```agda
 module _
@@ -250,17 +250,17 @@ module _
 
   is-section-map-over-fiberwise-map-over-eq-htpy :
     (α : fiberwise-map-over f g i) (x : X) →
-    (fiberwise-map-over-map-over (map-over-fiberwise-map-over α) x) ~ (α x)
+    fiberwise-map-over-map-over (map-over-fiberwise-map-over α) x ~ α x
   is-section-map-over-fiberwise-map-over-eq-htpy α .(f a) (pair a refl) =
     eq-pair-Σ refl (inv-inv (pr2 (α (f a) (pair a refl))))
 
   is-section-map-over-fiberwise-map-over :
-    (fiberwise-map-over-map-over ∘ map-over-fiberwise-map-over) ~ id
+    fiberwise-map-over-map-over ∘ map-over-fiberwise-map-over ~ id
   is-section-map-over-fiberwise-map-over α =
     eq-htpy (eq-htpy ∘ is-section-map-over-fiberwise-map-over-eq-htpy α)
 
   is-retraction-map-over-fiberwise-map-over :
-    (map-over-fiberwise-map-over ∘ fiberwise-map-over-map-over) ~ id
+    map-over-fiberwise-map-over ∘ fiberwise-map-over-map-over ~ id
   is-retraction-map-over-fiberwise-map-over (pair h H) =
     eq-pair-Σ refl (eq-htpy (inv-inv ∘ H))
 
@@ -466,7 +466,7 @@ module _
           ( universal-property-empty-is-empty A is-empty-A B)
           ( ex-falso ∘ is-empty-A)
           ( dependent-universal-property-empty-is-empty A is-empty-A
-            ( λ z → (i ∘ f) z ＝ (g ∘ (ex-falso ∘ is-empty-A)) z)))
+            ( eq-value (i ∘ f) (g ∘ ex-falso ∘ is-empty-A))))
 
   compute-fibered-map-is-empty : (X → Y) ≃ (fibered-map f g)
   compute-fibered-map-is-empty = inv-equiv inv-compute-fibered-map-is-empty
@@ -506,8 +506,7 @@ module _
       ( λ j →
         is-contr-Π
           ( λ x →
-            is-prop-is-contr
-              is-contr-Y (((λ _ → center is-contr-Y) ∘ f) x) ((g ∘ j) x)))) ∘e
+            is-prop-is-contr is-contr-Y (center is-contr-Y) (g (j x))))) ∘e
     ( left-unit-law-Σ-is-contr
       ( is-contr-function-type is-contr-Y)
       ( λ _ → center is-contr-Y))
diff --git a/src/foundation/fibers-of-maps.lagda.md b/src/foundation/fibers-of-maps.lagda.md
index 94b6f353dc..2cfb875685 100644
--- a/src/foundation/fibers-of-maps.lagda.md
+++ b/src/foundation/fibers-of-maps.lagda.md
@@ -34,8 +34,7 @@ module _
   where
 
   square-fiber :
-    ( f ∘ (pr1 {B = λ x → Id (f x) b})) ~
-    ( (const unit B b) ∘ (const (fiber f b) unit star))
+    f ∘ pr1 ~ const unit B b ∘ const (fiber f b) unit star
   square-fiber = pr2
 
   cone-fiber : cone f (const unit B b) (fiber f b)
@@ -47,7 +46,7 @@ module _
     is-pullback-cone-fiber : is-pullback f (const unit B b) cone-fiber
     is-pullback-cone-fiber =
       is-equiv-tot-is-fiberwise-equiv
-        (λ a → is-equiv-map-inv-left-unit-law-prod)
+        ( λ a → is-equiv-map-inv-left-unit-law-prod)
 
   abstract
     universal-property-pullback-cone-fiber :
diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md
index 48b82c08ac..092405f7c1 100644
--- a/src/foundation/functoriality-fibers-of-maps.lagda.md
+++ b/src/foundation/functoriality-fibers-of-maps.lagda.md
@@ -12,6 +12,7 @@ open import foundation.cones-over-cospans
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
+open import foundation-core.commuting-squares-of-maps
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
@@ -24,11 +25,62 @@ open import foundation-core.identity-types
 
 ## Idea
 
-Any [commuting square](foundation-core.commuting-squares-of-maps.md) induces a
-map between the fibers of the vertical maps.
+Any [commuting square](foundation-core.commuting-squares-of-maps.md)
+
+```text
+        f'
+    C -----> B
+    |        |
+  g'|        | g
+    v        v
+    A -----> X
+        f
+```
+
+induces a map between the [fibers](foundation-core.fibers-of-maps.md) of the
+vertical maps
+
+```text
+  fiber g' x → fiber g (f x).
+```
 
 ## Definitions
 
+### Any commuting square induces a family of maps between the fibers of the vertical maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
+  (top : C → B) (left : C → A) (right : B → X) (bottom : A → X)
+  where
+
+  map-fiber-square' :
+    (H : coherence-square-maps' top left right bottom)
+    (x : A) → fiber left x → fiber right (bottom x)
+  pr1 (map-fiber-square' H x (y , p)) = top y
+  pr2 (map-fiber-square' H x (y , p)) = H y ∙ ap bottom p
+
+  coherence-fiber-square' :
+    (H : coherence-square-maps' top left right bottom)
+    (x : A) → coherence-square-maps' (map-fiber-square' H x) pr1 pr1 top
+  coherence-fiber-square' H x p = refl
+
+  map-fiber-square :
+    (H : coherence-square-maps top left right bottom)
+    (x : A) → fiber left x → fiber right (bottom x)
+  map-fiber-square H = map-fiber-square' (inv-htpy H)
+
+  coherence-fiber-square :
+    (H : coherence-square-maps top left right bottom)
+    (x : A) → coherence-square-maps (map-fiber-square H x) pr1 pr1 top
+  coherence-fiber-square H x p = refl
+
+map-fiber-square-id :
+  {l1 l2 : Level} {B : UU l1} {X : UU l2} (g : B → X) (x : X) →
+  map-fiber-square id g g id refl-htpy x ~ id
+map-fiber-square-id g .(g b) (b , refl) = refl
+```
+
 ### Any cone induces a family of maps between the fibers of the vertical maps
 
 ```agda
@@ -38,14 +90,13 @@ module _
   where
 
   map-fiber-cone : (x : A) → fiber (pr1 c) x → fiber g (f x)
-  pr1 (map-fiber-cone x t) = pr1 (pr2 c) (pr1 t)
-  pr2 (map-fiber-cone x t) = (inv (pr2 (pr2 c) (pr1 t))) ∙ (ap f (pr2 t))
-
-map-fiber-cone-id :
-  {l1 l2 : Level} {B : UU l1} {X : UU l2} (g : B → X) (x : X) →
-  map-fiber-cone id g (g , id , refl-htpy) x ~ id
-map-fiber-cone-id g .(g b) (b , refl) =
-  refl
+  map-fiber-cone =
+    map-fiber-square
+      ( horizontal-map-cone f g c)
+      ( vertical-map-cone f g c)
+      ( g)
+      ( f)
+      ( coherence-square-cone f g c)
 ```
 
 ## Properties
@@ -114,6 +165,12 @@ module _
             ( ap (ap g) (inv right-unit)))))
 ```
 
+## See also
+
+- In [retracts of maps](orthogonal-factorization-systems.retracts-of-maps.md),
+  we show that if `g` is a retract of `g'`, then the fibers of `g` are retracts
+  of the fibers of `g'`.
+
 ## Table of files about fibers of maps
 
 The following table lists files that are about fibers of maps as a general
diff --git a/src/foundation/retractions.lagda.md b/src/foundation/retractions.lagda.md
index 0173641b96..a8d2543e94 100644
--- a/src/foundation/retractions.lagda.md
+++ b/src/foundation/retractions.lagda.md
@@ -66,8 +66,7 @@ is-retraction-retraction-comp-htpy :
 is-retraction-retraction-comp-htpy f g h H (l , L) (k , K) =
   eq-htpy-retraction
     ( ( retraction-right-factor-htpy f g h H
-        ( retraction-comp-htpy f g h H (l , L) (k , K)
-          )))
+        ( retraction-comp-htpy f g h H (l , L) (k , K))))
     ( k , K)
     ( k ·l L)
     ( ( inv-htpy-assoc-htpy
@@ -82,7 +81,7 @@ is-retraction-retraction-comp-htpy f g h H (l , L) (k , K) =
 
 retraction-right-factor-retract-of-retraction-left-factor :
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
+  (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h) →
   retraction g → (retraction h) retract-of (retraction f)
 pr1 (retraction-right-factor-retract-of-retraction-left-factor f g h H rg) =
   retraction-comp-htpy f g h H rg
diff --git a/src/foundation/sequential-limits.lagda.md b/src/foundation/sequential-limits.lagda.md
index 8a8503dce0..9a340a834a 100644
--- a/src/foundation/sequential-limits.lagda.md
+++ b/src/foundation/sequential-limits.lagda.md
@@ -158,10 +158,10 @@ module _
         sequence-standard-sequential-limit A t)
       ( λ H →
         coherence-square-homotopies
-          ( coherence-standard-sequential-limit A s)
-          ( λ n → ap (map-tower A n) (H (succ-ℕ n)))
           ( H)
-          ( coherence-standard-sequential-limit A t))
+          ( coherence-standard-sequential-limit A s)
+          ( coherence-standard-sequential-limit A t)
+          ( λ n → ap (map-tower A n) (H (succ-ℕ n))))
 
   refl-Eq-standard-sequential-limit :
     (s : standard-sequential-limit A) → Eq-standard-sequential-limit s s
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index 31bc562be6..0a9661d35f 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -37,6 +37,7 @@ open import orthogonal-factorization-systems.pullback-hom public
 open import orthogonal-factorization-systems.raise-modalities public
 open import orthogonal-factorization-systems.reflective-modalities public
 open import orthogonal-factorization-systems.reflective-subuniverses public
+open import orthogonal-factorization-systems.retracts-of-maps public
 open import orthogonal-factorization-systems.separated-types public
 open import orthogonal-factorization-systems.sigma-closed-modalities public
 open import orthogonal-factorization-systems.sigma-closed-reflective-modalities public
diff --git a/src/orthogonal-factorization-systems/retracts-of-maps.lagda.md b/src/orthogonal-factorization-systems/retracts-of-maps.lagda.md
new file mode 100644
index 0000000000..a7b4972564
--- /dev/null
+++ b/src/orthogonal-factorization-systems/retracts-of-maps.lagda.md
@@ -0,0 +1,524 @@
+# Retracts of maps
+
+```agda
+module orthogonal-factorization-systems.retracts-of-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-homotopies
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equality-fibers-of-maps
+open import foundation.equivalences
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-fibers-of-maps
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.retractions
+open import foundation.sections
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies
+```
+
+</details>
+
+## Idea
+
+A **retract** of `f : X → Y` is a map `g : A → B` that is a retract in the arrow
+category of types. Hence, it consists of
+[retracts](foundation-core.retractions.md) `A` of `X` and `B` of `Y` that fit
+into a commutative diagram
+
+```text
+       s         r
+  A ------> X ------> A
+  |         |         |
+  g    S    f    R    g
+  v         v         v
+  B ------> Y ------> B
+       s'        r'
+```
+
+with coherences
+
+```text
+  S : s' ∘ g ~ f ∘ s  and   R : r' ∘ f ~ g ∘ r
+```
+
+and a higher coherence
+
+```text
+                  R ·r s
+       r' ∘ f ∘ s ------ g ∘ r ∘ s
+            |                |
+            |                |
+  r' ·l S⁻¹ |        L       | g ·l H
+            |                |
+            |                |
+      r' ∘ s' ∘ g ---------- g
+                  H' ·r g
+```
+
+Where `H` and `H'` are the retracting homotopies of `r ∘ s` and `r' ∘ s'`
+respectively.
+
+## Definition
+
+### The predicate of being a retract of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (r : A retract-of X) (r' : B retract-of Y)
+  where
+
+  statement-coherence-is-retract-of-map :
+    coherence-square-maps (section-retract-of r) g f (section-retract-of r') →
+    coherence-square-maps
+      ( retraction-retract-of r) f g (retraction-retract-of r') →
+    UU (l1 ⊔ l2)
+  statement-coherence-is-retract-of-map S R =
+    coherence-square-homotopies
+      ( R ·r section-retract-of r)
+      ( retraction-retract-of r' ·l inv-htpy S)
+      ( g ·l is-retract-retract-of r)
+      ( is-retract-retract-of r' ·r g)
+
+  is-retract-of-map : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-retract-of-map =
+    Σ ( coherence-square-maps
+        ( section-retract-of r) g f (section-retract-of r'))
+      ( λ S →
+        Σ ( coherence-square-maps
+            ( retraction-retract-of r) f g (retraction-retract-of r'))
+          ( statement-coherence-is-retract-of-map S))
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (r : A retract-of X) (r' : B retract-of Y)
+  (k : is-retract-of-map f g r r')
+  where
+
+  coherence-section-is-retract-of-map :
+    coherence-square-maps (section-retract-of r) g f (section-retract-of r')
+  coherence-section-is-retract-of-map = pr1 k
+
+  coherence-retraction-is-retract-of-map :
+    coherence-square-maps
+      ( retraction-retract-of r) f g (retraction-retract-of r')
+  coherence-retraction-is-retract-of-map = pr1 (pr2 k)
+
+  coherence-is-retract-of-map :
+    statement-coherence-is-retract-of-map f g r r'
+      coherence-section-is-retract-of-map
+      coherence-retraction-is-retract-of-map
+  coherence-is-retract-of-map = pr2 (pr2 k)
+```
+
+### The type of retracts of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (g : A → B) (f : X → Y)
+  where
+
+  _retract-of-map_ : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  _retract-of-map_ =
+    Σ (A retract-of X) (λ r → Σ (B retract-of Y) (is-retract-of-map f g r))
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (k : g retract-of-map f)
+  where
+
+  retract-of-domain-retract-of-map : A retract-of X
+  retract-of-domain-retract-of-map = pr1 k
+
+  retract-of-codomain-retract-of-map : B retract-of Y
+  retract-of-codomain-retract-of-map = pr1 (pr2 k)
+
+  is-retract-of-map-retract-of-map :
+    is-retract-of-map f g
+      retract-of-domain-retract-of-map
+      retract-of-codomain-retract-of-map
+  is-retract-of-map-retract-of-map = pr2 (pr2 k)
+
+  section-of-domain-retract-of-map : A → X
+  section-of-domain-retract-of-map =
+    section-retract-of retract-of-domain-retract-of-map
+
+  retraction-of-domain-retract-of-map : X → A
+  retraction-of-domain-retract-of-map =
+    retraction-retract-of retract-of-domain-retract-of-map
+
+  is-retract-of-domain-retract-of-map :
+    retraction-of-domain-retract-of-map ∘ section-of-domain-retract-of-map ~ id
+  is-retract-of-domain-retract-of-map =
+    is-retract-retract-of retract-of-domain-retract-of-map
+
+  section-of-codomain-retract-of-map : B → Y
+  section-of-codomain-retract-of-map =
+    section-retract-of retract-of-codomain-retract-of-map
+
+  retraction-of-codomain-retract-of-map : Y → B
+  retraction-of-codomain-retract-of-map =
+    retraction-retract-of retract-of-codomain-retract-of-map
+
+  is-retract-of-codomain-retract-of-map :
+    retraction-of-codomain-retract-of-map ∘ section-of-codomain-retract-of-map ~
+    id
+  is-retract-of-codomain-retract-of-map =
+    is-retract-retract-of retract-of-codomain-retract-of-map
+
+  coherence-section-retract-of-map :
+    coherence-square-maps
+      ( section-of-domain-retract-of-map)
+      ( g)
+      ( f)
+      ( section-of-codomain-retract-of-map)
+  coherence-section-retract-of-map =
+    coherence-section-is-retract-of-map f g
+      ( retract-of-domain-retract-of-map)
+      ( retract-of-codomain-retract-of-map)
+      ( is-retract-of-map-retract-of-map)
+
+  coherence-retraction-retract-of-map :
+    coherence-square-maps
+      ( retraction-of-domain-retract-of-map)
+      ( f)
+      ( g)
+      ( retraction-of-codomain-retract-of-map)
+  coherence-retraction-retract-of-map =
+    coherence-retraction-is-retract-of-map f g
+      ( retract-of-domain-retract-of-map)
+      ( retract-of-codomain-retract-of-map)
+      ( is-retract-of-map-retract-of-map)
+
+  coherence-retract-of-map :
+    statement-coherence-is-retract-of-map f g
+      retract-of-domain-retract-of-map
+      retract-of-codomain-retract-of-map
+      coherence-section-retract-of-map
+      coherence-retraction-retract-of-map
+  coherence-retract-of-map =
+    coherence-is-retract-of-map f g
+      ( retract-of-domain-retract-of-map)
+      ( retract-of-codomain-retract-of-map)
+      ( is-retract-of-map-retract-of-map)
+```
+
+## Properties
+
+### If `g` is a retract of `f`, then the fibers of `g` are retracts of the fibers of `f`
+
+```text
+      s''        r''
+ g⁻¹x -> f⁻¹(s'x) -> g⁻¹x
+  |         |         |
+  |    S'   |    R'   |
+  v         v         v
+  A -- s -> X -- r -> A
+  |         |         |
+  g    S    f    R    g
+  v         v         v
+  B ------> Y ------> B
+       s'        r'
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (k : g retract-of-map f)
+  where
+
+  map-section-fiber-retract-of-map :
+    (y : B) → fiber g y → fiber f (section-of-codomain-retract-of-map f g k y)
+  map-section-fiber-retract-of-map =
+    map-fiber-square
+      ( section-of-domain-retract-of-map f g k)
+      ( g)
+      ( f)
+      ( section-of-codomain-retract-of-map f g k)
+      ( coherence-section-retract-of-map f g k)
+
+  map-retraction-fiber-retract-of-map' :
+    (y : Y) →
+    fiber f y → fiber g (retraction-of-codomain-retract-of-map f g k y)
+  map-retraction-fiber-retract-of-map' =
+    map-fiber-square
+      ( retraction-of-domain-retract-of-map f g k)
+      ( f)
+      ( g)
+      ( retraction-of-codomain-retract-of-map f g k)
+      ( coherence-retraction-retract-of-map f g k)
+
+  map-retraction-fiber-retract-of-map :
+    (y : B) → fiber f (section-of-codomain-retract-of-map f g k y) → fiber g y
+  pr1 (map-retraction-fiber-retract-of-map y (x , p)) =
+    retraction-of-domain-retract-of-map f g k x
+  pr2 (map-retraction-fiber-retract-of-map y (x , p)) =
+    ( inv (coherence-retraction-retract-of-map f g k x)) ∙
+    ( ap (retraction-of-codomain-retract-of-map f g k) p) ∙
+    ( is-retract-of-codomain-retract-of-map f g k y)
+
+  abstract
+    coherence-is-retraction-fiber-retract-of-map :
+      (y : B) ((x , p) : fiber g y) →
+      (g ·l is-retract-of-domain-retract-of-map f g k) x ＝
+      ( inv
+        ( coherence-retraction-retract-of-map f g k
+          ( pr1 (map-section-fiber-retract-of-map y (x , p))))) ∙
+      ( ap
+        ( retraction-of-codomain-retract-of-map f g k)
+        ( pr2 (map-section-fiber-retract-of-map y (x , p)))) ∙
+      ( is-retract-of-codomain-retract-of-map f g k y) ∙
+      ( inv p)
+    coherence-is-retraction-fiber-retract-of-map y (x , refl) =
+      ( ( ( left-transpose-htpy-concat
+            ( coherence-retraction-retract-of-map f g k ·r
+              section-of-domain-retract-of-map f g k)
+            ( g ·l is-retract-of-domain-retract-of-map f g k)
+            ( ( retraction-of-codomain-retract-of-map f g k ·l
+                inv-htpy (coherence-section-retract-of-map f g k)) ∙h
+              ( is-retract-of-codomain-retract-of-map f g k ·r g))
+            ( inv-htpy (coherence-retract-of-map f g k))) ∙h
+          ( inv-htpy-assoc-htpy
+            ( inv-htpy
+              ( coherence-retraction-retract-of-map f g k ·r
+                section-of-domain-retract-of-map f g k))
+            ( retraction-of-codomain-retract-of-map f g k ·l
+              inv-htpy (coherence-section-retract-of-map f g k))
+            ( is-retract-of-codomain-retract-of-map f g k ·r g)))
+        ( x)) ∙
+      ( ap
+        ( λ p →
+          ( inv
+            ( coherence-retraction-retract-of-map f g k
+              ( section-of-domain-retract-of-map f g k x))) ∙
+          ( ap (retraction-of-codomain-retract-of-map f g k) p) ∙
+          ( is-retract-of-codomain-retract-of-map f g k y))
+        ( inv right-unit)) ∙
+      ( inv right-unit)
+
+  is-retraction-fiber-retract-of-map :
+    (y : B) →
+    ( map-retraction-fiber-retract-of-map y ∘
+      map-section-fiber-retract-of-map y) ~
+    id
+  is-retraction-fiber-retract-of-map y (x , p) =
+    map-inv-fiber-ap-eq-fiber g
+      ( map-retraction-fiber-retract-of-map y
+        ( map-section-fiber-retract-of-map y (x , p)))
+      ( x , p)
+      ( ( is-retract-of-domain-retract-of-map f g k x) ,
+        ( coherence-is-retraction-fiber-retract-of-map y (x , p)))
+
+  retract-of-fiber-retract-of-map :
+    (y : B) →
+    ( fiber g y) retract-of
+    ( fiber f (section-of-codomain-retract-of-map f g k y))
+  pr1 (retract-of-fiber-retract-of-map y) =
+    map-section-fiber-retract-of-map y
+  pr1 (pr2 (retract-of-fiber-retract-of-map y)) =
+    map-retraction-fiber-retract-of-map y
+  pr2 (pr2 (retract-of-fiber-retract-of-map y)) =
+    is-retraction-fiber-retract-of-map y
+```
+
+### If `g` is a retract of `f`, then the fiber projections of `g` are retracts of the fiber projections of `f`
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (k : g retract-of-map f) (y : B)
+  where
+
+  is-retract-of-map-fiber-retract-of-map :
+    is-retract-of-map
+      ( pr1)
+      ( pr1)
+      ( retract-of-fiber-retract-of-map f g k y)
+      ( retract-of-domain-retract-of-map f g k)
+  pr1 is-retract-of-map-fiber-retract-of-map = refl-htpy
+  pr1 (pr2 is-retract-of-map-fiber-retract-of-map) = refl-htpy
+  pr2 (pr2 is-retract-of-map-fiber-retract-of-map) (x , p) =
+    inv (ap-pr1-map-inv-fiber-ap-eq-fiber g _ (x , p) _)
+
+  retract-of-map-fiber-retract-of-map : pr1 retract-of-map pr1
+  pr1 retract-of-map-fiber-retract-of-map =
+    retract-of-fiber-retract-of-map f g k y
+  pr1 (pr2 retract-of-map-fiber-retract-of-map) =
+    retract-of-domain-retract-of-map f g k
+  pr2 (pr2 retract-of-map-fiber-retract-of-map) =
+    is-retract-of-map-fiber-retract-of-map
+```
+
+### If `f` has a section, then retracts of `f` have a section
+
+In fact, we only need the following data to show this:
+
+```text
+                 r
+            X ------> A
+            |         |
+            f    R    g
+            v         v
+  B ------> Y ------> B.
+       s'   H'   r'
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (r : X → A) (r' : B retract-of Y)
+  (R : coherence-square-maps r f g (retraction-retract-of r'))
+  (section-f : section f)
+  where
+
+  map-has-section-is-retract-of-has-section' : B → A
+  map-has-section-is-retract-of-has-section' =
+    r ∘ map-section f section-f ∘ section-retract-of r'
+
+  is-section-map-has-section-is-retract-of-has-section' :
+    g ∘ map-has-section-is-retract-of-has-section' ~ id
+  is-section-map-has-section-is-retract-of-has-section' =
+    ( inv-htpy R ·r (map-section f section-f ∘ section-retract-of r')) ∙h
+    ( ( retraction-retract-of r') ·l
+      ( is-section-map-section f section-f ·r section-retract-of r')) ∙h
+    ( is-retract-retract-of r')
+
+  has-section-is-retract-of-has-section' : section g
+  pr1 has-section-is-retract-of-has-section' =
+    map-has-section-is-retract-of-has-section'
+  pr2 has-section-is-retract-of-has-section' =
+    is-section-map-has-section-is-retract-of-has-section'
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (k : g retract-of-map f)
+  where
+
+  has-section-retract-of-has-section : section f → section g
+  has-section-retract-of-has-section =
+    has-section-is-retract-of-has-section' f g
+      ( retraction-of-domain-retract-of-map f g k)
+      ( retract-of-codomain-retract-of-map f g k)
+      ( coherence-retraction-retract-of-map f g k)
+```
+
+### If `f` has a retraction, then retracts of `f` have a retraction
+
+In fact, we only need the following data to show this:
+
+```text
+       s    H    r
+  A ------> X ------> A
+  |         |
+  g    S    f
+  v         v
+  B ------> Y.
+       s'
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (r : A retract-of X) (s' : B → Y)
+  (S : coherence-square-maps (section-retract-of r) g f s')
+  (retraction-f : retraction f)
+  where
+
+  map-has-retraction-is-retract-of-has-retraction' : B → A
+  map-has-retraction-is-retract-of-has-retraction' =
+    retraction-retract-of r ∘ map-retraction f retraction-f ∘ s'
+
+  is-retraction-map-has-retraction-is-retract-of-has-retraction' :
+    map-has-retraction-is-retract-of-has-retraction' ∘ g ~ id
+  is-retraction-map-has-retraction-is-retract-of-has-retraction' =
+    ( ( retraction-retract-of r ∘ map-retraction f retraction-f) ·l S) ∙h
+    ( ( retraction-retract-of r) ·l
+      ( is-retraction-map-retraction f retraction-f ·r section-retract-of r)) ∙h
+    ( is-retract-retract-of r)
+
+  has-retraction-is-retract-of-has-retraction' : retraction g
+  pr1 has-retraction-is-retract-of-has-retraction' =
+    map-has-retraction-is-retract-of-has-retraction'
+  pr2 has-retraction-is-retract-of-has-retraction' =
+    is-retraction-map-has-retraction-is-retract-of-has-retraction'
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (k : g retract-of-map f)
+  where
+
+  has-retraction-retract-of-has-retraction : retraction f → retraction g
+  has-retraction-retract-of-has-retraction =
+    has-retraction-is-retract-of-has-retraction' f g
+      ( retract-of-domain-retract-of-map f g k)
+      ( section-of-codomain-retract-of-map f g k)
+      ( coherence-section-retract-of-map f g k)
+```
+
+### Equivalences are closed under retracts of maps
+
+Note that the higher coherence of a retract of maps is not needed.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (r : A retract-of X) (r' : B retract-of Y)
+  (S : coherence-square-maps (section-retract-of r) g f (section-retract-of r'))
+  (R :
+    coherence-square-maps
+      ( retraction-retract-of r) f g (retraction-retract-of r'))
+  (is-equiv-f : is-equiv f)
+  where
+
+  is-equiv-is-retract-of-is-equiv' : is-equiv g
+  pr1 is-equiv-is-retract-of-is-equiv' =
+    has-section-is-retract-of-has-section' f g
+      ( retraction-retract-of r)
+      ( r')
+      ( R)
+      ( section-is-equiv is-equiv-f)
+  pr2 is-equiv-is-retract-of-is-equiv' =
+    has-retraction-is-retract-of-has-retraction' f g
+      ( r)
+      ( section-retract-of r')
+      ( S)
+      ( retraction-is-equiv is-equiv-f)
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : X → Y) (g : A → B) (k : g retract-of-map f) (is-equiv-f : is-equiv f)
+  where
+
+  is-equiv-retract-of-is-equiv : is-equiv g
+  pr1 is-equiv-retract-of-is-equiv =
+    has-section-retract-of-has-section f g k
+      ( section-is-equiv is-equiv-f)
+  pr2 is-equiv-retract-of-is-equiv =
+    has-retraction-retract-of-has-retraction f g k
+      ( retraction-is-equiv is-equiv-f)
+```
+
+## References
+
+1. Section 4.7 of Univalent Foundations Project, _Homotopy Type Theory –
+   Univalent Foundations of Mathematics_ (2013)
+   ([website](https://homotopytypetheory.org/book/),
+   [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
+
+## External links
+
+- [Retracts in arrow categories](https://ncatlab.org/nlab/show/retract#in_arrow_categories)
+  at nlab
+
+A wikidata identifier was not available for this concept.
diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
index 1c66c18e04..9d444b5566 100644
--- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
@@ -120,10 +120,10 @@ module _
   coherence-htpy-cocone-sequential-diagram c c' K =
     ( n : ℕ) →
     coherence-square-homotopies
-      ( coherence-triangle-cocone-sequential-diagram A c n)
-      ( K (succ-ℕ n) ·r map-sequential-diagram A n)
       ( K n)
+      ( coherence-triangle-cocone-sequential-diagram A c n)
       ( coherence-triangle-cocone-sequential-diagram A c' n)
+      ( K (succ-ℕ n) ·r map-sequential-diagram A n)
 
   htpy-cocone-sequential-diagram :
     ( c c' : cocone-sequential-diagram A X) → UU (l1 ⊔ l2)
diff --git a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
index 7adbaf5f53..36b52d62a1 100644
--- a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
@@ -177,10 +177,10 @@ module _
   coherence-htpy-sequential-diagram H =
     ( n : ℕ) →
     coherence-square-homotopies
-      ( naturality-map-hom-sequential-diagram B f n)
-      ( H (succ-ℕ n) ·r map-sequential-diagram A n)
       ( map-sequential-diagram B n ·l H n)
+      ( naturality-map-hom-sequential-diagram B f n)
       ( naturality-map-hom-sequential-diagram B g n)
+      ( H (succ-ℕ n) ·r map-sequential-diagram A n)
 
   htpy-hom-sequential-diagram : UU (l1 ⊔ l2)
   htpy-hom-sequential-diagram =