The metalogic of matrix categories is higher-order: composition is dual to transformation, giving $\mathbb{M}\mathrm{at}\mathbb{C}\mathrm{at}$ closure.

In the same way that the set of transformations between profunctors forms an end, the category of matrix functors between matrix categories forms a descent object.

The set of transformations is an equalizer, for the equation of naturality. Yet a matrix functor is only “natural" up to isomorphism: the following iso-inserter forms the category of span functors equipped with a pair of joins $\odot_\mathbb{A}$ and $\odot_\mathbb{B}$. (We shorten $\mathrm{Span}\mathbb{C}\mathrm{at}$ to $\mathbb{S}$.)

image.png

Each coherence equation is then imposed by an \textit{equifier}. For joining composites:

image.png

and for joining units.

image.png

All together, this forms the descent object in $\mathbb{C}\mathrm{at}$ of the above functors and transformations.

image.png

We denote the descent object by an “arrow product” notation.

$$ \mathbb{M}\mathrm{at}\mathbb{C}\mathrm{at} [\mathcal{R_0\to R_1}] \;\equiv\; \vec{\mathsf{\Pi}} \, \mathrm{A,B}.\; \mathcal{R}_0(\mathrm{A,B})\to \mathcal{R}_1([\![\mathrm{A}]\!], [\![\mathrm{B}]\!]) $$

Based on the hom of matrix categories, we define the hom of matrix profunctors.

Let $i_0(f_0,g_0): \mathcal{Q_0}(\mathbb{X_0,Y_0})\,|\, \mathcal{R_0}(\mathbb{A_0,B_0})$ and $i_1(f_1,g_1): \mathcal{Q_1}(\mathbb{X_1,Y_1})\,|\, \mathcal{R_1}(\mathbb{A_1,B_1})$ be matrix profunctors. Matrix transformations $i_0\Rightarrow i_1$ form a profunctor from $\mathbb{M}[\mathcal{Q_0\to Q_1}]$ to $\mathbb{M}[\mathcal{R_0\to R_1}]$, which is constructed by the following equalizer.

image.png

We denote this equalizer as follows.

$$ \mathbb{M}[i_0\Rightarrow i_1] \;\equiv\; \vec{\mathsf{\Pi}} \, \mathrm{f,g}.\; i_0(\mathrm{f,g})\Rightarrow i_1([\![\mathrm{f}]\!], [\![\mathrm{g}]\!]) $$