Add hott book target

Add a target for `contrib/HoTTBook.v`.  Also fix some typos, and add a .dir-locals.el to contrib.

We may eventually want to make contrib/HoTTBook.v friendlier to coqdoc, i.e., make the python file make comments that show up in the html page, and maybe even link to an online pdf or html file of the book.  (Perhaps set up travis to auto-compile the book and link to that, or something.)