We have seen thus far that a span profunctor can be understood as a system of inference. Now, metalogic is the language of such systems of inference, and transformations thereof. Completing the logic of span categories, we define span transformations.

Let $\mathcal{Q_0}(\mathbb{X_0,Y_0}) , \mathcal{R_0}(\mathbb{A_0,B_0}),\mathcal{Q_1}(\mathbb{X_1,Y_1}), \mathcal{R_1}(\mathbb{A_1,B_1})$ be span categories.

Let $[\![\mathcal{Q}]\!]:\mathcal{Q_0\to Q_1}$ and $[\![\mathcal{R}]\!]:\mathcal{R_0\to R_1}$ be span functors over functors $[\![\mathbb{X}]\!],[\![\mathbb{Y}]\!]$ and $[\![\mathbb{A}]\!], [\![\mathbb{B}]\!]$.

Let $i_0:\mathcal{Q_0}(\mathbb{X_0,Y_0}) \,|\, \mathcal{R_0}(\mathbb{A_0,B_0})$ and $i_1:\mathcal{Q_1}(\mathbb{X_1,Y_1}) \,|\, \mathcal{R_1}(\mathbb{A_1,B_1})$ be span profunctors.

A span transformation $[\![i]\!]:i_0\Rightarrow i_1$ is a pair of transformations

$[\![f]\!]:f_0\Rightarrow f_1$ over $[\![\mathbb{X}]\!], [\![\mathbb{A}]\!]$ and $[\![g]\!]:g_0\Rightarrow g_1$ over $[\![\mathbb{Y}]\!], [\![\mathbb{B}]\!]$, and

a transformation $[\![i]\!]:i_0\Rightarrow i_1$ over $[\![\mathcal{Q}]\!], [\![\mathcal{R}]\!]$,

such that the two squares commute.

image.png

In two dimensions, this is “sliced” as follows.

image.png

Note this is equivalent to one commutative square of transformations.

image.png

Just as a span profunctor determines a matrix of profunctors, a span transformation determines a matrix of transformations.

Let $i_0: f_0\times g_0\to \mathrm{Prof}$ and $i_1: f_1\times g_1\to \mathrm{Prof}$ be displayed profunctors, and $[\![f]\!]:f_0\Rightarrow f_1$ and $[\![g]\!]: g_0\Rightarrow g_1$ be transformations.

A displayed transformation $[\![i]\!]: i_0\Rightarrow i_1$ is a map

https://q.uiver.app/#q=WzAsNCxbMCwwLCJmXzBcXHRpbWVzIGdfMCJdLFsyLDAsImZfMVxcdGltZXMgZ18xIl0sWzAsMiwiXFxtYXRocm17UHJvZn0iXSxbMiwyLCJcXG1hdGhybXtQcm9mfSJdLFsyLDMsIlxcbWF0aHJte1RyYW5zfSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFswLDEsIltcXCFbZl1cXCFdXFx0aW1lcyBbXFwhW2ddXFwhXSJdLFswLDIsImlfMCIsMV0sWzEsMywiaV8xIiwxXSxbNSw0LCJbXFwhW2ldXFwhXSIsMSx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH19XV0=&embed

which gives for each pair of

morphisms $\mathrm{f_0}:f_0(\mathrm{X_0,A_0}), \mathrm{g_0}:g_0(\mathrm{Y_0,B_0})$ a transformation $[\![i]\!]:i_0(\mathrm{f_0,g_0})\Rightarrow i_1([\![\mathrm{f_0}]\!], [\![\mathrm{g_0}]\!])$
composable pair $q:\vec{\mathcal{Q}_0}(\mathrm{x_0,y_0}), i:i_0(\mathrm{f_0,g_0})$ an equality $[\![q]\!]\cdot [\![i]\!] = [\![q\cdot i]\!]$
composable pair $i:i_0(\mathrm{f_0,g_0}), r:\vec{\mathcal{R}}_0(\mathrm{a_0,b_0})$ an equality $[\![i]\!]\cdot [\![r]\!] = [\![i\cdot r]\!]$

We now expound the idea, completing the visual language of $\mathrm{Span\mathbb{C}at}$.