String Diagrams for Monoidal Categories, in Rocq

TL;DR

This paper introduces a Rocq library for monoidal categories that facilitates graphical reasoning, automated equality proofs, and visual editing of string diagrams, enhancing formal proof clarity and usability.

Contribution

It provides a novel Rocq library with decision procedures and visualization tools for monoidal categories, enabling intuitive graphical reasoning and automated proof translation.

Findings

Automates equality proofs of morphisms in monoidal categories.

Allows graphical rewriting and editing of string diagrams.

Translates graphical proofs into concise textual formal proofs.

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.