Example and Exercises added

Example 3.6.2 to HoTTBook.v
Exercises 3.2 and 3.3 to HoTTBookExercises.v
I think we should probably call it `Book_3_1_easy` (that is, we should always start with `Book_...`, so that it's easy to, e.g., `grep` for theorems of the relevant name.)