Composition operations on spans of spans (#1231)

This PR defines
- composition of spans
- spans of spans
- vertical composition of spans of spans
- horizontal composition of spans of spans

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

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
@@ -475,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

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
+```

src/foundation/horizontal-composition-spans-of-spans.lagda.md

@@ -0,0 +1,175 @@
+# Horizontal composition of spans of 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`.
+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₀.
+```
+
+**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 choice avoids inversions of coherences as part of the construction,
+given our choice of orientation for coherences of spans of spans.
+
+## 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
+```