Why do dependent types require universe levels to be consistent? I mostly see that in the context of the type of all types and similar, which doesn't seem especially necessary to express. A variable that denotes a type could have type 'any' or 'unspecified', as opposed to a type T^1 or similar.
I believe the parent was referring to Girard's paradox [1], but it's been a while and I'm not a specialist in this area.
They do not really require it but note my other answer in this subthread.
You lose a very large amount of expressive power if you don't.
Any formalisation of the reals requires at least 3 levels, if I remember correctly.
You would have to not use a type-based proof system. I think those are not going to be the "as simple as possible" ones. Consider metamath for example.