Spahn Ho TT-Coq - references (Rev #2)

References

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

• https://github.com/HoTT/HoTT/tree/master/Coq

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

• Ho TT-Coq code (HoTT-Coq-code.pdf) .

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

• Proviola/HoTT .

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:

• Andrej Bauer, (GitHub)

• Peter LeFanu Lumsdaine, (GitHub)

• Mike Shulman and others, Higher inductive types (GitHub)

• Mike Shulman, Reflective subcategories and cohesive toposes (GitHub)

• Vladimir Voevodsky, Foundations (GitHub)