HoTT/HoTT — pull request #399 by JasonGross (2014-05-29 18:27:09+00:00)
Title: Less restrictive Funext_downward_closed

Funext has three universes, and we want them all to be independent; this
seems to be necessary to eliminate universe inconsistencies in the
latest version of trunk.