A logic, or bifibrant double category, is a pseudomonad in $\mathbb{M}\mathrm{at}\mathbb{C}\mathrm{at}$.

Hence a logic is a category $\underline{\mathbb{A}}$ of types and processes

with a matrix category $\mathbb{A}(\underline{\mathbb{A}}, \underline{\mathbb{A}})$ of relations and inferences

1.png

$\mathbb{A}(\underline{\mathbb{A}}, \underline{\mathbb{A}}):\mathbb{M}\mathrm{at}\mathbb{C}\mathrm{at}$

with matrix functors, parallel composition and identity

2-comp.png

$\circ: \mathbb{A}\otimes \mathbb{A}\to \mathbb{A}$

2-unit.png

$\mathrm{id}:\underline{\mathbb{A}}\to \mathbb{A}$

and invertible matrix transformations, the associator

3-assoc.png

$\alpha: (\mathbb{A}\circ \mathbb{A}) \circ \mathbb{A}\cong \mathbb{A}\circ (\mathbb{A}\circ \mathbb{A})$

and the left unitor, and right unitor

3-lunit.png

$\upsilon_\ell: \mathbb{A}\cong \mathrm{id}.\underline{\mathbb{A}}\circ \mathbb{A}$

3-runit.png

$\upsilon_r: \mathbb{A}\cong \mathbb{A} \circ \mathrm{id}.\underline{\mathbb{A}}$

so that reassociating a composite is well-defined,

and reassociating an identity is well-defined.

4-comp.png

$(\mathbb{A}\circ(\mathbb{A}\circ \mathbb{A}))\circ \mathbb{A} \rightrightarrows \mathbb{A}\circ ((\mathbb{A}\circ \mathbb{A})\circ \mathbb{A})$

4-unit.png

$(\mathbb{A}\circ \mathrm{id}.\underline{\mathbb{A}})\circ \mathbb{A} \rightrightarrows \mathbb{A}\circ (\mathrm{id}.\underline{\mathbb{A}}\circ \mathbb{A})$