2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/75563This preprint contains the Coq proof files for Gabriel-Zisman localization, bundled with the source. The text of this preprint consists of the definitions and lemma statements of the main files, with proofs removed. See the other preprint ``Explaining GZ localization to the computer'' for explanation and discussion.Category Theorytext