feat(library/hott) funext_from_ua.lean almost done

What's missing is to fix the universes, but I guess we have to start fixing path.lean and trunc.lean