<aside> 🛠 [Need to draw.]

</aside>

In giving the correspondence of span categories and displayed categories, we have essentially turned $\mathrm{Span\mathbb{C}at}$ “inside out”: given a span transformation

span categories become lax functors, and and span functors become transformations thereof; span profunctors become bimodules of lax functors, and span transformations become transformations thereof.

This fact is the realization of the collage completeness of $\mathbb{C}\mathrm{at}$ [GS13], by which $\mathbb{C}\mathrm{at}$ forms a classifying object for spans of categories.

Let $i:f\times g\to \mathrm{Prof}$ be a displayed profunctor. The collage $\mathsf{\Sigma}i$ is the set $\mathsf{\Sigma}\; \mathrm{f,g}.\; i(\mathrm{f,g})$ which is equipped with projections to $f$ and $g$.

The actions $\vec{\mathcal{Q}}(\mathrm{x,y})\circ i(\mathrm{f,g})\Rightarrow i(\mathrm{xf,yg})$ define an action $\vec{\mathcal{Q}}\circ \mathsf{\Sigma}i\Rightarrow \mathsf{\Sigma i}$; and similarly for $\mathcal{R}$. The associativity and unitality of the former give that of the latter.

This construction is functorial: given a displayed transformation $[\![i]\!]:i_0\Rightarrow i_1$, as above, the collage $\mathsf{\Sigma}[\![i]\!]: \mathsf{\Sigma}i_0\Rightarrow \mathsf{\Sigma} i_1$ is a span transformation.

This gives a bijection of squares between the double category $\mathrm{Span\mathbb{C}at}$ and $\mathrm{Dis\mathbb{C}at}$.

We now complete the equivalence of double categories $\mathrm{Span\mathbb{C}at}\simeq \mathrm{Dis\mathbb{C}at}$. It remains to define sequential composition of span profunctors and displayed profunctors, as this is the horizontal composition of each double category.

Let $m(f,k): \mathcal{R}(\mathbb{X,A})\,|\, \mathcal{S}(\mathbb{Y,B})$ and $n(g,\ell):\mathcal{S}(\mathbb{Y,B})\,|\, \mathcal{T}(\mathbb{Z,C})$ be a composable pair of span profunctors. The sequential composite $(m\circ n)(f\circ g,k\circ \ell): \mathcal{R}(\mathbb{X,A})\,|\, \mathcal{T}(\mathbb{Z,C})$ is the span of profunctor composites.

An element of $f\circ g$ is an indexed pair $\mathrm{Y.(f,g)}:f(\mathrm{X,Y})\times g(\mathrm{Y,Z})$, and of $k\circ \ell$ is $\mathrm{B.(k,l)}: k(\mathrm{A,B})\times \ell(\mathrm{B,C})$. Then an element of $m\circ n$ over $\mathrm{(Y.(f,g), B.(k,l))}$ is a pair $S.(m,n): m(R,S)\times n(S,T)$ quotiented by associativity: for any $s:\mathcal{S}(S_0,S_1)$ we have $S_0.(m,s\cdot n) = S_1.(m\cdot s, n)$.

The sequential composite of span transformations $[\![m]\!]:m_0\Rightarrow m_1$ and $[\![n]\!]:n_0\Rightarrow n_1$ is given by horizontal composition of transformations: $[\![m]\!]\circ [\![n]\!]: m_0\circ n_0\Rightarrow m_1\circ n_1$ maps $S_0.(m_0,n_0)$ to $[\![S_0]\!].([\![m_0]\!], [\![n_0]\!])$.

This defines horizontal composition of the double category of span categories.

Proposition Span categories and span functors, span profunctors and span transformations form a double category $\mathrm{Span\mathbb{C}at}$.

In the same way, displayed categories form a double category.

Proposition Displayed categories and displayed functors, displayed profunctors and displayed transformations form a double category $\mathrm{Dis\mathbb{C}at}$.

Proof Sequential composition of displayed profunctors is defined: given $m:f\times k\to \mathrm{Prof}$ and $n:g\times \ell\to \mathrm{Prof}$, the composite $(m\circ n):(f\circ g)\times (k\circ \ell)\to \mathrm{Prof}$ is $(m\circ n)(\mathrm{(f,g),(k,l))} = m(\mathrm{f,k})\times n(\mathrm{g,l)}$. This is functorial, defining parallel composition of the double category $\mathrm{Dis\mathbb{C}at}$.