Lemmas 3.3.2 and 3.3.3 and Exc. 3.9

Lemmas 3.3.2 and 3.3.3 added to HProp
Backrefs added to HoTTBook
Solution to Exc.3.9 added to HoTTBookExercises


We can prove something more general, right?  We can prove `forall T (f : T -> Empty), IsEquiv f`, and, since `~hprop` is just `hprop -> Empty`, we get this as a trivial corollary (and without the requirement that it be an hprop).