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.