HoTT/HoTT — pull request #332 by JasonGross (2014-03-03 04:22:13+00:00)
Title: UA implies funext

This closes #46. Unfortunately, the typeclass glue won't work very well until
we migrate to the polyproj branch of HoTT/coq, because typeclass resolution
currently doesn't take into account universe inconsistencies, so we'd need to
explicitly provide two instances of univalence to this theorem in order to use
it.