Metalogic

The co/descent calculus

We now define composition of matrix categories, and prove that $\mathbb{C}\mathrm{at} \leftarrow \mathbb{M}\mathrm{at}\mathbb{C}\mathrm{at} \to \mathbb{C}\mathrm{at}$ is a metalogic, i.e. a “bifibrant triple category without interchange".

Matrix categories compose in essentially the same way as profunctors; but rather than a coequalizer, the composite is formed by codescent, which adjoins to $\mathbb{A}\leftarrow \mathcal{R\ast S}\to \mathbb{C}$ a coherent associator of the inner actions of $\langle \mathbb{B}\rangle$.

Let $\mathcal{R}(\mathbb{A,B})$ and $\mathcal{S}(\mathbb{B,C})$ be matrix categories. The parallel composite matrix category

$$ (\mathcal{R}\otimes \mathcal{S}) (\mathbb{A,C}) $$

is constructed as follows. To the composite span category $\mathcal{R\ast S}$, an associator isomorphism is adjoined, by the following iso-coinserter.

image.png

This associator is natural by universality, so for every $w_\mathrm{B}:\langle \mathbb{B}\rangle$, $r: \vec{\mathcal{R}}$, $s:\vec{\mathcal{S}}$ the following commutes.

image.png

Then, two equations are imposed by coequifier, for reassociating a composite and a unit.

image.png

image.png

All together, the composite matrix category $(\mathcal{R\otimes S}) (\mathbb{A,C})$ is the following codescent object.

image.png

We denote the codescent object by the following “arrow sum" notation.

$$ (\mathcal{R\otimes S})(\mathrm{A,C}) \;\equiv\; \vec{\mathsf{\Sigma}}\, \mathrm{B}: \mathbb{B}.\; \mathcal{R}(\mathrm{A,B})\times \mathcal{S}(\mathrm{B,C}) $$