Split off HoTTBookExercises.v from HoTTBook.v.

Since exercise formalizations tend to be a lot wordier than mere
backreferences to theorems in the library (as discussed in PR #302),
this patch splits HoTTBook.v into a separate exercises file, which
contains formalizations for the exercises in the HoTT book.  etc/Book.v
now takes a new flag, '--exercises', which instructs it to extract out
only exercises from the book; its default setting now no longer inserts
markers for exercises.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>