diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md
index 8291e2bc800..5d5fe0818ea 100644
--- a/src/foundation-core.lagda.md
+++ b/src/foundation-core.lagda.md
@@ -39,6 +39,8 @@ open import foundation-core.injective-maps public
 open import foundation-core.invertible-maps public
 open import foundation-core.iterating-functions public
 open import foundation-core.negation public
+open import foundation-core.operations-cospan-diagrams public
+open import foundation-core.operations-cospans public
 open import foundation-core.operations-span-diagrams public
 open import foundation-core.operations-spans public
 open import foundation-core.path-split-maps public
diff --git a/src/foundation-core/operations-cospan-diagrams.lagda.md b/src/foundation-core/operations-cospan-diagrams.lagda.md
new file mode 100644
index 00000000000..7778dc6a38a
--- /dev/null
+++ b/src/foundation-core/operations-cospan-diagrams.lagda.md
@@ -0,0 +1,266 @@
+# Operations on cospan diagrams
+
+```agda
+module foundation-core.operations-cospan-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cospan-diagrams
+open import foundation.cospans
+open import foundation.dependent-pair-types
+open import foundation.morphisms-arrows
+open import foundation.operations-cospans
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+This file contains some operations on
+[cospan diagrams](foundation.cospan-diagrams.md) that produce new cospan
+diagrams from given cospan diagrams and possibly other data.
+
+## Definitions
+
+### Concatenating cospan diagrams and maps on both sides
+
+Consider a [cospan diagram](foundation.cospan-diagrams.md) `𝒮` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and maps `i : A' → A` and `j : B' → B`. The
+{{#concept "concatenation-cospan-diagram" Disambiguation="cospan diagram" Agda=concat-cospan-diagram}}
+of `𝒮`, `i`, and `j` is the cospan diagram
+
+```text
+      f ∘ i     g ∘ j
+  A' ------> S <------ B'.
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  where
+
+  concat-cospan-diagram :
+    (𝒮 : cospan-diagram l1 l2 l3)
+    {A' : UU l4} (i : A' → domain-cospan-diagram 𝒮)
+    {B' : UU l5} (j : B' → codomain-cospan-diagram 𝒮) →
+    cospan-diagram l4 l5 l3
+  pr1 (concat-cospan-diagram 𝒮 {A'} i {B'} j) =
+    A'
+  pr1 (pr2 (concat-cospan-diagram 𝒮 {A'} i {B'} j)) =
+    B'
+  pr2 (pr2 (concat-cospan-diagram 𝒮 {A'} i {B'} j)) =
+    concat-cospan (cospan-cospan-diagram 𝒮) i j
+```
+
+### Concatenating cospan diagrams and maps on the left
+
+Consider a [cospan diagram](foundation.cospan-diagrams.md) `𝒮` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a map `i : A' → A`. The
+{{#concept "left concatenation" Disambiguation="cospan diagram" Agda=left-concat-cospan-diagram}}
+of `𝒮` and `i` is the cospan diagram
+
+```text
+      f ∘ i       g
+  A' ------> S <------ B.
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  where
+
+  left-concat-cospan-diagram :
+    (𝒮 : cospan-diagram l1 l2 l3) {A' : UU l4} →
+    (A' → domain-cospan-diagram 𝒮) → cospan-diagram l4 l2 l3
+  left-concat-cospan-diagram 𝒮 f = concat-cospan-diagram 𝒮 f id
+```
+
+### Concatenating cospan diagrams and maps on the right
+
+Consider a [cospan diagram](foundation.cospan-diagrams.md) `𝒮` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a map `j : B' → B`. The
+{{#concept "right concatenation" Disambiguation="cospan diagram" Agda=right-concat-cospan-diagram}}
+of `𝒮` by `j` is the cospan diagram
+
+```text
+        f       g ∘ j
+  A' ------> S <------ B'.
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  where
+
+  right-concat-cospan-diagram :
+    (𝒮 : cospan-diagram l1 l2 l3) {B' : UU l4} →
+    (B' → codomain-cospan-diagram 𝒮) → cospan-diagram l1 l4 l3
+  right-concat-cospan-diagram 𝒮 g = concat-cospan-diagram 𝒮 id g
+```
+
+### Concatenation of cospan diagrams and morphisms of arrows on the left
+
+Consider a cospan diagram `𝒮` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow f' f`
+as indicated in the diagram
+
+```text
+          f         g
+     A ------> S <------ B.
+     |         |
+  h₀ |         | h₁
+     ∨         ∨
+     A' -----> S'
+          f'
+```
+
+Then we obtain a cospan diagram `A' --> S' <-- B`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (𝒮 : cospan-diagram l1 l2 l3)
+  {S' : UU l4} {A' : UU l5} (f' : A' → S')
+  (h : hom-arrow (left-map-cospan-diagram 𝒮) f')
+  where
+
+  domain-left-concat-hom-arrow-cospan-diagram : UU l5
+  domain-left-concat-hom-arrow-cospan-diagram = A'
+
+  codomain-left-concat-hom-arrow-cospan-diagram : UU l2
+  codomain-left-concat-hom-arrow-cospan-diagram = codomain-cospan-diagram 𝒮
+
+  cospan-left-concat-hom-arrow-cospan-diagram :
+    cospan l4
+      ( domain-left-concat-hom-arrow-cospan-diagram)
+      ( codomain-left-concat-hom-arrow-cospan-diagram)
+  cospan-left-concat-hom-arrow-cospan-diagram =
+    left-concat-hom-arrow-cospan
+      ( cospan-cospan-diagram 𝒮)
+      ( f')
+      ( h)
+
+  left-concat-hom-arrow-cospan-diagram : cospan-diagram l5 l2 l4
+  pr1 left-concat-hom-arrow-cospan-diagram =
+    domain-left-concat-hom-arrow-cospan-diagram
+  pr1 (pr2 left-concat-hom-arrow-cospan-diagram) =
+    codomain-left-concat-hom-arrow-cospan-diagram
+  pr2 (pr2 left-concat-hom-arrow-cospan-diagram) =
+    cospan-left-concat-hom-arrow-cospan-diagram
+
+  cospanning-type-left-concat-hom-arrow-cospan-diagram : UU l4
+  cospanning-type-left-concat-hom-arrow-cospan-diagram =
+    cospanning-type-cospan-diagram left-concat-hom-arrow-cospan-diagram
+
+  left-map-left-concat-hom-arrow-cospan-diagram :
+    domain-left-concat-hom-arrow-cospan-diagram →
+    cospanning-type-left-concat-hom-arrow-cospan-diagram
+  left-map-left-concat-hom-arrow-cospan-diagram =
+    left-map-cospan-diagram left-concat-hom-arrow-cospan-diagram
+
+  right-map-left-concat-hom-arrow-cospan-diagram :
+    codomain-left-concat-hom-arrow-cospan-diagram →
+    cospanning-type-left-concat-hom-arrow-cospan-diagram
+  right-map-left-concat-hom-arrow-cospan-diagram =
+    right-map-cospan-diagram left-concat-hom-arrow-cospan-diagram
+```
+
+### Concatenation of cospan diagrams and morphisms of arrows on the right
+
+Consider a cospan diagram `𝒮` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g`
+as indicated in the diagram
+
+```text
+       f         g
+  A ------> S <------ B.
+            |         |
+         h₀ |         | h₁
+            ∨         ∨
+            S' <----- B'
+                 g'
+```
+
+Then we obtain a cospan diagram `A --> S' <-- B'`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (𝒮 : cospan-diagram l1 l2 l3)
+  {S' : UU l4} {B' : UU l5} (g' : B' → S')
+  (h : hom-arrow (right-map-cospan-diagram 𝒮) g')
+  where
+
+  domain-right-concat-hom-arrow-cospan-diagram : UU l1
+  domain-right-concat-hom-arrow-cospan-diagram = domain-cospan-diagram 𝒮
+
+  codomain-right-concat-hom-arrow-cospan-diagram : UU l5
+  codomain-right-concat-hom-arrow-cospan-diagram = B'
+
+  cospan-right-concat-hom-arrow-cospan-diagram :
+    cospan l4
+      ( domain-right-concat-hom-arrow-cospan-diagram)
+      ( codomain-right-concat-hom-arrow-cospan-diagram)
+  cospan-right-concat-hom-arrow-cospan-diagram =
+    right-concat-hom-arrow-cospan
+      ( cospan-cospan-diagram 𝒮)
+      ( g')
+      ( h)
+
+  right-concat-hom-arrow-cospan-diagram : cospan-diagram l1 l5 l4
+  pr1 right-concat-hom-arrow-cospan-diagram =
+    domain-right-concat-hom-arrow-cospan-diagram
+  pr1 (pr2 right-concat-hom-arrow-cospan-diagram) =
+    codomain-right-concat-hom-arrow-cospan-diagram
+  pr2 (pr2 right-concat-hom-arrow-cospan-diagram) =
+    cospan-right-concat-hom-arrow-cospan-diagram
+
+  cospanning-type-right-concat-hom-arrow-cospan-diagram : UU l4
+  cospanning-type-right-concat-hom-arrow-cospan-diagram =
+    cospanning-type-cospan-diagram right-concat-hom-arrow-cospan-diagram
+
+  left-map-right-concat-hom-arrow-cospan-diagram :
+    domain-right-concat-hom-arrow-cospan-diagram →
+    cospanning-type-right-concat-hom-arrow-cospan-diagram
+  left-map-right-concat-hom-arrow-cospan-diagram =
+    left-map-cospan-diagram right-concat-hom-arrow-cospan-diagram
+
+  right-map-right-concat-hom-arrow-cospan-diagram :
+    codomain-right-concat-hom-arrow-cospan-diagram →
+    cospanning-type-right-concat-hom-arrow-cospan-diagram
+  right-map-right-concat-hom-arrow-cospan-diagram =
+    right-map-cospan-diagram right-concat-hom-arrow-cospan-diagram
+```
diff --git a/src/foundation-core/operations-cospans.lagda.md b/src/foundation-core/operations-cospans.lagda.md
new file mode 100644
index 00000000000..4b5c1f7ae52
--- /dev/null
+++ b/src/foundation-core/operations-cospans.lagda.md
@@ -0,0 +1,219 @@
+# Operations on cospans
+
+```agda
+module foundation-core.operations-cospans where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cospans
+open import foundation.dependent-pair-types
+open import foundation.morphisms-arrows
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+This file contains some operations on [cospans](foundation.cospans.md) that
+produce new cospans from given cospans and possibly other data.
+
+## Definitions
+
+### Concatenating cospans and maps on both sides
+
+Consider a [cospan](foundation.cospans.md) `s` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and maps `i : A' → A` and `j : B' → B`. The
+{{#concept "concatenation cospan" Disambiguation="cospan" Agda=concat-cospan}}
+of `i`, `s`, and `j` is the cospan
+
+```text
+      f ∘ i     g ∘ j
+  A' ------> S <------ B.
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {A' : UU l2}
+  {B : UU l3} {B' : UU l4}
+  where
+
+  concat-cospan : cospan l5 A B → (A' → A) → (B' → B) → cospan l5 A' B'
+  pr1 (concat-cospan s i j) = cospanning-type-cospan s
+  pr1 (pr2 (concat-cospan s i j)) = left-map-cospan s ∘ i
+  pr2 (pr2 (concat-cospan s i j)) = right-map-cospan s ∘ j
+```
+
+### Concatenating cospans and maps on the left
+
+Consider a [cospan](foundation.cospans.md) `s` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a map `i : A' → A`. The
+{{#concept "left concatenation" Disambiguation="cospan" Agda=left-concat-cospan}}
+of `s` by `i` is the cospan
+
+```text
+      f ∘ i       g
+  A' ------> S <------ B.
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {A' : UU l2} {B : UU l3}
+  where
+
+  left-concat-cospan : cospan l4 A B → (A' → A) → cospan l4 A' B
+  left-concat-cospan s f = concat-cospan s f id
+```
+
+### Concatenating cospans and maps on the right
+
+Consider a [cospan](foundation.cospans.md) `s` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a map `j : B' → B`. The
+{{#concept "right concatenation" Disambiguation="cospan" Agda=right-concat-cospan}}
+of `s` by `j` is the cospan
+
+```text
+        f       g ∘ j
+  A' ------> S <------ B.
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1}
+  {B : UU l3} {B' : UU l4}
+  where
+
+  right-concat-cospan : cospan l4 A B → (B' → B) → cospan l4 A B'
+  right-concat-cospan s g = concat-cospan s id g
+```
+
+### Concatenating cospans and morphisms of arrows on the left
+
+Consider a cospan `s` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow f f'`
+as indicated in the diagram
+
+```text
+          f         g
+     A ------> S <------ B.
+     |         |
+  h₀ |         | h₁
+     ∨         ∨
+     A' -----> S'
+          f'
+```
+
+Then we obtain a cospan `A' --> S' <-- B`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} (s : cospan l3 A B)
+  {S' : UU l4} {A' : UU l5} (f' : A' → S')
+  (h : hom-arrow (left-map-cospan s) f')
+  where
+
+  cospanning-type-left-concat-hom-arrow-cospan : UU l4
+  cospanning-type-left-concat-hom-arrow-cospan = S'
+
+  left-map-left-concat-hom-arrow-cospan :
+    A' → cospanning-type-left-concat-hom-arrow-cospan
+  left-map-left-concat-hom-arrow-cospan = f'
+
+  right-map-left-concat-hom-arrow-cospan :
+    B → cospanning-type-left-concat-hom-arrow-cospan
+  right-map-left-concat-hom-arrow-cospan =
+    map-codomain-hom-arrow (left-map-cospan s) f' h ∘ right-map-cospan s
+
+  left-concat-hom-arrow-cospan : cospan l4 A' B
+  pr1 left-concat-hom-arrow-cospan =
+    cospanning-type-left-concat-hom-arrow-cospan
+  pr1 (pr2 left-concat-hom-arrow-cospan) =
+    left-map-left-concat-hom-arrow-cospan
+  pr2 (pr2 left-concat-hom-arrow-cospan) =
+    right-map-left-concat-hom-arrow-cospan
+```
+
+### Concatenating cospans and morphisms of arrows on the right
+
+Consider a cospan `s` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g`
+as indicated in the diagram
+
+```text
+       f         g
+  A ------> S <------ B
+            |         |
+         h₀ |         | h₁
+            ∨         ∨
+            S' -----> B'.
+                 g'
+```
+
+Then we obtain a cospan `A --> S' <-- B'`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2}
+  (s : cospan l3 A B)
+  {S' : UU l4} {B' : UU l5} (g' : B' → S')
+  (h : hom-arrow (right-map-cospan s) g')
+  where
+
+  cospanning-type-right-concat-hom-arrow-cospan : UU l4
+  cospanning-type-right-concat-hom-arrow-cospan = S'
+
+  left-map-right-concat-hom-arrow-cospan :
+    A → cospanning-type-right-concat-hom-arrow-cospan
+  left-map-right-concat-hom-arrow-cospan =
+    map-codomain-hom-arrow (right-map-cospan s) g' h ∘ left-map-cospan s
+
+  right-map-right-concat-hom-arrow-cospan :
+    B' → cospanning-type-right-concat-hom-arrow-cospan
+  right-map-right-concat-hom-arrow-cospan = g'
+
+  right-concat-hom-arrow-cospan : cospan l4 A B'
+  pr1 right-concat-hom-arrow-cospan =
+    cospanning-type-right-concat-hom-arrow-cospan
+  pr1 (pr2 right-concat-hom-arrow-cospan) =
+    left-map-right-concat-hom-arrow-cospan
+  pr2 (pr2 right-concat-hom-arrow-cospan) =
+    right-map-right-concat-hom-arrow-cospan
+```
diff --git a/src/foundation-core/operations-span-diagrams.lagda.md b/src/foundation-core/operations-span-diagrams.lagda.md
index 78b68e8722c..f54aa595a5e 100644
--- a/src/foundation-core/operations-span-diagrams.lagda.md
+++ b/src/foundation-core/operations-span-diagrams.lagda.md
@@ -52,15 +52,15 @@ module _
 
   concat-span-diagram :
     (𝒮 : span-diagram l1 l2 l3)
-    {A' : UU l4} (f : domain-span-diagram 𝒮 → A')
-    {B' : UU l5} (g : codomain-span-diagram 𝒮 → B') →
+    {A' : UU l4} (i : domain-span-diagram 𝒮 → A')
+    {B' : UU l5} (j : codomain-span-diagram 𝒮 → B') →
     span-diagram l4 l5 l3
-  pr1 (concat-span-diagram 𝒮 {A'} f {B'} g) =
+  pr1 (concat-span-diagram 𝒮 {A'} i {B'} j) =
     A'
-  pr1 (pr2 (concat-span-diagram 𝒮 {A'} f {B'} g)) =
+  pr1 (pr2 (concat-span-diagram 𝒮 {A'} i {B'} j)) =
     B'
-  pr2 (pr2 (concat-span-diagram 𝒮 {A'} f {B'} g)) =
-    concat-span (span-span-diagram 𝒮) f g
+  pr2 (pr2 (concat-span-diagram 𝒮 {A'} i {B'} j)) =
+    concat-span (span-span-diagram 𝒮) i j
 ```
 
 ### Concatenating span diagrams and maps on the left
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 931de9244e3..90673604884 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -172,6 +172,7 @@ open import foundation.equality-coproduct-types public
 open import foundation.equality-dependent-function-types public
 open import foundation.equality-dependent-pair-types public
 open import foundation.equality-fibers-of-maps public
+open import foundation.equality-of-equality-cartesian-product-types public
 open import foundation.equality-truncation-levels public
 open import foundation.equivalence-classes public
 open import foundation.equivalence-extensionality public
@@ -180,8 +181,10 @@ open import foundation.equivalence-injective-type-families public
 open import foundation.equivalence-relations public
 open import foundation.equivalences public
 open import foundation.equivalences-arrows public
+open import foundation.equivalences-cospan-diagrams public
 open import foundation.equivalences-cospans public
 open import foundation.equivalences-double-arrows public
+open import foundation.equivalences-forks-over-equivalences-double-arrows public
 open import foundation.equivalences-inverse-sequential-diagrams public
 open import foundation.equivalences-maybe public
 open import foundation.equivalences-span-diagrams public
@@ -210,6 +213,7 @@ open import foundation.finitely-coherent-equivalences public
 open import foundation.finitely-coherently-invertible-maps public
 open import foundation.finitely-truncated-types public
 open import foundation.fixed-points-endofunctions public
+open import foundation.forks public
 open import foundation.freely-generated-equivalence-relations public
 open import foundation.full-subtypes public
 open import foundation.function-extensionality public
@@ -321,6 +325,7 @@ open import foundation.morphisms-coalgebras-maybe public
 open import foundation.morphisms-cospan-diagrams public
 open import foundation.morphisms-cospans public
 open import foundation.morphisms-double-arrows public
+open import foundation.morphisms-forks-over-morphisms-double-arrows public
 open import foundation.morphisms-inverse-sequential-diagrams public
 open import foundation.morphisms-span-diagrams public
 open import foundation.morphisms-spans public
@@ -339,9 +344,12 @@ open import foundation.negation public
 open import foundation.noncontractible-types public
 open import foundation.noninjective-maps public
 open import foundation.null-homotopic-maps public
+open import foundation.operations-cospan-diagrams public
+open import foundation.operations-cospans public
 open import foundation.operations-span-diagrams public
 open import foundation.operations-spans public
 open import foundation.operations-spans-families-of-types public
+open import foundation.opposite-cospans public
 open import foundation.opposite-spans public
 open import foundation.pairs-of-distinct-elements public
 open import foundation.partial-elements public
@@ -458,6 +466,7 @@ open import foundation.transport-along-higher-identifications public
 open import foundation.transport-along-homotopies public
 open import foundation.transport-along-identifications public
 open import foundation.transport-split-type-families public
+open import foundation.transposition-cospan-diagrams public
 open import foundation.transposition-identifications-along-equivalences public
 open import foundation.transposition-identifications-along-retractions public
 open import foundation.transposition-identifications-along-sections public
diff --git a/src/foundation/action-on-identifications-functions.lagda.md b/src/foundation/action-on-identifications-functions.lagda.md
index 5e4162ad9da..70bde81286d 100644
--- a/src/foundation/action-on-identifications-functions.lagda.md
+++ b/src/foundation/action-on-identifications-functions.lagda.md
@@ -31,7 +31,7 @@ identity types.
 ```agda
 ap :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} →
-  x ＝ y → (f x) ＝ (f y)
+  x ＝ y → f x ＝ f y
 ap f refl = refl
 ```
 
@@ -40,18 +40,29 @@ ap f refl = refl
 ### The identity function acts trivially on identifications
 
 ```agda
-ap-id :
-  {l : Level} {A : UU l} {x y : A} (p : x ＝ y) → (ap id p) ＝ p
-ap-id refl = refl
+module _
+  {l : Level} {A : UU l} {x y : A}
+  where
+
+  ap-id : (p : x ＝ y) → ap id p ＝ p
+  ap-id refl = refl
+
+  inv-ap-id : (p : x ＝ y) → p ＝ ap id p
+  inv-ap-id p = inv (ap-id p)
 ```
 
 ### The action on identifications of a composite function is the composite of the actions
 
 ```agda
-ap-comp :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (g : B → C)
-  (f : A → B) {x y : A} (p : x ＝ y) → (ap (g ∘ f) p) ＝ ((ap g ∘ ap f) p)
-ap-comp g f refl = refl
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (g : B → C) (f : A → B)
+  where
+
+  ap-comp : {x y : A} (p : x ＝ y) → ap (g ∘ f) p ＝ (ap g ∘ ap f) p
+  ap-comp refl = refl
+
+  inv-ap-comp : {x y : A} (p : x ＝ y) → (ap g ∘ ap f) p ＝ ap (g ∘ f) p
+  inv-ap-comp q = inv (ap-comp q)
 
 ap-comp-assoc :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
@@ -63,10 +74,12 @@ ap-comp-assoc h g f refl = refl
 ### The action on identifications of any map preserves `refl`
 
 ```agda
-ap-refl :
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (x : A) →
-  (ap f (refl {x = x})) ＝ refl
-ap-refl f x = refl
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (x : A)
+  where
+
+  ap-refl : ap f (refl {x = x}) ＝ refl
+  ap-refl = refl
 ```
 
 ### The action on identifications of any map preserves concatenation of identifications
@@ -80,6 +93,10 @@ module _
     {x y z : A} (p : x ＝ y) (q : y ＝ z) → ap f (p ∙ q) ＝ ap f p ∙ ap f q
   ap-concat refl q = refl
 
+  inv-ap-concat :
+    {x y z : A} (p : x ＝ y) (q : y ＝ z) → ap f p ∙ ap f q ＝ ap f (p ∙ q)
+  inv-ap-concat p q = inv (ap-concat p q)
+
   compute-right-refl-ap-concat :
     {x y : A} (p : x ＝ y) →
     ap-concat p refl ＝ ap (ap f) right-unit ∙ inv right-unit
@@ -89,19 +106,29 @@ module _
 ### The action on identifications of any map preserves inverses
 
 ```agda
-ap-inv :
+module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A}
-  (p : x ＝ y) → ap f (inv p) ＝ inv (ap f p)
-ap-inv f refl = refl
+  where
+
+  ap-inv : (p : x ＝ y) → ap f (inv p) ＝ inv (ap f p)
+  ap-inv refl = refl
+
+  inv-ap-inv : (p : x ＝ y) → inv (ap f p) ＝ ap f (inv p)
+  inv-ap-inv p = inv (ap-inv p)
 ```
 
 ### The action on identifications of a constant map is constant
 
 ```agda
-ap-const :
+module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) {x y : A}
-  (p : x ＝ y) → (ap (const A b) p) ＝ refl
-ap-const b refl = refl
+  where
+
+  ap-const : (p : x ＝ y) → ap (const A b) p ＝ refl
+  ap-const refl = refl
+
+  inv-ap-const : (p : x ＝ y) → refl ＝ ap (const A b) p
+  inv-ap-const p = inv (ap-const p)
 ```
 
 ## See also
diff --git a/src/foundation/cospan-diagrams.lagda.md b/src/foundation/cospan-diagrams.lagda.md
index 47673304e16..d99c68f8a5c 100644
--- a/src/foundation/cospan-diagrams.lagda.md
+++ b/src/foundation/cospan-diagrams.lagda.md
@@ -29,29 +29,34 @@ cospan-diagram :
 cospan-diagram l1 l2 l3 =
   Σ (UU l1) (λ A → Σ (UU l2) (cospan l3 A))
 
+make-cospan-diagram :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} →
+  (A → X) → (B → X) → cospan-diagram l1 l2 l3
+make-cospan-diagram {A = A} {B} {X} f g = (A , B , X , f , g)
+
 module _
   {l1 l2 l3 : Level} (c : cospan-diagram l1 l2 l3)
   where
 
-  left-type-cospan-diagram : UU l1
-  left-type-cospan-diagram = pr1 c
+  domain-cospan-diagram : UU l1
+  domain-cospan-diagram = pr1 c
 
-  right-type-cospan-diagram : UU l2
-  right-type-cospan-diagram = pr1 (pr2 c)
+  codomain-cospan-diagram : UU l2
+  codomain-cospan-diagram = pr1 (pr2 c)
 
   cospan-cospan-diagram :
-    cospan l3 left-type-cospan-diagram right-type-cospan-diagram
+    cospan l3 domain-cospan-diagram codomain-cospan-diagram
   cospan-cospan-diagram = pr2 (pr2 c)
 
   cospanning-type-cospan-diagram : UU l3
-  cospanning-type-cospan-diagram = codomain-cospan cospan-cospan-diagram
+  cospanning-type-cospan-diagram = cospanning-type-cospan cospan-cospan-diagram
 
   left-map-cospan-diagram :
-    left-type-cospan-diagram → cospanning-type-cospan-diagram
+    domain-cospan-diagram → cospanning-type-cospan-diagram
   left-map-cospan-diagram = left-map-cospan cospan-cospan-diagram
 
   right-map-cospan-diagram :
-    right-type-cospan-diagram → cospanning-type-cospan-diagram
+    codomain-cospan-diagram → cospanning-type-cospan-diagram
   right-map-cospan-diagram = right-map-cospan cospan-cospan-diagram
 ```
 
diff --git a/src/foundation/cospans.lagda.md b/src/foundation/cospans.lagda.md
index 41f0b583d6e..bbed314d7ee 100644
--- a/src/foundation/cospans.lagda.md
+++ b/src/foundation/cospans.lagda.md
@@ -61,13 +61,13 @@ module _
   {l1 l2 : Level} {l : Level} {A : UU l1} {B : UU l2} (c : cospan l A B)
   where
 
-  codomain-cospan : UU l
-  codomain-cospan = pr1 c
+  cospanning-type-cospan : UU l
+  cospanning-type-cospan = pr1 c
 
-  left-map-cospan : A → codomain-cospan
+  left-map-cospan : A → cospanning-type-cospan
   left-map-cospan = pr1 (pr2 c)
 
-  right-map-cospan : B → codomain-cospan
+  right-map-cospan : B → cospanning-type-cospan
   right-map-cospan = pr2 (pr2 c)
 ```
 
diff --git a/src/foundation/equality-cartesian-product-types.lagda.md b/src/foundation/equality-cartesian-product-types.lagda.md
index b500eb9d43d..699a19820a0 100644
--- a/src/foundation/equality-cartesian-product-types.lagda.md
+++ b/src/foundation/equality-cartesian-product-types.lagda.md
@@ -135,6 +135,32 @@ ap-pr2-eq-pair :
 ap-pr2-eq-pair refl refl = refl
 ```
 
+###
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {x : A} {y y' : B x}
+  where
+
+  ap-pr1-ap-pair :
+    (p : y ＝ y') → ap pr1 (ap (pair {B = B} x) p) ＝ refl
+  ap-pr1-ap-pair refl = refl
+
+  inv-ap-pr1-ap-pair :
+    (p : y ＝ y') → refl ＝ ap pr1 (ap (pair {B = B} x) p)
+  inv-ap-pr1-ap-pair p = inv (ap-pr1-ap-pair p)
+
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {x : A} {y y' : B}
+  where
+
+  ap-pr2-ap-pair : (p : y ＝ y') → ap pr2 (ap (pair {B = λ _ → B} x) p) ＝ p
+  ap-pr2-ap-pair refl = refl
+
+  inv-ap-pr2-ap-pair : (p : y ＝ y') → p ＝ ap pr2 (ap (pair {B = λ _ → B} x) p)
+  inv-ap-pr2-ap-pair p = inv (ap-pr2-ap-pair p)
+```
+
 #### Computing transport along a path of the form `eq-pair`
 
 ```agda
diff --git a/src/foundation/equality-of-equality-cartesian-product-types.lagda.md b/src/foundation/equality-of-equality-cartesian-product-types.lagda.md
new file mode 100644
index 00000000000..e044031369e
--- /dev/null
+++ b/src/foundation/equality-of-equality-cartesian-product-types.lagda.md
@@ -0,0 +1,94 @@
+# Equality of equality of cartesian product types
+
+```agda
+module foundation.equality-of-equality-cartesian-product-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equality-cartesian-product-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.structure-identity-principle
+open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
+open import foundation-core.equality-dependent-pair-types
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.torsorial-type-families
+open import foundation-core.transport-along-identifications
+```
+
+</details>
+
+## Idea
+
+[Identifications](foundation-core.identity-types.md) of identifications in a
+[cartesian product](foundation-core.cartesian-product-types.md) are
+[equivalently](foundation-core.equivalences.md) described as pairs of
+identifications. This provides us with a characterization of the identity types
+of identity types of cartesian product types.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  Eq²-product : {s t : A × B} (p q : s ＝ t) → UU (l1 ⊔ l2)
+  Eq²-product p q = Eq-product (pair-eq p) (pair-eq q)
+
+  pair-eq² : {s t : A × B} {p q : s ＝ t} → p ＝ q → Eq²-product p q
+  pair-eq² r = pair-eq (ap pair-eq r)
+```
+
+## Properties
+
+### Characterizing equality of equality in cartesian products
+
+```agda
+abstract
+  is-torsorial-Eq-product :
+      {l1 l2 : Level} {A : UU l1} {B : UU l2} (s : A × B) →
+      is-torsorial (Eq-product s)
+  is-torsorial-Eq-product s =
+    fundamental-theorem-id' (λ t → pair-eq) (is-equiv-pair-eq s)
+
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  abstract
+    is-torsorial-Eq²-product :
+      {s t : A × B} (p : s ＝ t) → is-torsorial (Eq²-product p)
+    is-torsorial-Eq²-product {s} {t} p =
+      is-contr-equiv
+        ( Σ (Eq-product s t) (Eq-product (pair-eq p)))
+        ( equiv-Σ-equiv-base
+          ( Eq-product (pair-eq p))
+          ( equiv-pair-eq s t))
+        ( is-torsorial-Eq-product (pair-eq p))
+
+  abstract
+    is-equiv-pair-eq² :
+      {s t : A × B} (p q : s ＝ t) → is-equiv (pair-eq² {p = p} {q = q})
+    is-equiv-pair-eq² p =
+      fundamental-theorem-id (is-torsorial-Eq²-product p) (λ q → pair-eq²)
+
+  equiv-pair-eq² :
+    {s t : A × B} (p q : s ＝ t) → (p ＝ q) ≃ Eq²-product p q
+  pr1 (equiv-pair-eq² p q) = pair-eq²
+  pr2 (equiv-pair-eq² p q) = is-equiv-pair-eq² p q
+
+  eq-pair² : {s t : A × B} {p q : s ＝ t} → Eq²-product p q → p ＝ q
+  eq-pair² {p = p} {q} = map-inv-equiv (equiv-pair-eq² p q)
+```
diff --git a/src/foundation/equivalences-cospan-diagrams.lagda.md b/src/foundation/equivalences-cospan-diagrams.lagda.md
new file mode 100644
index 00000000000..42bb459a494
--- /dev/null
+++ b/src/foundation/equivalences-cospan-diagrams.lagda.md
@@ -0,0 +1,331 @@
+# Equivalences of cospan diagrams
+
+```agda
+module foundation.equivalences-cospan-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.equivalences-cospans
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.morphisms-cospan-diagrams
+open import foundation.morphisms-cospans
+open import foundation.operations-cospans
+open import foundation.propositions
+open import foundation.structure-identity-principle
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import foundation-core.commuting-squares-of-maps
+open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.identity-types
+open import foundation-core.torsorial-type-families
+```
+
+</details>
+
+## Idea
+
+An {{#concept "equivalence of cospan diagrams" Agda=equiv-cospan-diagram}} from
+a [cospan diagram](foundation.cospan-diagrams.md) `A -f-> S <-g- B` to a cospan
+diagram `C -h-> T <-k- D` consists of
+[equivalences](foundation-core.equivalences.md) `u : A ≃ C`, `v : B ≃ D`, and
+`w : S ≃ T` [equipped](foundation.structure.md) with two
+[homotopies](foundation-core.homotopies.md) witnessing that the diagram
+
+```text
+         f         g
+    A ------> S <------ B
+    |         |         |
+  u |         | w       | v
+    ∨         ∨         ∨
+    C ------> T <------ D
+         h         k
+```
+
+[commutes](foundation-core.commuting-squares-of-maps.md).
+
+## Definitions
+
+### The predicate of being an equivalence of cospan diagrams
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (𝒮 : cospan-diagram l1 l2 l3) (𝒯 : cospan-diagram l4 l5 l6)
+  (f : hom-cospan-diagram 𝒮 𝒯)
+  where
+
+  is-equiv-prop-hom-cospan-diagram : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
+  is-equiv-prop-hom-cospan-diagram =
+    product-Prop
+      ( is-equiv-Prop (map-domain-hom-cospan-diagram 𝒮 𝒯 f))
+      ( product-Prop
+        ( is-equiv-Prop (map-codomain-hom-cospan-diagram 𝒮 𝒯 f))
+        ( is-equiv-Prop (cospanning-map-hom-cospan-diagram 𝒮 𝒯 f)))
+
+  is-equiv-hom-cospan-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
+  is-equiv-hom-cospan-diagram = type-Prop is-equiv-prop-hom-cospan-diagram
+
+  is-prop-is-equiv-hom-cospan-diagram : is-prop is-equiv-hom-cospan-diagram
+  is-prop-is-equiv-hom-cospan-diagram =
+    is-prop-type-Prop is-equiv-prop-hom-cospan-diagram
+```
+
+### Equivalences of cospan diagrams
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (𝒮 : cospan-diagram l1 l2 l3) (𝒯 : cospan-diagram l4 l5 l6)
+  where
+
+  equiv-cospan-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
+  equiv-cospan-diagram =
+    Σ ( domain-cospan-diagram 𝒮 ≃ domain-cospan-diagram 𝒯)
+      ( λ e →
+        Σ ( codomain-cospan-diagram 𝒮 ≃ codomain-cospan-diagram 𝒯)
+          ( λ f →
+            equiv-cospan
+              ( cospan-cospan-diagram 𝒮)
+              ( concat-cospan
+                ( cospan-cospan-diagram 𝒯)
+                ( map-equiv e)
+                ( map-equiv f))))
+
+  module _
+    (e : equiv-cospan-diagram)
+    where
+
+    equiv-domain-equiv-cospan-diagram :
+      domain-cospan-diagram 𝒮 ≃ domain-cospan-diagram 𝒯
+    equiv-domain-equiv-cospan-diagram = pr1 e
+
+    map-domain-equiv-cospan-diagram :
+      domain-cospan-diagram 𝒮 → domain-cospan-diagram 𝒯
+    map-domain-equiv-cospan-diagram =
+      map-equiv equiv-domain-equiv-cospan-diagram
+
+    is-equiv-map-domain-equiv-cospan-diagram :
+      is-equiv map-domain-equiv-cospan-diagram
+    is-equiv-map-domain-equiv-cospan-diagram =
+      is-equiv-map-equiv equiv-domain-equiv-cospan-diagram
+
+    equiv-codomain-equiv-cospan-diagram :
+      codomain-cospan-diagram 𝒮 ≃ codomain-cospan-diagram 𝒯
+    equiv-codomain-equiv-cospan-diagram = pr1 (pr2 e)
+
+    map-codomain-equiv-cospan-diagram :
+      codomain-cospan-diagram 𝒮 → codomain-cospan-diagram 𝒯
+    map-codomain-equiv-cospan-diagram =
+      map-equiv equiv-codomain-equiv-cospan-diagram
+
+    is-equiv-map-codomain-equiv-cospan-diagram :
+      is-equiv map-codomain-equiv-cospan-diagram
+    is-equiv-map-codomain-equiv-cospan-diagram =
+      is-equiv-map-equiv equiv-codomain-equiv-cospan-diagram
+
+    equiv-cospan-equiv-cospan-diagram :
+      equiv-cospan
+        ( cospan-cospan-diagram 𝒮)
+        ( concat-cospan
+          ( cospan-cospan-diagram 𝒯)
+          ( map-domain-equiv-cospan-diagram)
+          ( map-codomain-equiv-cospan-diagram))
+    equiv-cospan-equiv-cospan-diagram =
+      pr2 (pr2 e)
+
+    cospanning-equiv-equiv-cospan-diagram :
+      cospanning-type-cospan-diagram 𝒮 ≃ cospanning-type-cospan-diagram 𝒯
+    cospanning-equiv-equiv-cospan-diagram =
+      equiv-equiv-cospan
+        ( cospan-cospan-diagram 𝒮)
+        ( concat-cospan
+          ( cospan-cospan-diagram 𝒯)
+          ( map-domain-equiv-cospan-diagram)
+          ( map-codomain-equiv-cospan-diagram))
+        ( equiv-cospan-equiv-cospan-diagram)
+
+    cospanning-map-equiv-cospan-diagram :
+      cospanning-type-cospan-diagram 𝒮 → cospanning-type-cospan-diagram 𝒯
+    cospanning-map-equiv-cospan-diagram =
+      map-equiv-cospan
+        ( cospan-cospan-diagram 𝒮)
+        ( concat-cospan
+          ( cospan-cospan-diagram 𝒯)
+          ( map-domain-equiv-cospan-diagram)
+          ( map-codomain-equiv-cospan-diagram))
+        ( equiv-cospan-equiv-cospan-diagram)
+
+    is-equiv-cospanning-map-equiv-cospan-diagram :
+      is-equiv cospanning-map-equiv-cospan-diagram
+    is-equiv-cospanning-map-equiv-cospan-diagram =
+      is-equiv-equiv-cospan
+        ( cospan-cospan-diagram 𝒮)
+        ( concat-cospan
+          ( cospan-cospan-diagram 𝒯)
+          ( map-domain-equiv-cospan-diagram)
+          ( map-codomain-equiv-cospan-diagram))
+        ( equiv-cospan-equiv-cospan-diagram)
+
+    left-square-equiv-cospan-diagram :
+      coherence-square-maps
+        ( left-map-cospan-diagram 𝒮)
+        ( map-domain-equiv-cospan-diagram)
+        ( cospanning-map-equiv-cospan-diagram)
+        ( left-map-cospan-diagram 𝒯)
+    left-square-equiv-cospan-diagram =
+      left-triangle-equiv-cospan
+        ( cospan-cospan-diagram 𝒮)
+        ( concat-cospan
+          ( cospan-cospan-diagram 𝒯)
+          ( map-domain-equiv-cospan-diagram)
+          ( map-codomain-equiv-cospan-diagram))
+        ( equiv-cospan-equiv-cospan-diagram)
+
+    equiv-left-arrow-equiv-cospan-diagram :
+      equiv-arrow (left-map-cospan-diagram 𝒮) (left-map-cospan-diagram 𝒯)
+    pr1 equiv-left-arrow-equiv-cospan-diagram =
+      equiv-domain-equiv-cospan-diagram
+    pr1 (pr2 equiv-left-arrow-equiv-cospan-diagram) =
+      cospanning-equiv-equiv-cospan-diagram
+    pr2 (pr2 equiv-left-arrow-equiv-cospan-diagram) =
+      inv-htpy left-square-equiv-cospan-diagram
+
+    right-square-equiv-cospan-diagram :
+      coherence-square-maps
+        ( right-map-cospan-diagram 𝒮)
+        ( map-codomain-equiv-cospan-diagram)
+        ( cospanning-map-equiv-cospan-diagram)
+        ( right-map-cospan-diagram 𝒯)
+    right-square-equiv-cospan-diagram =
+      right-triangle-equiv-cospan
+        ( cospan-cospan-diagram 𝒮)
+        ( concat-cospan
+          ( cospan-cospan-diagram 𝒯)
+          ( map-domain-equiv-cospan-diagram)
+          ( map-codomain-equiv-cospan-diagram))
+        ( equiv-cospan-equiv-cospan-diagram)
+
+    equiv-right-arrow-equiv-cospan-diagram :
+      equiv-arrow (right-map-cospan-diagram 𝒮) (right-map-cospan-diagram 𝒯)
+    pr1 equiv-right-arrow-equiv-cospan-diagram =
+      equiv-codomain-equiv-cospan-diagram
+    pr1 (pr2 equiv-right-arrow-equiv-cospan-diagram) =
+      cospanning-equiv-equiv-cospan-diagram
+    pr2 (pr2 equiv-right-arrow-equiv-cospan-diagram) =
+      inv-htpy right-square-equiv-cospan-diagram
+
+    hom-cospan-equiv-cospan-diagram :
+      hom-cospan
+        ( cospan-cospan-diagram 𝒮)
+        ( concat-cospan
+          ( cospan-cospan-diagram 𝒯)
+          ( map-domain-equiv-cospan-diagram)
+          ( map-codomain-equiv-cospan-diagram))
+    hom-cospan-equiv-cospan-diagram =
+      hom-equiv-cospan
+        ( cospan-cospan-diagram 𝒮)
+        ( concat-cospan
+          ( cospan-cospan-diagram 𝒯)
+          ( map-domain-equiv-cospan-diagram)
+          ( map-codomain-equiv-cospan-diagram))
+        ( equiv-cospan-equiv-cospan-diagram)
+
+    hom-equiv-cospan-diagram : hom-cospan-diagram 𝒮 𝒯
+    pr1 hom-equiv-cospan-diagram = map-domain-equiv-cospan-diagram
+    pr1 (pr2 hom-equiv-cospan-diagram) = map-codomain-equiv-cospan-diagram
+    pr2 (pr2 hom-equiv-cospan-diagram) = hom-cospan-equiv-cospan-diagram
+
+    is-equiv-equiv-cospan-diagram :
+      is-equiv-hom-cospan-diagram 𝒮 𝒯 hom-equiv-cospan-diagram
+    pr1 is-equiv-equiv-cospan-diagram =
+      is-equiv-map-domain-equiv-cospan-diagram
+    pr1 (pr2 is-equiv-equiv-cospan-diagram) =
+      is-equiv-map-codomain-equiv-cospan-diagram
+    pr2 (pr2 is-equiv-equiv-cospan-diagram) =
+      is-equiv-cospanning-map-equiv-cospan-diagram
+
+  compute-equiv-cospan-diagram :
+    Σ (hom-cospan-diagram 𝒮 𝒯) (is-equiv-hom-cospan-diagram 𝒮 𝒯) ≃
+    equiv-cospan-diagram
+  compute-equiv-cospan-diagram =
+    ( equiv-tot
+      ( λ a →
+        ( equiv-tot
+          ( λ b →
+            compute-equiv-cospan
+              ( cospan-cospan-diagram 𝒮)
+              ( concat-cospan
+                ( cospan-cospan-diagram 𝒯)
+                ( map-equiv a)
+                ( map-equiv b)))) ∘e
+        ( interchange-Σ-Σ _))) ∘e
+    ( interchange-Σ-Σ _)
+```
+
+### The identity equivalence of cospan diagrams
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒮 : cospan-diagram l1 l2 l3)
+  where
+
+  id-equiv-cospan-diagram : equiv-cospan-diagram 𝒮 𝒮
+  pr1 id-equiv-cospan-diagram = id-equiv
+  pr1 (pr2 id-equiv-cospan-diagram) = id-equiv
+  pr2 (pr2 id-equiv-cospan-diagram) = id-equiv-cospan (cospan-cospan-diagram 𝒮)
+```
+
+## Properties
+
+### Extensionality of cospan diagrams
+
+Equality of cospan diagrams is equivalent to equivalences of cospan diagrams.
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒮 : cospan-diagram l1 l2 l3)
+  where
+
+  equiv-eq-cospan-diagram :
+    (𝒯 : cospan-diagram l1 l2 l3) → 𝒮 ＝ 𝒯 → equiv-cospan-diagram 𝒮 𝒯
+  equiv-eq-cospan-diagram 𝒯 refl = id-equiv-cospan-diagram 𝒮
+
+  abstract
+    is-torsorial-equiv-cospan-diagram :
+      is-torsorial (equiv-cospan-diagram {l1} {l2} {l3} {l1} {l2} {l3} 𝒮)
+    is-torsorial-equiv-cospan-diagram =
+      is-torsorial-Eq-structure
+        ( is-torsorial-equiv (domain-cospan-diagram 𝒮))
+        ( domain-cospan-diagram 𝒮 , id-equiv)
+        ( is-torsorial-Eq-structure
+          ( is-torsorial-equiv (codomain-cospan-diagram 𝒮))
+          ( codomain-cospan-diagram 𝒮 , id-equiv)
+          ( is-torsorial-equiv-cospan (cospan-cospan-diagram 𝒮)))
+
+  abstract
+    is-equiv-equiv-eq-cospan-diagram :
+      (𝒯 : cospan-diagram l1 l2 l3) → is-equiv (equiv-eq-cospan-diagram 𝒯)
+    is-equiv-equiv-eq-cospan-diagram =
+      fundamental-theorem-id
+        ( is-torsorial-equiv-cospan-diagram)
+        ( equiv-eq-cospan-diagram)
+
+  extensionality-cospan-diagram :
+    (𝒯 : cospan-diagram l1 l2 l3) → (𝒮 ＝ 𝒯) ≃ equiv-cospan-diagram 𝒮 𝒯
+  pr1 (extensionality-cospan-diagram 𝒯) = equiv-eq-cospan-diagram 𝒯
+  pr2 (extensionality-cospan-diagram 𝒯) = is-equiv-equiv-eq-cospan-diagram 𝒯
+
+  eq-equiv-cospan-diagram :
+    (𝒯 : cospan-diagram l1 l2 l3) → equiv-cospan-diagram 𝒮 𝒯 → 𝒮 ＝ 𝒯
+  eq-equiv-cospan-diagram 𝒯 = map-inv-equiv (extensionality-cospan-diagram 𝒯)
+```
diff --git a/src/foundation/equivalences-cospans.lagda.md b/src/foundation/equivalences-cospans.lagda.md
index a44b7e3b112..769fa13bfab 100644
--- a/src/foundation/equivalences-cospans.lagda.md
+++ b/src/foundation/equivalences-cospans.lagda.md
@@ -13,6 +13,7 @@ open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopy-induction
 open import foundation.morphisms-cospans
 open import foundation.structure-identity-principle
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.univalence
 open import foundation.universe-levels
 
@@ -44,17 +45,59 @@ both [commute](foundation.commuting-triangles-of-maps.md).
 
 ## Definitions
 
+### The predicate of being an equivalence of cospans
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
+  (s : cospan l3 A B) (t : cospan l4 A B)
+  where
+
+  is-equiv-hom-cospan : hom-cospan s t → UU (l3 ⊔ l4)
+  is-equiv-hom-cospan f = is-equiv (map-hom-cospan s t f)
+```
+
 ### Equivalences of cospans
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
+  (s : cospan l3 A B) (t : cospan l4 A B)
   where
 
-  equiv-cospan : cospan l3 A B → cospan l4 A B → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  equiv-cospan c d =
-    Σ ( codomain-cospan c ≃ codomain-cospan d)
-      ( λ e → coherence-hom-cospan c d (map-equiv e))
+  equiv-cospan : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  equiv-cospan =
+    Σ ( cospanning-type-cospan s ≃ cospanning-type-cospan t)
+      ( λ e → coherence-hom-cospan s t (map-equiv e))
+
+  equiv-equiv-cospan :
+    equiv-cospan → cospanning-type-cospan s ≃ cospanning-type-cospan t
+  equiv-equiv-cospan = pr1
+
+  map-equiv-cospan :
+    equiv-cospan → cospanning-type-cospan s → cospanning-type-cospan t
+  map-equiv-cospan e = map-equiv (equiv-equiv-cospan e)
+
+  left-triangle-equiv-cospan :
+    (e : equiv-cospan) → left-coherence-hom-cospan s t (map-equiv-cospan e)
+  left-triangle-equiv-cospan e = pr1 (pr2 e)
+
+  right-triangle-equiv-cospan :
+    (e : equiv-cospan) → right-coherence-hom-cospan s t (map-equiv-cospan e)
+  right-triangle-equiv-cospan e = pr2 (pr2 e)
+
+  hom-equiv-cospan : equiv-cospan → hom-cospan s t
+  pr1 (hom-equiv-cospan e) = map-equiv-cospan e
+  pr1 (pr2 (hom-equiv-cospan e)) = left-triangle-equiv-cospan e
+  pr2 (pr2 (hom-equiv-cospan e)) = right-triangle-equiv-cospan e
+
+  is-equiv-equiv-cospan :
+    (e : equiv-cospan) → is-equiv-hom-cospan s t (hom-equiv-cospan e)
+  is-equiv-equiv-cospan e = is-equiv-map-equiv (equiv-equiv-cospan e)
+
+  compute-equiv-cospan :
+    Σ (hom-cospan s t) (is-equiv-hom-cospan s t) ≃ equiv-cospan
+  compute-equiv-cospan = equiv-right-swap-Σ
 ```
 
 ### The identity equivalence of cospans
@@ -82,21 +125,23 @@ module _
   equiv-eq-cospan : (c d : cospan l3 A B) → c ＝ d → equiv-cospan c d
   equiv-eq-cospan c .c refl = id-equiv-cospan c
 
-  is-torsorial-equiv-cospan :
-    (c : cospan l3 A B) → is-torsorial (equiv-cospan c)
-  is-torsorial-equiv-cospan c =
-    is-torsorial-Eq-structure
-      ( is-torsorial-equiv (pr1 c))
-      ( codomain-cospan c , id-equiv)
-      ( is-torsorial-Eq-structure
-        ( is-torsorial-htpy' (left-map-cospan c))
-        ( left-map-cospan c , refl-htpy)
-        ( is-torsorial-htpy' (right-map-cospan c)))
-
-  is-equiv-equiv-eq-cospan :
-    (c d : cospan l3 A B) → is-equiv (equiv-eq-cospan c d)
-  is-equiv-equiv-eq-cospan c =
-    fundamental-theorem-id (is-torsorial-equiv-cospan c) (equiv-eq-cospan c)
+  abstract
+    is-torsorial-equiv-cospan :
+      (c : cospan l3 A B) → is-torsorial (equiv-cospan {l1} {l2} {l3} {l3} c)
+    is-torsorial-equiv-cospan c =
+      is-torsorial-Eq-structure
+        ( is-torsorial-equiv (pr1 c))
+        ( cospanning-type-cospan c , id-equiv)
+        ( is-torsorial-Eq-structure
+          ( is-torsorial-htpy' (left-map-cospan c))
+          ( left-map-cospan c , refl-htpy)
+          ( is-torsorial-htpy' (right-map-cospan c)))
+
+  abstract
+    is-equiv-equiv-eq-cospan :
+      (c d : cospan l3 A B) → is-equiv (equiv-eq-cospan c d)
+    is-equiv-equiv-eq-cospan c =
+      fundamental-theorem-id (is-torsorial-equiv-cospan c) (equiv-eq-cospan c)
 
   extensionality-cospan :
     (c d : cospan l3 A B) → (c ＝ d) ≃ (equiv-cospan c d)
diff --git a/src/foundation/equivalences-forks-over-equivalences-double-arrows.lagda.md b/src/foundation/equivalences-forks-over-equivalences-double-arrows.lagda.md
new file mode 100644
index 00000000000..f195d7a8022
--- /dev/null
+++ b/src/foundation/equivalences-forks-over-equivalences-double-arrows.lagda.md
@@ -0,0 +1,265 @@
+# Equivalences of forks over equivalences of double arrows
+
+```agda
+module foundation.equivalences-forks-over-equivalences-double-arrows where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.equivalences-double-arrows
+open import foundation.forks
+open import foundation.homotopies
+open import foundation.morphisms-arrows
+open import foundation.morphisms-forks-over-morphisms-double-arrows
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+```
+
+</details>
+
+## Idea
+
+Consider two [double arrows](foundation.double-arrows.md) `f, g : A → B` and
+`h, k : U → V`, equipped with [forks](foundation.forks.md) `c : X → A` and
+`c' : Y → U`, respectively, and an
+[equivalence of double arrows](foundation.equivalences-double-arrows.md)
+`e : (f, g) ≃ (h, k)`.
+
+Then an
+{{#concept "equivalence of forks" Disambiguation="over an equivalence of double arrows" Agda=equiv-fork-equiv-double-arrow}}
+over `e` is a triple `(m, H, K)`, with `m : X ≃ Y` an
+[equivalence](foundation-core.equivalences.md) of vertices of the forks, `H` a
+[homotopy](foundation-core.homotopies.md) witnessing that the bottom square in
+the diagram
+
+```text
+           m
+     X --------> Y
+     |     ≃     |
+   c |           | c'
+     |           |
+     ∨     i     ∨
+     A --------> U
+    | |    ≃    | |
+  f | | g     h | | k
+    | |         | |
+    ∨ ∨    ≃    ∨ ∨
+     B --------> V
+           j
+```
+
+[commutes](foundation-core.commuting-squares-of-maps.md), and `K` a coherence
+datum "filling the inside" --- we have two stacks of squares
+
+```text
+           m                        m
+     X --------> Y            X --------> Y
+     |     ≃     |            |     ≃     |
+   c |           | c'       c |           | c'
+     |           |            |           |
+     ∨     i     ∨            ∨     i     ∨
+     A --------> U            A --------> U
+     |     ≃     |            |     ≃     |
+   f |           | h        g |           | k
+     |           |            |           |
+     ∨     ≃     ∨            ∨     ≃     ∨
+     B --------> V            B --------> V
+           j                        j
+```
+
+which share the top map `i` and the bottom square, and the coherences of `c` and
+`c'` filling the sides; that gives the homotopies
+
+```text
+                                               m                 m
+     X                 X                 X --------> Y     X --------> Y
+     |                 |                             |                 |
+   c |               c |                             | c'              | c'
+     |                 |                             |                 |
+     ∨                 ∨     i                       ∨                 ∨
+     A        ~        A --------> U        ~        U        ~        U
+     |                             |                 |                 |
+   f |                             | h               | h               | k
+     |                             |                 |                 |
+     ∨                             ∨                 ∨                 ∨
+     B --------> V                 V                 V                 V
+           j
+```
+
+and
+
+```text
+                                                                 m
+     X                 X                 X                 X --------> Y
+     |                 |                 |                             |
+   c |               c |               c |                             | c'
+     |                 |                 |                             |
+     ∨                 ∨                 ∨     i                       ∨
+     A        ~        A        ~        A --------> U        ~        U
+     |                 |                             |                 |
+   f |               g |                             | k               | k
+     |                 |                             |                 |
+     ∨                 ∨                             ∨                 ∨
+     B --------> Y     B --------> V                 V                 V ,
+           j                 j
+```
+
+which are required to be homotopic.
+
+## Definitions
+
+### Equivalences of forks
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (a : double-arrow l1 l2)
+  (a' : double-arrow l4 l5)
+  {X : UU l3} {Y : UU l6}
+  (c : fork a X) (c' : fork a' Y)
+  (e : equiv-double-arrow a a')
+  where
+
+  coherence-map-fork-equiv-fork-equiv-double-arrow : (X ≃ Y) → UU (l3 ⊔ l4)
+  coherence-map-fork-equiv-fork-equiv-double-arrow m =
+    coherence-map-fork-hom-fork-hom-double-arrow a a' c c'
+      ( hom-equiv-double-arrow a a' e)
+      ( map-equiv m)
+
+  coherence-equiv-fork-equiv-double-arrow :
+    (m : X ≃ Y) → coherence-map-fork-equiv-fork-equiv-double-arrow m →
+    UU (l3 ⊔ l5)
+  coherence-equiv-fork-equiv-double-arrow m =
+    coherence-hom-fork-hom-double-arrow a a' c c'
+      ( hom-equiv-double-arrow a a' e)
+      ( map-equiv m)
+
+  equiv-fork-equiv-double-arrow : UU (l3 ⊔ l4 ⊔ l5 ⊔ l6)
+  equiv-fork-equiv-double-arrow =
+    Σ ( X ≃ Y)
+      ( λ m →
+        Σ ( coherence-map-fork-equiv-fork-equiv-double-arrow m)
+          ( coherence-equiv-fork-equiv-double-arrow m))
+
+  module _
+    (e' : equiv-fork-equiv-double-arrow)
+    where
+
+    equiv-equiv-fork-equiv-double-arrow : X ≃ Y
+    equiv-equiv-fork-equiv-double-arrow = pr1 e'
+
+    map-equiv-fork-equiv-double-arrow : X → Y
+    map-equiv-fork-equiv-double-arrow =
+      map-equiv equiv-equiv-fork-equiv-double-arrow
+
+    is-equiv-map-equiv-fork-equiv-double-arrow :
+      is-equiv map-equiv-fork-equiv-double-arrow
+    is-equiv-map-equiv-fork-equiv-double-arrow =
+      is-equiv-map-equiv equiv-equiv-fork-equiv-double-arrow
+
+    coh-map-fork-equiv-fork-equiv-double-arrow :
+      coherence-map-fork-equiv-fork-equiv-double-arrow
+        ( equiv-equiv-fork-equiv-double-arrow)
+    coh-map-fork-equiv-fork-equiv-double-arrow = pr1 (pr2 e')
+
+    equiv-map-fork-equiv-fork-equiv-double-arrow :
+      equiv-arrow (map-fork a c) (map-fork a' c')
+    pr1 equiv-map-fork-equiv-fork-equiv-double-arrow =
+      equiv-equiv-fork-equiv-double-arrow
+    pr1 (pr2 equiv-map-fork-equiv-fork-equiv-double-arrow) =
+      domain-equiv-equiv-double-arrow a a' e
+    pr2 (pr2 equiv-map-fork-equiv-fork-equiv-double-arrow) =
+      coh-map-fork-equiv-fork-equiv-double-arrow
+
+    hom-map-fork-equiv-fork-equiv-double-arrow :
+      hom-arrow (map-fork a c) (map-fork a' c')
+    hom-map-fork-equiv-fork-equiv-double-arrow =
+      hom-equiv-arrow
+        ( map-fork a c)
+        ( map-fork a' c')
+        ( equiv-map-fork-equiv-fork-equiv-double-arrow)
+
+    coh-equiv-fork-equiv-double-arrow :
+      coherence-equiv-fork-equiv-double-arrow
+        ( equiv-equiv-fork-equiv-double-arrow)
+        ( coh-map-fork-equiv-fork-equiv-double-arrow)
+    coh-equiv-fork-equiv-double-arrow = pr2 (pr2 e')
+
+    hom-equiv-fork-equiv-double-arrow :
+      hom-fork-hom-double-arrow a a' c c' (hom-equiv-double-arrow a a' e)
+    pr1 hom-equiv-fork-equiv-double-arrow =
+      map-equiv-fork-equiv-double-arrow
+    pr1 (pr2 hom-equiv-fork-equiv-double-arrow) =
+      coh-map-fork-equiv-fork-equiv-double-arrow
+    pr2 (pr2 hom-equiv-fork-equiv-double-arrow) =
+      coh-equiv-fork-equiv-double-arrow
+```
+
+### The predicate on morphisms of forks over equivalences of double arrows of being an equivalence
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (a : double-arrow l1 l2)
+  (a' : double-arrow l4 l5)
+  {X : UU l3} {Y : UU l6}
+  (c : fork a X) (c' : fork a' Y)
+  (e : equiv-double-arrow a a')
+  where
+
+  is-equiv-hom-fork-equiv-double-arrow :
+    hom-fork-hom-double-arrow a a' c c' (hom-equiv-double-arrow a a' e) →
+    UU (l3 ⊔ l6)
+  is-equiv-hom-fork-equiv-double-arrow h =
+    is-equiv
+      ( map-hom-fork-hom-double-arrow a a' c c'
+        ( hom-equiv-double-arrow a a' e)
+        ( h))
+
+  is-equiv-hom-equiv-fork-equiv-double-arrow :
+    (e' : equiv-fork-equiv-double-arrow a a' c c' e) →
+    is-equiv-hom-fork-equiv-double-arrow
+      ( hom-equiv-fork-equiv-double-arrow a a' c c' e e')
+  is-equiv-hom-equiv-fork-equiv-double-arrow e' =
+    is-equiv-map-equiv-fork-equiv-double-arrow a a' c c' e e'
+```
+
+## Properties
+
+### Morphisms of forks over equivalences of arrows which are equivalences are equivalences of forks
+
+To construct an equivalence of forks over an equivalence `e` of double arrows,
+it suffices to construct a morphism of forks over the underlying morphism of
+double arrows of `e`, and show that the map `X → Y` is an equivalence.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (a : double-arrow l1 l2)
+  (a' : double-arrow l4 l5)
+  {X : UU l3} {Y : UU l6}
+  (c : fork a X) (c' : fork a' Y)
+  (e : equiv-double-arrow a a')
+  where
+
+  equiv-hom-fork-equiv-double-arrow :
+    (h : hom-fork-hom-double-arrow a a' c c' (hom-equiv-double-arrow a a' e)) →
+    is-equiv-hom-fork-equiv-double-arrow a a' c c' e h →
+    equiv-fork-equiv-double-arrow a a' c c' e
+  pr1 (pr1 (equiv-hom-fork-equiv-double-arrow h is-equiv-map-fork)) =
+    map-hom-fork-hom-double-arrow a a' c c' (hom-equiv-double-arrow a a' e) h
+  pr2 (pr1 (equiv-hom-fork-equiv-double-arrow h is-equiv-map-fork)) =
+    is-equiv-map-fork
+  pr1 (pr2 (equiv-hom-fork-equiv-double-arrow h _)) =
+    coh-map-fork-hom-fork-hom-double-arrow a a' c c'
+      ( hom-equiv-double-arrow a a' e)
+      ( h)
+  pr2 (pr2 (equiv-hom-fork-equiv-double-arrow h _)) =
+    coh-hom-fork-hom-double-arrow a a' c c' (hom-equiv-double-arrow a a' e) h
+```
diff --git a/src/foundation/equivalences-span-diagrams.lagda.md b/src/foundation/equivalences-span-diagrams.lagda.md
index 92238d6cff9..ca8b7fe1174 100644
--- a/src/foundation/equivalences-span-diagrams.lagda.md
+++ b/src/foundation/equivalences-span-diagrams.lagda.md
@@ -294,21 +294,25 @@ module _
     (𝒯 : span-diagram l1 l2 l3) → 𝒮 ＝ 𝒯 → equiv-span-diagram 𝒮 𝒯
   equiv-eq-span-diagram 𝒯 refl = id-equiv-span-diagram 𝒮
 
-  is-torsorial-equiv-span-diagram :
-    is-torsorial (equiv-span-diagram 𝒮)
-  is-torsorial-equiv-span-diagram =
-    is-torsorial-Eq-structure
-      ( is-torsorial-equiv (domain-span-diagram 𝒮))
-      ( domain-span-diagram 𝒮 , id-equiv)
-      ( is-torsorial-Eq-structure
-        ( is-torsorial-equiv (codomain-span-diagram 𝒮))
-        ( codomain-span-diagram 𝒮 , id-equiv)
-        ( is-torsorial-equiv-span (span-span-diagram 𝒮)))
-
-  is-equiv-equiv-eq-span-diagram :
-    (𝒯 : span-diagram l1 l2 l3) → is-equiv (equiv-eq-span-diagram 𝒯)
-  is-equiv-equiv-eq-span-diagram =
-    fundamental-theorem-id is-torsorial-equiv-span-diagram equiv-eq-span-diagram
+  abstract
+    is-torsorial-equiv-span-diagram :
+      is-torsorial (equiv-span-diagram {l1} {l2} {l3} {l1} {l2} {l3} 𝒮)
+    is-torsorial-equiv-span-diagram =
+      is-torsorial-Eq-structure
+        ( is-torsorial-equiv (domain-span-diagram 𝒮))
+        ( domain-span-diagram 𝒮 , id-equiv)
+        ( is-torsorial-Eq-structure
+          ( is-torsorial-equiv (codomain-span-diagram 𝒮))
+          ( codomain-span-diagram 𝒮 , id-equiv)
+          ( is-torsorial-equiv-span (span-span-diagram 𝒮)))
+
+  abstract
+    is-equiv-equiv-eq-span-diagram :
+      (𝒯 : span-diagram l1 l2 l3) → is-equiv (equiv-eq-span-diagram 𝒯)
+    is-equiv-equiv-eq-span-diagram =
+      fundamental-theorem-id
+        ( is-torsorial-equiv-span-diagram)
+        ( equiv-eq-span-diagram)
 
   extensionality-span-diagram :
     (𝒯 : span-diagram l1 l2 l3) → (𝒮 ＝ 𝒯) ≃ equiv-span-diagram 𝒮 𝒯
diff --git a/src/foundation/equivalences-spans.lagda.md b/src/foundation/equivalences-spans.lagda.md
index 4e804c318a2..b712f62b6f9 100644
--- a/src/foundation/equivalences-spans.lagda.md
+++ b/src/foundation/equivalences-spans.lagda.md
@@ -148,19 +148,22 @@ module _
   equiv-eq-span : (s t : span l3 A B) → s ＝ t → equiv-span s t
   equiv-eq-span s .s refl = id-equiv-span s
 
-  is-torsorial-equiv-span : (s : span l3 A B) → is-torsorial (equiv-span s)
-  is-torsorial-equiv-span s =
-    is-torsorial-Eq-structure
-      ( is-torsorial-equiv (spanning-type-span s))
-      ( spanning-type-span s , id-equiv)
-      ( is-torsorial-Eq-structure
-        ( is-torsorial-htpy (left-map-span s))
-        ( left-map-span s , refl-htpy)
-        ( is-torsorial-htpy (right-map-span s)))
-
-  is-equiv-equiv-eq-span : (c d : span l3 A B) → is-equiv (equiv-eq-span c d)
-  is-equiv-equiv-eq-span c =
-    fundamental-theorem-id (is-torsorial-equiv-span c) (equiv-eq-span c)
+  abstract
+    is-torsorial-equiv-span :
+      (s : span l3 A B) → is-torsorial (equiv-span {l1} {l2} {l3} {l3} s)
+    is-torsorial-equiv-span s =
+      is-torsorial-Eq-structure
+        ( is-torsorial-equiv (spanning-type-span s))
+        ( spanning-type-span s , id-equiv)
+        ( is-torsorial-Eq-structure
+          ( is-torsorial-htpy (left-map-span s))
+          ( left-map-span s , refl-htpy)
+          ( is-torsorial-htpy (right-map-span s)))
+
+  abstract
+    is-equiv-equiv-eq-span : (c d : span l3 A B) → is-equiv (equiv-eq-span c d)
+    is-equiv-equiv-eq-span c =
+      fundamental-theorem-id (is-torsorial-equiv-span c) (equiv-eq-span c)
 
   extensionality-span : (c d : span l3 A B) → (c ＝ d) ≃ (equiv-span c d)
   pr1 (extensionality-span c d) = equiv-eq-span c d
diff --git a/src/foundation/forks.lagda.md b/src/foundation/forks.lagda.md
new file mode 100644
index 00000000000..3b3b3785a2a
--- /dev/null
+++ b/src/foundation/forks.lagda.md
@@ -0,0 +1,608 @@
+# Forks
+
+```agda
+module foundation.forks where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.codiagonal-maps-of-types
+open import foundation.commuting-squares-of-maps
+open import foundation.commuting-triangles-of-maps
+open import foundation.cones-over-cospan-diagrams
+open import foundation.contractible-types
+open import foundation.cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equality-cartesian-product-types
+open import foundation.equality-of-equality-cartesian-product-types
+open import foundation.equivalences
+open import foundation.equivalences-cospan-diagrams
+open import foundation.equivalences-double-arrows
+open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.morphisms-cospan-diagrams
+open import foundation.morphisms-double-arrows
+open import foundation.structure-identity-principle
+open import foundation.torsorial-type-families
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.diagonal-maps-cartesian-products-of-types
+```
+
+</details>
+
+## Idea
+
+A {{#concept "fork" Disambiguation="of types" Agda=fork}} of a
+[double arrow](foundation.double-arrows.md) `f, g : A → B` with vertext `X` is a
+map `e : X → A` together with a [homotopy](foundation.homotopies.md)
+`H : f ∘ e ~ g ∘ e`. The name comes from the diagram
+
+```text
+                g
+      e      ------>
+ X ------> A         B
+             ------>
+                f
+```
+
+which looks like a fork.
+
+Forks are an analog of
+[cones over cospan diagrams](foundation.cones-over-cospan-diagrams.md) for
+double arrows. The universal fork of a double arrow is their equalizer.
+
+## Definitions
+
+### Forks
+
+```agda
+module _
+  {l1 l2 l3 : Level} (a : double-arrow l1 l2)
+  where
+
+  coherence-fork : {X : UU l3} → (X → domain-double-arrow a) → UU (l2 ⊔ l3)
+  coherence-fork e =
+    left-map-double-arrow a ∘ e ~
+    right-map-double-arrow a ∘ e
+
+  fork : UU l3 → UU (l1 ⊔ l2 ⊔ l3)
+  fork X = Σ (X → domain-double-arrow a) (coherence-fork)
+
+  module _
+    {X : UU l3} (e : fork X)
+    where
+
+    map-fork : X → domain-double-arrow a
+    map-fork = pr1 e
+
+    coh-fork : coherence-fork map-fork
+    coh-fork = pr2 e
+```
+
+### Homotopies of forks
+
+A homotopy between forks with the same vertex is given by a homotopy between the
+two maps, together with a coherence datum asserting that we may apply the given
+homotopy and the appropriate fork homotopy in either order.
+
+```agda
+module _
+  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  where
+
+  coherence-htpy-fork :
+    (e e' : fork a X) →
+    (K : map-fork a e ~ map-fork a e') →
+    UU (l2 ⊔ l3)
+  coherence-htpy-fork e e' K =
+    ( coh-fork a e ∙h right-map-double-arrow a ·l K) ~
+    ( left-map-double-arrow a ·l K ∙h coh-fork a e')
+
+  htpy-fork : fork a X → fork a X → UU (l1 ⊔ l2 ⊔ l3)
+  htpy-fork e e' =
+    Σ ( map-fork a e ~ map-fork a e')
+      ( coherence-htpy-fork e e')
+```
+
+### Precomposing forks
+
+Given a fork `e : X → A` and a map `h : X → Y`, we may compose the two to get a
+new fork `e ∘ h`.
+
+```text
+                          g
+      e         h      ------>
+ Y ------> X ------> A         B
+                       ------>
+                          f
+```
+
+```agda
+module _
+  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  (e : fork a X)
+  where
+
+  fork-map : {l : Level} {Y : UU l} → (Y → X) → fork a Y
+  pr1 (fork-map h) = map-fork a e ∘ h
+  pr2 (fork-map h) = coh-fork a e ·r h
+```
+
+## Properties
+
+### Characterization of identity types of forks
+
+```agda
+module _
+  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  where
+
+  refl-htpy-fork : (e : fork a X) → htpy-fork a e e
+  pr1 (refl-htpy-fork e) = refl-htpy
+  pr2 (refl-htpy-fork e) = right-unit-htpy
+
+  htpy-fork-eq :
+    (e e' : fork a X) → (e ＝ e') → htpy-fork a e e'
+  htpy-fork-eq e .e refl = refl-htpy-fork e
+
+  abstract
+    is-torsorial-htpy-fork :
+      (e : fork a X) → is-torsorial (htpy-fork a e)
+    is-torsorial-htpy-fork e =
+      is-torsorial-Eq-structure
+        ( is-torsorial-htpy (map-fork a e))
+        ( map-fork a e , refl-htpy)
+        ( is-contr-is-equiv'
+          ( Σ ( coherence-fork a (map-fork a e))
+              ( λ K → coh-fork a e ~ K))
+          ( tot (λ K M → right-unit-htpy ∙h M))
+          ( is-equiv-tot-is-fiberwise-equiv
+            ( is-equiv-concat-htpy right-unit-htpy))
+          ( is-torsorial-htpy (coh-fork a e)))
+
+  abstract
+    is-equiv-htpy-fork-eq :
+      (e e' : fork a X) → is-equiv (htpy-fork-eq e e')
+    is-equiv-htpy-fork-eq e =
+      fundamental-theorem-id (is-torsorial-htpy-fork e) (htpy-fork-eq e)
+
+  eq-htpy-fork : (e e' : fork a X) → htpy-fork a e e' → e ＝ e'
+  eq-htpy-fork e e' = map-inv-is-equiv (is-equiv-htpy-fork-eq e e')
+```
+
+### Precomposing a fork by identity is the identity
+
+```agda
+module _
+  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  (e : fork a X)
+  where
+
+  fork-map-id : fork-map a e id ＝ e
+  fork-map-id =
+    eq-htpy-fork a
+      ( fork-map a e id)
+      ( e)
+      ( ( refl-htpy) ,
+        ( right-unit-htpy ∙h
+          inv-left-unit-law-left-whisker-comp (coh-fork a e) ∙h
+          left-unit-law-left-whisker-comp (coh-fork a e)))
+```
+
+### Precomposing forks distributes over function composition
+
+```text
+                                 g
+      k        h        e      ----->
+  Z -----> Y -----> X -----> A        B
+                               ----->
+                                 f
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (a : double-arrow l1 l2)
+  {X : UU l3} {Y : UU l4} {Z : UU l5}
+  (e : fork a X)
+  where
+
+  fork-map-comp :
+    (h : Y → X) (k : Z → Y) →
+    fork-map a e (h ∘ k) ＝ fork-map a (fork-map a e h) k
+  fork-map-comp h k =
+    eq-htpy-fork a
+      ( fork-map a e (h ∘ k))
+      ( fork-map a (fork-map a e h) k)
+      ( refl-htpy , right-unit-htpy)
+```
+
+### Forks are special cases of cones over cospans
+
+The type of forks of a double arrow `f, g : A → B` is equivalent to the type of
+[cones](foundation.cones-over-cospan-diagrams.md) over the cospan
+
+```text
+       Δ           (f,g)
+  B ------> B × B <------ A.
+```
+
+```agda
+module _
+  {l1 l2 : Level} (a@(A , B , f , g) : double-arrow l1 l2)
+  where
+
+  vertical-map-cospan-cone-fork :
+    codomain-double-arrow a → codomain-double-arrow a × codomain-double-arrow a
+  vertical-map-cospan-cone-fork = diagonal-product (codomain-double-arrow a)
+
+  horizontal-map-cospan-cone-fork :
+    domain-double-arrow a → codomain-double-arrow a × codomain-double-arrow a
+  horizontal-map-cospan-cone-fork x =
+    ( left-map-double-arrow a x , right-map-double-arrow a x)
+
+  cospan-diagram-fork : cospan-diagram l1 l2 l2
+  cospan-diagram-fork =
+    make-cospan-diagram
+      ( horizontal-map-cospan-cone-fork)
+      ( vertical-map-cospan-cone-fork)
+
+module _
+  {l1 l2 l3 : Level} (a@(A , B , f , g) : double-arrow l1 l2) {X : UU l3}
+  where
+
+  fork-cone-diagonal :
+    cone
+      ( vertical-map-cospan-cone-fork a)
+      ( horizontal-map-cospan-cone-fork a)
+      ( X) →
+    fork a X
+  pr1 (fork-cone-diagonal (f' , g' , H)) = g'
+  pr2 (fork-cone-diagonal (f' , g' , H)) = inv-htpy (pr1 ·l H) ∙h pr2 ·l H
+
+  horizontal-map-cone-fork : fork a X → X → codomain-double-arrow a
+  horizontal-map-cone-fork e = left-map-double-arrow a ∘ map-fork a e
+
+  vertical-map-cone-fork : fork a X → X → domain-double-arrow a
+  vertical-map-cone-fork e = map-fork a e
+
+  coherence-square-cone-fork :
+    (e : fork a X) →
+    coherence-square-maps
+      ( vertical-map-cone-fork e)
+      ( horizontal-map-cone-fork e)
+      ( horizontal-map-cospan-cone-fork a)
+      ( vertical-map-cospan-cone-fork a)
+  coherence-square-cone-fork e x = eq-pair refl (coh-fork a e x)
+
+  cone-diagonal-fork :
+    fork a X →
+    cone
+      ( vertical-map-cospan-cone-fork a)
+      ( horizontal-map-cospan-cone-fork a)
+      ( X)
+  pr1 (cone-diagonal-fork e) = horizontal-map-cone-fork e
+  pr1 (pr2 (cone-diagonal-fork e)) = vertical-map-cone-fork e
+  pr2 (pr2 (cone-diagonal-fork e)) = coherence-square-cone-fork e
+
+  abstract
+    is-section-cone-diagonal-fork :
+      fork-cone-diagonal ∘ cone-diagonal-fork ~ id
+    is-section-cone-diagonal-fork e =
+      eq-htpy-fork a
+        ( fork-cone-diagonal (cone-diagonal-fork e))
+        ( e)
+        ( refl-htpy ,
+          ( λ x →
+            right-unit ∙
+            ap-binary
+              ( _∙_)
+              ( ap inv (ap-pr1-ap-pair (coh-fork a e x)))
+              ( ap-pr2-eq-pair refl (coh-fork a e x))))
+
+  abstract
+    is-retraction-cone-diagonal-fork' :
+      id ~ cone-diagonal-fork ∘ fork-cone-diagonal
+    is-retraction-cone-diagonal-fork' c@(f' , g' , H) =
+      eq-htpy-cone
+        ( vertical-map-cospan-cone-fork a)
+        ( horizontal-map-cospan-cone-fork a)
+        ( c)
+        ( cone-diagonal-fork (fork-cone-diagonal c))
+        ( pr1 ·l H ,
+          refl-htpy ,
+          λ x →
+          eq-pair²
+            ( ( equational-reasoning
+                ap pr1 (H x ∙ refl)
+                ＝ ap pr1 (H x) ∙ refl
+                  by ap-concat pr1 (H x) refl
+                ＝
+                  ( ap pr1 (ap (diagonal-product B) (ap pr1 (H x)))) ∙
+                  ( ap pr1
+                    ( ap
+                      ( left-map-double-arrow a (g' x) ,_)
+                      ( inv (ap pr1 (H x)) ∙ ap pr2 (H x))))
+                  by
+                  ap-binary
+                    ( _∙_)
+                    ( inv-ap-id (ap pr1 (H x)) ∙
+                      ap-comp pr1 (diagonal-product B) (ap pr1 (H x)))
+                    ( inv-ap-pr1-ap-pair (inv (ap pr1 (H x)) ∙ ap pr2 (H x)))
+                ＝
+                  ap
+                    ( pr1)
+                    ( ap (diagonal-product B) (ap pr1 (H x)) ∙
+                      ap
+                        ( left-map-double-arrow a (g' x) ,_)
+                        ( inv (ap pr1 (H x)) ∙ ap pr2 (H x)))
+                  by
+                  inv-ap-concat
+                    ( pr1)
+                    ( ap (diagonal-product B) (ap pr1 (H x)))
+                    ( ap
+                      ( left-map-double-arrow a (g' x) ,_)
+                      ( inv (ap pr1 (H x)) ∙ ap pr2 (H x)))) ,
+              ( equational-reasoning
+                ap pr2 (H x ∙ refl)
+                ＝ ap pr2 (H x)
+                  by ap (ap pr2) right-unit
+                ＝ ap pr1 (H x) ∙ (inv (ap pr1 (H x)) ∙ ap pr2 (H x))
+                  by inv (is-section-inv-concat (ap pr1 (H x)) (ap pr2 (H x)))
+                ＝ ap pr2 (ap (diagonal-product B) (ap pr1 (H x))) ∙
+                  ap
+                    ( pr2)
+                    ( ap
+                      ( left-map-double-arrow a (g' x) ,_)
+                      ( inv (ap pr1 (H x)) ∙ ap pr2 (H x)))
+                  by
+                  ap-binary
+                    ( _∙_)
+                    ( ( inv-ap-id (ap pr1 (H x))) ∙
+                      ( ap-comp pr2 (diagonal-product B) (ap pr1 (H x))))
+                    ( inv-ap-pr2-ap-pair (inv (ap pr1 (H x)) ∙ ap pr2 (H x)))
+                ＝
+                  ( ap pr2
+                    ( ( ap (diagonal-product B) (ap pr1 (H x))) ∙
+                      ( ap
+                        ( left-map-double-arrow a (g' x) ,_)
+                        ( inv (ap pr1 (H x)) ∙ ap pr2 (H x)))))
+                  by
+                  inv-ap-concat
+                    ( pr2)
+                    ( ap (diagonal-product B) (ap pr1 (H x)))
+                    ( ap
+                      ( left-map-double-arrow a (g' x) ,_)
+                      ( inv (ap pr1 (H x)) ∙ ap pr2 (H x))))))
+
+    is-retraction-cone-diagonal-fork :
+      cone-diagonal-fork ∘ fork-cone-diagonal ~ id
+    is-retraction-cone-diagonal-fork =
+      inv-htpy is-retraction-cone-diagonal-fork'
+
+  is-equiv-fork-cone-diagonal :
+    is-equiv fork-cone-diagonal
+  is-equiv-fork-cone-diagonal =
+    is-equiv-is-invertible
+      ( cone-diagonal-fork)
+      ( is-section-cone-diagonal-fork)
+      ( is-retraction-cone-diagonal-fork)
+
+  equiv-cone-diagonal-fork :
+    cone
+      ( vertical-map-cospan-cone-fork a)
+      ( horizontal-map-cospan-cone-fork a)
+      ( X) ≃
+    fork a X
+  pr1 equiv-cone-diagonal-fork = fork-cone-diagonal
+  pr2 equiv-cone-diagonal-fork = is-equiv-fork-cone-diagonal
+
+module _
+  {l1 l2 : Level} (a@(A , B , f , g) : double-arrow l1 l2)
+  where
+
+  abstract
+    triangle-fork-cone :
+      {l3 l4 : Level} {X : UU l3} {Y : UU l4} →
+      (e : fork a X) →
+      coherence-triangle-maps
+        ( fork-map a e {Y = Y})
+        ( fork-cone-diagonal a)
+        ( cone-map
+          ( vertical-map-cospan-cone-fork a)
+          ( horizontal-map-cospan-cone-fork a)
+          ( cone-diagonal-fork a e))
+    triangle-fork-cone e h =
+      eq-htpy-fork a
+        ( fork-map a e h)
+        ( fork-cone-diagonal
+          ( a)
+          ( cone-map
+            ( vertical-map-cospan-cone-fork a)
+            ( horizontal-map-cospan-cone-fork a)
+            ( cone-diagonal-fork a e)
+            ( h)))
+        ( refl-htpy ,
+          λ x →
+          equational-reasoning
+            coh-fork a e (h x) ∙ refl
+            ＝ coh-fork a e (h x) by right-unit
+            ＝ inv
+                ( ap
+                  ( pr1)
+                  ( ap
+                    ( left-map-double-arrow a (map-fork a e (h x)) ,_)
+                    ( coh-fork a e (h x)))) ∙
+                ( ap
+                    ( pr2)
+                    ( ap
+                      ( left-map-double-arrow a (map-fork a e (h x)) ,_)
+                      ( coh-fork a e (h x))))
+              by
+              ap-binary
+                ( _∙_)
+                ( ap inv (inv-ap-pr1-ap-pair (coh-fork a e (h x))))
+                ( inv-ap-pr2-ap-pair (coh-fork a e (h x))))
+```
+
+### Morphisms between double arrows induce morphisms between fork cospan diagrams
+
+A [morphism of double arrows](foundation.morphisms-double-arrows.md)
+
+```text
+           i
+     A --------> X
+    | |         | |
+  f | | g     h | | k
+    | |         | |
+    ∨ ∨         ∨ ∨
+     B --------> Y
+           j
+```
+
+induces a [morphism of cospan diagrams](foundation.morphisms-cospan-diagrams.md)
+
+```text
+        (f,g)             Δ
+    A --------> B × B <-------- B
+    |             |             |
+  i |             | j × j       | j
+    ∨             ∨             ∨
+    X --------> Y × Y <-------- Y
+        (h,k)             Δ
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) (a' : double-arrow l3 l4)
+  (h : hom-double-arrow a a')
+  where
+
+  cospanning-map-hom-cospan-diagram-fork-hom-double-arrow :
+    codomain-double-arrow a × codomain-double-arrow a →
+    codomain-double-arrow a' × codomain-double-arrow a'
+  cospanning-map-hom-cospan-diagram-fork-hom-double-arrow =
+    map-product
+      ( codomain-map-hom-double-arrow a a' h)
+      ( codomain-map-hom-double-arrow a a' h)
+
+  left-square-hom-cospan-diagram-fork-hom-double-arrow :
+    coherence-square-maps
+      ( horizontal-map-cospan-cone-fork a)
+      ( domain-map-hom-double-arrow a a' h)
+      ( cospanning-map-hom-cospan-diagram-fork-hom-double-arrow)
+      ( horizontal-map-cospan-cone-fork a')
+  left-square-hom-cospan-diagram-fork-hom-double-arrow x =
+    inv
+      ( eq-pair
+        ( left-square-hom-double-arrow a a' h x)
+        ( right-square-hom-double-arrow a a' h x))
+
+  right-square-hom-cospan-diagram-fork-hom-double-arrow :
+    coherence-square-maps
+        ( vertical-map-cospan-cone-fork a)
+        ( codomain-map-hom-double-arrow a a' h)
+        ( cospanning-map-hom-cospan-diagram-fork-hom-double-arrow)
+        ( vertical-map-cospan-cone-fork a')
+  right-square-hom-cospan-diagram-fork-hom-double-arrow = refl-htpy
+
+  hom-cospan-diagram-fork-hom-double-arrow :
+    hom-cospan-diagram (cospan-diagram-fork a) (cospan-diagram-fork a')
+  pr1 hom-cospan-diagram-fork-hom-double-arrow =
+    domain-map-hom-double-arrow a a' h
+  pr1 (pr2 hom-cospan-diagram-fork-hom-double-arrow) =
+    codomain-map-hom-double-arrow a a' h
+  pr1 (pr2 (pr2 hom-cospan-diagram-fork-hom-double-arrow)) =
+    cospanning-map-hom-cospan-diagram-fork-hom-double-arrow
+  pr1 (pr2 (pr2 (pr2 hom-cospan-diagram-fork-hom-double-arrow))) =
+    left-square-hom-cospan-diagram-fork-hom-double-arrow
+  pr2 (pr2 (pr2 (pr2 hom-cospan-diagram-fork-hom-double-arrow))) =
+    right-square-hom-cospan-diagram-fork-hom-double-arrow
+```
+
+### Equivalences between double arrows induce equivalences between fork cospan diagrams
+
+An [equivalence of double arrows](foundation.equivalences-double-arrows.md)
+
+```text
+           i
+     A --------> X
+    | |    ≃    | |
+  f | | g     h | | k
+    | |         | |
+    ∨ ∨    ≃    ∨ ∨
+     B --------> Y
+           j
+```
+
+induces an
+[equivalence of cospan diagrams](foundation.equivalences-cospan-diagrams.md)
+
+```text
+        (f,g)             Δ
+    A --------> B × B <-------- B
+    |             |             |
+  i | ≃         ≃ | j × j     ≃ | j
+    ∨             ∨             ∨
+    X --------> Y × Y <-------- Y
+        (h,k)             Δ
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) (a' : double-arrow l3 l4)
+  (e : equiv-double-arrow a a')
+  where
+
+  cospanning-equiv-equiv-cospan-diagram-fork-equiv-double-arrow :
+    codomain-double-arrow a × codomain-double-arrow a ≃
+    codomain-double-arrow a' × codomain-double-arrow a'
+  cospanning-equiv-equiv-cospan-diagram-fork-equiv-double-arrow =
+    equiv-product
+      ( codomain-equiv-equiv-double-arrow a a' e)
+      ( codomain-equiv-equiv-double-arrow a a' e)
+
+  left-square-equiv-cospan-diagram-fork-equiv-double-arrow :
+    coherence-square-maps
+      ( horizontal-map-cospan-cone-fork a)
+      ( domain-map-equiv-double-arrow a a' e)
+      ( map-equiv cospanning-equiv-equiv-cospan-diagram-fork-equiv-double-arrow)
+      ( horizontal-map-cospan-cone-fork a')
+  left-square-equiv-cospan-diagram-fork-equiv-double-arrow =
+    left-square-hom-cospan-diagram-fork-hom-double-arrow a a'
+      ( hom-equiv-double-arrow a a' e)
+
+  right-square-equiv-cospan-diagram-fork-equiv-double-arrow :
+    coherence-square-maps'
+      ( vertical-map-cospan-cone-fork a)
+      ( codomain-map-equiv-double-arrow a a' e)
+      ( map-equiv cospanning-equiv-equiv-cospan-diagram-fork-equiv-double-arrow)
+      ( vertical-map-cospan-cone-fork a')
+  right-square-equiv-cospan-diagram-fork-equiv-double-arrow =
+    right-square-hom-cospan-diagram-fork-hom-double-arrow a a'
+      ( hom-equiv-double-arrow a a' e)
+
+  equiv-cospan-diagram-fork-equiv-double-arrow :
+    equiv-cospan-diagram (cospan-diagram-fork a) (cospan-diagram-fork a')
+  pr1 equiv-cospan-diagram-fork-equiv-double-arrow =
+    domain-equiv-equiv-double-arrow a a' e
+  pr1 (pr2 equiv-cospan-diagram-fork-equiv-double-arrow) =
+    codomain-equiv-equiv-double-arrow a a' e
+  pr1 (pr2 (pr2 equiv-cospan-diagram-fork-equiv-double-arrow)) =
+    cospanning-equiv-equiv-cospan-diagram-fork-equiv-double-arrow
+  pr1 (pr2 (pr2 (pr2 equiv-cospan-diagram-fork-equiv-double-arrow))) =
+    left-square-equiv-cospan-diagram-fork-equiv-double-arrow
+  pr2 (pr2 (pr2 (pr2 equiv-cospan-diagram-fork-equiv-double-arrow))) =
+    right-square-equiv-cospan-diagram-fork-equiv-double-arrow
+```
diff --git a/src/foundation/homotopies-morphisms-cospan-diagrams.lagda.md b/src/foundation/homotopies-morphisms-cospan-diagrams.lagda.md
index 0b4e7d6bb55..6eae5c3328a 100644
--- a/src/foundation/homotopies-morphisms-cospan-diagrams.lagda.md
+++ b/src/foundation/homotopies-morphisms-cospan-diagrams.lagda.md
@@ -69,8 +69,8 @@ module _
 
   left-square-coherence-htpy-hom-cospan-diagram :
     (h h' : hom-cospan-diagram 𝒮 𝒯) →
-    left-map-hom-cospan-diagram 𝒮 𝒯 h ~
-    left-map-hom-cospan-diagram 𝒮 𝒯 h' →
+    map-domain-hom-cospan-diagram 𝒮 𝒯 h ~
+    map-domain-hom-cospan-diagram 𝒮 𝒯 h' →
     cospanning-map-hom-cospan-diagram 𝒮 𝒯 h ~
     cospanning-map-hom-cospan-diagram 𝒮 𝒯 h' → UU (l1 ⊔ l3')
   left-square-coherence-htpy-hom-cospan-diagram h h' L C =
@@ -82,8 +82,8 @@ module _
 
   right-square-coherence-htpy-hom-cospan-diagram :
     (h h' : hom-cospan-diagram 𝒮 𝒯) →
-    right-map-hom-cospan-diagram 𝒮 𝒯 h ~
-    right-map-hom-cospan-diagram 𝒮 𝒯 h' →
+    map-codomain-hom-cospan-diagram 𝒮 𝒯 h ~
+    map-codomain-hom-cospan-diagram 𝒮 𝒯 h' →
     cospanning-map-hom-cospan-diagram 𝒮 𝒯 h ~
     cospanning-map-hom-cospan-diagram 𝒮 𝒯 h' → UU (l2 ⊔ l3')
   right-square-coherence-htpy-hom-cospan-diagram h h' R C =
@@ -95,10 +95,10 @@ module _
 
   coherence-htpy-hom-cospan-diagram :
     (h h' : hom-cospan-diagram 𝒮 𝒯) →
-    left-map-hom-cospan-diagram 𝒮 𝒯 h ~
-    left-map-hom-cospan-diagram 𝒮 𝒯 h' →
-    right-map-hom-cospan-diagram 𝒮 𝒯 h ~
-    right-map-hom-cospan-diagram 𝒮 𝒯 h' →
+    map-domain-hom-cospan-diagram 𝒮 𝒯 h ~
+    map-domain-hom-cospan-diagram 𝒮 𝒯 h' →
+    map-codomain-hom-cospan-diagram 𝒮 𝒯 h ~
+    map-codomain-hom-cospan-diagram 𝒮 𝒯 h' →
     cospanning-map-hom-cospan-diagram 𝒮 𝒯 h ~
     cospanning-map-hom-cospan-diagram 𝒮 𝒯 h' → UU (l1 ⊔ l2 ⊔ l3')
   coherence-htpy-hom-cospan-diagram h h' L R C =
@@ -108,11 +108,11 @@ module _
   htpy-hom-cospan-diagram :
     (h h' : hom-cospan-diagram 𝒮 𝒯) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l1' ⊔ l2' ⊔ l3')
   htpy-hom-cospan-diagram h h' =
-    Σ ( left-map-hom-cospan-diagram 𝒮 𝒯 h ~
-        left-map-hom-cospan-diagram 𝒮 𝒯 h')
+    Σ ( map-domain-hom-cospan-diagram 𝒮 𝒯 h ~
+        map-domain-hom-cospan-diagram 𝒮 𝒯 h')
       ( λ L →
-        Σ ( right-map-hom-cospan-diagram 𝒮 𝒯 h ~
-            right-map-hom-cospan-diagram 𝒮 𝒯 h')
+        Σ ( map-codomain-hom-cospan-diagram 𝒮 𝒯 h ~
+            map-codomain-hom-cospan-diagram 𝒮 𝒯 h')
           ( λ R →
             Σ ( cospanning-map-hom-cospan-diagram 𝒮 𝒯 h ~
                 cospanning-map-hom-cospan-diagram 𝒮 𝒯 h')
@@ -127,11 +127,13 @@ module _
   where
 
   htpy-left-map-htpy-hom-cospan-diagram :
-    left-map-hom-cospan-diagram 𝒮 𝒯 h ~ left-map-hom-cospan-diagram 𝒮 𝒯 h'
+    map-domain-hom-cospan-diagram 𝒮 𝒯 h ~
+    map-domain-hom-cospan-diagram 𝒮 𝒯 h'
   htpy-left-map-htpy-hom-cospan-diagram = pr1 H
 
   htpy-right-map-htpy-hom-cospan-diagram :
-    right-map-hom-cospan-diagram 𝒮 𝒯 h ~ right-map-hom-cospan-diagram 𝒮 𝒯 h'
+    map-codomain-hom-cospan-diagram 𝒮 𝒯 h ~
+    map-codomain-hom-cospan-diagram 𝒮 𝒯 h'
   htpy-right-map-htpy-hom-cospan-diagram = pr1 (pr2 H)
 
   htpy-cospanning-map-htpy-hom-cospan-diagram :
@@ -183,11 +185,11 @@ module _
     (h : hom-cospan-diagram 𝒮 𝒯) → is-torsorial (htpy-hom-cospan-diagram 𝒮 𝒯 h)
   is-torsorial-htpy-hom-cospan-diagram h =
     is-torsorial-Eq-structure
-      ( is-torsorial-htpy (left-map-hom-cospan-diagram 𝒮 𝒯 h))
-      ( left-map-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy)
+      ( is-torsorial-htpy (map-domain-hom-cospan-diagram 𝒮 𝒯 h))
+      ( map-domain-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy)
       ( is-torsorial-Eq-structure
-        ( is-torsorial-htpy (right-map-hom-cospan-diagram 𝒮 𝒯 h))
-        ( right-map-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy)
+        ( is-torsorial-htpy (map-codomain-hom-cospan-diagram 𝒮 𝒯 h))
+        ( map-codomain-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy)
         ( is-torsorial-Eq-structure
           ( is-torsorial-htpy (cospanning-map-hom-cospan-diagram 𝒮 𝒯 h))
           ( cospanning-map-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy)
diff --git a/src/foundation/morphisms-cospan-diagrams.lagda.md b/src/foundation/morphisms-cospan-diagrams.lagda.md
index d1e4aa62c21..2f92052155b 100644
--- a/src/foundation/morphisms-cospan-diagrams.lagda.md
+++ b/src/foundation/morphisms-cospan-diagrams.lagda.md
@@ -9,6 +9,7 @@ module foundation.morphisms-cospan-diagrams where
 ```agda
 open import foundation.cospan-diagrams
 open import foundation.dependent-pair-types
+open import foundation.morphisms-arrows
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
@@ -58,27 +59,57 @@ module _
   (h : hom-cospan-diagram 𝒮 𝒯)
   where
 
-  left-map-hom-cospan-diagram :
-    left-type-cospan-diagram 𝒮 → left-type-cospan-diagram 𝒯
-  left-map-hom-cospan-diagram = pr1 h
+  map-domain-hom-cospan-diagram :
+    domain-cospan-diagram 𝒮 → domain-cospan-diagram 𝒯
+  map-domain-hom-cospan-diagram = pr1 h
 
-  right-map-hom-cospan-diagram :
-    right-type-cospan-diagram 𝒮 → right-type-cospan-diagram 𝒯
-  right-map-hom-cospan-diagram = pr1 (pr2 h)
+  map-codomain-hom-cospan-diagram :
+    codomain-cospan-diagram 𝒮 → codomain-cospan-diagram 𝒯
+  map-codomain-hom-cospan-diagram = pr1 (pr2 h)
 
   cospanning-map-hom-cospan-diagram :
     cospanning-type-cospan-diagram 𝒮 → cospanning-type-cospan-diagram 𝒯
   cospanning-map-hom-cospan-diagram = pr1 (pr2 (pr2 h))
 
   left-square-hom-cospan-diagram :
-    left-map-cospan-diagram 𝒯 ∘ left-map-hom-cospan-diagram ~
+    left-map-cospan-diagram 𝒯 ∘ map-domain-hom-cospan-diagram ~
     cospanning-map-hom-cospan-diagram ∘ left-map-cospan-diagram 𝒮
   left-square-hom-cospan-diagram = pr1 (pr2 (pr2 (pr2 h)))
 
   right-square-hom-cospan-diagram :
-    right-map-cospan-diagram 𝒯 ∘ right-map-hom-cospan-diagram ~
+    right-map-cospan-diagram 𝒯 ∘ map-codomain-hom-cospan-diagram ~
     cospanning-map-hom-cospan-diagram ∘ right-map-cospan-diagram 𝒮
   right-square-hom-cospan-diagram = pr2 (pr2 (pr2 (pr2 h)))
+
+  hom-left-arrow-hom-cospan-diagram' :
+    hom-arrow' (left-map-cospan-diagram 𝒮) (left-map-cospan-diagram 𝒯)
+  hom-left-arrow-hom-cospan-diagram' =
+    ( map-domain-hom-cospan-diagram ,
+      cospanning-map-hom-cospan-diagram ,
+      left-square-hom-cospan-diagram)
+
+  hom-right-arrow-hom-cospan-diagram' :
+    hom-arrow' (right-map-cospan-diagram 𝒮) (right-map-cospan-diagram 𝒯)
+  hom-right-arrow-hom-cospan-diagram' =
+    ( map-codomain-hom-cospan-diagram ,
+      cospanning-map-hom-cospan-diagram ,
+      right-square-hom-cospan-diagram)
+
+  hom-left-arrow-hom-cospan-diagram :
+    hom-arrow (left-map-cospan-diagram 𝒮) (left-map-cospan-diagram 𝒯)
+  hom-left-arrow-hom-cospan-diagram =
+    hom-arrow-hom-arrow'
+      ( left-map-cospan-diagram 𝒮)
+      ( left-map-cospan-diagram 𝒯)
+      ( hom-left-arrow-hom-cospan-diagram')
+
+  hom-right-arrow-hom-cospan-diagram :
+    hom-arrow (right-map-cospan-diagram 𝒮) (right-map-cospan-diagram 𝒯)
+  hom-right-arrow-hom-cospan-diagram =
+    hom-arrow-hom-arrow'
+      ( right-map-cospan-diagram 𝒮)
+      ( right-map-cospan-diagram 𝒯)
+      ( hom-right-arrow-hom-cospan-diagram')
 ```
 
 ### Identity morphisms of cospan diagrams
@@ -131,11 +162,11 @@ module _
   hom-cospan-diagram-rotate :
     (h : hom-cospan-diagram 𝒯 𝒮) (h' : hom-cospan-diagram ℛ 𝒮) →
     hom-cospan-diagram
-      ( left-type-cospan-diagram 𝒯 ,
-        left-type-cospan-diagram ℛ ,
-        left-type-cospan-diagram 𝒮 ,
-        left-map-hom-cospan-diagram 𝒯 𝒮 h ,
-        left-map-hom-cospan-diagram ℛ 𝒮 h')
+      ( domain-cospan-diagram 𝒯 ,
+        domain-cospan-diagram ℛ ,
+        domain-cospan-diagram 𝒮 ,
+        map-domain-hom-cospan-diagram 𝒯 𝒮 h ,
+        map-domain-hom-cospan-diagram ℛ 𝒮 h')
       ( codomain-hom-cospan-diagram-rotate h h')
   hom-cospan-diagram-rotate
     ( hA , hB , hX , HA , HB)
@@ -149,11 +180,11 @@ module _
   hom-cospan-diagram-rotate' :
     (h : hom-cospan-diagram 𝒯 𝒮) (h' : hom-cospan-diagram ℛ 𝒮) →
     hom-cospan-diagram
-      ( right-type-cospan-diagram 𝒯 ,
-        right-type-cospan-diagram ℛ ,
-        right-type-cospan-diagram 𝒮 ,
-        right-map-hom-cospan-diagram 𝒯 𝒮 h ,
-        right-map-hom-cospan-diagram ℛ 𝒮 h')
+      ( codomain-cospan-diagram 𝒯 ,
+        codomain-cospan-diagram ℛ ,
+        codomain-cospan-diagram 𝒮 ,
+        map-codomain-hom-cospan-diagram 𝒯 𝒮 h ,
+        map-codomain-hom-cospan-diagram ℛ 𝒮 h')
       ( codomain-hom-cospan-diagram-rotate h h')
   hom-cospan-diagram-rotate'
     ( hA , hB , hX , HA , HB)
diff --git a/src/foundation/morphisms-cospans.lagda.md b/src/foundation/morphisms-cospans.lagda.md
index b3cdf33eb6a..5780e800bbd 100644
--- a/src/foundation/morphisms-cospans.lagda.md
+++ b/src/foundation/morphisms-cospans.lagda.md
@@ -19,9 +19,9 @@ open import foundation-core.commuting-triangles-of-maps
 
 ## Idea
 
-Consider two [cospans](foundation.cospans.md) `c := (X , f , g)` and
-`d := (Y , h , k)` from `A` to `B`. A
-{{#concept "morphism of cospans" Agda=hom-cospan}} from `c` to `d` consists of a
+Consider two [cospans](foundation.cospans.md) `s := (X , f , g)` and
+`t := (Y , h , k)` from `A` to `B`. A
+{{#concept "morphism of cospans" Agda=hom-cospan}} from `s` to `t` consists of a
 map `u : X → Y` equipped with [homotopies](foundation-core.homotopies.md)
 witnessing that the two triangles
 
@@ -43,17 +43,40 @@ witnessing that the two triangles
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
-  (c : cospan l3 A B) (d : cospan l4 A B)
+  (s : cospan l3 A B) (t : cospan l4 A B)
   where
 
+  left-coherence-hom-cospan :
+    (cospanning-type-cospan s → cospanning-type-cospan t) → UU (l1 ⊔ l4)
+  left-coherence-hom-cospan h =
+    coherence-triangle-maps (left-map-cospan t) h (left-map-cospan s)
+
+  right-coherence-hom-cospan :
+    (cospanning-type-cospan s → cospanning-type-cospan t) → UU (l2 ⊔ l4)
+  right-coherence-hom-cospan h =
+    coherence-triangle-maps (right-map-cospan t) h (right-map-cospan s)
+
   coherence-hom-cospan :
-    (codomain-cospan c → codomain-cospan d) → UU (l1 ⊔ l2 ⊔ l4)
-  coherence-hom-cospan h =
-    ( coherence-triangle-maps (left-map-cospan d) h (left-map-cospan c)) ×
-    ( coherence-triangle-maps (right-map-cospan d) h (right-map-cospan c))
+    (cospanning-type-cospan s → cospanning-type-cospan t) → UU (l1 ⊔ l2 ⊔ l4)
+  coherence-hom-cospan f =
+    left-coherence-hom-cospan f × right-coherence-hom-cospan f
 
   hom-cospan : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   hom-cospan =
-    Σ ( codomain-cospan c → codomain-cospan d)
+    Σ ( cospanning-type-cospan s → cospanning-type-cospan t)
       ( coherence-hom-cospan)
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
+  (s : cospan l3 A B) (t : cospan l4 A B) (f : hom-cospan s t)
+  where
+
+  map-hom-cospan : cospanning-type-cospan s → cospanning-type-cospan t
+  map-hom-cospan = pr1 f
+
+  left-triangle-hom-cospan : left-coherence-hom-cospan s t map-hom-cospan
+  left-triangle-hom-cospan = pr1 (pr2 f)
+
+  right-triangle-hom-cospan : right-coherence-hom-cospan s t map-hom-cospan
+  right-triangle-hom-cospan = pr2 (pr2 f)
 ```
diff --git a/src/foundation/morphisms-forks-over-morphisms-double-arrows.lagda.md b/src/foundation/morphisms-forks-over-morphisms-double-arrows.lagda.md
new file mode 100644
index 00000000000..e9a62dd0ea0
--- /dev/null
+++ b/src/foundation/morphisms-forks-over-morphisms-double-arrows.lagda.md
@@ -0,0 +1,185 @@
+# Morphisms of forks over morphisms of double arrows
+
+```agda
+module foundation.morphisms-forks-over-morphisms-double-arrows where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.forks
+open import foundation.homotopies
+open import foundation.morphisms-arrows
+open import foundation.morphisms-double-arrows
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+```
+
+</details>
+
+## Idea
+
+Consider two [double arrows](foundation.double-arrows.md) `f, g : A → B` and
+`h, k : U → V`, equipped with [forks](foundation.forks.md) `c : X → A` and
+`c' : Y → U`, respectively, and a
+[morphism of double arrows](foundation.morphisms-double-arrows.md)
+`e : (f, g) → (h, k)`.
+
+Then a
+{{#concept "morphism of forks" Disambiguation="over a morphism of double arrows" Agda=hom-fork-hom-double-arrow}}
+over `e` is a triple `(m, H, K)`, with `m : X → Y` a map of vertices of the
+forks, `H` a [homotopy](foundation-core.homotopies.md) witnessing that the top
+square in the diagram
+
+```text
+           m
+     X --------> Y
+     |           |
+   c |           | c'
+     |           |
+     ∨     i     ∨
+     A --------> U
+    | |         | |
+  f | | g     h | | k
+    | |         | |
+    ∨ ∨         ∨ ∨
+     B --------> V
+           j
+```
+
+[commutes](foundation-core.commuting-squares-of-maps.md), and `K` a coherence
+datum "filling the inside" --- we have two stacks of squares
+
+```text
+           m                        m
+     X --------> Y            X --------> Y
+     |           |            |           |
+   c |           | c'       c |           | c'
+     |           |            |           |
+     ∨     i     ∨            ∨     i     ∨
+     A --------> U            A --------> U
+     |           |            |           |
+   f |           | h        g |           | k
+     |           |            |           |
+     ∨           ∨            ∨           ∨
+     B --------> V            B --------> V
+           j                        j
+```
+
+which share the top map `i` and the bottom square, and the coherences of `c` and
+`c'` filling the sides; that gives the homotopies
+
+```text
+                                               m                 m
+     X                 X                 X --------> Y     X --------> Y
+     |                 |                             |                 |
+   c |               c |                             | c'              | c'
+     |                 |                             |                 |
+     ∨                 ∨     i                       ∨                 ∨
+     A        ~        A --------> U        ~        U        ~        U
+     |                             |                 |                 |
+   f |                             | h               | h               | k
+     |                             |                 |                 |
+     ∨                             ∨                 ∨                 ∨
+     B --------> V                 V                 V                 V
+           j
+```
+
+and
+
+```text
+                                                                 m
+     X                 X                 X                 X --------> Y
+     |                 |                 |                             |
+   c |               c |               c |                             | c'
+     |                 |                 |                             |
+     ∨                 ∨                 ∨     i                       ∨
+     A        ~        A        ~        A --------> U        ~        U
+     |                 |                             |                 |
+   f |               g |                             | k               | k
+     |                 |                             |                 |
+     ∨                 ∨                             ∨                 ∨
+     B --------> Y     B --------> V                 V                 V ,
+           j                 j
+```
+
+which are required to be homotopic.
+
+## Definitions
+
+### Morphisms of forks over morphisms of double arrows
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (a : double-arrow l1 l2) (a' : double-arrow l4 l5)
+  {X : UU l3} {Y : UU l6}
+  (c : fork a X) (c' : fork a' Y)
+  (h : hom-double-arrow a a')
+  where
+
+  coherence-map-fork-hom-fork-hom-double-arrow : (X → Y) → UU (l3 ⊔ l4)
+  coherence-map-fork-hom-fork-hom-double-arrow u =
+    coherence-square-maps
+      ( u)
+      ( map-fork a c)
+      ( map-fork a' c')
+      ( domain-map-hom-double-arrow a a' h)
+
+  coherence-hom-fork-hom-double-arrow :
+    (u : X → Y) → coherence-map-fork-hom-fork-hom-double-arrow u →
+    UU (l3 ⊔ l5)
+  coherence-hom-fork-hom-double-arrow u H =
+    ( left-square-hom-double-arrow a a' h ·r map-fork a c) ∙h
+    ( ( left-map-double-arrow a' ·l H) ∙h
+      ( coh-fork a' c' ·r u)) ~
+    ( codomain-map-hom-double-arrow a a' h ·l coh-fork a c) ∙h
+    ( ( right-square-hom-double-arrow a a' h ·r map-fork a c) ∙h
+      ( right-map-double-arrow a' ·l H))
+
+  hom-fork-hom-double-arrow : UU (l3 ⊔ l4 ⊔ l5 ⊔ l6)
+  hom-fork-hom-double-arrow =
+    Σ ( X → Y)
+      ( λ u →
+        Σ ( coherence-map-fork-hom-fork-hom-double-arrow u)
+          ( coherence-hom-fork-hom-double-arrow u))
+```
+
+### Components of a morphism of forks over a morphism of double arrows
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (a : double-arrow l1 l2) (a' : double-arrow l4 l5)
+  {X : UU l3} {Y : UU l6}
+  (c : fork a X) (c' : fork a' Y)
+  (h : hom-double-arrow a a')
+  (m : hom-fork-hom-double-arrow a a' c c' h)
+  where
+
+  map-hom-fork-hom-double-arrow : X → Y
+  map-hom-fork-hom-double-arrow = pr1 m
+
+  coh-map-fork-hom-fork-hom-double-arrow :
+    coherence-map-fork-hom-fork-hom-double-arrow a a' c c' h
+      ( map-hom-fork-hom-double-arrow)
+  coh-map-fork-hom-fork-hom-double-arrow = pr1 (pr2 m)
+
+  hom-map-fork-hom-fork-hom-double-arrow :
+    hom-arrow (map-fork a c) (map-fork a' c')
+  pr1 hom-map-fork-hom-fork-hom-double-arrow =
+    map-hom-fork-hom-double-arrow
+  pr1 (pr2 hom-map-fork-hom-fork-hom-double-arrow) =
+    domain-map-hom-double-arrow a a' h
+  pr2 (pr2 hom-map-fork-hom-fork-hom-double-arrow) =
+    coh-map-fork-hom-fork-hom-double-arrow
+
+  coh-hom-fork-hom-double-arrow :
+    coherence-hom-fork-hom-double-arrow a a' c c' h
+      ( map-hom-fork-hom-double-arrow)
+      ( coh-map-fork-hom-fork-hom-double-arrow)
+  coh-hom-fork-hom-double-arrow = pr2 (pr2 m)
+```
diff --git a/src/foundation/operations-cospan-diagrams.lagda.md b/src/foundation/operations-cospan-diagrams.lagda.md
new file mode 100644
index 00000000000..73aae85aa48
--- /dev/null
+++ b/src/foundation/operations-cospan-diagrams.lagda.md
@@ -0,0 +1,168 @@
+# Operations on cospan diagrams
+
+```agda
+module foundation.operations-cospan-diagrams where
+
+open import foundation-core.operations-cospan-diagrams public
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cospan-diagrams
+open import foundation.cospans
+open import foundation.dependent-pair-types
+open import foundation.equivalences-arrows
+open import foundation.operations-cospans
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+This file contains some further operations on
+[cospan diagrams](foundation.cospan-diagrams.md) that produce new cospan
+diagrams from given cospan diagrams and possibly other data. Previous operations
+on cospan diagrams were defined in
+[`foundation-core.operations-cospan-diagrams`](foundation-core.operations-cospan-diagrams.md).
+
+## Definitions
+
+### Concatenating cospan diagrams and equivalences of arrows on the left
+
+Consider a cospan diagram `𝒮` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and an [equivalence of arrows](foundation.equivalences-arrows.md)
+`h : equiv-arrow f' f` as indicated in the diagram
+
+```text
+          f         g
+     A ------> S <------ B.
+     |         |
+  h₀ | ≃     ≃ | h₁
+     ∨         ∨
+     A' -----> S'
+          f'
+```
+
+Then we obtain a cospan diagram `A' --> S' <-- B`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (𝒮 : cospan-diagram l1 l2 l3)
+  {S' : UU l4} {A' : UU l5} (f' : A' → S')
+  (h : equiv-arrow (left-map-cospan-diagram 𝒮) f')
+  where
+
+  domain-left-concat-equiv-arrow-cospan-diagram : UU l5
+  domain-left-concat-equiv-arrow-cospan-diagram = A'
+
+  codomain-left-concat-equiv-arrow-cospan-diagram : UU l2
+  codomain-left-concat-equiv-arrow-cospan-diagram = codomain-cospan-diagram 𝒮
+
+  cospan-left-concat-equiv-arrow-cospan-diagram :
+    cospan l4
+      ( domain-left-concat-equiv-arrow-cospan-diagram)
+      ( codomain-left-concat-equiv-arrow-cospan-diagram)
+  cospan-left-concat-equiv-arrow-cospan-diagram =
+    left-concat-equiv-arrow-cospan (cospan-cospan-diagram 𝒮) f' h
+
+  left-concat-equiv-arrow-cospan-diagram : cospan-diagram l5 l2 l4
+  pr1 left-concat-equiv-arrow-cospan-diagram =
+    domain-left-concat-equiv-arrow-cospan-diagram
+  pr1 (pr2 left-concat-equiv-arrow-cospan-diagram) =
+    codomain-left-concat-equiv-arrow-cospan-diagram
+  pr2 (pr2 left-concat-equiv-arrow-cospan-diagram) =
+    cospan-left-concat-equiv-arrow-cospan-diagram
+
+  cospanning-type-left-concat-equiv-arrow-cospan-diagram : UU l4
+  cospanning-type-left-concat-equiv-arrow-cospan-diagram =
+    cospanning-type-cospan-diagram left-concat-equiv-arrow-cospan-diagram
+
+  left-map-left-concat-equiv-arrow-cospan-diagram :
+    domain-left-concat-equiv-arrow-cospan-diagram →
+    cospanning-type-left-concat-equiv-arrow-cospan-diagram
+  left-map-left-concat-equiv-arrow-cospan-diagram =
+    left-map-cospan-diagram left-concat-equiv-arrow-cospan-diagram
+
+  right-map-left-concat-equiv-arrow-cospan-diagram :
+    codomain-left-concat-equiv-arrow-cospan-diagram →
+    cospanning-type-left-concat-equiv-arrow-cospan-diagram
+  right-map-left-concat-equiv-arrow-cospan-diagram =
+    right-map-cospan-diagram left-concat-equiv-arrow-cospan-diagram
+```
+
+### Concatenating cospan diagrams and equivalences of arrows on the right
+
+Consider a cospan diagram `𝒮` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and a [equivalence of arrows](foundation.equivalences-arrows.md)
+`h : equiv-arrow g' g` as indicated in the diagram
+
+```text
+       f         g
+  A ------> S <------ B.
+            |         |
+         h₀ | ≃     ≃ | h₁
+            ∨         ∨
+            S' <----- B'
+                 g'
+```
+
+Then we obtain a cospan diagram `A --> S' <-- B'`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (𝒮 : cospan-diagram l1 l2 l3)
+  {S' : UU l4} {B' : UU l5} (g' : B' → S')
+  (h : equiv-arrow (right-map-cospan-diagram 𝒮) g')
+  where
+
+  domain-right-concat-equiv-arrow-cospan-diagram : UU l1
+  domain-right-concat-equiv-arrow-cospan-diagram = domain-cospan-diagram 𝒮
+
+  codomain-right-concat-equiv-arrow-cospan-diagram : UU l5
+  codomain-right-concat-equiv-arrow-cospan-diagram = B'
+
+  cospan-right-concat-equiv-arrow-cospan-diagram :
+    cospan l4
+      ( domain-right-concat-equiv-arrow-cospan-diagram)
+      ( codomain-right-concat-equiv-arrow-cospan-diagram)
+  cospan-right-concat-equiv-arrow-cospan-diagram =
+    right-concat-equiv-arrow-cospan (cospan-cospan-diagram 𝒮) g' h
+
+  right-concat-equiv-arrow-cospan-diagram : cospan-diagram l1 l5 l4
+  pr1 right-concat-equiv-arrow-cospan-diagram =
+    domain-right-concat-equiv-arrow-cospan-diagram
+  pr1 (pr2 right-concat-equiv-arrow-cospan-diagram) =
+    codomain-right-concat-equiv-arrow-cospan-diagram
+  pr2 (pr2 right-concat-equiv-arrow-cospan-diagram) =
+    cospan-right-concat-equiv-arrow-cospan-diagram
+
+  cospanning-type-right-concat-equiv-arrow-cospan-diagram : UU l4
+  cospanning-type-right-concat-equiv-arrow-cospan-diagram =
+    cospanning-type-cospan-diagram right-concat-equiv-arrow-cospan-diagram
+
+  left-map-right-concat-equiv-arrow-cospan-diagram :
+    domain-right-concat-equiv-arrow-cospan-diagram →
+    cospanning-type-right-concat-equiv-arrow-cospan-diagram
+  left-map-right-concat-equiv-arrow-cospan-diagram =
+    left-map-cospan-diagram right-concat-equiv-arrow-cospan-diagram
+
+  right-map-right-concat-equiv-arrow-cospan-diagram :
+    codomain-right-concat-equiv-arrow-cospan-diagram →
+    cospanning-type-right-concat-equiv-arrow-cospan-diagram
+  right-map-right-concat-equiv-arrow-cospan-diagram =
+    right-map-cospan-diagram right-concat-equiv-arrow-cospan-diagram
+```
diff --git a/src/foundation/operations-cospans.lagda.md b/src/foundation/operations-cospans.lagda.md
new file mode 100644
index 00000000000..9574a13156d
--- /dev/null
+++ b/src/foundation/operations-cospans.lagda.md
@@ -0,0 +1,142 @@
+# Operations on cospans
+
+```agda
+module foundation.operations-cospans where
+
+open import foundation-core.operations-cospans public
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cospans
+open import foundation.dependent-pair-types
+open import foundation.equivalences-arrows
+open import foundation.morphisms-arrows
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+This file contains some further operations on [cospans](foundation.cospans.md)
+that produce new cospans from given cospans and possibly other data. Previous
+operations on cospans were defined in
+[`foundation-core.operations-cospans`](foundation-core.operations-cospans.md).
+
+## Definitions
+
+### Concatenating cospans and equivalences of arrows on the left
+
+Consider a cospan `s` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and an [equivalence of arrows](foundation.equivalences-arrows.md)
+`h : equiv-arrow f' f` as indicated in the diagram
+
+```text
+          f         g
+     A ------> S <------ B.
+     |         |
+  h₀ | ≃     ≃ | h₁
+     ∨         ∨
+     A' -----> S'
+          f'
+```
+
+Then we obtain a cospan `A' --> S' <-- B`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2}
+  (s : cospan l3 A B)
+  {S' : UU l4} {A' : UU l5} (f' : A' → S')
+  (h : equiv-arrow (left-map-cospan s) f')
+  where
+
+  cospanning-type-left-concat-equiv-arrow-cospan : UU l4
+  cospanning-type-left-concat-equiv-arrow-cospan = S'
+
+  left-map-left-concat-equiv-arrow-cospan :
+    A' → cospanning-type-left-concat-equiv-arrow-cospan
+  left-map-left-concat-equiv-arrow-cospan = f'
+
+  right-map-left-concat-equiv-arrow-cospan :
+    B → cospanning-type-left-concat-equiv-arrow-cospan
+  right-map-left-concat-equiv-arrow-cospan =
+    map-codomain-equiv-arrow (left-map-cospan s) f' h ∘ right-map-cospan s
+
+  left-concat-equiv-arrow-cospan :
+    cospan l4 A' B
+  pr1 left-concat-equiv-arrow-cospan =
+    cospanning-type-left-concat-equiv-arrow-cospan
+  pr1 (pr2 left-concat-equiv-arrow-cospan) =
+    left-map-left-concat-equiv-arrow-cospan
+  pr2 (pr2 left-concat-equiv-arrow-cospan) =
+    right-map-left-concat-equiv-arrow-cospan
+```
+
+### Concatenating cospans and equivalences of arrows on the right
+
+Consider a cospan `s` given by
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+and an equivalence of arrows `h : equiv-arrow g' g` as indicated in the diagram
+
+```text
+       f         g
+  A ------> S <------ B
+            |         |
+         h₀ | ≃     ≃ | h₁
+            ∨         ∨
+            S' <----- B'.
+                 g'
+```
+
+Then we obtain a cospan `A --> S' <-- B'`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2}
+  (s : cospan l3 A B)
+  {S' : UU l4} {B' : UU l5} (g' : B' → S')
+  (h : equiv-arrow (right-map-cospan s) g')
+  where
+
+  cospanning-type-right-concat-equiv-arrow-cospan : UU l4
+  cospanning-type-right-concat-equiv-arrow-cospan = S'
+
+  left-map-right-concat-equiv-arrow-cospan :
+    A → cospanning-type-right-concat-equiv-arrow-cospan
+  left-map-right-concat-equiv-arrow-cospan =
+    map-codomain-equiv-arrow (right-map-cospan s) g' h ∘ left-map-cospan s
+
+  right-map-right-concat-equiv-arrow-cospan :
+    B' → cospanning-type-right-concat-equiv-arrow-cospan
+  right-map-right-concat-equiv-arrow-cospan = g'
+
+  right-concat-equiv-arrow-cospan :
+    cospan l4 A B'
+  pr1 right-concat-equiv-arrow-cospan =
+    cospanning-type-right-concat-equiv-arrow-cospan
+  pr1 (pr2 right-concat-equiv-arrow-cospan) =
+    left-map-right-concat-equiv-arrow-cospan
+  pr2 (pr2 right-concat-equiv-arrow-cospan) =
+    right-map-right-concat-equiv-arrow-cospan
+```
+
+## See also
+
+- [Composition of cospans](synthetic-homotopy-theory.composition-cospans.md)
+- [Opposite cospans](foundation.opposite-cospans.md)
diff --git a/src/foundation/operations-spans.lagda.md b/src/foundation/operations-spans.lagda.md
index 6562513941e..31d310e4287 100644
--- a/src/foundation/operations-spans.lagda.md
+++ b/src/foundation/operations-spans.lagda.md
@@ -93,8 +93,7 @@ Consider a span `s` given by
   A <----- S -----> B
 ```
 
-and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g`
-as indicated in the diagram
+and a equivalence of arrows `h : equiv-arrow g' g` as indicated in the diagram
 
 ```text
                g'
diff --git a/src/foundation/opposite-cospans.lagda.md b/src/foundation/opposite-cospans.lagda.md
new file mode 100644
index 00000000000..07ac51d7c09
--- /dev/null
+++ b/src/foundation/opposite-cospans.lagda.md
@@ -0,0 +1,52 @@
+# Opposite cospans
+
+```agda
+module foundation.opposite-cospans where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cospans
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a [cospan](foundation.cospans.md) `(S , f , g)` from `A` to `B`. The
+{{#concept "opposite cospan" Agda=opposite-cospan}} of `(S , f , g)` is the
+cospan `(S , g , f)` from `B` to `A`. In other words, the opposite of a cospan
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+is the cospan
+
+```text
+       g         f
+  B ------> S <------ A.
+```
+
+## Definitions
+
+### The opposite of a cospan
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  opposite-cospan : cospan l3 A B → cospan l3 B A
+  pr1 (opposite-cospan s) = cospanning-type-cospan s
+  pr1 (pr2 (opposite-cospan s)) = right-map-cospan s
+  pr2 (pr2 (opposite-cospan s)) = left-map-cospan s
+```
+
+## See also
+
+- [Transpositions of cospan diagrams](foundation.transposition-cospan-diagrams.md)
diff --git a/src/foundation/pullback-cones.lagda.md b/src/foundation/pullback-cones.lagda.md
index f35b29848dd..22cbef99c49 100644
--- a/src/foundation/pullback-cones.lagda.md
+++ b/src/foundation/pullback-cones.lagda.md
@@ -88,7 +88,7 @@ module _
   cone-pullback-cone = pr2 (pr1 c)
 
   vertical-map-pullback-cone :
-    domain-pullback-cone → left-type-cospan-diagram 𝒮
+    domain-pullback-cone → domain-cospan-diagram 𝒮
   vertical-map-pullback-cone =
     vertical-map-cone
       ( left-map-cospan-diagram 𝒮)
@@ -96,7 +96,7 @@ module _
       ( cone-pullback-cone)
 
   horizontal-map-pullback-cone :
-    domain-pullback-cone → right-type-cospan-diagram 𝒮
+    domain-pullback-cone → codomain-cospan-diagram 𝒮
   horizontal-map-pullback-cone =
     horizontal-map-cone
       ( left-map-cospan-diagram 𝒮)
diff --git a/src/foundation/transposition-cospan-diagrams.lagda.md b/src/foundation/transposition-cospan-diagrams.lagda.md
new file mode 100644
index 00000000000..330d7540876
--- /dev/null
+++ b/src/foundation/transposition-cospan-diagrams.lagda.md
@@ -0,0 +1,58 @@
+# Transposition of cospan diagrams
+
+```agda
+module foundation.transposition-cospan-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cospan-diagrams
+open import foundation.cospans
+open import foundation.dependent-pair-types
+open import foundation.opposite-cospans
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "transposition" Disambiguation="cospan diagram" Agda=transposition-cospan-diagram}}
+of a [cospan diagram](foundation.cospan-diagrams.md)
+
+```text
+       f         g
+  A ------> S <------ B
+```
+
+is the cospan diagram
+
+```text
+       g         f
+  B ------> S <------ A.
+```
+
+In other words, the transposition of a cospan diagram `(A , B , s)` is the
+cospan diagram `(B , A , opposite-cospan s)` where `opposite-cospan s` is the
+[opposite](foundation.opposite-cospans.md) of the
+[cospan](foundation.cospans.md) `s` from `A` to `B`.
+
+## Definitions
+
+### Transposition of cospan diagrams
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒮 : cospan-diagram l1 l2 l3)
+  where
+
+  transposition-cospan-diagram : cospan-diagram l2 l1 l3
+  pr1 transposition-cospan-diagram =
+    codomain-cospan-diagram 𝒮
+  pr1 (pr2 transposition-cospan-diagram) =
+    domain-cospan-diagram 𝒮
+  pr2 (pr2 transposition-cospan-diagram) =
+    opposite-cospan (cospan-cospan-diagram 𝒮)
+```
diff --git a/src/foundation/whiskering-homotopies-composition.lagda.md b/src/foundation/whiskering-homotopies-composition.lagda.md
index 864abbcd6e0..3705eba700b 100644
--- a/src/foundation/whiskering-homotopies-composition.lagda.md
+++ b/src/foundation/whiskering-homotopies-composition.lagda.md
@@ -152,6 +152,11 @@ module _
     {f f' : (x : A) → B x} (H : f ~ f') → id ·l H ~ H
   left-unit-law-left-whisker-comp H x = ap-id (H x)
 
+  inv-left-unit-law-left-whisker-comp :
+    {f f' : (x : A) → B x} (H : f ~ f') → H ~ id ·l H
+  inv-left-unit-law-left-whisker-comp H =
+    inv-htpy (left-unit-law-left-whisker-comp H)
+
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
   where
diff --git a/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md
index 94a477b5ada..488c8bf339d 100644
--- a/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md
@@ -490,24 +490,24 @@ module _
 
   is-equiv-map-compute-cone-pullback-localization-global-subuniverse :
     is-in-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) →
-    is-in-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) →
-    is-in-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (domain-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (codomain-cospan-diagram 𝒮) →
     is-equiv map-compute-cone-pullback-localization-global-subuniverse
   is-equiv-map-compute-cone-pullback-localization-global-subuniverse x a b =
     is-equiv-map-Σ _
       ( up-localization-global-subuniverse LC
-        ( left-type-cospan-diagram 𝒮 , a))
+        ( domain-cospan-diagram 𝒮 , a))
       ( λ _ →
         is-equiv-map-Σ _
           ( up-localization-global-subuniverse LC
-            ( right-type-cospan-diagram 𝒮 , b))
+            ( codomain-cospan-diagram 𝒮 , b))
           ( λ _ →
             is-equiv-right-whisker-unit-localization-global-subuniverse 𝒫 LC x))
 
   is-in-global-subuniverse-pullback-localization-global-subuniverse :
     is-in-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) →
-    is-in-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) →
-    is-in-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (domain-cospan-diagram 𝒮) →
+    is-in-global-subuniverse 𝒫 (codomain-cospan-diagram 𝒮) →
     is-in-global-subuniverse 𝒫 (domain-pullback-cone 𝒮 c)
   is-in-global-subuniverse-pullback-localization-global-subuniverse x a b =
     is-in-global-subuniverse-is-local-type-universal-property-localization-global-subuniverse
diff --git a/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md
index 787a9630516..343258360c5 100644
--- a/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md
@@ -376,8 +376,8 @@ module _
 
   is-in-reflective-global-subuniverse-pullback :
     is-in-reflective-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) →
-    is-in-reflective-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) →
-    is-in-reflective-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) →
+    is-in-reflective-global-subuniverse 𝒫 (domain-cospan-diagram 𝒮) →
+    is-in-reflective-global-subuniverse 𝒫 (codomain-cospan-diagram 𝒮) →
     is-in-reflective-global-subuniverse 𝒫 (domain-pullback-cone 𝒮 c)
   is-in-reflective-global-subuniverse-pullback =
     is-in-global-subuniverse-pullback-localization-global-subuniverse
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 2839f2a8162..01685d014b9 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -27,6 +27,7 @@ open import synthetic-homotopy-theory.cofibers-of-maps public
 open import synthetic-homotopy-theory.cofibers-of-pointed-maps public
 open import synthetic-homotopy-theory.coforks public
 open import synthetic-homotopy-theory.coforks-cocones-under-sequential-diagrams public
+open import synthetic-homotopy-theory.composition-cospans public
 open import synthetic-homotopy-theory.conjugation-loops public
 open import synthetic-homotopy-theory.connected-set-bundles-circle public
 open import synthetic-homotopy-theory.connective-prespectra public
diff --git a/src/synthetic-homotopy-theory/coforks.lagda.md b/src/synthetic-homotopy-theory/coforks.lagda.md
index 34222f1a4f8..50b820ed967 100644
--- a/src/synthetic-homotopy-theory/coforks.lagda.md
+++ b/src/synthetic-homotopy-theory/coforks.lagda.md
@@ -47,7 +47,8 @@ map `e : B → X` together with a [homotopy](foundation.homotopies.md)
 ```text
      g
    ----->     e
- A -----> B -----> X
+ A        B -----> X
+   ----->
      f
 ```
 
@@ -120,7 +121,8 @@ a new cofork `h ∘ e`.
 ```text
      g
    ----->     e        h
- A -----> B -----> X -----> Y
+ A        B -----> X -----> Y
+   ----->
      f
 ```
 
@@ -198,7 +200,8 @@ module _
 ```text
      g
    ----->     e        h        k
- A -----> B -----> X -----> Y -----> Z
+ A        B -----> X -----> Y -----> Z
+   ----->
      f
 ```
 
@@ -443,15 +446,15 @@ module _
     hom-span-diagram
       ( span-diagram-cofork a)
       ( span-diagram-cofork a')
-  pr1 (hom-span-diagram-cofork-hom-double-arrow) =
+  pr1 hom-span-diagram-cofork-hom-double-arrow =
     domain-map-hom-double-arrow a a' h
-  pr1 (pr2 (hom-span-diagram-cofork-hom-double-arrow)) =
+  pr1 (pr2 hom-span-diagram-cofork-hom-double-arrow) =
     codomain-map-hom-double-arrow a a' h
-  pr1 (pr2 (pr2 (hom-span-diagram-cofork-hom-double-arrow))) =
+  pr1 (pr2 (pr2 hom-span-diagram-cofork-hom-double-arrow)) =
     spanning-map-hom-span-diagram-cofork-hom-double-arrow
-  pr1 (pr2 (pr2 (pr2 (hom-span-diagram-cofork-hom-double-arrow)))) =
+  pr1 (pr2 (pr2 (pr2 hom-span-diagram-cofork-hom-double-arrow))) =
     left-square-hom-span-diagram-cofork-hom-double-arrow
-  pr2 (pr2 (pr2 (pr2 (hom-span-diagram-cofork-hom-double-arrow)))) =
+  pr2 (pr2 (pr2 (pr2 hom-span-diagram-cofork-hom-double-arrow))) =
     right-square-hom-span-diagram-cofork-hom-double-arrow
 ```
 
@@ -504,7 +507,8 @@ module _
       ( domain-map-equiv-double-arrow a a' e)
       ( vertical-map-span-cocone-cofork a')
   left-square-equiv-span-diagram-cofork-equiv-double-arrow =
-    ind-coproduct _ refl-htpy refl-htpy
+    left-square-hom-span-diagram-cofork-hom-double-arrow a a'
+      ( hom-equiv-double-arrow a a' e)
 
   right-square-equiv-span-diagram-cofork-equiv-double-arrow :
     coherence-square-maps'
@@ -513,22 +517,21 @@ module _
       ( codomain-map-equiv-double-arrow a a' e)
       ( horizontal-map-span-cocone-cofork a')
   right-square-equiv-span-diagram-cofork-equiv-double-arrow =
-    ind-coproduct _
-      ( left-square-equiv-double-arrow a a' e)
-      ( right-square-equiv-double-arrow a a' e)
+    right-square-hom-span-diagram-cofork-hom-double-arrow a a'
+      ( hom-equiv-double-arrow a a' e)
 
   equiv-span-diagram-cofork-equiv-double-arrow :
     equiv-span-diagram
       ( span-diagram-cofork a)
       ( span-diagram-cofork a')
-  pr1 (equiv-span-diagram-cofork-equiv-double-arrow) =
+  pr1 equiv-span-diagram-cofork-equiv-double-arrow =
     domain-equiv-equiv-double-arrow a a' e
-  pr1 (pr2 (equiv-span-diagram-cofork-equiv-double-arrow)) =
+  pr1 (pr2 equiv-span-diagram-cofork-equiv-double-arrow) =
     codomain-equiv-equiv-double-arrow a a' e
-  pr1 (pr2 (pr2 (equiv-span-diagram-cofork-equiv-double-arrow))) =
+  pr1 (pr2 (pr2 equiv-span-diagram-cofork-equiv-double-arrow)) =
     spanning-equiv-equiv-span-diagram-cofork-equiv-double-arrow
-  pr1 (pr2 (pr2 (pr2 (equiv-span-diagram-cofork-equiv-double-arrow)))) =
+  pr1 (pr2 (pr2 (pr2 equiv-span-diagram-cofork-equiv-double-arrow))) =
     left-square-equiv-span-diagram-cofork-equiv-double-arrow
-  pr2 (pr2 (pr2 (pr2 (equiv-span-diagram-cofork-equiv-double-arrow)))) =
+  pr2 (pr2 (pr2 (pr2 equiv-span-diagram-cofork-equiv-double-arrow))) =
     right-square-equiv-span-diagram-cofork-equiv-double-arrow
 ```
diff --git a/src/synthetic-homotopy-theory/composition-cospans.lagda.md b/src/synthetic-homotopy-theory/composition-cospans.lagda.md
new file mode 100644
index 00000000000..d24699e3082
--- /dev/null
+++ b/src/synthetic-homotopy-theory/composition-cospans.lagda.md
@@ -0,0 +1,79 @@
+# Composition of cospans
+
+```agda
+module synthetic-homotopy-theory.composition-cospans where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cospans
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+
+open import synthetic-homotopy-theory.pushouts
+```
+
+</details>
+
+## Idea
+
+Given two [cospans](foundation.cospans.md) `F` and `G` such that the source of
+`G` is the target of `F`
+
+```text
+           F                 G
+
+  A -----> S <----- B -----> T <----- C,
+```
+
+then we may
+{{#concept "compose" Disambiguation="cospans of types" Agda=comp-cospan}} the
+two cospans by forming the [pushout](synthetic-homotopy-theory.pushouts.md) of
+the middle [cospan diagram](foundation.cospan-diagrams.md)
+
+```text
+                      C
+                      |
+                      |
+                      ∨
+            B ------> T
+            |         |
+            |         |
+            ∨       ⌜ ∨
+  A ------> S ------> ∙
+```
+
+giving us a cospan `G ∘ F` from `A` to `C`.
+
+## Definitions
+
+### Composition of cospans
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3}
+  (G : cospan l4 B C) (F : cospan l5 A B)
+  where
+
+  cospanning-type-comp-cospan : UU (l2 ⊔ l4 ⊔ l5)
+  cospanning-type-comp-cospan =
+    pushout (right-map-cospan F) (left-map-cospan G)
+
+  left-map-comp-cospan : A → cospanning-type-comp-cospan
+  left-map-comp-cospan =
+    inl-pushout (right-map-cospan F) (left-map-cospan G) ∘ left-map-cospan F
+
+  right-map-comp-cospan : C → cospanning-type-comp-cospan
+  right-map-comp-cospan =
+    inr-pushout (right-map-cospan F) (left-map-cospan G) ∘ right-map-cospan G
+
+  comp-cospan : cospan (l2 ⊔ l4 ⊔ l5) A C
+  comp-cospan =
+    ( cospanning-type-comp-cospan ,
+      left-map-comp-cospan ,
+      right-map-comp-cospan)
+```
diff --git a/src/synthetic-homotopy-theory/equivalences-coforks-under-equivalences-double-arrows.lagda.md b/src/synthetic-homotopy-theory/equivalences-coforks-under-equivalences-double-arrows.lagda.md
index a5fa74bee97..f3a1beb94e1 100644
--- a/src/synthetic-homotopy-theory/equivalences-coforks-under-equivalences-double-arrows.lagda.md
+++ b/src/synthetic-homotopy-theory/equivalences-coforks-under-equivalences-double-arrows.lagda.md
@@ -1,4 +1,4 @@
-# Equivalences of coforks
+# Equivalences of coforks under equivalences of double arrows
 
 ```agda
 module synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows where
@@ -78,36 +78,36 @@ which share the top map `i` and the bottom square, and the coherences of `c` and
 `c'` filling the sides; that gives the homotopies
 
 ```text
-                                                i                 i
-     A                  A                 A --------> U     A --------> U
-     |                  |                             |                 |
-   f |                f |                             | h               | k
-     |                  |                             |                 |
-     ∨                  ∨     j                       ∨                 ∨
-     B         ~        B --------> V       ~         V        ~        V
-     |                              |                 |                 |
-   c |                              | c'              | c'              | c'
-     |                              |                 |                 |
-     ∨                              ∨                 ∨                 ∨
-     X --------> Y                  Y                 Y                 Y
+                                               i                 i
+     A                 A                 A --------> U     A --------> U
+     |                 |                             |                 |
+   f |               f |                             | h               | k
+     |                 |                             |                 |
+     ∨                 ∨     j                       ∨                 ∨
+     B        ~        B --------> V        ~        V        ~        V
+     |                             |                 |                 |
+   c |                             | c'              | c'              | c'
+     |                             |                 |                 |
+     ∨                             ∨                 ∨                 ∨
+     X --------> Y                 Y                 Y                 Y
            m
 ```
 
 and
 
 ```text
-                                                                  i
-     A                 A               A                    A --------> U
-     |                 |               |                                |
-   f |               g |             g |                                | k
-     |                 |               |                                |
-     ∨                 ∨               ∨     j                          ∨
-     B         ~       B       ~       B --------> V           ~        V
-     |                 |                           |                    |
-   c |               c |                           | c'                 | c'
-     |                 |                           |                    |
-     ∨                 ∨                           ∨                    ∨
-     X --------> Y     X --------> Y               Y                    Y ,
+                                                                 i
+     A                 A                 A                 A --------> U
+     |                 |                 |                             |
+   f |               g |               g |                             | k
+     |                 |                 |                             |
+     ∨                 ∨                 ∨     j                       ∨
+     B        ~        B        ~        B --------> V        ~        V
+     |                 |                             |                 |
+   c |               c |                             | c'              | c'
+     |                 |                             |                 |
+     ∨                 ∨                             ∨                 ∨
+     X --------> Y     X --------> Y                 Y                 Y ,
            m                 m
 ```
 
@@ -127,23 +127,17 @@ module _
 
   coherence-map-cofork-equiv-cofork-equiv-double-arrow : (X ≃ Y) → UU (l2 ⊔ l6)
   coherence-map-cofork-equiv-cofork-equiv-double-arrow m =
-    coherence-square-maps
-      ( codomain-map-equiv-double-arrow a a' e)
-      ( map-cofork a c)
-      ( map-cofork a' c')
+    coherence-map-cofork-hom-cofork-hom-double-arrow c c'
+      ( hom-equiv-double-arrow a a' e)
       ( map-equiv m)
 
   coherence-equiv-cofork-equiv-double-arrow :
     (m : X ≃ Y) → coherence-map-cofork-equiv-cofork-equiv-double-arrow m →
     UU (l1 ⊔ l6)
-  coherence-equiv-cofork-equiv-double-arrow m H =
-    ( ( H ·r (left-map-double-arrow a)) ∙h
-      ( ( map-cofork a' c') ·l
-        ( left-square-equiv-double-arrow a a' e)) ∙h
-      ( (coh-cofork a' c') ·r (domain-map-equiv-double-arrow a a' e))) ~
-    ( ( (map-equiv m) ·l (coh-cofork a c)) ∙h
-      ( H ·r (right-map-double-arrow a)) ∙h
-      ( (map-cofork a' c') ·l (right-square-equiv-double-arrow a a' e)))
+  coherence-equiv-cofork-equiv-double-arrow m =
+    coherence-hom-cofork-hom-double-arrow c c'
+      ( hom-equiv-double-arrow a a' e)
+      ( map-equiv m)
 
   equiv-cofork-equiv-double-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l6)
   equiv-cofork-equiv-double-arrow =
diff --git a/src/synthetic-homotopy-theory/morphisms-coforks-under-morphisms-double-arrows.lagda.md b/src/synthetic-homotopy-theory/morphisms-coforks-under-morphisms-double-arrows.lagda.md
index 05c6762c56e..75a6f5973c4 100644
--- a/src/synthetic-homotopy-theory/morphisms-coforks-under-morphisms-double-arrows.lagda.md
+++ b/src/synthetic-homotopy-theory/morphisms-coforks-under-morphisms-double-arrows.lagda.md
@@ -1,4 +1,4 @@
-# Morphisms of coforks
+# Morphisms of coforks under morphisms of double arrows
 
 ```agda
 module synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows where
@@ -74,36 +74,36 @@ which share the top map `i` and the bottom square, and the coherences of `c` and
 `c'` filling the sides; that gives the homotopies
 
 ```text
-                                                i                 i
-     A                  A                 A --------> U     A --------> U
-     |                  |                             |                 |
-   f |                f |                             | h               | k
-     |                  |                             |                 |
-     ∨                  ∨     j                       ∨                 ∨
-     B         ~        B --------> V       ~         V        ~        V
-     |                              |                 |                 |
-   c |                              | c'              | c'              | c'
-     |                              |                 |                 |
-     ∨                              ∨                 ∨                 ∨
-     X --------> Y                  Y                 Y                 Y
+                                               i                 i
+     A                 A                 A --------> U     A --------> U
+     |                 |                             |                 |
+   f |               f |                             | h               | k
+     |                 |                             |                 |
+     ∨                 ∨     j                       ∨                 ∨
+     B        ~        B --------> V        ~        V        ~        V
+     |                             |                 |                 |
+   c |                             | c'              | c'              | c'
+     |                             |                 |                 |
+     ∨                             ∨                 ∨                 ∨
+     X --------> Y                 Y                 Y                 Y
            m
 ```
 
 and
 
 ```text
-                                                                  i
-     A                 A               A                    A --------> U
-     |                 |               |                                |
-   f |               g |             g |                                | k
-     |                 |               |                                |
-     ∨                 ∨               ∨     j                          ∨
-     B         ~       B       ~       B --------> V           ~        V
-     |                 |                           |                    |
-   c |               c |                           | c'                 | c'
-     |                 |                           |                    |
-     ∨                 ∨                           ∨                    ∨
-     X --------> Y     X --------> Y               Y                    Y ,
+                                                                 i
+     A                 A                 A                 A --------> U
+     |                 |                 |                             |
+   f |               g |               g |                             | k
+     |                 |                 |                             |
+     ∨                 ∨                 ∨     j                       ∨
+     B        ~        B        ~        B --------> V        ~        V
+     |                 |                             |                 |
+   c |               c |                             | c'              | c'
+     |                 |                             |                 |
+     ∨                 ∨                             ∨                 ∨
+     X --------> Y     X --------> Y                 Y                 Y ,
            m                 m
 ```