Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time
August 23, 2015 15:55
May 10, 2017 16:31
March 15, 2023 13:22
November 3, 2022 14:26
November 3, 2022 11:18
December 8, 2022 13:39

Univalent Mathematics

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






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 or work using it 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

For the style guide and other instructions, see UniMath/

Discussing UniMath & Getting Help

Citing UniMath

To cite UniMath in your article, you can use the following bibtex item:

    author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
    title = {{UniMath --- a computer-checked library of univalent mathematics}},
    url = {},
    howpublished = {available at \url{}}

Note that this requires \usepackage{url} or \usepackage{hyperref}.

The UniMath Coordinating Committee

The UniMath project was started in 2014 by merging the repository Foundations, by Vladimir Voevodsky (written in 2010), with two repositories based on it: rezk_completion, by Benedikt Ahrens, and Ktheory, by Daniel Grayson. Vladimir Voevodsky was a member of the team until his death in September, 2017.

The current members of the UniMath Coordinating Committee are:

  • Benedikt Ahrens
  • Daniel Grayson
  • Michael Lindgren
  • Peter LeFanu Lumsdaine
  • Ralph Matthes
  • Niels van der Weide


The UniMath development team gratefully acknowledges the great work by the Coq development team in providing the Coq proof assistant, as well as their support in keeping UniMath compatible with Coq.