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
- Cospan diagrams
- Diagonal span diagrams
- Extensions of span diagrams
- Kernel span diagrams of maps
- Spans of families of types
- Transposition of span diagrams
Recent changes
- 2024-01-28. Egbert Rijke. Span diagrams (#1007).