leanprover/lean — pull request #300 by javra (2014-11-06 18:18:46+00:00)
Title: feat(library/hott) add one new theorem, cleanup file

Equivalences.v from Coq-HoTT is completely ported now.