Comment by JonChesterfield
2 years ago
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.
[1] https://en.wikipedia.org/wiki/System_U#Girard's_paradox
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.
They do not really require it but note my other answer in this subthread.