Connect the HoTT book to the Coq library

[andrejbauer]

Everything is in place for linking up the theorems in the book with the theorems in the Coq HoTT library, see the files etc/Book.py and contrib/HoTTBook.v in the HoTT library. They are amply documented.

I am not sure whtether this is an issue for HoTT/book or HoTT/HoTT.

[ezyang]

What would it mean to "link them up"? Is there even any toolchain support for this?

[andrejbauer]

There is a script which munches the book and creates a coq file into which we can then put definitions that show how to things from the book in coq using the HoTT library. So the idea is that you can look at this coq file to find places in the coq library that correspond to theorems in the book. But it takes manual work to actually link up a book theorem with the corresponding coq theorem.

[ezyang]

(For the record: this script lives in HoTT/HoTT, not the book repo!)

[JasonGross]

Also for the record, the linking is making progress, thanks to contributors such as @marcbezem and @ezyang. There are prettified versions at http://hott.github.io/HoTT/proviola-html/HoTTBook.html and http://hott.github.io/HoTT/proviola-html/HoTTBookExercises.html.

[mikeshulman]

Do we need to keep this issue open?

[andrejbauer]

Nope, the system is working, I think.