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?
$\begingroup$
$\endgroup$
$\begingroup$
$\endgroup$
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
- You can carry out this reasoning in the above type theory
- 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.
