# Spans of types

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2023-09-15.

module foundation.spans where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.function-types


## Idea

A binary span from A to B consists of a spanning type S and a pair of functions f : S → A and g : S → B. The types A and B in the specification of a binary span are also referred to as the domain and codomain of the span, respectively.

In foundation.binary-type-duality we show that binary relations are equivalently described as spans of types.

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. As mentioned previously, 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.

## Definitions

### (Binary) spans

span :
{l1 l2 : Level} (l : Level) (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2 ⊔ lsuc l)
span l A B = Σ (UU l) (λ X → (X → A) × (X → B))

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
(c : span l3 A B)
where

spanning-type-span : UU l3
spanning-type-span = pr1 c

left-map-span : spanning-type-span → A
left-map-span = pr1 (pr2 c)

right-map-span : spanning-type-span → B
right-map-span = pr2 (pr2 c)


### Identity spans

module _
{l1 : Level} {X : UU l1}
where

id-span : span l1 X X
pr1 id-span = X
pr1 (pr2 id-span) = id
pr2 (pr2 id-span) = id