Homotopy Type Theory is an interpretation of Martin-Löf’s intensional type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos.

The HoTT library is a development of homotopy-theoretic ideas in the Rocq (formerly Coq) proof assistant. It draws many ideas from Vladimir Voevodsky's Foundations library (which has since been incorporated into the UniMath library) and also cross-pollinates with the HoTT-Agda library. See also: HoTT in Lean2, Spectral Sequences in Lean2, and Cubical Agda.

More information about this library can be found in:

• The HoTT Library: A formalization of homotopy type theory in Coq, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016 arXiv CPP17

Other publications related to the library can be found here.

Installation

The HoTT library can be installed using opam. Detailed installation instructions are provided in doc/INSTALL.md.

Usage

The HoTT library can be used like any other Rocq library. If you wish to use the HoTT library in your own project, make sure to put the following arguments in your _CoqProject file:

-arg -noinit
-arg -indices-matter

For more advanced use such as contribution see doc/INSTALL.md.

For recommended text editors see our recommended editors list. Other methods of developing in Rocq will work as long as the correct arguments are passed.

Documentation

The library can be browsed on the web using the documentation generated by rocq doc and Alectryon, which is linked to from the wiki.

Contributing

Contributions to the HoTT library are very welcome! For style guidelines and further information, see the file doc/STYLE.md.

Timing

See doc/TIMING.md for tips about timing builds in various ways.

Licensing

The library is released under the permissive BSD 2-clause license, see the file LICENSE.txt for further information. In brief, this means you can do whatever you like with it, as long as you preserve the Copyright messages. And of course, no warranty!

Wiki

More information can be found in the Wiki.