GirardParadoxGirard’s paradox [1] is a proof that type is not a type, an adaptation of set theory’s Burali-Forti paradox into type theory.
The proof works by observing that the collection of all well-founded posets looks like a poset itself, using strict embedding as the order. That poset of well-founded posets, let’s call it P, would need to reside one level higher in the universe hierarchy, but if the universe hierarchy is collapsed, P is a poset at the same level. Moreover, (if the universe hierarchy is collapsed) we can show that P is well-founded. However, P embeds into itself, which is a contradiction.
We express the proposition that type is a type in Istari by saying
that U (1 + i) <: U i, for some level i. From that it would
follow that U i : U i. However, unlike the direct statement, the
statement using subtyping is
negatable.
girard_paradox : forall (i : level) . not (U (1 + i) <: U i)
[1] Jean-Yves Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types, 1972.