Example and Exercises added

Example 3.6.2 to HoTTBook.v
Exercises 3.2 and 3.3 to HoTTBookExercises.v
[`types.Sigma.trunc_sigma`](https://github.com/HoTT/HoTT/blob/master/theories/types/Sigma.v#L478) applied to `0`