Port UnivalenceImpliesFunext

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.