HoTT/HoTT — pull request #84 by mikeshulman (2013-02-20 04:52:37+00:00)
Title: Comparing notions of equivalence (with some other minor changes)

I've added a file `EquivalenceVarieties.v` (suggestions for better names are welcome) which proves that all notions of equivalence are equivalent -- and, along the way, that being a (half-adjoint) equivalence is an hprop. I think these proofs were in `FunextEquivalences` in the old library. Along the way, I had to add several additional lemmas, and I found myself wanting to change the implicitness status of some arguments on other lemmas, so this commit changes half a dozen other files as well.

I'm not completely satisfied with these proofs; I feel like I had to give more explicit arguments than ought to be necessary, making them look more imposing than they really are. Suggestions for improvements are welcome.