  One very strong form of universe is obtained by adding the axiom \(U:U\). This was suggested by P. Martin-Löf in 1970. J.Y. Girard showed that the resulting type theory is inconsistent as a logical system (Girard 1972). Though it seems at first that one could directly reproduce Russell’s paradox using a set of all sets, such a direct paradox is actually not possible due to the difference between sets and types. Indeed the derivation of a contradiction in such a system is subtle and has been rather indirect (though, as noticed in Miquel 2001, it can now be reduced to Russell’s paradox by representing sets as pointed graphs). J.Y. Girard first obtained his paradox for a weaker system. This paradox was refined later (Coquand 1994 and Hurkens 1995). (The notion of pure type system, introduced in Barendregt 1992, is convenient for getting a sharp formulation of these paradoxes.) Instead of the axiom \(U:U\) one assumes only