The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

    Girard paradox was formulated within certain version of certain Per Martin-Löf axiomatic system.
    It is cited, but for me it is not trivial to judge whether I really reading the right version of that system. Not fine.

The relevant type system is "Type:Type". It is has two type formation rules:

Γ,A:Type ⊢ B:Type
—————————
Γ ⊢ Πx:A.B : Type


Γ ⊢ Type:Type

The original Girard's paradox was on an apparently weaker system called system U that had two different sorts.

The problem is similar to that in set theory: type which are too self-referential don't work well.

The essence of the problem is the liar paradox: we can't have an entity which can truthfully claim "I'm a liar" (the self reference is clear here). The Russell paradox quite literally constructs such a liar. The Burali-Forti paradox is a prior version which constructs a set of all the ordinals (which are equivalence classes of well-orderings and are, themselves, well-ordered). The set of the ordinals happens to be an ordinal, so it belongs to itself, but this isn't possible because it contradicts well-ordering.

Both paradox can be adapted in Type:Type but the Burali-Forti paradox is more direct (for the Russell Paradox see Alexandre Miquel's PhD thesis, he builds an encoding of a ZF-style type theory in which the Russel paradox can be written).

From this point of view, I almost got it, but not quite.
It is non-obvious why universes has to form total order.

They don't need to, actually. But if it helps, you can safely assume they do for the sake of the argument.

/Arnaud