2005/06/23 by Carlos T. Simpson, Simpson, Carlos T.
Mathematics · #Category Theory (math.CT) #FOS: Mathematics #math.CT
paper · pdf · doi:10.48550/arxiv.math/0506470
arxiv created 2005/06/23 · arxiv updated 2009/12/01
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.