Matrix categories and functors
Matrix profunctors and transformations
In Span categories we establish the basic data of a logic: a category of types and processes $\underline{\mathbb{A}}$, and a span category of relations and inferences $\mathbb{\underline{A}\leftarrow A\to \underline{A}}$.
Now, we add the basic structure: processes act on relations, i.e. morphisms of $\mathbb{\underline{A}}$ act on objects of $\mathbb{A}$.
We define matrix category, or two-sided bifibration: a span category $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ equipped with both “push and pull” actions by $\mathbb{A}$ and $\mathbb{B}$.
$\odot_\mathbb{A}: \langle \mathbb{A}\rangle \ast \mathcal{R}\to \mathcal{R}$
$\odot_\mathbb{B}:\mathcal{R}\ast \langle \mathbb{B}\rangle \to \mathcal{R}$
Matrix categories form a double category $\mathrm{Mat\mathbb{C}at}$, which is fibered over $\mathbb{C}\mathrm{at} \times \mathbb{C}\mathrm{at}$; then $\mathbb{C}\mathrm{at} \leftarrow \mathrm{Mat\mathbb{C}at}\to \mathbb{C}\mathrm{at}$ forms a three-dimensional structure which we call a metalogic.
Arrows and oparrows. To act on span categories, we first determine how a category $\mathbb{A}$ forms a logic $\mathbb{A\leftarrow \langle A\rangle \to A}$. Two-sided fibrations have been defined as bimodules of arrow double categories [Gle18]; yet these are not logics, because they lack conjoints. So, we define the logic of the weave double category to be the coproduct of the arrow double category with its opposite, $\mathbb{\langle A\rangle = \overrightarrow{A} + \overleftarrow{A}}$.
Matrix categories. We define a matrix category to be a bimodule of weave double categories. The “weave construction” extends to profunctors, giving the new concept of matrix profunctor. This is a relation of dependent categories; and to the author’s knowledge, such a notion has yet to be defined nor explored.
We show why bifibrations are necessary to define sequential composition. Matrix categories and matrix functors, matrix profunctors and matrix transformations form a double category $\mathrm{Mat\mathbb{C}at}$, which is fibered over $\mathbb{C}\mathrm{at} \times \mathbb{C}\mathrm{at}$, forming a fibered logic.
Parallel composition. Just as a profunctor consists of processes, a matrix category consists of relations, and hence forms a meta relation between logics (h-profunctor of bf.dbl.cats). So to conclude the chapter, we define composition of these relations.
While profunctors compose by forming a coequalizer for associativity, matrix categories compose by forming a codescent object, a weak colimit which adjoins a coherent associator isomorphism.
