Dependent Types: Universes, or Types of Types

In set theory, a universal set has a proper subset of itself, which is a kind of paradox. If you seperat universal sets into those that have paradoxes and those that do not, then, You would assume that the universal Set without paradoxes is neither a proper subset of itself or that it is not universal, which is a paradox putting the universal set without paradoxes into the set of paradoxical universal sets. ( This is all just a small single line of prepositional calculus. )

Now I see that I assumed that you can cleave the universal set and wind up with a universal set which means it's a proper set of itself, but I am not sure You can cleave a non-paradoxal set from a universal set.