some more exercises on W-types
one more exercise
oops, fix some typos
yet one more exercise
exercises on plump ordinals
refer to Taylor's book, clarify injectivity of i_Ord
Update cleveref from 0.17.9 to 0.19

I'm trying to get the book to compile with htlatex so that we can have a
nice kindle-compatible epub, and it requires updating cleveref.
(Although I am a fan of MathML and the epubs for #287, e.g., of
@loopspace and @dvanduzer, Kindle doesn't currently support MathML at
all, and htlatex uses embedded images for the math.)
Merge pull request #652 from JasonGross/update-cleveref

Update cleveref from 0.17.9 to 0.19
Add labels to a number of ct theorems and defns

They were missing them, and I want them for HoTTBook.v in HoTT/HoTT.
Merge pull request #653 from JasonGross/label-ct

Add labels to a number of ct theorems and defns
fix a misprint
add an erratum for the previous correction
Merge pull request #654 from DanGrayson/pull-2

fix a misprint
Mark Errata (auto)
fix typos in 6.12.1, close #656
errata for d5b2a65
added exercise to chapter 3
added reference to old exercise in chapter 3
Minor tweaks to allow cleveref's poorman .sed files to work better

We'll still need to patch them to deal with autoref vs cref, but at
least we won't error or have missing braces.

The poorman option to cleveref was the only way I've found to get
htlatex to compile the book.
Tweaks to allow latex (and not only pdflatex) to compile the book

This is required for getting htlatex to work, for an eventual
html/non-MathML-epub target.  The main changes are:
(1) we use \DeclareGraphicsExtension and never pass .png explicitly
now
(2) we patch \includegraphics when not in pdf mode to read bounding
boxes using bmpsize-base, to silence "can't determine size" errors