HoTT/HoTT — pull request #584 by mikeshulman (2014-10-21 05:53:16+00:00)
Title: 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.