Some claims quoted below need to be rectified, given that this is a public forum: On 29/07/15 06:54, Patrik Eklund wrote:
Yes, we cannot create the set of all sets, similarly as we shouldn't even try out creating the type of all types. Nevertheless, Martin-L??f took the liberty of doing that, and was opportunistic enough to publish it. Things went wrong but it was not called a paradox.
It is called Girard's Paradox, and the construction resembles Burali-Forti's Paradox, rather than Russell's paradox. The idea was to have a type U of all types, including U itself, written U:U. This may seem naive given Russell's Paradox was known. However, there is more to U:U than Russell's paradox, because "U:U" is not a proposition (it is a so-called judgment), and hence it cannot be true or false, or taken as a hypothesis in a mathematical statement. In particular, using U:U, you cannot form the type of all types that don't belong to themselves, because there is no "belong" relation in type theory, and for instance writing something such as "not(X:X)" is not even grammatically correct. To derive a contradiction using U:U (in a type theory extended with this judgement) is much harder than to derive a contradiction from the hypothetical existence of a set of all sets (in set theory).
Constructions were "improved" over decades, but the HoTT community still uses universality, so that paradox just appears as the emperors new clothes.
The improvement adopted both in MLTT in the 1980's, and in MLTT+HoTT axioms now, was already available, and is the same as the one Russell proposed a century ago to avoid his paradox, and adopted in Principia Mathematica, namely to instead have a hierarchical stratification U_0 : U_1 : U_2 : U_3 : ... by "size", where U_0 is the type of all small types, which lives in the type U_1 of large types, which lives in the type U_2 of even larger types, etc. The idea is at least 107 years old. M. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]