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.

翻译：本文介绍了一个使用Coq证明助手开发的形式化证明库，旨在辅助用户编写关于1-范畴的正确图示证明。该库提出了一种深度嵌入的领域特定形式语言，其特色在于配备专用证明命令，可自动综合与验证文献中常被省略的技术性部分。