Example and Exercises added

Example 3.6.2 to HoTTBook.v
Exercises 3.2 and 3.3 to HoTTBookExercises.v
This should already be in `types/Forall` or `HProp` or `Truncations`, right?