Exercises 3.4 and 3.5

If there is a shorter solution to 3.4, then I'd like to know (and will add/substitute).
> There is some magic going on in that coq understands that IsHProp A implies IsHProp (A->A).

We have taught Coq that to prove `IsHProp (A -> B)`, it suffices to prove `IsHProp B`, if you have `Funext`.  This is the magic of typeclass resolution.