Spahn
Ho TT-Coq - references (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

category: references

References

The basic Coq-code libraries that set up identity types and the resulting homotopy type theory are at

Vladimir Voevodsky’ files:

  • HTML-version of the library, web

  • link to the source files, github

A slightly more human readable version is collected as a single pdf in

A collection of all this code equipped with html-functionality that does display also the proofs (which otherwise only display when the code is loaded into a Coq-system) is at

A further translation of these proofs into ordinary text is in

  • Carlo Angiuli, Univalence implies function extensionality (pdf)

More is in the repositories of various authors:

Revision on November 25, 2012 at 17:44:04 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.