feat(library/hott) extend equivalences.lean

add precomposition lemma, use class inference (not entirely sure if this is really desirable in this case)