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.