From 35434231a5ef699aa8aa16557275f70e3b344b3a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 3 Jan 2025 17:19:00 +0100
Subject: [PATCH 1/6] =?UTF-8?q?work=20from=20wild-=CF=89-semicategories?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/foundation-core/pullbacks.lagda.md        |   1 +
 src/foundation.lagda.md                       |   5 +
 src/foundation/composition-spans.lagda.md     | 163 +++++++
 ...zontal-composition-spans-of-spans.lagda.md | 174 ++++++++
 src/foundation/operations-spans.lagda.md      |   5 +
 src/foundation/spans-of-spans.lagda.md        | 137 ++++++
 src/foundation/standard-pullbacks.lagda.md    | 255 -----------
 .../standard-ternary-pullbacks.lagda.md       |  76 ++++
 ...ype-arithmetic-standard-pullbacks.lagda.md | 417 ++++++++++++++++++
 9 files changed, 978 insertions(+), 255 deletions(-)
 create mode 100644 src/foundation/composition-spans.lagda.md
 create mode 100644 src/foundation/horizontal-composition-spans-of-spans.lagda.md
 create mode 100644 src/foundation/spans-of-spans.lagda.md
 create mode 100644 src/foundation/standard-ternary-pullbacks.lagda.md
 create mode 100644 src/foundation/type-arithmetic-standard-pullbacks.lagda.md

diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
index 9749065efc..332e6e96e2 100644
--- a/src/foundation-core/pullbacks.lagda.md
+++ b/src/foundation-core/pullbacks.lagda.md
@@ -15,6 +15,7 @@ open import foundation.functoriality-fibers-of-maps
 open import foundation.identity-types
 open import foundation.morphisms-arrows
 open import foundation.standard-pullbacks
+open import foundation.type-arithmetic-standard-pullbacks
 open import foundation.universe-levels
 
 open import foundation-core.commuting-triangles-of-maps
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 78a7642b23..6858aa69d0 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -76,6 +76,7 @@ open import foundation.complements public
 open import foundation.complements-subtypes public
 open import foundation.composite-maps-in-inverse-sequential-diagrams public
 open import foundation.composition-algebra public
+open import foundation.composition-spans public
 open import foundation.computational-identity-types public
 open import foundation.cones-over-cospan-diagrams public
 open import foundation.cones-over-inverse-sequential-diagrams public
@@ -220,6 +221,7 @@ open import foundation.homotopies-morphisms-cospan-diagrams public
 open import foundation.homotopy-algebra public
 open import foundation.homotopy-induction public
 open import foundation.homotopy-preorder-of-types public
+open import foundation.horizontal-composition-spans-of-spans public
 open import foundation.idempotent-maps public
 open import foundation.identity-systems public
 open import foundation.identity-truncated-types public
@@ -376,10 +378,12 @@ open import foundation.span-diagrams public
 open import foundation.span-diagrams-families-of-types public
 open import foundation.spans public
 open import foundation.spans-families-of-types public
+open import foundation.spans-of-spans public
 open import foundation.split-idempotent-maps public
 open import foundation.split-surjective-maps public
 open import foundation.standard-apartness-relations public
 open import foundation.standard-pullbacks public
+open import foundation.standard-ternary-pullbacks public
 open import foundation.strict-symmetrization-binary-relations public
 open import foundation.strictly-involutive-identity-types public
 open import foundation.strictly-right-unital-concatenation-identifications public
@@ -432,6 +436,7 @@ open import foundation.type-arithmetic-coproduct-types public
 open import foundation.type-arithmetic-dependent-function-types public
 open import foundation.type-arithmetic-dependent-pair-types public
 open import foundation.type-arithmetic-empty-type public
+open import foundation.type-arithmetic-standard-pullbacks public
 open import foundation.type-arithmetic-unit-type public
 open import foundation.type-duality public
 open import foundation.type-theoretic-principle-of-choice public
diff --git a/src/foundation/composition-spans.lagda.md b/src/foundation/composition-spans.lagda.md
new file mode 100644
index 0000000000..2611cdf5b1
--- /dev/null
+++ b/src/foundation/composition-spans.lagda.md
@@ -0,0 +1,163 @@
+# Composition of spans
+
+```agda
+module foundation.composition-spans where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-triangles-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.equivalences-spans
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.morphisms-arrows
+open import foundation.morphisms-spans
+open import foundation.pullbacks
+open import foundation.spans
+open import foundation.standard-pullbacks
+open import foundation.type-arithmetic-standard-pullbacks
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Given two [spans](foundation.spans.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="spans of types" Agda=comp-span}} the two
+spans by forming the [pullback](foundation.standard-pullbacks.md) of the middle
+[cospan diagram](foundation.cospan-diagrams.md)
+
+```text
+  ∙ ------> T ------> C
+  | ⌟       |
+  |         |    G
+  ∨         ∨
+  S ------> B
+  |
+  |    F
+  ∨
+  A
+```
+
+giving us a span `G ∘ F` from `A` to `C`. This operation is unital and
+associative.
+
+## Definitions
+
+### Composition of spans
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3}
+  (G : span l4 B C) (F : span l5 A B)
+  where
+
+  spanning-type-comp-span : UU (l2 ⊔ l4 ⊔ l5)
+  spanning-type-comp-span =
+    standard-pullback (right-map-span F) (left-map-span G)
+
+  left-map-comp-span : spanning-type-comp-span → A
+  left-map-comp-span = left-map-span F ∘ vertical-map-standard-pullback
+
+  right-map-comp-span : spanning-type-comp-span → C
+  right-map-comp-span = right-map-span G ∘ horizontal-map-standard-pullback
+
+  comp-span : span (l2 ⊔ l4 ⊔ l5) A C
+  comp-span = spanning-type-comp-span , left-map-comp-span , right-map-comp-span
+```
+
+## Properties
+
+### Associativity of composition of spans
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (H : span l5 C D) (G : span l6 B C) (F : span l7 A B)
+  where
+
+  essentially-associative-spanning-type-comp-span :
+    spanning-type-comp-span (comp-span H G) F ≃
+    spanning-type-comp-span H (comp-span G F)
+  essentially-associative-spanning-type-comp-span =
+    inv-associative-standard-pullback
+      ( right-map-span F)
+      ( left-map-span G)
+      ( right-map-span G)
+      ( left-map-span H)
+
+  essentially-associative-comp-span :
+    equiv-span (comp-span (comp-span H G) F) (comp-span H (comp-span G F))
+  essentially-associative-comp-span =
+    ( essentially-associative-spanning-type-comp-span , refl-htpy , refl-htpy)
+
+  associative-comp-span :
+    comp-span (comp-span H G) F ＝ comp-span H (comp-span G F)
+  associative-comp-span =
+    eq-equiv-span
+      ( comp-span (comp-span H G) F)
+      ( comp-span H (comp-span G F))
+      ( essentially-associative-comp-span)
+```
+
+### The left unit law for composition of spans
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (F : span l3 A B)
+  where
+
+  left-unit-law-comp-span' :
+    equiv-span F (comp-span id-span F)
+  left-unit-law-comp-span' =
+    inv-right-unit-law-standard-pullback (right-map-span F) ,
+    refl-htpy ,
+    refl-htpy
+
+  left-unit-law-comp-span :
+    equiv-span (comp-span id-span F) F
+  left-unit-law-comp-span =
+    right-unit-law-standard-pullback (right-map-span F) ,
+    refl-htpy ,
+    inv-htpy coherence-square-standard-pullback
+```
+
+### The right unit law for composition of spans
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (F : span l3 A B)
+  where
+
+  right-unit-law-comp-span' :
+    equiv-span F (comp-span F id-span)
+  right-unit-law-comp-span' =
+    inv-left-unit-law-standard-pullback (left-map-span F) ,
+    refl-htpy ,
+    refl-htpy
+
+  right-unit-law-comp-span :
+    equiv-span (comp-span F id-span) F
+  right-unit-law-comp-span =
+    left-unit-law-standard-pullback (left-map-span F) ,
+    coherence-square-standard-pullback ,
+    refl-htpy
+```
diff --git a/src/foundation/horizontal-composition-spans-of-spans.lagda.md b/src/foundation/horizontal-composition-spans-of-spans.lagda.md
new file mode 100644
index 0000000000..76d9afec8c
--- /dev/null
+++ b/src/foundation/horizontal-composition-spans-of-spans.lagda.md
@@ -0,0 +1,174 @@
+# Horizontal composition of higher spans
+
+```agda
+module foundation.horizontal-composition-spans-of-spans where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-triangles-of-maps
+open import foundation.composition-spans
+open import foundation.cones-over-cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.equivalences-spans
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.morphisms-arrows
+open import foundation.morphisms-spans
+open import foundation.pullbacks
+open import foundation.spans
+open import foundation.spans-of-spans
+open import foundation.standard-pullbacks
+open import foundation.type-arithmetic-standard-pullbacks
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Given two [spans](foundation.spans.md) `F` and `G` from `A` to `B` and two spans
+`H` and `I` from `B` to `C` together with
+[higher spans](foundation.spans-of-spans.md) `α` from `F` to `G` and `β` from
+`H` to `I`, i.e., we have a commuting diagram of types of the form
+
+```text
+      F₀      H₀
+    ↙ ↑ ↘   ↙ ↑ ↘
+  A   α₀  B   β₀  C,
+    ↖ ↓ ↗   ↖ ↓ ↗
+      G₀      I₀
+```
+
+then we may
+{{#concept "horizontally compose" Disambiguation="spans of spans" Agda=horizontal-comp-span-of-spans}}
+`α` and `β` to obtain a span of spans from `H ∘ F` to `I ∘ G`. The horizontal
+composite is given by the span of spans
+
+```text
+  F₀ ×_B H₀ ---------> C
+     |    ↖            ∧
+     |    α₀ ×_B β₀    |
+     ∨            ↘    |
+     A <----------- G₀ ×_B I₀.
+```
+
+**Note.** There are four equivalent, but judgmentally different choices of
+spanning type `α₀ ×_B β₀` of the horizontal composite. We pick
+
+```text
+  α₀ ×_B β₀ ------> I₀
+      | ⌟           |
+      |             |
+      ∨             ∨
+      F₀ ---------> B
+```
+
+as this is the only choice that avoids inversions of coherences as part of the
+construction.
+
+## Definitions
+
+### Horizontal composition of spans of spans
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3}
+  (F : span l4 A B) (G : span l5 A B)
+  (H : span l6 B C) (I : span l7 B C)
+  (α : span-of-spans l8 F G)
+  (β : span-of-spans l9 H I)
+  where
+
+  spanning-type-horizontal-comp-span-of-spans : UU (l2 ⊔ l8 ⊔ l9)
+  spanning-type-horizontal-comp-span-of-spans =
+    standard-pullback
+      ( right-map-span F ∘ left-map-span-of-spans F G α)
+      ( left-map-span I ∘ right-map-span-of-spans H I β)
+
+  cone-left-map-horizontal-comp-span-of-spans :
+    cone
+      ( right-map-span F)
+      ( left-map-span H)
+      ( spanning-type-horizontal-comp-span-of-spans)
+  cone-left-map-horizontal-comp-span-of-spans =
+    left-map-span-of-spans F G α ∘ vertical-map-standard-pullback ,
+    left-map-span-of-spans H I β ∘ horizontal-map-standard-pullback ,
+    coherence-square-standard-pullback ∙h
+    coh-left-span-of-spans H I β ·r horizontal-map-standard-pullback
+
+  left-map-horizontal-comp-span-of-spans :
+    spanning-type-horizontal-comp-span-of-spans → spanning-type-comp-span H F
+  left-map-horizontal-comp-span-of-spans =
+    gap
+      ( right-map-span F)
+      ( left-map-span H)
+      ( cone-left-map-horizontal-comp-span-of-spans)
+
+  cone-right-map-horizontal-comp-span-of-spans :
+    cone
+      ( right-map-span G)
+      ( left-map-span I)
+      ( spanning-type-horizontal-comp-span-of-spans)
+  cone-right-map-horizontal-comp-span-of-spans =
+    right-map-span-of-spans F G α ∘ vertical-map-standard-pullback ,
+    right-map-span-of-spans H I β ∘ horizontal-map-standard-pullback ,
+    coh-right-span-of-spans F G α ·r vertical-map-standard-pullback ∙h
+    coherence-square-standard-pullback
+
+  right-map-horizontal-comp-span-of-spans :
+    spanning-type-horizontal-comp-span-of-spans → spanning-type-comp-span I G
+  right-map-horizontal-comp-span-of-spans =
+    gap
+      ( right-map-span G)
+      ( left-map-span I)
+      ( cone-right-map-horizontal-comp-span-of-spans)
+
+  span-horizontal-comp-span-of-spans :
+    span
+      ( l2 ⊔ l8 ⊔ l9)
+      ( spanning-type-comp-span H F)
+      ( spanning-type-comp-span I G)
+  span-horizontal-comp-span-of-spans =
+    spanning-type-horizontal-comp-span-of-spans ,
+    left-map-horizontal-comp-span-of-spans ,
+    right-map-horizontal-comp-span-of-spans
+
+  coherence-left-horizontal-comp-span-of-spans :
+    coherence-left-span-of-spans
+      ( comp-span H F)
+      ( comp-span I G)
+      ( span-horizontal-comp-span-of-spans)
+  coherence-left-horizontal-comp-span-of-spans =
+    coh-left-span-of-spans F G α ·r vertical-map-standard-pullback
+
+  coherence-right-horizontal-comp-span-of-spans :
+    coherence-right-span-of-spans
+      ( comp-span H F)
+      ( comp-span I G)
+      ( span-horizontal-comp-span-of-spans)
+  coherence-right-horizontal-comp-span-of-spans =
+    coh-right-span-of-spans H I β ·r horizontal-map-standard-pullback
+
+  coherence-horizontal-comp-span-of-spans :
+    coherence-span-of-spans
+      ( comp-span H F)
+      ( comp-span I G)
+      ( span-horizontal-comp-span-of-spans)
+  coherence-horizontal-comp-span-of-spans =
+    coherence-left-horizontal-comp-span-of-spans ,
+    coherence-right-horizontal-comp-span-of-spans
+
+  horizontal-comp-span-of-spans :
+    span-of-spans (l2 ⊔ l8 ⊔ l9) (comp-span H F) (comp-span I G)
+  horizontal-comp-span-of-spans =
+    span-horizontal-comp-span-of-spans ,
+    coherence-horizontal-comp-span-of-spans
+```
diff --git a/src/foundation/operations-spans.lagda.md b/src/foundation/operations-spans.lagda.md
index 9037d78969..6562513941 100644
--- a/src/foundation/operations-spans.lagda.md
+++ b/src/foundation/operations-spans.lagda.md
@@ -138,3 +138,8 @@ module _
   pr2 (pr2 right-concat-equiv-arrow-span) =
     right-map-right-concat-equiv-arrow-span
 ```
+
+## See also
+
+- [Composition of spans](foundation.composition-spans.md)
+- [Opposite spans](foundation.opposite-spans.md)
diff --git a/src/foundation/spans-of-spans.lagda.md b/src/foundation/spans-of-spans.lagda.md
new file mode 100644
index 0000000000..792737abe6
--- /dev/null
+++ b/src/foundation/spans-of-spans.lagda.md
@@ -0,0 +1,137 @@
+# Spans of spans
+
+```agda
+module foundation.spans-of-spans where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.spans
+open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Given two [spans](foundation.spans.md) `F` and `G` from `A` to `B`
+
+```text
+  S ------> B
+  | F       ∧
+  |         |
+  ∨       G |
+  A <------ T,
+```
+
+then a {{#concept "span of spans" Disambiguation="of types" Agda=span-of-spans}}
+from `F` to `G` is a span `S <--- W ---> T` such that the diagram
+
+```text
+  S ------> B
+  |  ↖      ∧
+  |    W    |
+  ∨      ↘  |
+  A <------ T
+```
+
+commutes.
+
+## Definitions
+
+### Spans of (binary) spans
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  coherence-left-span-of-spans :
+    {l : Level} (𝒮 : span l3 A B) (𝒯 : span l4 A B) →
+    span l (spanning-type-span 𝒮) (spanning-type-span 𝒯) → UU (l1 ⊔ l)
+  coherence-left-span-of-spans {l} 𝒮 𝒯 F =
+    coherence-square-maps
+      ( left-map-span F)
+      ( right-map-span F)
+      ( left-map-span 𝒮)
+      ( left-map-span 𝒯)
+
+  coherence-right-span-of-spans :
+    {l : Level} (𝒮 : span l3 A B) (𝒯 : span l4 A B) →
+    span l (spanning-type-span 𝒮) (spanning-type-span 𝒯) → UU (l2 ⊔ l)
+  coherence-right-span-of-spans {l} 𝒮 𝒯 F =
+    coherence-square-maps
+      ( left-map-span F)
+      ( right-map-span F)
+      ( right-map-span 𝒮)
+      ( right-map-span 𝒯)
+
+  coherence-span-of-spans :
+    {l : Level} (𝒮 : span l3 A B) (𝒯 : span l4 A B) →
+    span l (spanning-type-span 𝒮) (spanning-type-span 𝒯) → UU (l1 ⊔ l2 ⊔ l)
+  coherence-span-of-spans 𝒮 𝒯 F =
+    ( coherence-left-span-of-spans 𝒮 𝒯 F) ×
+    ( coherence-right-span-of-spans 𝒮 𝒯 F)
+
+  span-of-spans :
+    (l : Level) → span l3 A B → span l4 A B → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
+  span-of-spans l 𝒮 𝒯 =
+    Σ ( span l (spanning-type-span 𝒮) (spanning-type-span 𝒯))
+      ( coherence-span-of-spans 𝒮 𝒯)
+
+module _
+  {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2}
+  (𝒮 : span l3 A B) (𝒯 : span l4 A B)
+  (F : span-of-spans l5 𝒮 𝒯)
+  where
+
+  span-span-of-spans : span l5 (spanning-type-span 𝒮) (spanning-type-span 𝒯)
+  span-span-of-spans = pr1 F
+
+  spanning-type-span-of-spans : UU l5
+  spanning-type-span-of-spans = spanning-type-span span-span-of-spans
+
+  left-map-span-of-spans : spanning-type-span-of-spans → spanning-type-span 𝒮
+  left-map-span-of-spans = left-map-span span-span-of-spans
+
+  right-map-span-of-spans : spanning-type-span-of-spans → spanning-type-span 𝒯
+  right-map-span-of-spans = right-map-span span-span-of-spans
+
+  coh-span-of-spans : coherence-span-of-spans 𝒮 𝒯 span-span-of-spans
+  coh-span-of-spans = pr2 F
+
+  coh-left-span-of-spans :
+    coherence-square-maps
+      ( left-map-span-of-spans)
+      ( right-map-span-of-spans)
+      ( left-map-span 𝒮)
+      ( left-map-span 𝒯)
+  coh-left-span-of-spans = pr1 coh-span-of-spans
+
+  coh-right-span-of-spans :
+    coherence-square-maps
+      ( left-map-span-of-spans)
+      ( right-map-span-of-spans)
+      ( right-map-span 𝒮)
+      ( right-map-span 𝒯)
+  coh-right-span-of-spans = pr2 coh-span-of-spans
+```
+
+### Identity spans of spans
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
+  (𝒮 : span l3 A B)
+  where
+
+  id-span-of-spans : span-of-spans l3 𝒮 𝒮
+  id-span-of-spans = id-span , refl-htpy , refl-htpy
+```
diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md
index bd7131a988..8f0db009ca 100644
--- a/src/foundation/standard-pullbacks.lagda.md
+++ b/src/foundation/standard-pullbacks.lagda.md
@@ -129,36 +129,6 @@ module _
   pr2 (pr2 (gap c z)) = coherence-square-cone f g c z
 ```
 
-#### The standard ternary pullback
-
-Given two cospans with a shared vertex `B`:
-
-```text
-      f       g       h       i
-  A ----> X <---- B ----> Y <---- C,
-```
-
-we call the standard limit of the diagram the
-{{#concept "standard ternary pullback" Disambiguation="of types" Agda=standard-ternary-pullback}}.
-It is defined as the sum
-
-```text
-  standard-ternary-pullback f g h i :=
-    Σ (a : A) (b : B) (c : C), ((f a ＝ g b) × (h b ＝ i c)).
-```
-
-```agda
-module _
-  {l1 l2 l3 l4 l5 : Level}
-  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
-  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
-  where
-
-  standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
-  standard-ternary-pullback =
-    Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (h b ＝ i c))))
-```
-
 ## Properties
 
 ### Characterization of the identity type of the standard pullback
@@ -257,231 +227,6 @@ module _
   pr2 (pr2 (htpy-cone-up-pullback-standard-pullback c)) = right-unit-htpy
 ```
 
-### Standard pullbacks are symmetric
-
-The standard pullback of `f : A -> X <- B : g` is equivalent to the standard
-pullback of `g : B -> X <- A : f`.
-
-```agda
-map-commutative-standard-pullback :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) → standard-pullback f g → standard-pullback g f
-pr1 (map-commutative-standard-pullback f g x) =
-  horizontal-map-standard-pullback x
-pr1 (pr2 (map-commutative-standard-pullback f g x)) =
-  vertical-map-standard-pullback x
-pr2 (pr2 (map-commutative-standard-pullback f g x)) =
-  inv (coherence-square-standard-pullback x)
-
-inv-inv-map-commutative-standard-pullback :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) →
-  ( map-commutative-standard-pullback f g ∘
-    map-commutative-standard-pullback g f) ~ id
-inv-inv-map-commutative-standard-pullback f g x =
-  eq-pair-eq-fiber
-    ( eq-pair-eq-fiber
-      ( inv-inv (coherence-square-standard-pullback x)))
-
-abstract
-  is-equiv-map-commutative-standard-pullback :
-    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-    (f : A → X) (g : B → X) → is-equiv (map-commutative-standard-pullback f g)
-  is-equiv-map-commutative-standard-pullback f g =
-    is-equiv-is-invertible
-      ( map-commutative-standard-pullback g f)
-      ( inv-inv-map-commutative-standard-pullback f g)
-      ( inv-inv-map-commutative-standard-pullback g f)
-
-commutative-standard-pullback :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) →
-  standard-pullback f g ≃ standard-pullback g f
-pr1 (commutative-standard-pullback f g) =
-  map-commutative-standard-pullback f g
-pr2 (commutative-standard-pullback f g) =
-  is-equiv-map-commutative-standard-pullback f g
-```
-
-#### The gap map of the swapped cone computes as the underlying gap map followed by a swap
-
-```agda
-triangle-map-commutative-standard-pullback :
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-  (f : A → X) (g : B → X) (c : cone f g C) →
-  gap g f (swap-cone f g c) ~
-  map-commutative-standard-pullback f g ∘ gap f g c
-triangle-map-commutative-standard-pullback f g c = refl-htpy
-```
-
-### Standard pullbacks are associative
-
-Consider two cospans with a shared vertex `B`:
-
-```text
-      f       g       h       i
-  A ----> X <---- B ----> Y <---- C,
-```
-
-then we can construct their limit using standard pullbacks in two equivalent
-ways. We can construct it by first forming the standard pullback of `f` and `g`,
-and then forming the standard pullback of the resulting `h ∘ f'` and `i`
-
-```text
-  (A ×_X B) ×_Y C ---------------------> C
-         | ⌟                             |
-         |                               | i
-         ∨                               ∨
-      A ×_X B ---------> B ------------> Y
-         | ⌟     f'      |       h
-         |               | g
-         ∨               ∨
-         A ------------> X,
-                 f
-```
-
-or we can first form the pullback of `h` and `i`, and then form the pullback of
-`f` and the resulting `g ∘ i'`:
-
-```text
-  A ×_X (B ×_Y C) --> B ×_Y C ---------> C
-         | ⌟             | ⌟             |
-         |               | i'            | i
-         |               ∨               ∨
-         |               B ------------> Y
-         |               |       h
-         |               | g
-         ∨               ∨
-         A ------------> X.
-                 f
-```
-
-We show that both of these constructions are equivalent by showing they are
-equivalent to the standard ternary pullback.
-
-**Note:** Associativity with respect to ternary cospans
-
-```text
-              B
-              |
-              | g
-              ∨
-    A ------> X <------ C
-         f         h
-```
-
-is a special case of what we consider here that is recovered by using
-
-```text
-      f       g       g       h
-  A ----> X <---- B ----> X <---- C.
-```
-
-- See also the following relevant stack exchange question:
-  [Associativity of pullbacks](https://math.stackexchange.com/questions/2046276/associativity-of-pullbacks).
-
-#### Computing the left associated iterated standard pullback
-
-```agda
-module _
-  {l1 l2 l3 l4 l5 : Level}
-  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
-  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
-  where
-
-  map-left-associative-standard-pullback :
-    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
-    standard-ternary-pullback f g h i
-  map-left-associative-standard-pullback ((a , b , p) , c , q) =
-    ( a , b , c , p , q)
-
-  map-inv-left-associative-standard-pullback :
-    standard-ternary-pullback f g h i →
-    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
-  map-inv-left-associative-standard-pullback (a , b , c , p , q) =
-    ( ( a , b , p) , c , q)
-
-  is-equiv-map-left-associative-standard-pullback :
-    is-equiv map-left-associative-standard-pullback
-  is-equiv-map-left-associative-standard-pullback =
-    is-equiv-is-invertible
-      ( map-inv-left-associative-standard-pullback)
-      ( refl-htpy)
-      ( refl-htpy)
-
-  compute-left-associative-standard-pullback :
-    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
-    standard-ternary-pullback f g h i
-  compute-left-associative-standard-pullback =
-    ( map-left-associative-standard-pullback ,
-      is-equiv-map-left-associative-standard-pullback)
-```
-
-#### Computing the right associated iterated dependent pullback
-
-```agda
-module _
-  {l1 l2 l3 l4 l5 : Level}
-  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
-  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
-  where
-
-  map-right-associative-standard-pullback :
-    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
-    standard-ternary-pullback f g h i
-  map-right-associative-standard-pullback (a , (b , c , p) , q) =
-    ( a , b , c , q , p)
-
-  map-inv-right-associative-standard-pullback :
-    standard-ternary-pullback f g h i →
-    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
-  map-inv-right-associative-standard-pullback (a , b , c , p , q) =
-    ( a , (b , c , q) , p)
-
-  is-equiv-map-right-associative-standard-pullback :
-    is-equiv map-right-associative-standard-pullback
-  is-equiv-map-right-associative-standard-pullback =
-    is-equiv-is-invertible
-      ( map-inv-right-associative-standard-pullback)
-      ( refl-htpy)
-      ( refl-htpy)
-
-  compute-right-associative-standard-pullback :
-    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃
-    standard-ternary-pullback f g h i
-  compute-right-associative-standard-pullback =
-    ( map-right-associative-standard-pullback ,
-      is-equiv-map-right-associative-standard-pullback)
-```
-
-#### Standard pullbacks are associative
-
-```agda
-module _
-  {l1 l2 l3 l4 l5 : Level}
-  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
-  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
-  where
-
-  associative-standard-pullback :
-    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
-    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
-  associative-standard-pullback =
-    ( inv-equiv (compute-right-associative-standard-pullback f g h i)) ∘e
-    ( compute-left-associative-standard-pullback f g h i)
-
-  map-associative-standard-pullback :
-    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
-    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
-  map-associative-standard-pullback = map-equiv associative-standard-pullback
-
-  map-inv-associative-standard-pullback :
-    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
-    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
-  map-inv-associative-standard-pullback =
-    map-inv-equiv associative-standard-pullback
-```
-
 ### Pullbacks can be "folded"
 
 Given a standard pullback square
diff --git a/src/foundation/standard-ternary-pullbacks.lagda.md b/src/foundation/standard-ternary-pullbacks.lagda.md
new file mode 100644
index 0000000000..6ca4fd1596
--- /dev/null
+++ b/src/foundation/standard-ternary-pullbacks.lagda.md
@@ -0,0 +1,76 @@
+# Standard ternary pullbacks
+
+```agda
+module foundation.standard-ternary-pullbacks where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cones-over-cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equality-cartesian-product-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.identity-types
+open import foundation.structure-identity-principle
+open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
+open import foundation-core.commuting-squares-of-maps
+open import foundation-core.diagonal-maps-cartesian-products-of-types
+open import foundation-core.equality-dependent-pair-types
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.homotopies
+open import foundation-core.retractions
+open import foundation-core.sections
+open import foundation-core.type-theoretic-principle-of-choice
+open import foundation-core.universal-property-pullbacks
+open import foundation-core.whiskering-identifications-concatenation
+```
+
+</details>
+
+## Idea
+
+Given two [cospan of types](foundation.cospans.md) with a shared vertex `B`:
+
+```text
+      f       g       h       i
+  A ----> X <---- B ----> Y <---- C,
+```
+
+we call the standard limit of the diagram the
+{{#concept "standard ternary pullback" Disambiguation="of types" Agda=standard-ternary-pullback}}.
+It is defined as the [sum](foundation.dependent-pair-types.md)
+
+```text
+  standard-ternary-pullback f g h i :=
+    Σ (a : A) (b : B) (c : C), ((f a ＝ g b) × (h b ＝ i c)).
+```
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  where
+
+  standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  standard-ternary-pullback =
+    Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (h b ＝ i c))))
+```
+
+## See also
+
+- [Type arithmetic with standard pullbacks](foundation.type-arithmetic-standard-pullbacks.md)
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation/type-arithmetic-standard-pullbacks.lagda.md b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md
new file mode 100644
index 0000000000..09335074fa
--- /dev/null
+++ b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md
@@ -0,0 +1,417 @@
+# Type arithmetic with standard pullbacks
+
+```agda
+module foundation.type-arithmetic-standard-pullbacks where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cones-over-cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.standard-pullbacks
+open import foundation.standard-ternary-pullbacks
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
+open import foundation-core.contractible-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.propositions
+open import foundation-core.retractions
+open import foundation-core.sections
+```
+
+</details>
+
+## Idea
+
+We prove laws for the manipulation of
+[standard pullbacks](foundation.standard-pullbacks.md) with respect to
+themselves.
+
+## Laws
+
+### Standard pullbacks are associative
+
+Consider two cospans with a shared vertex `B`:
+
+```text
+      f       g       h       i
+  A ----> X <---- B ----> Y <---- C,
+```
+
+then we can construct their limit using standard pullbacks in two equivalent
+ways. We can construct it by first forming the standard pullback of `f` and `g`,
+and then forming the standard pullback of the resulting `h ∘ f'` and `i`
+
+```text
+  (A ×_X B) ×_Y C ---------------------> C
+         | ⌟                             |
+         |                               | i
+         ∨                               ∨
+      A ×_X B ---------> B ------------> Y
+         | ⌟     f'      |       h
+         |               | g
+         ∨               ∨
+         A ------------> X,
+                 f
+```
+
+or we can first form the pullback of `h` and `i`, and then form the pullback of
+`f` and the resulting `g ∘ i'`:
+
+```text
+  A ×_X (B ×_Y C) --> B ×_Y C ---------> C
+         | ⌟             | ⌟             |
+         |               | i'            | i
+         |               ∨               ∨
+         |               B ------------> Y
+         |               |       h
+         |               | g
+         ∨               ∨
+         A ------------> X.
+                 f
+```
+
+We show that both of these constructions are equivalent by showing they are
+equivalent to the standard ternary pullback.
+
+**Note:** Associativity with respect to ternary cospans
+
+```text
+              B
+              |
+              | g
+              ∨
+    A ------> X <------ C
+         f         h
+```
+
+is a special case of what we consider here that is recovered by using
+
+```text
+      f       g       g       h
+  A ----> X <---- B ----> X <---- C.
+```
+
+- See also the following relevant stack exchange question:
+  [Associativity of pullbacks](https://math.stackexchange.com/questions/2046276/associativity-of-pullbacks).
+
+#### Computing the left associated iterated standard pullback
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  where
+
+  map-left-associative-standard-pullback :
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
+    standard-ternary-pullback f g h i
+  map-left-associative-standard-pullback ((a , b , p) , c , q) =
+    ( a , b , c , p , q)
+
+  map-inv-left-associative-standard-pullback :
+    standard-ternary-pullback f g h i →
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
+  map-inv-left-associative-standard-pullback (a , b , c , p , q) =
+    ( ( a , b , p) , c , q)
+
+  is-equiv-map-left-associative-standard-pullback :
+    is-equiv map-left-associative-standard-pullback
+  is-equiv-map-left-associative-standard-pullback =
+    is-equiv-is-invertible
+      ( map-inv-left-associative-standard-pullback)
+      ( refl-htpy)
+      ( refl-htpy)
+
+  is-equiv-map-inv-left-associative-standard-pullback :
+    is-equiv map-inv-left-associative-standard-pullback
+  is-equiv-map-inv-left-associative-standard-pullback =
+    is-equiv-is-invertible
+      ( map-left-associative-standard-pullback)
+      ( refl-htpy)
+      ( refl-htpy)
+
+  compute-left-associative-standard-pullback :
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
+    standard-ternary-pullback f g h i
+  compute-left-associative-standard-pullback =
+    ( map-left-associative-standard-pullback ,
+      is-equiv-map-left-associative-standard-pullback)
+
+  compute-inv-left-associative-standard-pullback :
+    standard-ternary-pullback f g h i ≃
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
+  compute-inv-left-associative-standard-pullback =
+    ( map-inv-left-associative-standard-pullback ,
+      is-equiv-map-inv-left-associative-standard-pullback)
+```
+
+#### Computing the right associated iterated dependent pullback
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  where
+
+  map-right-associative-standard-pullback :
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
+    standard-ternary-pullback f g h i
+  map-right-associative-standard-pullback (a , (b , c , p) , q) =
+    ( a , b , c , q , p)
+
+  map-inv-right-associative-standard-pullback :
+    standard-ternary-pullback f g h i →
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
+  map-inv-right-associative-standard-pullback (a , b , c , p , q) =
+    ( a , (b , c , q) , p)
+
+  is-equiv-map-right-associative-standard-pullback :
+    is-equiv map-right-associative-standard-pullback
+  is-equiv-map-right-associative-standard-pullback =
+    is-equiv-is-invertible
+      ( map-inv-right-associative-standard-pullback)
+      ( refl-htpy)
+      ( refl-htpy)
+
+  is-equiv-map-inv-right-associative-standard-pullback :
+    is-equiv map-inv-right-associative-standard-pullback
+  is-equiv-map-inv-right-associative-standard-pullback =
+    is-equiv-is-invertible
+      ( map-right-associative-standard-pullback)
+      ( refl-htpy)
+      ( refl-htpy)
+
+  compute-right-associative-standard-pullback :
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃
+    standard-ternary-pullback f g h i
+  compute-right-associative-standard-pullback =
+    ( map-right-associative-standard-pullback ,
+      is-equiv-map-right-associative-standard-pullback)
+
+  compute-inv-right-associative-standard-pullback :
+    standard-ternary-pullback f g h i ≃
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
+  compute-inv-right-associative-standard-pullback =
+    ( map-inv-right-associative-standard-pullback ,
+      is-equiv-map-inv-right-associative-standard-pullback)
+```
+
+#### Standard pullbacks are associative
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  where
+
+  associative-standard-pullback :
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
+  associative-standard-pullback =
+    ( compute-inv-right-associative-standard-pullback f g h i) ∘e
+    ( compute-left-associative-standard-pullback f g h i)
+
+  inv-associative-standard-pullback :
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
+  inv-associative-standard-pullback =
+    ( compute-inv-left-associative-standard-pullback f g h i) ∘e
+    ( compute-right-associative-standard-pullback f g h i)
+
+  map-associative-standard-pullback :
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
+  map-associative-standard-pullback = map-equiv associative-standard-pullback
+
+  map-inv-associative-standard-pullback :
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
+  map-inv-associative-standard-pullback =
+    map-inv-equiv associative-standard-pullback
+```
+
+### Unit laws for standard pullbacks
+
+Pulling back along the identity map
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X)
+  where
+
+  map-left-unit-law-standard-pullback :
+    standard-pullback id f → A
+  map-left-unit-law-standard-pullback (x , a , p) = a
+
+  map-inv-left-unit-law-standard-pullback :
+    A → standard-pullback id f
+  map-inv-left-unit-law-standard-pullback a = f a , a , refl
+
+  is-section-map-inv-left-unit-law-standard-pullback :
+    is-section
+      map-left-unit-law-standard-pullback
+      map-inv-left-unit-law-standard-pullback
+  is-section-map-inv-left-unit-law-standard-pullback = refl-htpy
+
+  is-retraction-map-inv-left-unit-law-standard-pullback :
+    is-retraction
+      map-left-unit-law-standard-pullback
+      map-inv-left-unit-law-standard-pullback
+  is-retraction-map-inv-left-unit-law-standard-pullback (.(f a) , a , refl) =
+    refl
+
+  is-equiv-map-left-unit-law-standard-pullback :
+    is-equiv map-left-unit-law-standard-pullback
+  is-equiv-map-left-unit-law-standard-pullback =
+    is-equiv-is-invertible
+      map-inv-left-unit-law-standard-pullback
+      is-section-map-inv-left-unit-law-standard-pullback
+      is-retraction-map-inv-left-unit-law-standard-pullback
+
+  is-equiv-map-inv-left-unit-law-standard-pullback :
+    is-equiv map-inv-left-unit-law-standard-pullback
+  is-equiv-map-inv-left-unit-law-standard-pullback =
+    is-equiv-is-invertible
+      map-left-unit-law-standard-pullback
+      is-retraction-map-inv-left-unit-law-standard-pullback
+      is-section-map-inv-left-unit-law-standard-pullback
+
+  left-unit-law-standard-pullback :
+    standard-pullback id f ≃ A
+  left-unit-law-standard-pullback =
+    map-left-unit-law-standard-pullback ,
+    is-equiv-map-left-unit-law-standard-pullback
+
+  inv-left-unit-law-standard-pullback :
+    A ≃ standard-pullback id f
+  inv-left-unit-law-standard-pullback =
+    map-inv-left-unit-law-standard-pullback ,
+    is-equiv-map-inv-left-unit-law-standard-pullback
+```
+
+### Unit laws for standard pullbacks
+
+Pulling back along the identity map is the identity operation.
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X)
+  where
+
+  map-right-unit-law-standard-pullback :
+    standard-pullback f id → A
+  map-right-unit-law-standard-pullback (a , x , p) = a
+
+  map-inv-right-unit-law-standard-pullback :
+    A → standard-pullback f id
+  map-inv-right-unit-law-standard-pullback a = a , f a , refl
+
+  is-section-map-inv-right-unit-law-standard-pullback :
+    is-section
+      map-right-unit-law-standard-pullback
+      map-inv-right-unit-law-standard-pullback
+  is-section-map-inv-right-unit-law-standard-pullback = refl-htpy
+
+  is-retraction-map-inv-right-unit-law-standard-pullback :
+    is-retraction
+      map-right-unit-law-standard-pullback
+      map-inv-right-unit-law-standard-pullback
+  is-retraction-map-inv-right-unit-law-standard-pullback (a , .(f a) , refl) =
+    refl
+
+  is-equiv-map-right-unit-law-standard-pullback :
+    is-equiv map-right-unit-law-standard-pullback
+  is-equiv-map-right-unit-law-standard-pullback =
+    is-equiv-is-invertible
+      map-inv-right-unit-law-standard-pullback
+      is-section-map-inv-right-unit-law-standard-pullback
+      is-retraction-map-inv-right-unit-law-standard-pullback
+
+  is-equiv-map-inv-right-unit-law-standard-pullback :
+    is-equiv map-inv-right-unit-law-standard-pullback
+  is-equiv-map-inv-right-unit-law-standard-pullback =
+    is-equiv-is-invertible
+      map-right-unit-law-standard-pullback
+      is-retraction-map-inv-right-unit-law-standard-pullback
+      is-section-map-inv-right-unit-law-standard-pullback
+
+  right-unit-law-standard-pullback :
+    standard-pullback f id ≃ A
+  right-unit-law-standard-pullback =
+    map-right-unit-law-standard-pullback ,
+    is-equiv-map-right-unit-law-standard-pullback
+
+  inv-right-unit-law-standard-pullback :
+    A ≃ standard-pullback f id
+  inv-right-unit-law-standard-pullback =
+    map-inv-right-unit-law-standard-pullback ,
+    is-equiv-map-inv-right-unit-law-standard-pullback
+```
+
+### Standard pullbacks are symmetric
+
+The standard pullback of `f : A -> X <- B : g` is equivalent to the standard
+pullback of `g : B -> X <- A : f`.
+
+```agda
+map-commutative-standard-pullback :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) → standard-pullback f g → standard-pullback g f
+pr1 (map-commutative-standard-pullback f g x) =
+  horizontal-map-standard-pullback x
+pr1 (pr2 (map-commutative-standard-pullback f g x)) =
+  vertical-map-standard-pullback x
+pr2 (pr2 (map-commutative-standard-pullback f g x)) =
+  inv (coherence-square-standard-pullback x)
+
+inv-inv-map-commutative-standard-pullback :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) →
+  ( map-commutative-standard-pullback f g ∘
+    map-commutative-standard-pullback g f) ~ id
+inv-inv-map-commutative-standard-pullback f g x =
+  eq-pair-eq-fiber
+    ( eq-pair-eq-fiber
+      ( inv-inv (coherence-square-standard-pullback x)))
+
+abstract
+  is-equiv-map-commutative-standard-pullback :
+    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+    (f : A → X) (g : B → X) → is-equiv (map-commutative-standard-pullback f g)
+  is-equiv-map-commutative-standard-pullback f g =
+    is-equiv-is-invertible
+      ( map-commutative-standard-pullback g f)
+      ( inv-inv-map-commutative-standard-pullback f g)
+      ( inv-inv-map-commutative-standard-pullback g f)
+
+commutative-standard-pullback :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) →
+  standard-pullback f g ≃ standard-pullback g f
+pr1 (commutative-standard-pullback f g) =
+  map-commutative-standard-pullback f g
+pr2 (commutative-standard-pullback f g) =
+  is-equiv-map-commutative-standard-pullback f g
+```
+
+#### The gap map of the swapped cone computes as the underlying gap map followed by a swap
+
+```agda
+triangle-map-commutative-standard-pullback :
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
+  (f : A → X) (g : B → X) (c : cone f g C) →
+  gap g f (swap-cone f g c) ~
+  map-commutative-standard-pullback f g ∘ gap f g c
+triangle-map-commutative-standard-pullback f g c = refl-htpy
+```

From 6e5e8cf703bbf492704b5c7fa7c97db610e15962 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 3 Jan 2025 18:43:51 +0100
Subject: [PATCH 2/6] vertical composition spans of spans

---
 src/foundation.lagda.md                       |   1 +
 ...zontal-composition-spans-of-spans.lagda.md |   4 +-
 ...rtical-composition-spans-of-spans.lagda.md | 185 ++++++++++++++++++
 3 files changed, 188 insertions(+), 2 deletions(-)
 create mode 100644 src/foundation/vertical-composition-spans-of-spans.lagda.md

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 6858aa69d0..8d049c7d4c 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -480,6 +480,7 @@ open import foundation.unordered-pairs-of-types public
 open import foundation.unordered-tuples public
 open import foundation.unordered-tuples-of-types public
 open import foundation.vectors-set-quotients public
+open import foundation.vertical-composition-spans-of-spans public
 open import foundation.weak-function-extensionality public
 open import foundation.weak-limited-principle-of-omniscience public
 open import foundation.weakly-constant-maps public
diff --git a/src/foundation/horizontal-composition-spans-of-spans.lagda.md b/src/foundation/horizontal-composition-spans-of-spans.lagda.md
index 76d9afec8c..b0e0ab2a94 100644
--- a/src/foundation/horizontal-composition-spans-of-spans.lagda.md
+++ b/src/foundation/horizontal-composition-spans-of-spans.lagda.md
@@ -48,8 +48,8 @@ Given two [spans](foundation.spans.md) `F` and `G` from `A` to `B` and two spans
 
 then we may
 {{#concept "horizontally compose" Disambiguation="spans of spans" Agda=horizontal-comp-span-of-spans}}
-`α` and `β` to obtain a span of spans from `H ∘ F` to `I ∘ G`. The horizontal
-composite is given by the span of spans
+`α` and `β` to obtain a span of spans from `H ∘ F` to `I ∘ G` denoted as
+`α ∙ β`. Explicitly, the horizontal composite is given by the span of spans
 
 ```text
   F₀ ×_B H₀ ---------> C
diff --git a/src/foundation/vertical-composition-spans-of-spans.lagda.md b/src/foundation/vertical-composition-spans-of-spans.lagda.md
new file mode 100644
index 0000000000..08e78ef65d
--- /dev/null
+++ b/src/foundation/vertical-composition-spans-of-spans.lagda.md
@@ -0,0 +1,185 @@
+# Vertical composition of spans of spans
+
+```agda
+module foundation.vertical-composition-spans-of-spans where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-triangles-of-maps
+open import foundation.composition-spans
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.equivalences-spans
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.morphisms-arrows
+open import foundation.morphisms-spans
+open import foundation.pullbacks
+open import foundation.spans
+open import foundation.spans-of-spans
+open import foundation.standard-pullbacks
+open import foundation.type-arithmetic-standard-pullbacks
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Given three [spans](foundation.spans.md) `F`, `G` and `H` from `A` to `B`, a
+[span of spans](foundation.spans-of-spans.md) `α` from `F` to `G` and a span of
+spans `β` from `G` to `H`
+
+```text
+         F₀
+      /  ↑  \
+     /   α₀  \
+    ∨    ↓    ∨
+  A <--- G₀---> B
+    ∧    ↑    ∧
+     \   β₀  /
+      \  ↓  /
+         H₀
+```
+
+then we may
+{{#concept "vertically compose" Disambiguation="spans of types" Agda=vertical-comp-span-of-spans-of-spans}}
+the two spans of spans, denoted `β ∘ α`. The underlying span of the vertical
+composite is given by the composition of the underlying spans.
+
+## Definitions
+
+### Vertical composition of spans of spans
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {A : UU l1} {B : UU l2}
+  (F : span l3 A B) (G : span l4 A B) (H : span l5 A B)
+  (β : span-of-spans l6 G H) (α : span-of-spans l7 F G)
+  where
+
+  spanning-type-vertical-comp-span-of-spans : UU (l4 ⊔ l6 ⊔ l7)
+  spanning-type-vertical-comp-span-of-spans =
+    spanning-type-comp-span
+      ( span-span-of-spans G H β)
+      ( span-span-of-spans F G α)
+
+  left-map-vertical-comp-span-of-spans :
+    spanning-type-vertical-comp-span-of-spans → spanning-type-span F
+  left-map-vertical-comp-span-of-spans =
+    left-map-comp-span
+      ( span-span-of-spans G H β)
+      ( span-span-of-spans F G α)
+
+  right-map-vertical-comp-span-of-spans :
+    spanning-type-vertical-comp-span-of-spans → spanning-type-span H
+  right-map-vertical-comp-span-of-spans =
+    right-map-comp-span
+      ( span-span-of-spans G H β)
+      ( span-span-of-spans F G α)
+
+  span-vertical-comp-span-of-spans :
+    span (l4 ⊔ l6 ⊔ l7) (spanning-type-span F) (spanning-type-span H)
+  span-vertical-comp-span-of-spans =
+    comp-span (span-span-of-spans G H β) (span-span-of-spans F G α)
+
+  coherence-left-vertical-comp-span-of-spans :
+    coherence-left-span-of-spans F H span-vertical-comp-span-of-spans
+  coherence-left-vertical-comp-span-of-spans =
+    homotopy-reasoning
+      ( left-map-span H ∘
+        right-map-span-of-spans G H β ∘
+        horizontal-map-standard-pullback)
+    ~ ( left-map-span G ∘
+        left-map-span-of-spans G H β ∘
+        horizontal-map-standard-pullback)
+    by coh-left-span-of-spans G H β ·r horizontal-map-standard-pullback
+    ~ ( left-map-span G ∘
+        right-map-span-of-spans F G α ∘
+        vertical-map-standard-pullback)
+    by left-map-span G ·l inv-htpy coherence-square-standard-pullback
+    ~ ( left-map-span F ∘
+        left-map-span-of-spans F G α ∘
+        vertical-map-standard-pullback)
+    by coh-left-span-of-spans F G α ·r vertical-map-standard-pullback
+
+  coherence-right-vertical-comp-span-of-spans :
+    coherence-right-span-of-spans F H span-vertical-comp-span-of-spans
+  coherence-right-vertical-comp-span-of-spans =
+    homotopy-reasoning
+      ( right-map-span H ∘
+        right-map-span-of-spans G H β ∘
+        horizontal-map-standard-pullback)
+    ~ ( right-map-span G ∘
+        left-map-span-of-spans G H β ∘
+        horizontal-map-standard-pullback)
+    by coh-right-span-of-spans G H β ·r horizontal-map-standard-pullback
+    ~ ( right-map-span G ∘
+        right-map-span-of-spans F G α ∘
+        vertical-map-standard-pullback)
+    by right-map-span G ·l inv-htpy coherence-square-standard-pullback
+    ~ ( right-map-span F ∘
+        left-map-span-of-spans F G α ∘
+        vertical-map-standard-pullback)
+    by coh-right-span-of-spans F G α ·r vertical-map-standard-pullback
+
+  coherence-vertical-comp-span-of-spans :
+    coherence-span-of-spans F H span-vertical-comp-span-of-spans
+  coherence-vertical-comp-span-of-spans =
+    coherence-left-vertical-comp-span-of-spans ,
+    coherence-right-vertical-comp-span-of-spans
+
+  vertical-comp-span-of-spans : span-of-spans (l4 ⊔ l6 ⊔ l7) F H
+  vertical-comp-span-of-spans =
+    span-vertical-comp-span-of-spans , coherence-vertical-comp-span-of-spans
+```
+
+## Properties
+
+### Associativity of vertical composition of spans of spans
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} {A : UU l1} {B : UU l2}
+  (F : span l3 A B) (G : span l4 A B) (H : span l5 A B) (I : span l6 A B)
+  (γ : span-of-spans l7 H I)
+  (β : span-of-spans l8 G H)
+  (α : span-of-spans l9 F G)
+  where
+
+  essentially-associative-spanning-type-vertical-comp-span-of-spans :
+    spanning-type-vertical-comp-span-of-spans F G I
+      ( vertical-comp-span-of-spans G H I γ β)
+      ( α) ≃
+    spanning-type-vertical-comp-span-of-spans F H I
+      ( γ)
+      ( vertical-comp-span-of-spans F G H β α)
+  essentially-associative-spanning-type-vertical-comp-span-of-spans =
+    essentially-associative-spanning-type-comp-span
+      ( span-span-of-spans H I γ)
+      ( span-span-of-spans G H β)
+      ( span-span-of-spans F G α)
+
+  essentially-associative-span-vertical-comp-span-of-spans :
+    equiv-span
+      ( span-vertical-comp-span-of-spans F G I
+        ( vertical-comp-span-of-spans G H I γ β)
+        ( α))
+      ( span-vertical-comp-span-of-spans F H I
+        ( γ)
+        ( vertical-comp-span-of-spans F G H β α))
+  essentially-associative-span-vertical-comp-span-of-spans =
+    essentially-associative-comp-span
+      ( span-span-of-spans H I γ)
+      ( span-span-of-spans G H β)
+      ( span-span-of-spans F G α)
+```
+
+> It remains to show that this equivalence is part of an equivalence of spans of
+> spans.

From 894958cca0da953b1ca0c0a0e0c3c5ceff4f62a7 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 3 Jan 2025 18:53:00 +0100
Subject: [PATCH 3/6] edits

---
 ...zontal-composition-spans-of-spans.lagda.md | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/foundation/horizontal-composition-spans-of-spans.lagda.md b/src/foundation/horizontal-composition-spans-of-spans.lagda.md
index b0e0ab2a94..75cc0e0d80 100644
--- a/src/foundation/horizontal-composition-spans-of-spans.lagda.md
+++ b/src/foundation/horizontal-composition-spans-of-spans.lagda.md
@@ -48,15 +48,16 @@ Given two [spans](foundation.spans.md) `F` and `G` from `A` to `B` and two spans
 
 then we may
 {{#concept "horizontally compose" Disambiguation="spans of spans" Agda=horizontal-comp-span-of-spans}}
-`α` and `β` to obtain a span of spans from `H ∘ F` to `I ∘ G` denoted as
-`α ∙ β`. Explicitly, the horizontal composite is given by the span of spans
+`α` and `β` to obtain a span of spans `α ∙ β` from `H ∘ F` to `I ∘ G`.
+Explicitly, the horizontal composite is given by the unique construction of a
+span of spans
 
 ```text
-  F₀ ×_B H₀ ---------> C
-     |    ↖            ∧
-     |    α₀ ×_B β₀    |
-     ∨            ↘    |
-     A <----------- G₀ ×_B I₀.
+  F₀ ×_B H₀ ----------> C
+      |    ↖            ∧
+      |    α₀ ×_B β₀    |
+      ∨            ↘    |
+      A <---------- G₀ ×_B I₀.
 ```
 
 **Note.** There are four equivalent, but judgmentally different choices of
@@ -70,8 +71,8 @@ spanning type `α₀ ×_B β₀` of the horizontal composite. We pick
       F₀ ---------> B
 ```
 
-as this is the only choice that avoids inversions of coherences as part of the
-construction.
+as this choice avoids inversions of coherences as part of the construction,
+given our choice of orientation for coherences of spans of spans.
 
 ## Definitions
 

From c6ed144999059e1417cffc1f9587fa4cd40e2a62 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 3 Jan 2025 19:01:36 +0100
Subject: [PATCH 4/6] fix title `horizontal-composition-spans-of-spans`

---
 src/foundation/horizontal-composition-spans-of-spans.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/horizontal-composition-spans-of-spans.lagda.md b/src/foundation/horizontal-composition-spans-of-spans.lagda.md
index 75cc0e0d80..eed1567115 100644
--- a/src/foundation/horizontal-composition-spans-of-spans.lagda.md
+++ b/src/foundation/horizontal-composition-spans-of-spans.lagda.md
@@ -1,4 +1,4 @@
-# Horizontal composition of higher spans
+# Horizontal composition of spans of spans
 
 ```agda
 module foundation.horizontal-composition-spans-of-spans where

From 4aa05c97ee5f5af649804ada5c8748e8b26987f9 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 3 Jan 2025 19:02:38 +0100
Subject: [PATCH 5/6] another edit

---
 .../vertical-composition-spans-of-spans.lagda.md         | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/foundation/vertical-composition-spans-of-spans.lagda.md b/src/foundation/vertical-composition-spans-of-spans.lagda.md
index 08e78ef65d..070009add5 100644
--- a/src/foundation/vertical-composition-spans-of-spans.lagda.md
+++ b/src/foundation/vertical-composition-spans-of-spans.lagda.md
@@ -41,7 +41,7 @@ spans `β` from `G` to `H`
       /  ↑  \
      /   α₀  \
     ∨    ↓    ∨
-  A <--- G₀---> B
+  A <--- G₀---> B,
     ∧    ↑    ∧
      \   β₀  /
       \  ↓  /
@@ -49,9 +49,10 @@ spans `β` from `G` to `H`
 ```
 
 then we may
-{{#concept "vertically compose" Disambiguation="spans of types" Agda=vertical-comp-span-of-spans-of-spans}}
-the two spans of spans, denoted `β ∘ α`. The underlying span of the vertical
-composite is given by the composition of the underlying spans.
+{{#concept "vertically compose" Disambiguation="spans of spans of types" Agda=vertical-comp-span-of-spans-of-spans}}
+the two spans of spans to obtain a span of spans `β ∘ α` from `F` to `H`. The
+underlying span of the vertical composite is given by the composition of the
+underlying spans.
 
 ## Definitions
 

From 525b4faa978f3a24b0ca8413db24bba9f0e29cb4 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 3 Jan 2025 20:26:23 +0100
Subject: [PATCH 6/6] fix link

---
 src/foundation/vertical-composition-spans-of-spans.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/vertical-composition-spans-of-spans.lagda.md b/src/foundation/vertical-composition-spans-of-spans.lagda.md
index 070009add5..785b482745 100644
--- a/src/foundation/vertical-composition-spans-of-spans.lagda.md
+++ b/src/foundation/vertical-composition-spans-of-spans.lagda.md
@@ -49,7 +49,7 @@ spans `β` from `G` to `H`
 ```
 
 then we may
-{{#concept "vertically compose" Disambiguation="spans of spans of types" Agda=vertical-comp-span-of-spans-of-spans}}
+{{#concept "vertically compose" Disambiguation="spans of spans of types" Agda=vertical-comp-span-of-spans}}
 the two spans of spans to obtain a span of spans `β ∘ α` from `F` to `H`. The
 underlying span of the vertical composite is given by the composition of the
 underlying spans.