feat(library/hott) add one new theorem, cleanup file

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