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?


1 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.

  • $\begingroup$ So do you think of French as a bug or a feature? $\endgroup$ Nov 27, 2021 at 9:15
  • 1
    $\begingroup$ @AndrejBauer it does seem to be a natural language for paradoxes :) $\endgroup$
    – cody
    Nov 28, 2021 at 17:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.