diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 8bab74d7ad3..bca74bfc132 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -181,6 +181,7 @@ 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-inverse-sequential-diagrams public
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 2f2dac5bde8..ca494a0f821 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 =
-    Σ ( cospanning-type-cospan c ≃ cospanning-type-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
diff --git a/src/foundation/equivalences-span-diagrams.lagda.md b/src/foundation/equivalences-span-diagrams.lagda.md
index 83c132a950f..1b7f0f1c819 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/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 4e6184a65e2..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 :
+  map-domain-hom-cospan-diagram :
     domain-cospan-diagram 𝒮 → domain-cospan-diagram 𝒯
-  left-map-hom-cospan-diagram = pr1 h
+  map-domain-hom-cospan-diagram = pr1 h
 
-  right-map-hom-cospan-diagram :
+  map-codomain-hom-cospan-diagram :
     codomain-cospan-diagram 𝒮 → codomain-cospan-diagram 𝒯
-  right-map-hom-cospan-diagram = pr1 (pr2 h)
+  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
@@ -134,8 +165,8 @@ module _
       ( domain-cospan-diagram 𝒯 ,
         domain-cospan-diagram ℛ ,
         domain-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')
       ( codomain-hom-cospan-diagram-rotate h h')
   hom-cospan-diagram-rotate
     ( hA , hB , hX , HA , HB)
@@ -152,8 +183,8 @@ module _
       ( codomain-cospan-diagram 𝒯 ,
         codomain-cospan-diagram ℛ ,
         codomain-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')
       ( 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 64fd44b3715..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 :
-    (cospanning-type-cospan c → cospanning-type-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 =
-    Σ ( cospanning-type-cospan c → cospanning-type-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)
 ```