HoTT/HoTT — pull request #391 by JasonGross (2014-05-12 21:25:47+00:00)
Title: Use NaiveFunext for proving funext_downward_closed

The new version of @mattam82's universe polymorphism isn't as libral
with inductive universes. So we use NaiveFunext to allow a simpler
transformation of universes.