A development of homotopy-theoretic foundations of mathematics.
This is the repository for the Coq files of the Homotopy Type Theory project. You can fork this repository to your own and then be automatically kept up to date on new developments. You can also contribute back into it by sending a pull request.
You will need Coq version 8.3 to compile the files. They probably do not work with Coq 8.4 because of the introduction of the eta rule in Coq 8.4.