Matrix category

Matrix functor

We are now ready to define the structures which underlie a logic.

We simplify the presentation of structures and coherences in two ways.

• We denote a transformation by its components, e.g. the associator of a matrix category $\overline{\mathrm{a}}\odot (R\odot \overline{\mathrm{b}})\cong (\overline{\mathrm{a}}\odot R)\odot \overline{\mathrm{b}}$
• We use the symbol $x\rightrightarrows y$ to denote that the two transformations from $x$ to $y$, inferrable from context, are equal; e.g. the two ways to reassociate four elements are equal. $\mathrm{((\overline{a}_1\odot \overline{a}_2)\odot \overline{a}_3)} \odot R \rightrightarrows \mathrm{\overline{a}_1\odot (\overline{a}_2\odot (\overline{a}_3\odot } R))$

Additionally, we elide the associators and unitors of $\mathrm{Span\mathbb{C}at}$, as they can be inferred.