diff --git a/src/foundation/commuting-triangles-of-identifications.lagda.md b/src/foundation/commuting-triangles-of-identifications.lagda.md
index 540eeebbce..63fdd6e73b 100644
--- a/src/foundation/commuting-triangles-of-identifications.lagda.md
+++ b/src/foundation/commuting-triangles-of-identifications.lagda.md
@@ -8,8 +8,10 @@ module foundation.commuting-triangles-of-identifications where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.path-algebra
 open import foundation.universe-levels
 
+open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
@@ -47,3 +49,153 @@ module _
     (left : x ＝ z) (right : y ＝ z) (top : x ＝ y) → UU l
   coherence-triangle-identifications' left right top = (top ∙ right) ＝ left
 ```
+
+## Properties
+
+### Whiskering of triangles of identifications
+
+Given a commuting triangle of identifications
+
+```text
+       top
+    x ----- y
+     \     /
+ left \   / right
+       \ /
+        z     ,
+```
+
+we may consider three ways of attaching new identifications to it: prepending
+`p : u ＝ x` to the left, which gives us a commuting triangle
+
+```text
+         p ∙ top
+        u ----- y
+         \     /
+ p ∙ left \   / right
+           \ /
+            z     ,
+```
+
+or appending an identification `p : z ＝ u` to the right, which gives
+
+```text
+           top
+        u ----- y
+         \     /
+ left ∙ p \   / right ∙ p
+           \ /
+            z     ,
+```
+
+or splicing an identification `p : y ＝ u` and its inverse into the middle, to
+get
+
+```text
+     top ∙ p
+    u ----- y
+     \     /
+ left \   / p⁻¹ ∙ right
+       \ /
+        z     ,
+```
+
+which isn't formalized yet.
+
+Because concatenation of identifications is an equivalence, it follows that all
+of these transformations are equivalences.
+
+These lemmas are useful in proofs involving path algebra, because taking
+`equiv-right-whisk-triangle-identicications` as an example, it provides us with
+two maps: the forward direction states `(p ＝ q ∙ r) → (p ∙ s ＝ q ∙ (r ∙ s))`,
+which allows one to append an identification without needing to reassociate on
+the right, and the backwards direction conversely allows one to cancel out an
+identification in parentheses.
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z u : A}
+  (left : x ＝ z) (top : x ＝ y) {right : y ＝ z} (p : z ＝ u)
+  where
+
+  equiv-right-whisk-triangle-identifications :
+    ( coherence-triangle-identifications left right top) ≃
+    ( coherence-triangle-identifications (left ∙ p) (right ∙ p) top)
+  equiv-right-whisk-triangle-identifications =
+    ( equiv-concat-assoc' (left ∙ p) top right p) ∘e
+    ( equiv-identification-right-whisk p)
+
+  right-whisk-triangle-identifications :
+    coherence-triangle-identifications left right top →
+    coherence-triangle-identifications (left ∙ p) (right ∙ p) top
+  right-whisk-triangle-identifications =
+    map-equiv equiv-right-whisk-triangle-identifications
+
+  right-unwhisk-triangle-identifications :
+    coherence-triangle-identifications (left ∙ p) (right ∙ p) top →
+    coherence-triangle-identifications left right top
+  right-unwhisk-triangle-identifications =
+    map-inv-equiv equiv-right-whisk-triangle-identifications
+
+  equiv-right-whisk-triangle-identifications' :
+    ( coherence-triangle-identifications' left right top) ≃
+    ( coherence-triangle-identifications' (left ∙ p) (right ∙ p) top)
+  equiv-right-whisk-triangle-identifications' =
+    ( equiv-concat-assoc top right p (left ∙ p)) ∘e
+    ( equiv-identification-right-whisk p)
+
+  right-whisk-triangle-identifications' :
+    coherence-triangle-identifications' left right top →
+    coherence-triangle-identifications' (left ∙ p) (right ∙ p) top
+  right-whisk-triangle-identifications' =
+    map-equiv equiv-right-whisk-triangle-identifications'
+
+  right-unwhisk-triangle-identifications' :
+    coherence-triangle-identifications' (left ∙ p) (right ∙ p) top →
+    coherence-triangle-identifications' left right top
+  right-unwhisk-triangle-identifications' =
+    map-inv-equiv equiv-right-whisk-triangle-identifications'
+
+module _
+  {l : Level} {A : UU l} {x y z u : A}
+  (p : u ＝ x) {left : x ＝ z} {right : y ＝ z} {top : x ＝ y}
+  where
+
+  equiv-left-whisk-triangle-identifications :
+    ( coherence-triangle-identifications left right top) ≃
+    ( coherence-triangle-identifications (p ∙ left) right (p ∙ top))
+  equiv-left-whisk-triangle-identifications =
+    ( inv-equiv (equiv-concat-assoc' (p ∙ left) p top right)) ∘e
+    ( equiv-identification-left-whisk p)
+
+  left-whisk-triangle-identifications :
+    coherence-triangle-identifications left right top →
+    coherence-triangle-identifications (p ∙ left) right (p ∙ top)
+  left-whisk-triangle-identifications =
+    map-equiv equiv-left-whisk-triangle-identifications
+
+  left-unwhisk-triangle-identifications :
+    coherence-triangle-identifications (p ∙ left) right (p ∙ top) →
+    coherence-triangle-identifications left right top
+  left-unwhisk-triangle-identifications =
+    map-inv-equiv equiv-left-whisk-triangle-identifications
+
+  equiv-left-whisk-triangle-identifications' :
+    ( coherence-triangle-identifications' left right top) ≃
+    ( coherence-triangle-identifications' (p ∙ left) right (p ∙ top))
+  equiv-left-whisk-triangle-identifications' =
+    ( inv-equiv (equiv-concat-assoc p top right (p ∙ left))) ∘e
+    ( equiv-identification-left-whisk p)
+
+  left-whisk-triangle-identifications' :
+    coherence-triangle-identifications' left right top →
+    coherence-triangle-identifications' (p ∙ left) right (p ∙ top)
+  left-whisk-triangle-identifications' =
+    map-equiv equiv-left-whisk-triangle-identifications'
+
+  left-unwhisk-triangle-identifications' :
+    coherence-triangle-identifications' (p ∙ left) right (p ∙ top) →
+    coherence-triangle-identifications' left right top
+  left-unwhisk-triangle-identifications' =
+    map-inv-equiv equiv-left-whisk-triangle-identifications'
+```
diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md
index ba4348f969..08e151eb16 100644
--- a/src/foundation/functoriality-dependent-pair-types.lagda.md
+++ b/src/foundation/functoriality-dependent-pair-types.lagda.md
@@ -19,6 +19,7 @@ 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.commuting-triangles-of-maps
 open import foundation-core.dependent-identifications
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
@@ -375,6 +376,24 @@ module _
   coherence-square-maps-map-Σ-map-base H (a , p) = eq-pair-Σ (H a) refl
 ```
 
+#### `map-Σ-map-base` preserves commuting triangles of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} (S : X → UU l4)
+  (left : A → X) (right : B → X) (top : A → B)
+  where
+
+  coherence-triangle-maps-map-Σ-map-base :
+    (H : coherence-triangle-maps left right top) →
+    coherence-triangle-maps
+      ( map-Σ-map-base left S)
+      ( map-Σ-map-base right S)
+      ( map-Σ (S ∘ right) top (λ a → tr S (H a)))
+  coherence-triangle-maps-map-Σ-map-base H (a , _) = eq-pair-Σ (H a) refl
+```
+
 ### The action of `map-Σ-map-base` on identifications of the form `eq-pair-Σ` is given by the action on the base
 
 ```agda
diff --git a/src/foundation/morphisms-arrows.lagda.md b/src/foundation/morphisms-arrows.lagda.md
index 49084f0757..b0b4ed1604 100644
--- a/src/foundation/morphisms-arrows.lagda.md
+++ b/src/foundation/morphisms-arrows.lagda.md
@@ -10,9 +10,11 @@ module foundation.morphisms-arrows where
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-homotopies
 open import foundation.commuting-squares-of-identifications
+open import foundation.commuting-triangles-of-identifications
 open import foundation.dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopy-induction
+open import foundation.path-algebra
 open import foundation.structure-identity-principle
 open import foundation.universe-levels
 
@@ -163,7 +165,7 @@ module _
     coh-comp-hom-arrow
 ```
 
-### Homotopies of morphsims of arrows
+### Homotopies of morphisms of arrows
 
 A **homotopy of morphisms of arrows** from `(i , j , H)` to `(i' , j' , H')` is
 a triple `(I , J , K)` consisting of homotopies `I : i ~ i'` and `J : j ~ j'`
@@ -377,60 +379,36 @@ module _
       ( htpy-domain-left-whisker-htpy-hom-arrow)
       ( htpy-codomain-left-whisker-htpy-hom-arrow)
   coh-left-whisker-htpy-hom-arrow a =
-    ( inv
-      ( ap
-        ( concat _ _)
-        ( ap-comp h
-          ( map-domain-hom-arrow g h γ)
-          ( htpy-domain-htpy-hom-arrow f g α β H a)))) ∙
-    ( assoc
+    ( left-whisk-triangle-identifications'
       ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
-      ( coh-hom-arrow g h γ (map-domain-hom-arrow f g α a))
+      ( ( ap
+          ( coh-hom-arrow g h γ (map-domain-hom-arrow f g α a) ∙_)
+          ( inv
+            ( ap-comp h
+              ( map-domain-hom-arrow g h γ)
+              ( htpy-domain-htpy-hom-arrow f g α β H a)))) ∙
+        ( nat-htpy
+          ( coh-hom-arrow g h γ)
+          ( htpy-domain-htpy-hom-arrow f g α β H a)))) ∙
+    ( right-whisk-square-identification
       ( ap
-        ( h ∘ map-domain-hom-arrow g h γ)
-        ( htpy-domain-htpy-hom-arrow f g α β H a))) ∙
-    ( ap
-      ( concat
-        ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
-        ( h _))
-      ( nat-htpy
-        ( coh-hom-arrow g h γ)
-        ( htpy-domain-htpy-hom-arrow f g α β H a))) ∙
-    ( inv
-      ( assoc
-        ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
-        ( ap
-          ( map-codomain-hom-arrow g h γ ∘ g)
-          ( htpy-domain-htpy-hom-arrow f g α β H a))
-        ( coh-hom-arrow g h γ (map-domain-hom-arrow f g β a)))) ∙
-    ( ap
-      ( concat' _ (coh-hom-arrow g h γ (map-domain-hom-arrow f g β a)))
+        ( map-codomain-hom-arrow g h γ)
+        ( htpy-codomain-htpy-hom-arrow f g α β H (f a)))
+      ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
+      ( coh-hom-arrow g h γ (map-domain-hom-arrow f g β a))
       ( ( ap
-          ( concat
-            ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
-            ( _))
+          ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a) ∙_)
           ( ap-comp
             ( map-codomain-hom-arrow g h γ)
             ( g)
             ( htpy-domain-htpy-hom-arrow f g α β H a))) ∙
-        ( ( inv
-            ( ap-concat
-              ( map-codomain-hom-arrow g h γ)
-              ( coh-hom-arrow f g α a)
-              ( ap g (htpy-domain-htpy-hom-arrow f g α β H a)))) ∙
-          ( ap
-            ( ap (map-codomain-hom-arrow g h γ))
-            ( coh-htpy-hom-arrow f g α β H a)) ∙
-          ( ap-concat
-            ( map-codomain-hom-arrow g h γ)
-            ( htpy-codomain-htpy-hom-arrow f g α β H (f a))
-            ( coh-hom-arrow f g β a))))) ∙
-    ( assoc
-      ( ap
-        ( map-codomain-hom-arrow g h γ)
-        ( htpy-codomain-htpy-hom-arrow f g α β H (f a)))
-      ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g β a))
-      ( coh-hom-arrow g h γ (map-domain-hom-arrow f g β a)))
+        ( coherence-square-identifications-ap
+          ( map-codomain-hom-arrow g h γ)
+          ( htpy-codomain-htpy-hom-arrow f g α β H (f a))
+          ( coh-hom-arrow f g α a)
+          ( coh-hom-arrow f g β a)
+          ( ap g (htpy-domain-htpy-hom-arrow f g α β H a))
+          ( coh-htpy-hom-arrow f g α β H a))))
 
   left-whisker-htpy-hom-arrow :
     htpy-hom-arrow f h
diff --git a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md
index ebca7b4ac0..731454fb58 100644
--- a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md
+++ b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md
@@ -201,13 +201,17 @@ module _
   pr1 associative-Σ = map-associative-Σ
   pr2 associative-Σ = is-equiv-map-associative-Σ
 
+  abstract
+    is-equiv-map-inv-associative-Σ : is-equiv map-inv-associative-Σ
+    is-equiv-map-inv-associative-Σ =
+      is-equiv-is-invertible
+        map-associative-Σ
+        is-retraction-map-inv-associative-Σ
+        is-section-map-inv-associative-Σ
+
   inv-associative-Σ : Σ A (λ x → Σ (B x) (λ y → C (x , y))) ≃ Σ (Σ A B) C
   pr1 inv-associative-Σ = map-inv-associative-Σ
-  pr2 inv-associative-Σ =
-    is-equiv-is-invertible
-      map-associative-Σ
-      is-retraction-map-inv-associative-Σ
-      is-section-map-inv-associative-Σ
+  pr2 inv-associative-Σ = is-equiv-map-inv-associative-Σ
 ```
 
 ### Associativity, second formulation
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 0558cae6e7..47dbab16c5 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -48,6 +48,7 @@ open import synthetic-homotopy-theory.eckmann-hilton-argument public
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams public
 open import synthetic-homotopy-theory.flattening-lemma-coequalizers public
 open import synthetic-homotopy-theory.flattening-lemma-pushouts public
+open import synthetic-homotopy-theory.flattening-lemma-sequential-colimits public
 open import synthetic-homotopy-theory.free-loops public
 open import synthetic-homotopy-theory.functoriality-loop-spaces public
 open import synthetic-homotopy-theory.functoriality-sequential-colimits public
diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
index f8948f88e8..1b37a284fb 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
@@ -31,7 +31,7 @@ open import synthetic-homotopy-theory.universal-property-pushouts
 
 ## Idea
 
-The **flattening lemma** for
+The {{#concept "flattening lemma" Disambiguation="coequalizers"}} for
 [coequalizers](synthetic-homotopy-theory.coequalizers.md) states that
 coequalizers commute with
 [dependent pair types](foundation.dependent-pair-types.md). More precisely,
@@ -171,26 +171,18 @@ module _
             ( vertical-map-span-cocone-cofork f g)
             ( horizontal-map-span-cocone-cofork f g)
             ( cocone-codiagonal-cofork f g e))
-          ( λ where
-            (inl a , t) → refl
-            (inr a , t) → refl)
-          ( λ where
-            (inl a , t) → refl
-            (inr a , t) → refl)
+          ( ind-Σ (ind-coprod _ (ev-pair refl-htpy) (ev-pair refl-htpy)))
+          ( ind-Σ (ind-coprod _ (ev-pair refl-htpy) (ev-pair refl-htpy)))
           ( refl-htpy)
           ( refl-htpy)
           ( coherence-square-cocone-cofork
             ( bottom-map-cofork-flattening-lemma-coequalizer f g P e)
             ( top-map-cofork-flattening-lemma-coequalizer f g P e)
             ( cofork-flattening-lemma-coequalizer f g P e))
-          ( λ where
-            (inl a , t) → refl
-            (inr a , t) →
-              ( ap-id
-                ( eq-pair-Σ
-                  ( coherence-cofork f g e a)
-                  ( refl))) ∙
-              ( inv right-unit))
+          ( ind-Σ
+            ( ind-coprod _
+              ( ev-pair refl-htpy)
+              ( ev-pair (λ t → ap-id _ ∙ inv right-unit))))
           ( is-equiv-map-equiv
             ( right-distributive-Σ-coprod A A
               ( ( P) ∘
diff --git a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md
new file mode 100644
index 0000000000..0ad8516ee5
--- /dev/null
+++ b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md
@@ -0,0 +1,208 @@
+# The flattening lemma for sequential colimits
+
+```agda
+module synthetic-homotopy-theory.flattening-lemma-sequential-colimits where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
+open import synthetic-homotopy-theory.coforks
+open import synthetic-homotopy-theory.dependent-universal-property-sequential-colimits
+open import synthetic-homotopy-theory.flattening-lemma-coequalizers
+open import synthetic-homotopy-theory.sequential-diagrams
+open import synthetic-homotopy-theory.universal-property-coequalizers
+open import synthetic-homotopy-theory.universal-property-sequential-colimits
+```
+
+</details>
+
+## Idea
+
+The {{#concept "flattening lemma" Disambiguation="sequential colimits"}} for
+[sequential colimits](synthetic-homotopy-theory.universal-property-sequential-colimits.md)
+states that sequential colimits commute with
+[dependent pair types](foundation.dependent-pair-types.md). Specifically, given
+a [cocone](synthetic-homotopy-theory.cocones-under-sequential-diagrams.md)
+
+```text
+  A₀ ---> A₁ ---> A₂ ---> ⋯ ---> X
+```
+
+with the universal property of sequential colimits, and a family `P : X → 𝓤`, we
+obtain a cocone
+
+```text
+  Σ (a : A₀) P(i₀ a) ---> Σ (a : A₁) P(i₁ a) ---> ⋯ ---> Σ (x : X) P(x) ,
+```
+
+which is again a sequential colimit.
+
+The result may be read as
+`colimₙ (Σ (a : Aₙ) P(iₙ a)) ≃ Σ (a : colimₙ Aₙ) P(a)`.
+
+## Definitions
+
+### The sequential diagram for the flattening lemma
+
+```agda
+module _
+  { l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2}
+  ( c : cocone-sequential-diagram A X)
+  ( P : X → UU l3)
+  where
+
+  sequential-diagram-flattening-lemma : sequential-diagram (l1 ⊔ l3)
+  pr1 sequential-diagram-flattening-lemma n =
+    Σ ( family-sequential-diagram A n)
+      ( P ∘ map-cocone-sequential-diagram A c n)
+  pr2 sequential-diagram-flattening-lemma n =
+    map-Σ
+      ( P ∘ map-cocone-sequential-diagram A c (succ-ℕ n))
+      ( map-sequential-diagram A n)
+      ( λ a → tr P (coherence-triangle-cocone-sequential-diagram A c n a))
+
+  cocone-sequential-diagram-flattening-lemma :
+    cocone-sequential-diagram sequential-diagram-flattening-lemma (Σ X P)
+  pr1 cocone-sequential-diagram-flattening-lemma n =
+    map-Σ-map-base (map-cocone-sequential-diagram A c n) P
+  pr2 cocone-sequential-diagram-flattening-lemma n =
+    coherence-triangle-maps-map-Σ-map-base P
+      ( map-cocone-sequential-diagram A c n)
+      ( map-cocone-sequential-diagram A c (succ-ℕ n))
+      ( map-sequential-diagram A n)
+      ( coherence-triangle-cocone-sequential-diagram A c n)
+```
+
+### Statement of the flattening lemma
+
+```agda
+module _
+  { l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2}
+  ( c : cocone-sequential-diagram A X)
+  ( P : X → UU l3)
+  where
+
+  statement-flattening-lemma-sequential-colimit : UUω
+  statement-flattening-lemma-sequential-colimit =
+    dependent-universal-property-sequential-colimit A c →
+    universal-property-sequential-colimit
+      ( sequential-diagram-flattening-lemma c P)
+      ( cocone-sequential-diagram-flattening-lemma c P)
+```
+
+## Properties
+
+### Proof of the flattening lemma
+
+Similarly to the proof of the
+[flattening lemma for coequalizers](synthetic-homotopy-theory.flattening-lemma-coequalizers.md),
+this proof uses the fact that sequential colimits correspond to certain
+coequalizers, which is recorded in
+[`synthetic-homotopy-theory.dependent-universal-property-sequential-colimits`](synthetic-homotopy-theory.dependent-universal-property-sequential-colimits.md),
+so it suffices to invoke the flattening lemma for coequalizers.
+
+**Proof:** The diagram we construct is
+
+```text
+                               ------->
+  Σ (n : ℕ) Σ (a : Aₙ) P(iₙ a) -------> Σ (n : ℕ) Σ (a : Aₙ) P(iₙ a) ----> Σ (x : X) P(x)
+             |                                     |                            |
+ inv-assoc-Σ | ≃                       inv-assoc-Σ | ≃                       id | ≃
+             |                                     |                            |
+             V                --------->           V                            V
+   Σ ((n, a) : Σ ℕ A) P(iₙ a) ---------> Σ ((n, a) : Σ ℕ A) P(iₙ a) -----> Σ (x : X) P(x) ,
+```
+
+where the top is the cofork corresponding to the cocone for the flattening
+lemma, and the bottom is the cofork obtained by flattening the cofork
+corresponding to the given base cocone.
+
+By assumption, the original cocone is a sequential colimit, which implies that
+its corresponding cofork is a coequalizer. The flattening lemma for coequalizers
+implies that the bottom cofork is a coequalizer, which in turn implies that the
+top cofork is a coequalizer, hence the flattening of the original cocone is a
+sequential colimit.
+
+```agda
+module _
+  { l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2}
+  ( c : cocone-sequential-diagram A X)
+  ( P : X → UU l3)
+  where
+
+  abstract
+    flattening-lemma-sequential-colimit :
+      statement-flattening-lemma-sequential-colimit c P
+    flattening-lemma-sequential-colimit dup-c =
+      universal-property-sequential-colimit-universal-property-coequalizer
+        ( sequential-diagram-flattening-lemma c P)
+        ( cocone-sequential-diagram-flattening-lemma c P)
+        ( universal-property-coequalizer-top-universal-property-coequalizer-bottom-hom-arrow-is-equiv
+          ( map-inv-associative-Σ ℕ
+            ( family-sequential-diagram A)
+            ( P ∘ ind-Σ (map-cocone-sequential-diagram A c)))
+          ( map-inv-associative-Σ ℕ
+            ( family-sequential-diagram A)
+            ( P ∘ ind-Σ (map-cocone-sequential-diagram A c)))
+          ( id)
+          ( ( bottom-map-cofork-cocone-sequential-diagram
+              ( sequential-diagram-flattening-lemma c P)) ,
+            ( bottom-map-cofork-flattening-lemma-coequalizer _ _
+              ( P)
+              ( cofork-cocone-sequential-diagram A c)) ,
+            ( refl-htpy))
+          ( ( top-map-cofork-cocone-sequential-diagram
+              ( sequential-diagram-flattening-lemma c P)) ,
+            ( top-map-cofork-flattening-lemma-coequalizer _ _
+              ( P)
+              ( cofork-cocone-sequential-diagram A c)) ,
+            ( refl-htpy))
+          ( ( map-cofork _ _
+              ( cofork-cocone-sequential-diagram
+                ( sequential-diagram-flattening-lemma c P)
+                ( cocone-sequential-diagram-flattening-lemma c P))) ,
+            ( map-cofork _ _
+              ( cofork-flattening-lemma-coequalizer _ _ P
+                ( cofork-cocone-sequential-diagram A c))) ,
+            ( refl-htpy))
+          ( ind-Σ
+            ( coherence-triangle-cocone-sequential-diagram
+              ( sequential-diagram-flattening-lemma c P)
+              ( cocone-sequential-diagram-flattening-lemma c P)) ,
+            ( coherence-cofork _ _
+              ( cofork-flattening-lemma-coequalizer _ _ P
+                ( cofork-cocone-sequential-diagram A c))) ,
+            ( ind-Σ (λ n → ind-Σ (λ a p → ap-id _ ∙ inv right-unit))))
+          ( is-equiv-map-equiv
+            ( inv-associative-Σ ℕ
+              ( family-sequential-diagram A)
+              ( P ∘ ind-Σ (map-cocone-sequential-diagram A c))))
+          ( is-equiv-map-inv-associative-Σ ℕ
+            ( family-sequential-diagram A)
+            ( P ∘ ind-Σ (map-cocone-sequential-diagram A c)))
+          ( is-equiv-id)
+          ( flattening-lemma-coequalizer
+            ( bottom-map-cofork-cocone-sequential-diagram A)
+            ( top-map-cofork-cocone-sequential-diagram A)
+            ( P)
+            ( cofork-cocone-sequential-diagram A c)
+            ( dependent-universal-property-coequalizer-dependent-universal-property-sequential-colimit
+              ( A)
+              ( c)
+              ( dup-c))))
+```
diff --git a/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md b/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
index 191bcc9e4e..db1a3035d3 100644
--- a/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
@@ -9,10 +9,15 @@ module synthetic-homotopy-theory.universal-property-coequalizers where
 ```agda
 open import foundation.contractible-maps
 open import foundation.contractible-types
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.fibers-of-maps
+open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.morphisms-arrows
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.cocones-under-spans
@@ -33,7 +38,7 @@ postcomposition map
 cofork-map : (X → Y) → cofork Y
 ```
 
-is an equivalence.
+is an [equivalence](foundation.equivalences.md).
 
 ## Definitions
 
@@ -149,3 +154,135 @@ module _
       ( is-equiv-cofork-cocone-codiagonal f g)
       ( up-coequalizer Y)
 ```
+
+### In a cofork on equivalences in the category of arrows, the domain cofork is a coequalizer if and only if the codomain cofork is a coequalizer
+
+In other words, given two coforks connected vertically with equivalences, as in
+the following diagram:
+
+```text
+    ----->
+  A -----> B -----> C
+  |        |        |
+ ≃|        |≃       |≃
+  V  ----> V        V
+  A' ----> B' ----> C' ,
+```
+
+equipped with [commuting squares](foundation.commuting-squares-of-maps.md) for
+the three small squares, and a coherence datum expressing that the right square
+coequalizes the left squares in the category of arrows, we have that the top
+cofork is a coequalizer if and only if the bottom cofork is a coequalizer.
+
+```agda
+module _
+  { l1 l2 l3 l4 l5 l6 : Level}
+  { A : UU l1} {B : UU l2} {C : UU l3}
+  { A' : UU l4} {B' : UU l5} {C' : UU l6}
+  ( hA : A → A') (hB : B → B') (hC : C → C')
+  ( f : hom-arrow hA hB) (g : hom-arrow hA hB) (c : hom-arrow hB hC)
+  ( H :
+    htpy-hom-arrow hA hC
+      ( comp-hom-arrow hA hB hC c f)
+      ( comp-hom-arrow hA hB hC c g))
+  ( is-equiv-hA : is-equiv hA) (is-equiv-hB : is-equiv hB)
+  ( is-equiv-hC : is-equiv hC)
+  where
+
+  top-cofork-hom-arrow :
+    cofork (map-domain-hom-arrow hA hB f) (map-domain-hom-arrow hA hB g) C
+  pr1 top-cofork-hom-arrow = map-domain-hom-arrow hB hC c
+  pr2 top-cofork-hom-arrow = htpy-domain-htpy-hom-arrow hA hC _ _ H
+
+  bottom-cofork-hom-arrow :
+    cofork (map-codomain-hom-arrow hA hB f) (map-codomain-hom-arrow hA hB g) C'
+  pr1 bottom-cofork-hom-arrow = map-codomain-hom-arrow hB hC c
+  pr2 bottom-cofork-hom-arrow = htpy-codomain-htpy-hom-arrow hA hC _ _ H
+
+  universal-property-coequalizer-top-universal-property-coequalizer-bottom-hom-arrow-is-equiv :
+    ({l : Level} →
+      universal-property-coequalizer l _ _ bottom-cofork-hom-arrow) →
+    ({l : Level} → universal-property-coequalizer l _ _ top-cofork-hom-arrow)
+  universal-property-coequalizer-top-universal-property-coequalizer-bottom-hom-arrow-is-equiv
+    ( up-c') =
+    universal-property-coequalizer-universal-property-pushout _ _
+      ( top-cofork-hom-arrow)
+      ( universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv
+        ( vertical-map-span-cocone-cofork
+          ( map-codomain-hom-arrow hA hB f)
+          ( map-codomain-hom-arrow hA hB g))
+        ( horizontal-map-span-cocone-cofork
+          ( map-codomain-hom-arrow hA hB f)
+          ( map-codomain-hom-arrow hA hB g))
+        ( horizontal-map-cocone-cofork _ _ bottom-cofork-hom-arrow)
+        ( vertical-map-cocone-cofork _ _ bottom-cofork-hom-arrow)
+        ( vertical-map-span-cocone-cofork
+          ( map-domain-hom-arrow hA hB f)
+          ( map-domain-hom-arrow hA hB g))
+        ( horizontal-map-span-cocone-cofork
+          ( map-domain-hom-arrow hA hB f)
+          ( map-domain-hom-arrow hA hB g))
+        ( horizontal-map-cocone-cofork _ _ top-cofork-hom-arrow)
+        ( vertical-map-cocone-cofork _ _ top-cofork-hom-arrow)
+        ( map-coprod hA hA)
+        ( hA)
+        ( hB)
+        ( hC)
+        ( coherence-square-cocone-cofork _ _ top-cofork-hom-arrow)
+        ( ind-coprod _ refl-htpy refl-htpy)
+        ( ind-coprod _ (coh-hom-arrow hA hB f) (coh-hom-arrow hA hB g))
+        ( coh-comp-hom-arrow hA hB hC c f)
+        ( coh-hom-arrow hB hC c)
+        ( coherence-square-cocone-cofork _ _ bottom-cofork-hom-arrow)
+        ( ind-coprod _ (λ _ → right-unit) (coh-htpy-hom-arrow hA hC _ _ H))
+        ( is-equiv-map-coprod is-equiv-hA is-equiv-hA)
+        ( is-equiv-hA)
+        ( is-equiv-hB)
+        ( is-equiv-hC)
+        ( universal-property-pushout-universal-property-coequalizer _ _
+          ( bottom-cofork-hom-arrow)
+          ( up-c')))
+
+  universal-property-coequalizer-bottom-universal-property-coequalizer-top-hom-arrow-is-equiv :
+    ({l : Level} → universal-property-coequalizer l _ _ top-cofork-hom-arrow) →
+    ({l : Level} → universal-property-coequalizer l _ _ bottom-cofork-hom-arrow)
+  universal-property-coequalizer-bottom-universal-property-coequalizer-top-hom-arrow-is-equiv
+    ( up-c) =
+    universal-property-coequalizer-universal-property-pushout _ _
+      ( bottom-cofork-hom-arrow)
+      ( universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv
+        ( vertical-map-span-cocone-cofork
+          ( map-codomain-hom-arrow hA hB f)
+          ( map-codomain-hom-arrow hA hB g))
+        ( horizontal-map-span-cocone-cofork
+          ( map-codomain-hom-arrow hA hB f)
+          ( map-codomain-hom-arrow hA hB g))
+        ( horizontal-map-cocone-cofork _ _ bottom-cofork-hom-arrow)
+        ( vertical-map-cocone-cofork _ _ bottom-cofork-hom-arrow)
+        ( vertical-map-span-cocone-cofork
+          ( map-domain-hom-arrow hA hB f)
+          ( map-domain-hom-arrow hA hB g))
+        ( horizontal-map-span-cocone-cofork
+          ( map-domain-hom-arrow hA hB f)
+          ( map-domain-hom-arrow hA hB g))
+        ( horizontal-map-cocone-cofork _ _ top-cofork-hom-arrow)
+        ( vertical-map-cocone-cofork _ _ top-cofork-hom-arrow)
+        ( map-coprod hA hA)
+        ( hA)
+        ( hB)
+        ( hC)
+        ( coherence-square-cocone-cofork _ _ top-cofork-hom-arrow)
+        ( ind-coprod _ refl-htpy refl-htpy)
+        ( ind-coprod _ (coh-hom-arrow hA hB f) (coh-hom-arrow hA hB g))
+        ( coh-comp-hom-arrow hA hB hC c f)
+        ( coh-hom-arrow hB hC c)
+        ( coherence-square-cocone-cofork _ _ bottom-cofork-hom-arrow)
+        ( ind-coprod _ (λ _ → right-unit) (coh-htpy-hom-arrow hA hC _ _ H))
+        ( is-equiv-map-coprod is-equiv-hA is-equiv-hA)
+        ( is-equiv-hA)
+        ( is-equiv-hB)
+        ( is-equiv-hC)
+        ( universal-property-pushout-universal-property-coequalizer _ _
+          ( top-cofork-hom-arrow)
+          ( up-c)))
+```