Can you have a type theory where there is type of all types?

Question

Normally in a type theory, you can not have a type of all types, due to Girard's paradox. This is somewhat similar to how in set theory, you cannot have a set of all sets.

Therefore, usually you just have a type of types that have types, which itself has no type (Calculus of Construction as defined here), or you just define an infinite tower of types, such that every type is of the type of something in that tower (a.k.a. a tower of universes).

These two solutions are analogous to the set-theoretic notions of a class of all sets and the Von Neumann hierarchy.

In set theory, there is actually a third solution: the New Foundations (and its relatives). In it, there is in fact a set of all sets.

My question is, can you similarly have a type theory in which there is a type of all types, possibly using similar techniques as those of New Foundations. You obviously can not just "transfer over" the axioms of New Foundations, since set theory and type theory are quite different, but maybe you can use similar axioms.

One direction I was thinking about it somehow extending universe polymorphism. For example, in Coq "Type : Type" is valid. But that doesn't mean Type is of type Type. Rather, there is actually a type Type$_n$ for each $n$, and Coq automatically tries to assign a $n$ to each occurrence of "Type" in the code. If you tried to formalize Girard's paradox in Coq, this assignment would fail. This is rather similar to the idea of stratified formulas in NF. Perhaps we could say that Type is a member of Type, but in any formula involving Type, there must be a way to "stratify" the formula, or something like that.

Another possibility would be to establish to have a hierarchy of universes, but declare them all to be isomorphic (although this would make the theory incompatible with the univalence axiom).

Answer 1

Of course you can have $\mathsf{Type} : \mathsf{Type}$, the consequence of that is that all types are inhabited (by Girard's paradox). Some people call this an inconsistency, but that only makes sense if you view terms as proofs and types as logical statements.

In other contexts, for instance when we think of terms as programs, there is nothing wrong with all types being inhabited. After all, in a general-purpose programming language all types are inhabited, thanks to recursion. In fact, if we lean towards programming, $\mathsf{Type} : \mathsf{Type}$ will be desirable because it will say that there is a datatype of all datatypes. There will be no end to Haskell-style hackage after that.

There are very nice domain-theoretic models of $\mathsf{Type} : \mathsf{Type}$. For example, we can take countably-based algebraic lattices and continuous maps. Then every such lattice embeds as a retract into $\mathcal{P}(\omega)$, which means that $\mathcal{P}(\omega)$ is a universal lattice. It plays the role of $\mathsf{Type}$. But what is even cooler is that the (algebraic) retracts of $\mathcal{P}(\omega)$ themselves form a countably based algebraic lattice, and this gives us $\mathsf{Type} : \mathsf{Type}$.