向计算机解释Gabriel-Zisman本地化
Explaining Gabriel-Zisman localization to the computer
摘要：
这解释了计算机制定的加布里埃尔-齐斯曼本地化的类别在证明助理Coq。它既包括一般的本地化建设与GZ的引理1.2的证明，以及建设使用微积分的分数。校样文件与其他预印本“广州本地化文件”捆绑在一起同时发布。
英文摘要：
This explains a computer formulation of Gabriel-Zisman localization of categories in the proof assistant Coq. It includes both the general localization construction with the proof of GZ's Lemma 1.2, as well as the construction using calculus of fractions. The proof files are bundled with the other preprint "Files for GZ localization" posted simultaneously.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
