4 ms·
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 espec
by JonChesterfield 3y 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.
- deltasepsilon 3y agoI 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 https://en.wikipedia.org/wiki/System_U#Girard's_paradox
- cjfd 3y agoThey do not really require it but note my other answer in this subthread.
- blueberry87 3y agoYou 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.