open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Diagram.Pullback
open import Cat.Bi.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Bi.Instances.Spans {o β} (C : Precategory o β) where

private module C = Cat.Reasoning C
open C


# The bicategory of spansπ

Let $\mathcal{C}$ be a precategory. By a span in $\mathcal{C}$ (from an object $A : \mathcal{C}$ to an object $B : \mathcal{C}$), we mean a diagram of the form $A \leftarrow C \to B$. Note that the βvertexβ of this span, the object $C$, is part of the data, so that the collection of βspans in $\mathcal{C}$β will not be a set (unless $\mathcal{C}$ is strict) β so we can not construct a category where $\mathbf{Hom}(a,b)$ is the collection of spans from $a$ to $b$.

However, we can make spans in $\mathcal{C}$ the objects of a category, and the hom-sets are the maps in $\mathcal{C}$ between the vertices which βcommute with the legsβ. Diagramatically, a map between spans is the dashed line in

where both the left and right triangles must commute.

record Span (a b : Ob) : Type (o β β) where
constructor span
field
apex  : Ob
left  : Hom apex a
right : Hom apex b

open Span

record Span-hom {a b : Ob} (x y : Span a b) : Type β where
no-eta-equality
field
map   : Hom (x .apex) (y .apex)
left  : x .left  β‘ y .left β map
right : x .right β‘ y .right β map

open Span-hom
private unquoteDecl eqv = declare-record-iso eqv (quote Span-hom)

Span-hom-path
: {a b : Ob} {x y : Span a b} {f g : Span-hom x y}
β f .map β‘ g .map β f β‘ g
Span-hom-path p i .map = p i
Span-hom-path {x = x} {y} {f} {g} p i .left j =
is-setβsquarep (Ξ» i j β Hom-set _ _)
(Ξ» _ β x .left) (Ξ» j β f .left j) (Ξ» j β g .left j) (Ξ» j β y .left β p j) i j
Span-hom-path {x = x} {y} {f} {g} p i .right j =
is-setβsquarep (Ξ» i j β Hom-set _ _)
(Ξ» _ β x .right) (Ξ» j β f .right j) (Ξ» j β g .right j) (Ξ» j β y .right β p j) i j


The category $\operatorname{Spans}_\mathcal{C}(A, B)$ of spans between $A$ and $B$ admits a faithful functor to $\mathcal{C}$ (projecting the vertex and the βmiddle mapβ, respectively), so that equality of maps of spans can be compared at the level of maps in $\mathcal{C}$.

Spans : Ob β Ob β Precategory _ _
Spans x y .Precategory.Ob = Span x y
Spans x y .Precategory.Hom = Span-hom
Spans x y .Precategory.Hom-set _ _ = Isoβis-hlevel 2 eqv (hlevel 2)
Spans x y .Precategory.id .map = id
Spans x y .Precategory.id .left = intror refl
Spans x y .Precategory.id .right = intror refl
Spans x y .Precategory._β_ f g .map = f .map β g .map
Spans x y .Precategory._β_ f g .left = g .left β pushl (f .left)
Spans x y .Precategory._β_ f g .right = g .right β pushl (f .right)
Spans x y .Precategory.idr f = Span-hom-path (idr _)
Spans x y .Precategory.idl f = Span-hom-path (idl _)
Spans x y .Precategory.assoc f g h = Span-hom-path (assoc _ _ _)


Now suppose that $\mathcal{C}$ admits pullbacks for arbitrary pairs of maps. Supposing that we have some spans $S : A \to B$ and $S' : B \to C$, we can fit them in an M-shaped diagram like

so that taking the pullback of the diagram $S \to B \leftarrow S'$ gives us an universal solution to the problem of finding a span $A \leftarrow (S \times_B S') \to C$. Since pullbacks are universal, this composition operation is functorial, and so extends to a composition operation Span-β:

module _ (pb : β {a b c} (f : Hom a b) (g : Hom c b) β Pullback C f g) where
open Functor

Span-β : β {a b c} β Functor (Spans b c ΓαΆ Spans a b) (Spans a c)
Span-β .Fβ (sp1 , sp2) =
span pb.apex (sp2 .left β pb.pβ) (sp1 .right β pb.pβ)
where module pb = Pullback (pb (sp1 .left) (sp2 .right))

Span-β .Fβ {x1 , x2} {y1 , y2} (f , g) = res
where
module x = Pullback (pb (x1 .left) (x2 .right))
module y = Pullback (pb (y1 .left) (y2 .right))

xβy : Hom x.apex y.apex
xβy = y.universal {pβ' = f .map β x.pβ} {pβ' = g .map β x.pβ} comm
where abstract
open Pullback
comm : y1 .left β f .map β x.pβ β‘ y2 .right β g .map β x.pβ
comm = pulll (sym (f .left)) β x.square β pushl (g .right)

res : Span-hom _ _
res .map = xβy
res .left = sym (pullr y.pββuniversal β pulll (sym (g .left)))
res .right = sym (pullr y.pββuniversal β pulll (sym (f .right)))

Span-β .F-id {x1 , x2} = Span-hom-path $sym$ x.unique id-comm id-comm
where module x = Pullback (pb (x1 .left) (x2 .right))

Span-β .F-β {x1 , x2} {y1 , y2} {z1 , z2} f g =
Span-hom-path $sym$ z.unique
(pulll z.pββuniversal β pullr y.pββuniversal β assoc _ _ _)
(pulll z.pββuniversal β pullr y.pββuniversal β assoc _ _ _)
where
module x = Pullback (pb (x1 .left) (x2 .right))
module y = Pullback (pb (y1 .left) (y2 .right))
module z = Pullback (pb (z1 .left) (z2 .right))


What weβll show in the rest of this module is that Span-β lets us make Spans into the categories of 1-cells of a prebicategory, the (pre)bicategory of spans (of $\mathcal{C}$), $\operatorname{Spans}(\mathcal{C})$. As mentioned before, this prebicategory has (a priori) no upper bound on the h-levels of its 1-cells, so it is not locally strict. We remark that when $\mathcal{C}$ is univalent, then $\operatorname{Spans}(\mathcal{C})$ is locally so, and when $\mathcal{C}$ is gaunt, then $\operatorname{Spans}(\mathcal{C})$ is strict.

Since the details of the full construction are grueling, we will present only an overview of the unitors and the associator. For the left unitor, observe that the composition $\operatorname{id}_{} \circ S$ is implemented by a pullback diagram like

but observe that the maps $S \xrightarrow{f} A$ and $S \xrightarrow{\operatorname{id}_{}} S$ also form a cone over the cospan $A \to A \xleftarrow{f} S$, so that there is a unique map filling the dashed line in the diagram above such that everything commutes: hence there is an invertible 2-cell $\operatorname{id}_{} \circ S \Rightarrow S$. The right unitor is analogous.

  open Prebicategory
open Pullback

private
_Β€_ : β {a b c} (x : Span b c) (y : Span a b) β Span a c
f Β€ g = Span-β .Fβ (f , g)

sΞ»β : β {A B} (x : Span A B) β Span-hom x (span _ C.id C.id Β€ x)
sΞ»β x .map   = pb _ _ .universal id-comm-sym
sΞ»β x .left  = sym $pullr (pb _ _ .pββuniversal) β idr _ sΞ»β x .right = sym$ pullr (pb _ _ .pββuniversal) β idl _

sΟβ : β {A B} (x : Span A B) β Span-hom x (x Β€ span _ C.id C.id)
sΟβ x .map   = pb _ _ .universal id-comm
sΟβ x .left  = sym $pullr (pb _ _ .pββuniversal) β idl _ sΟβ x .right = sym$ pullr (pb _ _ .pββuniversal) β idr _


For the associator, while doing the construction in elementary terms is quite complicated, we observe that, diagramatically, the composite of three morphisms fits into a diagram like

so that, at a high level, there is no confusion as to which composite is meant. From then, itβs just a matter of proving pullbacks are associative (in a standard, but annoying, way), and showing that these canonically-obtained isomorphisms (are natural in all the possible variables and) satisfy the triangle and pentagon identities.

On second thought, letβs not read that. Tβis a silly theorem.
    sΞ±β : β {A B C D} ((f , g , h) : Span C D Γ Span B C Γ Span A B)
β Span-hom ((f Β€ g) Β€ h) (f Β€ (g Β€ h))
sΞ±β (f , g , h) .map = pb _ _ .universal respβ² where
abstract
resp : g .left C.β pb (f .left) (g .right) .pβ
C.β pb ((f Β€ g) .left) (h .right) .pβ
β‘ h .right C.β pb ((f Β€ g) .left) (h .right) .pβ
resp = assoc _ _ _ β pb _ _ .square

shuffle = pb _ _ .universal {pβ' = pb _ _ .pβ C.β pb _ _ .pβ} {pβ' = pb _ _ .pβ} resp

abstract
respβ² : f .left C.β pb (f .left) (g .right) .pβ
C.β pb ((f Β€ g) .left) (h .right) .pβ
β‘ (g Β€ h) .right C.β shuffle
respβ² = sym $pullr (pb _ _ .pββuniversal) β extendl (sym (pb _ _ .square)) sΞ±β (f , g , h) .left = sym$ pullr (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal)
sΞ±β (f , g , h) .right = sym $pullr (pb _ _ .pββuniversal) β assoc _ _ _ sΞ±β : β {A B C D} ((f , g , h) : Span C D Γ Span B C Γ Span A B) β Span-hom (f Β€ (g Β€ h)) ((f Β€ g) Β€ h) sΞ±β (f , g , h) .map = pb _ _ .universal respβ² where abstract resp : f .left C.β pb (f .left) ((g Β€ h) .right) .pβ β‘ g .right C.β pb (g .left) (h .right) .pβ C.β pb (f .left) ((g Β€ h) .right) .pβ resp = pb _ _ .square β sym (assoc _ _ _) shuffle = pb _ _ .universal {pβ' = pb _ _ .pβ} {pβ' = pb _ _ .pβ C.β pb _ _ .pβ} resp abstract respβ² : (f Β€ g) .left C.β shuffle β‘ h .right C.β pb (g .left) (h .right) .pβ C.β pb (f .left) ((g Β€ h) .right) .pβ respβ² = pullr (pb _ _ .pββuniversal) β extendl (pb _ _ .square) sΞ±β (f , g , h) .left = sym$ pullr (pb _ _ .pββuniversal) β assoc _ _ _
sΞ±β (f , g , h) .right = sym $pullr (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) open make-natural-iso {-# TERMINATING #-} Spanα΅ : Prebicategory _ _ _ Spanα΅ .Ob = C.Ob Spanα΅ .Hom = Spans Spanα΅ .id = span _ C.id C.id Spanα΅ .compose = Span-β Spanα΅ .unitor-l = to-natural-iso ni where ni : make-natural-iso (Id {C = Spans _ _}) _ ni .eta = sΞ»β ni .inv x .map = pb _ _ .pβ ni .inv x .left = refl ni .inv x .right = pb _ _ .square ni .etaβinv x = Span-hom-path (Pullback.uniqueβ (pb _ _) {p = idl _ β apβ C._β_ refl (introl refl)} (pulll (pb _ _ .pββuniversal)) (pulll (pb _ _ .pββuniversal)) (id-comm β pb _ _ .square) id-comm) ni .invβeta x = Span-hom-path (pb _ _ .pββuniversal) ni .natural x y f = Span-hom-path$
Pullback.uniqueβ (pb _ _) {p = idl _ β f .right}
(pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β idl _)
(pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β idr _)
(pulll (pb _ _ .pββuniversal) β sym (f .right))
(pulll (pb _ _ .pββuniversal) β idl _)
Spanα΅ .unitor-r = to-natural-iso ni where
ni : make-natural-iso (Id {C = Spans _ _}) _
ni .eta = sΟβ
ni .inv _ .map = pb _ _ .pβ
ni .inv _ .left = sym (pb _ _ .square)
ni .inv _ .right = refl
ni .etaβinv x = Span-hom-path (Pullback.uniqueβ (pb _ _) {p = introl refl}
(pulll (pb _ _ .pββuniversal) β idl _)
(pulll (pb _ _ .pββuniversal))
(idr _)
(id-comm β sym (pb _ _ .square)))
ni .invβeta x = Span-hom-path (pb _ _ .pββuniversal)
ni .natural x y f = Span-hom-path $Pullback.uniqueβ (pb _ _) {p = sym (f .left) β introl refl} (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β idr _) (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β idl _) (pulll (pb _ _ .pββuniversal) β idl _) (pulll (pb _ _ .pββuniversal) β sym (f .left)) Spanα΅ .associator = to-natural-iso ni where ni : make-natural-iso _ _ ni .eta = sΞ±β ni .inv = sΞ±β ni .etaβinv x = Span-hom-path$
Pullback.uniqueβ (pb _ _) {p = pb _ _ .square}
(pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β pb _ _ .pββuniversal)
(pulll (pb _ _ .pββuniversal) β uniqueβ (pb _ _) {p = extendl (pb _ _ .square)}
(pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β pb _ _ .pββuniversal)
(pulll (pb _ _ .pββuniversal) β pb _ _ .pββuniversal)
refl refl)
(idr _)
(idr _)
ni .invβeta x = Span-hom-path $Pullback.uniqueβ (pb _ _) {p = pb _ _ .square} (pulll (pb _ _ .pββuniversal) β uniqueβ (pb _ _) {p = extendl (pb _ _ .square)} (pulll (pb _ _ .pββuniversal) β pb _ _ .pββuniversal) (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β pb _ _ .pββuniversal) refl refl) (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β pb _ _ .pββuniversal) (idr _) (idr _) ni .natural x y f = Span-hom-path$ Pullback.uniqueβ (pb _ _)
{pβ' = f .fst .map C.β pb _ _ .pβ C.β pb _ _ .pβ}
{pβ' = pb _ _ .universal
{pβ' = f .snd .fst .map C.β pb _ _ .pβ C.β pb _ _ .pβ}
{pβ' = f .snd .snd .map C.β pb _ _ .pβ}
(pulll (sym (f .snd .fst .left)) β assoc _ _ _ β pb _ _ .square β pushl (f .snd .snd .right))}
{p = sym $pullr (pb _ _ .pββuniversal) β pulll (sym (f .snd .fst .right)) β extendl (sym (pb _ _ .square)) β pushl (f .fst .left)} (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal)) (pulll (pb _ _ .pββuniversal) β pb _ _ .unique (pulll (extendl (pb _ _ .pββuniversal)) β pullr (pullr (pb _ _ .pββuniversal)) β apβ C._β_ refl (pb _ _ .pββuniversal)) (pulll (extendl (pb _ _ .pββuniversal)) β pullr (pullr (pb _ _ .pββuniversal)) β apβ C._β_ refl (pb _ _ .pββuniversal))) (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β pulll (pb _ _ .pββuniversal) β sym (assoc _ _ _)) (pulll (pb _ _ .pββuniversal) β pb _ _ .unique (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β extendl (pb _ _ .pββuniversal)) (pulll (pb _ _ .pββuniversal) β pb _ _ .pββuniversal)) Spanα΅ .triangle f g = Span-hom-path$
pb _ _ .unique
(pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β pb _ _ .pββuniversal β introl refl)
(pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal) β eliml refl)
Spanα΅ .pentagon f g h i = Span-hom-path \$
Pullback.uniqueβ (pb _ _)
{p = pullr (pulll (pb _ _ .pββuniversal) β pullr (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal)) β apβ C._β_ refl (pulll (pb _ _ .pββuniversal)))
β apβ C._β_ refl (extendl (pb _ _ .pββuniversal)) β sym (apβ C._β_ refl (idl _ β extendl (pb _ _ .pββuniversal)) β extendl (sym (pb _ _ .square)))}
(pulll (pb _ _ .pββuniversal) β pullr (pulll (pb _ _ .pββuniversal)))
(pulll (pb _ _ .pββuniversal) β pullr (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal)))
(pulll (pb _ _ .pββuniversal)
β Pullback.uniqueβ (pb _ _) {p = pullr (pb _ _ .pββuniversal) β extendl (pb _ _ .square) β sym (assoc _ _ _)}
(pulll (pb _ _ .pββuniversal) β pb _ _ .pββuniversal)
(pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal))
(pulll (pb _ _ .pββuniversal) β pb _ _ .unique
(pulll (pb _ _ .pββuniversal) β pulll (pb _ _ .pββuniversal) β pb _ _ .pββuniversal β idl _)
(pulll (pb _ _ .pββuniversal) β pulll (pullr (pb _ _ .pββuniversal)) β pullr (pullr (pb _ _ .pββuniversal) β pulll (pb _ _ .pββuniversal)) β pulll (pb _ _ .pββuniversal)))
(pulll (pb _ _ .pββuniversal) β pullr (pulll (pb _ _ .pββuniversal) β pullr (pb _ _ .pββuniversal))
β apβ C._β_ refl (pulll (pb _ _ .pββuniversal)) β pulll (pb _ _ .pββuniversal) β sym (assoc _ _ _)))
( pulll (pb _ _ .pββuniversal)
Β·Β· pullr (pb _ _ .pββuniversal)
Β·Β· sym (idl _ Β·Β· pulll (pb _ _ .pββuniversal) Β·Β· sym (assoc _ _ _)))