A Diagram Editor to Mechanize Categorical Proofs

Explore a prototypical diagram editor designed to simplify the mechanization of categorical proofs in this 22-minute conference talk from CoqPL'24. Learn how this innovative tool, developed by Ambroise Lafont, addresses the challenges of translating diagrammatic proofs into text-based proof assistants like Coq. Discover the editor's integration with the coq-lsp VSCode extension and its web application counterpart. Understand its current focus on the UniMath mathematical library for Coq and its potential adaptability to other targets. Gain insights into how this editor aims to streamline the process of working with diagrammatic proofs, particularly in category theory, making mechanization more accessible and efficient for mathematicians and computer scientists.

[CoqPL'24] A diagram editor to mechanize categorical proofs