Let $\mathbb{A}$ and $\mathbb{B}$ be categories, with weave double categories $\langle\mathbb{A}\rangle$ and $\langle \mathbb{B}\rangle$.

A matrix category or two-sided bifibration $\mathcal{R}(\mathbb{A},\mathbb{B})$ is a span category $\mathbb{A} \leftarrow \mathcal{R}\to \mathbb{B}$ which forms a bimodule from $\langle\mathbb{A}\rangle$ to $\langle\mathbb{B}\rangle$.

The actions are span functors

and three invertible span transformations for associativity

and two invertible span transformations for unitality

so that the following transformations are well-defined, for associativity

and for unitality.

Now, the main idea.

<aside> 💗 A matrix category forms the relations and inferences of a logic, i.e. the loose morphisms and squares of a bifibrant double category.

</aside>

The actions by $\langle\mathbb{A}\rangle$ and $\langle \mathbb{B}\rangle$ define parallel composition of this double category.

Because a weave double category is a coproduct, an action by $\langle \mathbb{A}\rangle$,$\langle\mathbb{B}\rangle$ defines compositions by

$$ \overrightarrow{\mathbb{A}} \text{ and } \overleftarrow{\mathbb{A}}\;,\;\overrightarrow{\mathbb{B}} \text{ and } \overleftarrow{\mathbb{B}}. $$