Guillemet, Benoît

Machine-Checked Categorical Diagrammatic Reasoning

2024 · arXiv (Cornell University)

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 …