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?
Example of a false proposition when assuming Type : Type
type theory
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 thanType : TypeBut 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 showsYou can carry out this reasoning in the above type theoryThere 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.