Example of a false proposition when assuming Type : Type

Question

In Type Theory if one allows Type to be a member of itself, it makes the theory inconsistent. I understand it by analogy to Russel's paradox in Set Theory, but would prefer to see it done in Type Theory. Is there a short example of the equivalent in Type Theory?

Answer 1

The relevant literature is the following:

Thierry Coquand A new paradox in type theory (link). He describes his paradox in a system that is somewhat weaker than

Type : Type

But that can be easily transported to the above. The main idea is taking Reynolds proof that there are no models of system F in set theory. That proceeds by building an initial algebra of the form:

$$ A\simeq (A \rightarrow \mathrm{2}) \rightarrow \mathrm{2}$$

Where $\mathrm{2}$ is a set with 2 elements, and deriving a contradiction by a cardinality argument. Coquand shows

1. You can carry out this reasoning in the above type theory
2. There is a model of system F in that theory. This yields a contradiction.

The second article is from Antonius Hurkens, and is titled A simplification of Girard's paradox (link). The proof involves a construction of the "type of all well-founded types". I must admit that the general idea seems clear, but the details are quite devilish.

I'm afraid there is no simple, easy to understand contradiction in $\mathrm{Type} : \mathrm{Type}$. However the proof-terms obtained from the contradiction are relatively tractable: only a few lines are sufficient to define them.

Alexandre Miquel, in his thesis dissertation, showed that one could construct a model of naive set theory in these inconsistent type systems by using a pointed graph interpretation of sets. He can then simply apply Russel's paradox directly. Unfortunately the model construction takes a bit of work, and the dissertation is in French.