A Graphical Interface for Category Theory Proofs in Coq
Luc Chabassier
TL;DR
The paper addresses the difficulty of learning and proving category theory by introducing a Coq-integrated graphical interface that visualizes and advances proofs via diagrammatic reasoning. It presents a three-part workflow: automatic graph construction from a Coq goal, an interactive graphical interface with operations such as insertion, merging, decomposition, and lemma-based progress, and a replayable textual script capturing proof interactions. The main contributions include a robust set of graph-editing operations tailored to categorical proofs, a lemma-application framework using graph matching and pushouts, and a modular architecture that separates the Coq plugin from a Rust-based interface, with an optional web version. This work enables more intuitive teaching, exploration, and potential portability of diagrammatic proofs across proof assistants, potentially reducing cognitive load and increasing accessibility of category-theoretic reasoning.
Abstract
The importance of category theory in recent developments in both mathematics and in computer science cannot be overstated. However, its abstract nature makes it difficult to understand at first. Graphical languages have been developed to help manage this abstraction, but they have not been used in proof assistants, most of which are text-based. We believe that a graphical interface for categorical proofs integrated in a generic proof assistant would allow students to familiarize themselves with diagrammatic reasoning on concrete proofs that they are already familiar with. We present an implementation of a Coq plugin that enables both visualization and interactions with Coq proofs in a graphical manner.