A categorical diagram editor to help formalising commutation proofs

Abstract

I will present a categorical diagram editor (https://amblafont.github.io/graph-editor/index.html) implemented in Elm that generates Coq proof scripts (based on the UniMath library), letting the user prove manually commutation of each subdiagram. Conversely, the editor can parse a Coq goal stating equality between two composition of morphisms and generate a diagram out of it.