Simplify types/UniverseLevel.v

We don't actually need the fancy equality type, nor the paths.
Strictly speaking, we don't need [lift] or [lower] or the equivalence,
either.