Files for Gabriel-Zisman localization
classification
🧮 math.CT
keywords
fileslocalizationpreprintgabriel-zismanbundledcomputerconsistscontains
read the original abstract
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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.