Gabriel-Zisman本地化文件
Files for Gabriel-Zisman localization
摘要：
此预印本包含Gabriel-Zisman本地化的Coq证明文件，与源代码捆绑在一起。这个预印本的文本由主文件的定义和引理陈述组成，并删除了证明。请参阅其他预印本“向计算机解释GZ本地化”以获得解释和讨论。
英文摘要：
This 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
