A diagram editor to mechanise categorical proofs
Speaker:
Ambroise Lafont
Location:
Amphi Gilles Kahn + webex
Date:
Diagrammatic proofs are ubiquitous in certain areas of mathematics, especially in category theory. Mechanising such proofs is a tedious task because proof assistants (such as Coq) are text based. We present a prototypical diagram editor to make this process easier, building upon the vscode extension coq-lsp for the Coq proof assistant and a web application (you can try it on my personal website).