uniformize some implicit arguments

There is a collection of lemmas that assert that an object A has some property P because it is "equivalent" to an object B that has property P, like `trunc_equiv`, `contr_equiv`, `isequiv_homotopic`.  Using such a lemma involves specifying the object B and also the equivalence (`f`, say) from B to A, and of course Coq has no way to guess them, so there's not much point in making them all implicit.  It seems that sometimes we want to specify B and leave f as a new goal, whereas other times I want to specify f directly and have Coq deduce B.  So I propose that in all such lemmas we make `B` and `f` both explicit arguments and use `_` for one or the other where needed; this way we can avoid some `@` prefixes and it'll be easier to remember which arguments are explicit since it'll be consistent.