[JonChesterfield]

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.

[deltasepsilon]

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

[blueberry87]

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.

[cjfd]

They do not really require it but note my other answer in this subthread.