String Diagrams for Monoidal Categories, in Rocq

Abstract

We present a Rocq library for monoidal categories, which includes a decision procedure for proving equality of morphisms as well as notations that make it possible to reason as if they were strict, inferring MacLane isomorphims automatically in the background. Together with an external tool for visualising and editing string diagrams, this make it possible to perform rewriting steps in monoidal categories graphically, and to translate them into textual formal proofs which are concise and readable.

Figures (13)

• Figure 1: String diagrams corresponding to the identity on $A$ and to the expression $(f~{;}~ g)\cdot h$ with $f\colon A\otimes A\rightsquigarrow B$, $g\colon B\rightsquigarrow C$ and $h\colon B\rightsquigarrow C\otimes C$.
• Figure 2: Running example: composing the multiplications of two monoids $m$ and $n$, via a distributive law $x$. The goal on the right will be discussed only in Section \ref{['ssec:findmcl']}.
• Figure 3: Rendering of the goal from Figure \ref{['fig:rocqgoal']}.
• Figure 4: Performing a rewriting step graphically, by surrounding a matching subdiagram.
• Figure 5: Standard MacLane's coherence theorem.