Type universes

Stream: new members

[Kevin Lacker]

I have possibly a naive question about type universes. Why does there have to be an infinite hierarchy of universes of types? For example in Python the type of "type" is just "type".

>>> type(0)
<class 'int'>
>>> type(type(0))
<class 'type'>
>>> type(type(type(0)))
<class 'type'>

Does it lead to some sort of Russell's paradox problem if you let the type of "type" be "type" ?

[Kevin Buzzard]

Yes! You can prove false.

[Kevin Lacker]

I feel like it should be something like, it implies that you are allowed to define a function like def f(g): g(g) is false, but I don't see how that would be a result of letting the type of type be type

[Kevin Buzzard]

It's called Girard's Paradox. here is a proof in Lean.