Span diagrams

Content created by Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-01-28.

module foundation.span-diagrams where
Imports 
open import foundation.dependent-pair-types
open import foundation.morphisms-arrows
open import foundation.spans
open import foundation.universe-levels

Idea

A (binary) span diagram is a diagram of the form

       f       g
  A <----- S -----> B.

In other words, a span diagram consists of two types A and B and a span from A to B.

We disambiguate between spans and span diagrams. We consider spans from A to B to be morphisms from A to B in the category of types and spans between them, whereas we consider span diagrams to be objects in the category of diagrams of types of the form * <---- * ----> *. Conceptually there is a subtle, but important distinction between spans and span diagrams. In binary type duality we show a span from A to B is equivalently described as a binary relation from A to B. On the other hand, span diagrams are more suitable for functorial operations that take "spans" as input, but for which the functorial action takes a natural transformation, i.e., a morphism of span diagrams, as input. Examples of this kind include pushouts.

(Binary) span diagrams

span-diagram : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
span-diagram l1 l2 l3 =
  Σ (UU l1) (λ A → Σ (UU l2) (λ B → span l3 A B))

module _
  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  where

  make-span-diagram :
    (S → A) → (S → B) → span-diagram l2 l3 l1
  pr1 (make-span-diagram f g) = A
  pr1 (pr2 (make-span-diagram f g)) = B
  pr1 (pr2 (pr2 (make-span-diagram f g))) = S
  pr1 (pr2 (pr2 (pr2 (make-span-diagram f g)))) = f
  pr2 (pr2 (pr2 (pr2 (make-span-diagram f g)))) = g

module _
  {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3)
  where

  domain-span-diagram : UU l1
  domain-span-diagram = pr1 𝒮

  codomain-span-diagram : UU l2
  codomain-span-diagram = pr1 (pr2 𝒮)

  span-span-diagram :
    span l3 domain-span-diagram codomain-span-diagram
  span-span-diagram = pr2 (pr2 𝒮)

  spanning-type-span-diagram : UU l3
  spanning-type-span-diagram =
    spanning-type-span span-span-diagram

  left-map-span-diagram : spanning-type-span-diagram → domain-span-diagram
  left-map-span-diagram =
    left-map-span span-span-diagram

  right-map-span-diagram : spanning-type-span-diagram → codomain-span-diagram
  right-map-span-diagram =
    right-map-span span-span-diagram

The span diagram obtained from a morphism of arrows

Given maps f : A → B and g : X → Y and a morphism of arrows α : f → g, the span diagram associated to α is the span diagram

       f       α₀
  B <----- A -----> X.

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A → B) (g : X → Y) (α : hom-arrow f g)
  where

  domain-span-diagram-hom-arrow : UU l2
  domain-span-diagram-hom-arrow = B

  codomain-span-diagram-hom-arrow : UU l3
  codomain-span-diagram-hom-arrow = X

  spanning-type-hom-arrow : UU l1
  spanning-type-hom-arrow = A

  left-map-span-diagram-hom-arrow :
    spanning-type-hom-arrow → domain-span-diagram-hom-arrow
  left-map-span-diagram-hom-arrow = f

  right-map-span-diagram-hom-arrow :
    spanning-type-hom-arrow → codomain-span-diagram-hom-arrow
  right-map-span-diagram-hom-arrow = map-domain-hom-arrow f g α

  span-hom-arrow :
    span l1 B X
  pr1 span-hom-arrow = A
  pr1 (pr2 span-hom-arrow) = left-map-span-diagram-hom-arrow
  pr2 (pr2 span-hom-arrow) = right-map-span-diagram-hom-arrow

  span-diagram-hom-arrow : span-diagram l2 l3 l1
  pr1 span-diagram-hom-arrow = domain-span-diagram-hom-arrow
  pr1 (pr2 span-diagram-hom-arrow) = codomain-span-diagram-hom-arrow
  pr2 (pr2 span-diagram-hom-arrow) = span-hom-arrow

See also

Recent changes