UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

View the Project on GitHub UniMath/UniMath

Univalent Mathematics Coq files

Each subdirectory of this directory consists of a separate package, with various authors, as recorded in the README (or README.md) file in it.

Contributing code to UniMath

Volunteers may look at unassigned issues at github and volunteer to be assigned one of them. New proposals and ideas may be submitted as issues at github for discussion and feedback.

Contributions are submitted in the form of pull requests at github and are subject to approval by the UniMath Development Team.

Changes to the package “Foundations” are normally not accepted, for we are trying to keep it in a state close to what Vladimir Voevodsky originally intended. A warning is issued if you run make or make all and have changed a file in the Foundations package.

Adding a file to a package

Each package contains a subdirectory called “.package”. The file “.packages/files” consists of a list of the paths to the *.v files of the package, in order, i.e., a file is listed after files it depends on. (That’s just so the TAGS file will be correctly sequenced.) To add a file to a package, add its path to that file.

Adding a new package

Create a subdirectory of this directory, populate it with your files, add a README (or README.md) file, and add a file .package/files, listing the *.v files of your package, as above. Then add the name of your package to the head of the list assigned to “PACKAGES” in the file “./Makefile”, or, alternatively, if you’d like to test your package without modifying “./Makefile”, which you might accidentally commit and push, add its name to the head of the list in “../build/Makefile-configuration”, which is created from “../build/Makefile-configuration-template”.

The UniMath formal language

The formal language used in the UniMath project is based on Martin-Löf type theory, as present in MLTT79 below. We are currently on version 2.

UniMath-1 is MLTT79 except:

UniMath-2 is UniMath-1 except:

The axioms accepted are: the univalence axiom, the law of excluded middle, the axiom of choice, and a few new variants of the axiom of choice, validated by the semantic model.

MLTT79 is this paper:

@incollection {MLTT79,
    AUTHOR = {Martin-L\"of, Per},
     TITLE = {Constructive mathematics and computer programming},
 BOOKTITLE = {Logic, methodology and philosophy of science, {VI} ({H}annover, 1979)},
    SERIES = {Stud. Logic Found. Math.},
    VOLUME = {104},
     PAGES = {153--175},
 PUBLISHER = {North-Holland, Amsterdam},
      YEAR = {1982},
   MRCLASS = {03F50 (03B70 03F55 68Q45)},
  MRNUMBER = {682410},
MRREVIEWER = {B. H. Mayoh},
       DOI = {10.1016/S0049-237X(09)70189-2},
       URL = {http://dx.doi.org/10.1016/S0049-237X(09)70189-2},
}

UniMath coding style

In the following rules, we purposely restrict our use of Coq to a subset whose semantics is more likely to be rigorously verifiable and portable to new proof checking systems, and we follow a style of coding designed to render proofs less fragile and to make the files have a more uniform and pleasing appearance.

Our files don’t adhere yet to all of these conventions, but it’s a goal we strive for.

Another advantage of coding in this style is that the proofs should be easier to transport to another proof assistant.