HoTT/HoTT — pull request #319 by JasonGross (2014-02-16 20:30:28+00:00)
Title: Do most of Exercise 4.5

I'm still not sure how to give a higher-level proof of `IsEquiv f -> IsEquiv (ap f)`. Suggestions/hints are welcome. Also, I'm not sure if the `Proof with try typeclasses eauto.` and `...` are appropriate for HoTTBookExercises.