leanprover/lean — pull request #290 by javra (2014-11-04 05:12:24+00:00)
Title: feat(library/hott) extend equivalences.lean

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