feat(library/hott) make paths universe polymorphic

complete the proof of funext_from_ua. Note that for proving funext at the moment one needs to have univalence in two consecutive universes, this should probably be changed somehow.