This is the main trunk for the Homotopy Type Theory project, see

  https://homotopytypetheory.org/

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.

The Coq files contain fancy UTF-8 characters. To input these you have
to set up an appropriate input method, see

  https://coq.inria.fr/cocorico/TeXInputMethodForUnicodeNotations

for help on doing so with Emacs and CoqIDE.