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.