Matrix categories and matrix functors, matrix profunctors and matrix transformations form $\mathbb{M}\mathrm{at}\mathbb{C}\mathrm{at}$, a bifibrant double category which is fibered over $\mathbb{C}\mathrm{at}\times\mathbb{C}\mathrm{at}$.

To complete the logic of matrix categories, we define its relation composition: sequential composition of matrix profunctors.

<aside> 🌱 All of this can be visualized — it just hasn’t been drawn yet!

</aside>

Substitution of relations

Sequential composition

Substitution of types and processes

$\mathbb{M}\mathrm{at}

\mathbb{C}\mathrm{at}$ over $\mathbb{C}\mathrm{at}\times \mathbb{C}\mathrm{at}$