Skip to content

About-UniMath.md

Latest commit

 

History

History
66 lines (56 loc) · 3.89 KB

About-UniMath.md

File metadata and controls

66 lines (56 loc) · 3.89 KB

About UniMath

  • For articles that have accompanying proofs in UniMath or built upon UniMath, or articles that describe UniMath, see Articles with formalization.
  • For events about UniMath, see the Calendar.
  • For discussions of different aspects of formalization, see Discussions.
  • For the formal language used in the UniMath project, see Martin-Löf Type Theory.
  • For a summary of various attempts to introduce resizing rules, to get rid of -type-in-type, see Resizing Rules.
  • For an overview of the most important symbols used in UniMath, see Symbols List.

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{http://unimath.org}},
    doi          = {10.5281/zenodo.10849216},
    url          = {https://doi.org/10.5281/zenodo.10849216}
 }

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

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
  • Arnoud van der Leer
  • Michael Lindgren
  • Peter LeFanu Lumsdaine
  • Ralph Matthes
  • Niels van der Weide

Packages

The largest two packages in the repository are CategoryTheory and Bicategories. Most of the activity in UniMath is centered around these two.

Since a part of the Bicategories is quite heavy and takes a long time to compile, we generally avoid adding code in the rest of the library that depends on Bicategories.

The satellite repositories

The five satellites that fall within the continuous integration of this GitHub repository (SetHITs, GrpdHITs, TypeTheory, largecatmodules, Schools) are less integrated parts of UniMath, just like the "contributions" that Coq had a long time ago. Satellites do not need to conform to the coding style of UniMath as consistently as the UniMath library itself (HITs use more inductive types). They are maintained, even if this often only means propagating upstream changes.

To download and compile a satellite repository, for example SetHITs, go to the root directory of the UniMath repository (so you should see a UniMath directory as well as a README.md file) and run

git clone git@github.com:UniMath/SetHITs.git
dune build SetHITs

You can also compile all of UniMath together with the satellites, by cloning the 4 repositories and running the compilation command:

git clone git@github.com:UniMath/SetHITs.git
git clone git@github.com:UniMath/GrpdHITs.git
git clone git@github.com:UniMath/TypeTheory.git
git clone git@github.com:UniMath/largecatmodules.git
git clone git@github.com:UniMath/Schools.git
dune build

Note that changes to the satellites have to be filed to their respective repositories, so you should fork the satellite repository that you are working on, make sure that your local copy has its origin set to that fork, and push to that fork. When you are done, create a pull request to the satellite repository.