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.

翻译：本文提出一个用于幺半范畴的Rocq库，该库包含证明态射等价的判定过程，以及一套符号系统，使得在推理过程中能够将其视为严格范畴，并在后台自动推断MacLane同构。结合用于可视化和编辑弦图的外部工具，该系统支持以图形化方式执行幺半范畴中的重写步骤，并将其转化为简洁可读的文本形式化证明。