  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.
