Let $\mathbb{A}$ and $\mathbb{B}$ be categories.
A span category (”span of categories”) from $\mathbb{A}$ to $\mathbb{B}$ is a category $\mathcal{R}$ with a pair of functors $\pi_\mathcal{R}^\mathbb{A} : \mathcal{R}\to \mathbb{A}$ and $\pi_\mathcal{R}^\mathbb{B} : \mathcal{R}\to \mathbb{B}$.
We denote the span by $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$, or $\mathcal{R}: \mathbb{A}\,\|\, \mathbb{B}$. Note this data is equivalent to a functor $(\pi^\mathbb{A}\mathcal{R}, \pi^\mathbb{B}\mathcal{R}) : \mathcal{R}\to \mathbb{A\times B}$.
$\mathbb{A}$ and $\mathbb{B}$ are the base categories, and $\mathcal{R}$ is the total category; we may refer to the span simply as $\mathcal{R}$.
We can draw a span category $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ simply as a string.
We can see a span category as a matrix of categories, by inverse image along $\mathcal{R}\to \mathbb{A\times B}$. The notion of inverse image along a functor $\mathcal{S}\to \mathbb{C}$ has been given by Street in [Str01]; the resulting map $\mathcal{S}:\mathbb{C\to C}\mathrm{at}$ is called a normal lax functor. The notion was later developed for use in type theory, and rebranded as “displayed category” [AL18].
A displayed category $\mathcal{R}:\mathbb{A\times B\to C}\mathrm{at}$ gives, for each pair of:
| objects | $\mathrm{A}:\mathbb{A}, \mathrm{B}:\mathbb{B}$ | a category | $\mathcal{R}(\mathrm{A,B}): \mathrm{Cat}$ |
|---|---|---|---|
| morphisms | $\mathrm{a}:\mathbb{A}(\mathrm{A_0,A_1}), \mathrm{b}:\mathbb{B} | ||
| (\mathrm{B_0,B_1})$ | a profunctor | $\vec{\mathcal{R}}(\mathrm{a,b}): \mathcal{R}(\mathrm{A_0,B_0}) \, | \, \mathcal{R}(\mathrm{A_1,B_1})$ |
| composable pairs | $\mathrm{(a_1,b_1), (a_2,b_2)}$ | a transformation | $\vec{\mathcal{R}}(\mathrm{a_1,b_1})\circ \vec{\mathcal{R}}(\mathrm{a_2,b_2})\Rightarrow \vec{\mathcal{R}}(\mathrm{a_1a_2,b_1b_2})$ |
| objects | $\mathrm{A}:\mathbb{A}, \mathrm{B}:\mathbb{B}$ | an equality | $\mathcal{R}(\mathrm{A,B})(-,-) = \vec{\mathcal{R}}(\mathrm{id.A, id.B})$ |
We give the proposition, and then expound in the visual language of span categories.
Proposition. Let $\mathbb{A,B}$ be categories, and let $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ be a span of categories. Inverse image along $\mathcal{R}\to \mathbb{A\times B}$ determines a displayed category
$$ ⁍. $$
For each pair of objects $\mathrm{A}:\mathbb{A}, \mathrm{B}:\mathbb{B}$ there is a category $\mathcal{R}(\mathrm{A,B})$ of objects $R:\mathcal{R}$ which map to $(\mathrm{A,B})$, also known as the fiber category “over” $(\mathrm{A,B})$; this may also be denoted $\mathcal{R}^\mathrm{A}_\mathrm{B}$. This is given by pullback in $\mathrm{Cat}$, of $\mathcal{R}$ along the functor which selects the pair $(\mathrm{A,B})$.
We introduce color syntax, a visual language that unifies string diagrams and syntax. The basic principle is substitution: by writing a pair of objects $\mathrm{A,B}$ in the color of each category $\mathbb{A,B}$, we determine the fiber category $\mathcal{R}(\mathrm{A,B})$. An entry is drawn on the right as a type in $\mathbb{C}\mathrm{at}$, which we color white as the “ambient” logic, outlined in blue and green to indicate that it is a diagram indexed by categories $\mathbb{A}$ and $\mathbb{B}$.
Now for the morphisms of a span category $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$, we consider the span of hom-profunctors $\vec{\mathbb{A}} \Leftarrow \vec{\mathcal{R}} \Rightarrow \vec{\mathbb{B}}$. Profunctors are drawn as strings pointing downward, and the hom of $\mathcal{R}$ is drawn as a bead from the $\mathcal{R}$ string to itself, along the homs of $\mathbb{A}$ and $\mathbb{B}$.
