by Damien Pous
This webpage allows you to perform graphical proofs about monoidal categories, and to export Rocq proof script out of them. It is described in this paper, in Proc. ITP 2026.
Enter your terms and equations. Below you get to see the corresponding diagrams. You may move elements using the mouse, rewrite by circling sub-diagrams and press '1', or zoom using control-scroll. Other commands are available, press 'h' for a list (make sure you are not in the text area to enter such commands).
You may validate your rewriting steps in Rocq using the associated library about (monoidal) category theories.
Depending on your browser, there might be a bug in capturing the pointer position. In that case, please try another browser or use the GTK version of the program available below.
Click on the examples below to load them above.
The source code for this applet (as well as the standalone GTK program) is available on Github.
Klaus Kraßnitzer has forked the project to turn it into a small game usable on tablets; do not miss his demo!