[blueberry87]

What are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.

[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.

[lacker]

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.