Univalent Mathematics
This Coq library aims to formalize a substantial body of mathematics using the
univalent point of view.
It is licensed for use under the terms in the file LICENSE.md
.
Contents
The "UniMath" subdirectory contains various packages of formalized mathematics. Please see the file README (or README.md) in each package for more information about its contents.
Some articles describing the contents of UniMath are listed in the wiki.
Installation
For installation instructions, please see the file INSTALL.md.
Contributing to UniMath
To contribute to UniMath, submit a pull request or contact us. Your code will
be subject to the copyright and license agreement in the file LICENSE.md
.
Discussing UniMath & Getting Help
For questions about the UniMath library, compilation and installation of UniMath etc you can send an email to the UniMath mailing list. Emails to the mailing list are archived in the corresponding Google Group. Bugs should be reported in our UniMath bug tracker on Github.
Citing UniMath
To cite UniMath in your article, you can use the following bibtex item:
@Misc{UniMath,
author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
title = {{\em UniMath}: {Univalent} {Mathematics}},
howpublished = {Available at \url{https://github.com/UniMath}}
}
Note that this requires \usepackage{url}
or \usepackage{hyperref}
.
The UniMath Development Team
The members of the UniMath Development Team are Vladimir Voevodsky, Benedikt Ahrens, and Daniel Grayson.