Skip to content

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

License

Notifications You must be signed in to change notification settings

patrick-nicodemus/UniMath

This branch is 2374 commits behind UniMath/UniMath:master.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

author
Patrick Nicodemus
Dec 5, 2021
f9cb115 · Dec 5, 2021
Jun 6, 2021
Dec 5, 2021
Aug 8, 2019
Aug 23, 2015
May 10, 2017
Dec 24, 2020
Jan 23, 2018
Apr 27, 2020
Feb 19, 2018
Oct 2, 2020
Jun 5, 2021
Jun 1, 2021
Feb 26, 2019
Mar 14, 2020
May 15, 2020
Jun 1, 2021
Jan 30, 2016
Nov 1, 2021
Aug 5, 2021
Mar 25, 2019
Aug 4, 2021

Repository files navigation

Univalent Mathematics

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

Installation

See INSTALL.md.

Usage

See USAGE.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

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 = {{UniMath --- a computer-checked library of univalent mathematics}},
    url = {https://github.com/UniMath/UniMath},
    howpublished = { {available at \url{https://unimath.org} }
 }

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

Acknowledgments

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.

About

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

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Coq 99.4%
  • Emacs Lisp 0.4%
  • Makefile 0.2%
  • Perl 0.0%
  • Shell 0.0%
  • JavaScript 0.0%