String Diagrams for Monoidal Categories, in Rocq
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918350823620608 |
|---|---|
| author | Pous, Damien |
| author_facet | Pous, Damien |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_19806 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | String Diagrams for Monoidal Categories, in Rocq Pous, Damien Logic in Computer Science 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. |
| title | String Diagrams for Monoidal Categories, in Rocq |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.19806 |