String Diagrams for Monoidal Categories, in Rocq
Logic in Computer Science
2026-02-24 v1
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.
Keywords
Cite
@article{arxiv.2602.19806,
title = {String Diagrams for Monoidal Categories, in Rocq},
author = {Damien Pous},
journal= {arXiv preprint arXiv:2602.19806},
year = {2026}
}