HoTT/HoTT — pull request #408 by JasonGross (2014-07-16 00:10:12+00:00)
Title: Strip out uses of [Set]/[Type0]

In trunk, rigid polymorphic universes are not lowered to [Set], so
things work out better if we don't use [Set] anywhere. There's a bug in
HoTT/coq that forces us to manually choose the elimination schemes for
Unit and Empty, but it seems to be fixed in trunk.