The previous section gave the known equivalence between span categories $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ and displayed categories $\mathcal{R}: \mathbb{A\times B}\to \mathbb{C}\mathrm{at}$. We now extend this idea to spans of profunctors; surprisingly this has not been explored, and yet it works in the exact same way.

We introduce the concept of displayed profunctor, a bimodule of displayed categories, formed by inverse image along a transformation. These are the relations in the logic of displayed categories, which we prove equivalent to the logic of span categories.

Let $\mathbb{X}\leftarrow \mathcal{Q}\to \mathbb{Y}$ and $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ be span categories.

A span profunctor from $\mathcal{Q}$ to $\mathcal{R}$ is

a pair of profunctors $f:\mathbb{X}\,|\, \mathbb{A}$ and $g:\mathbb{Y}\,|\, \mathbb{B}$, and a profunctor $i:\mathcal{Q}\,|\, \mathcal{R}$

with transformations $\pi^f_i:i\Rightarrow f(\pi^\mathbb{X}\mathcal{Q}, \pi^\mathbb{A}\mathcal{R})$ and $\pi^g_i:i\Rightarrow g(\pi^\mathbb{Y}\mathcal{Q}, \pi^\mathbb{B}\mathcal{R})$,

denoted $i(f,g): \mathcal{Q}(\mathbb{X,Y})\,|\, \mathcal{R}(\mathbb{A,B})$.

Note this data is equivalent to a single transformation $i\Rightarrow f\times g$.

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

Let $\mathcal{Q}:\mathbb{X\times Y}\to \mathbb{C}\mathrm{at}$ and $\mathcal{R}:\mathbb{A\times B}\to \mathbb{C}\mathrm{at}$ be displayed categories.

A displayed profunctor $i:f\times g\to \mathrm{Prof}$ from $\mathcal{Q}$ to $\mathcal{R}$ is a map

which gives for each pair:

| morphisms | $\mathrm{f}:f(\mathrm{X,A}), \mathrm{g}:g(\mathrm{Y,B})$ | a profunctor | $i(\mathrm{f,g}): \mathcal{Q}(\mathrm{X,Y})\,|\, \mathcal{R}(\mathrm{A,B})$ | | --- | --- | --- | --- | | composable pairs | $(\mathrm{x,y}), (\mathrm{f,g})$ | a transformation | $q\cdot i:\vec{\mathcal{Q}}(\mathrm{x,y})\circ i(\mathrm{f,g})\Rightarrow i(\mathrm{xf,yg})$ | | composable pairs | $\mathrm{(f,g), (a,b)}$ | a transformation | $i\cdot r:i(\mathrm{f,g})\circ \vec{\mathcal{R}}(\mathrm{a,b})\Rightarrow i(\mathrm{fa,gb})$ | | composable triple | $\mathrm{(x,y),(f,g), (a,b)}$ | an equality | $q\cdot (i\cdot r) = (q\cdot i)\cdot r$ | | morphisms | $\mathrm{(f,g)}$ | equalities | $\mathrm{id}.Q \cdot i = i = i\cdot \mathrm{id}.R$ |

Proposition. Let $\mathcal{Q}(\mathrm{X,Y})$ and $\mathcal{R}(\mathrm{A,B})$ be span categories, and $i(\mathrm{f,g})$ a span profunctor. Inverse image along $i\Rightarrow f\times g$ determines a displayed profunctor $i:f\times g\to \mathrm{Prof}$.