Added universe hierarchy to avoid paradoxes.

Now U is of type U1, which is of type U2 and so on.
Ui -> Uj is of type U(max(i,j)+1).