Typeset NuPRL the same way as Coq and Agda.
Remove duplicate \indexsee{universal!quantifier}{quantifier, universal}.
Smaller font in index for US Trade, closing #252
Cleaned up bibliography
Remove stale remark, close #227
Ebook format, close #253
Indexed F words, #94
Fix #255
added some vspace above torus
Unconfuse backreferences from bibliography, #254
Merge branch 'master' of github.com:HoTT/book
wording/formatting in ch 6
detailed index "universal property"
wording/formatting in ch 7
two more
notation in 7.6.6 was a mes
Fix proofs of 7.6.5 and 7.6.6.

The proof of 7.6.5 implied that its second equality was definitional,
and that fact was used in the proof of 7.6.6.  However, I don't see
how to make the equality definitional.  Fortunately, the proof works
without it.