Univalent Mathematics

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

Installation

See INSTALL.md.

Contents

The UniMath subdirectory contains various packages of formalized mathematics. For more information, see the UniMath Table of Contents.

Some scientific articles describing the contents of the UniMath library are listed in the wiki.

Contributing to UniMath

To contribute to UniMath, submit a pull request. Your code will be subject to the copyright and license agreement in LICENSE.md.

For the style guide and other instructions, see UniMath/README.md.

Discussing UniMath & Getting Help

• Questions about the UniMath library, compilation, and installation of UniMath, etc., should be sent to the UniMath mailing list, which is archived in the 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.