Homotopy type theory
Clone or download
spitters Merge pull request #970 from SkySkimmer/autogen-skip-submodules
Add -skip-submodules option to autogen.sh
Latest commit 31c31c5 Nov 12, 2018
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
contrib Merge pull request #910 from siddharthist/not-brck-A-impl-A Jul 25, 2018
coq-HoTT @ 063abf1 Fix errors from numeral notation Sep 3, 2018
coq Fix errors from numeral notation Sep 3, 2018
etc [travis] Fail earlier on failure to build coq Oct 29, 2018
theories Adapt to local universes for opaque polymorphic definitions. Nov 5, 2018
.gitignore Use .v.d suffix for Coq dependency files. Jul 7, 2017
.gitmodules Drop support for Coq 8.8 in preparation for 8.9 Aug 28, 2018
.mailmap Update .mailmap Jul 13, 2016
.travis.yml Drop opam on travis Oct 29, 2018
CREDITS.txt Update CREDITS.txt Aug 26, 2013
INSTALL.md Drop support for Coq 8.8 in preparation for 8.9 Aug 28, 2018
LICENSE.txt Added legaleze Oct 3, 2012
Makefile.am Fix errors from numeral notation Sep 3, 2018
README.md mention hoqide in README Jun 8, 2018
STYLE.md consistent naming of non-dummy axioms Jun 20, 2017
UNICODE.txt Add unicode instructions Aug 26, 2014
_CoqProject Implement Escardo's bounded search Jul 23, 2018
autogen.sh Add -skip-submodules option to autogen.sh Nov 12, 2018
configure.ac Add hoqchk and a validate target Jun 1, 2017
hoq-config.in Add hoqchk and a validate target Jun 1, 2017
hoqc Strip -no-native-compiler Apr 19, 2016
hoqchk Add hoqchk and a validate target Jun 1, 2017
hoqdep Strip -no-native-compiler Apr 19, 2016
hoqide Strip -no-native-compiler Apr 19, 2016
hoqtop Strip -no-native-compiler Apr 19, 2016
hoqtop.byte Strip -no-native-compiler Apr 19, 2016

README.md

Build Status

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 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. Recently, there are also the Lean library and the cubical type checker.

More information about this libary 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

INSTALLATION

Installation details are explained in the file INSTALL.md.

USAGE

It is possible to use the HoTT library directly on the command line with the hoqtop script, but who does that?

It is probably better to use Proof General and Emacs. When Proof General asks you where to find the coqtop executable, just point it to the hoqtop script. If Emacs runs a coqtop without asking, you should probably customize set the variable proof-prog-name-ask to nil (in Emacs type C-h v proof-prog-name-ask RET to see what this is about).

There is also a script called hoqide that runs Coq's built-in GUI coqide with hoqtop as the underlying coqtop.

CONTRIBUTING

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

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.