category: references ## References The basic [[nLab:Coq]]-code libraries that set up [[nLab:identity types]] and the resulting homotopy type theory are at * [https://github.com/HoTT/HoTT/tree/master/Coq](https://github.com/HoTT/HoTT/tree/master/Coq) Vladimir Voevodsky' files: * HTML-version of the library, [web](http://www.math.ias.edu/~vladimir/Foundations_library/toc.html) * link to the source files, [github](https://github.com/vladimirias/Foundations/) A slightly more human readable version is collected as a single pdf in * _Ho TT-Coq code_ ([[nLab:HoTT-Coq-code.pdf:file]]) . 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](http://mws.cs.ru.nl/proviola/HoTT/)_ . A further translation of these proofs into ordinary text is in * Carlo Angiuli, _Univalence implies function extensionality_ ([pdf](http://hottheory.files.wordpress.com/2011/12/hott.pdf)) More is in the repositories of various authors: * [[nLab:Andrej Bauer]], ([GitHub](https://github.com/andrejbauer/Homotopy)) * [[nLab:Peter LeFanu Lumsdaine]], ([GitHub](https://github.com/peterlefanulumsdaine/Oberwolfach-explorations)) * [[nLab:Mike Shulman]] and others, _Higher inductive types_ ([GitHub](https://github.com/HoTT/HoTT/tree/master/Coq/HIT)) * [[nLab:Mike Shulman]], _Reflective subcategories and cohesive toposes_ ([GitHub](https://github.com/mikeshulman/HoTT/tree/master/Coq/Subcategories)) * [[nLab:Vladimir Voevodsky]], _Foundations_ ([GitHub](https://github.com/vladimirias/Foundations/))