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/theories 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
More is in the repositories of various authors:
Mike Shulman and others, higher inductive types (GitHub)
Mike Shulman, Reflective subcategories and cohesive toposes (GitHub)
Vladimir Voevodsky, Foundations (GitHub)