leanprover/lean — pull request #328 by javra (2014-11-19 22:20:31+00:00)
Title: 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.