Refer to the old version of this page for historical versions.
The latest version of everything,
ported to Coq 8.1, in
a small number of files. Each file is fairly big but organized into
modules:
set.v,
func.v,
ord.v,
comb.v,
cat.v,
gz.v.
Here is everything in a single tar
archive.
The project involves several
steps:
(1)---Construction of the free category on a graph and study of
functors and natural transformations from there;
(2)---Construction of the quotient category by a relation, and again
functors and natural transformation from there;
(3)---Defining the localization by the formula given in Gabriel-Zisman,
as a quotient of a free category; and
(4)---Proving the universal property as stated in their Theorem 1.2.
For the first step, we define the free category making free use of the Omega tactic to deal with arithmetic of indices in uples of arrows.
For the second step, we construct the quotient category by a relation (assuming the relation is trivial on objects). We also give a criterion for full faithfulness of the pullback or composition functor with a functor, with a view towards applying this to get GZ's Theorem 1.2 in step (4).
For the third and fourth steps, we define the Gabriel-Zisman graph and their relation on the associated free category; the localization is constructed as the quotient of the free category by this relation. The main step is to construct the dotted arrow completing the commutative diagram whenever we have a functor which sends elements of the multiplicative system to invertible morphisms.
Continuing on the same subject, we can treat the calculus of fractions. We give a construction of the localization by left fractions under the assumption that the multiplicative system has a calculus of left fractions; together with a proof of the easiest version of the universal property: just enough to be able to get it isomorphic to the localization constructed above.
At the end of the first version (January 2005) we complete the above by discussing the general definition of localization by universal property and show that our constructions satisfy this definition. This gives unicity up to a functorial isomorphism. We treat right fractions by equivalence with left fractions in the opposite category, and for both left and right fractions we draw the main conclusion which is that if the localizing system has a calculus of fractions then there is a simple description of the morphisms of the localized category (for example the general one defined in gzdef1.v). This description is not easy to find directly from the fraction condition and the general construction, rather its proof passes through the other specific construction in gzfractions1.v plus the unicity isomorphism of gzloc1.v.
In an update of March 2005, the first file is a collection of various results which logically should go back into previous places within the category theory development (recall that the above files are to be compiled within the category-theory environment available above). The next files are as above (with "gzfractions" renamed to "left_fractions"). The file "infinite.v" is a digression to prove some basic results about infinite cardinals, namely that the product and union operations preserve cardinality of infinite cardinals. The last file "lfcx.v" contains a construction of a little counterexample showing that there can be localizing systems which satisfy left fractions but in which the equivalence relation needs to be defined using intermediate arrows not in the localizing system, because we don't assume the "3 for 2" condition. The original files refered to above can be found on the old version of this page. In the latest version things have been reorganized into a small number of bigger files.
Here are the CCSD and ArXiV versions of the preprint Files for Gabriel-Zisman localization ps, pdf, gzfiles.tar.gz containing the files for this work. This preprint goes with the paper referred to above.
Here is a file containing a definition of first cohomology plus a proof of the first part of the long exact sequence, showing that the first cohomology is in a certain sense the obstruction to lifting sections of a surjection. The latest version is h1V8.v in Coq v8.0beta, January 2004
Functions in classical Zermelo-Fraenkel (with choice)
An experiment in writing formal
mathematics in Coq:
version 1: Friday, April 13th 2001;
(ps
file for version 1)---note however that there is extra source
materiel contained in the tex file.
widget5---a version of Friday, June 8th 2001.
Here is a rewriting of the start of the experimental ZFC file above, adapted for use with widget5: startA.v---a version of Monday, June 11th 2001.
For the faint of heart, here is a much smaller example showing how widget5 can do rewriting. Run widget5 specifying the following file; erase the Remarks in the section at the end, and run the command r (then recopy the resulting output from the OUT.html file back into the .v file): assoc1.v---then try to continue in the same way!
A weak version of the axiom of choiceWe develop some basic set theory within Coq, using a weak version of the axiom of choice (this version might be compatible with impredicativity of the sort Set but of course it doesnt allow creation of choice functions towards types of sort Set): Choice.v---a version of Monday, June 24th 2002.
Version of Tuesday, October 22nd 2002.
Version of Thursday, April 17th 2003.
Very preliminary version of Friday, May 16th 2003.