<aside> 🛠 [Need to draw.]

</aside>

As explored in this section, we can understand span categories to consist of relations, and span profunctors to consist of inferences. Composition thus far has only been sequential composition of inference.

To complete the underlying structure of metalogic, we define parallel composition of these “meta”relations and “meta”inferences.

Let $\mathcal{R}(\mathbb{A,B})$ and $\mathcal{S}(\mathbb{B,C})$ be span categories. The parallel composite $(\mathcal{R\ast S})(\mathbb{A},\mathbb{C})$ is a span category defined by composition of spans in $\mathbb{C}\mathrm{at}$.

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

This means that an object of $\mathcal{R\ast S}$ over $\mathrm{A}: \mathbb{A}, \mathrm{C}:\mathbb{C}$ is a pair $R:\mathcal{R}(\mathrm{A,B}), S:\mathcal{S}(\mathrm{B,C})$ for some $\mathrm{B}:\mathbb{B}$. Hence the composite is equivalent to the matrix of categories

$$ ⁍ $$

and similarly for morphisms.

$$ (\mathcal{\vec{R}\ast \vec{S}})(\mathrm{a,c}) = \mathsf{\Sigma} \mathrm{b}:\mathbb{\vec{B}}.\; \mathcal{\vec{R}}(\mathrm{a,b})\times \mathcal{\vec{S}}(\mathrm{b,c}) $$

Composition and unit of $\mathcal{R\ast S}$ are given by that of $\mathcal{R}$ and $\mathcal{S}$; this is associative and unital.

Just as a span category can be drawn as a string, composition of span categories can be drawn as juxtaposition of strings.

In color syntax, we interpret the juxtaposition as the above matrix of categories and profunctors; i.e. the sum is “built in".

Then to determine a specific object of the composite, substitute a mediating object $\mathrm{B}$, and a pair of objects $R:\mathcal{R}(\mathrm{A,B})$ and $S:\mathcal{S}(\mathrm{B,C})$.

In the same way, we define parallel composition of span profunctors.