HoTT/HoTT — pull request #339 by JasonGross (2014-03-12 03:21:13+00:00)
Title: Prove that Funext is downward closed.

To do this, add some simple definitions to types.UniverseLevel. I
figured I'd mimic Agda, though we probably don't need [lift] or [lower]
or [isequiv_lift] because we get cumulativity. The proof of functional
extensionality being downward closed with respect to universe levels is
also straightforward, due to cumulativity. As a demo, I've made the
lemmas in hit.iso take only one instance of Funext.

Hopefully, this will be the end of most of our woes with universe
inconsistencies and Funext.

As Univalence is not, in fact, downward closed, (see
https://groups.google.com/forum/#!topic/homotopytypetheory/3wp32xV7OX0),
this closes #334.

We should probably go through and remove all of our instances of double `Funext`s.