Machine-Checked Categorical Diagrammatic Reasoning

Stream: homology

[Antoine Chambert-Loir]

Machine-Checked Categorical Diagrammatic Reasoning, by Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez

This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature.

https://arxiv.org/abs/2402.14485v1