Can you have a type theory where there is type of all types? 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).
 A: 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}$.
A: The argument for accepting $\mathsf{Type} : \mathsf{Type}$ while enduring the Girard's paradox would be essentially no different from accepting "Axiom 0=1". It is just an funny and meaningless argument in pure mathematics, And a small offense to the Platonism of Type Theory. lol.
The larger question is whether $\mathsf{Type} : \mathsf{Type}$ has violated certain constraints (of the philosophy) of type theory.
Only the Predicative Universe needs Universe Polymorphism, and $\mathsf{Type} : \mathsf{Type}$ seems to be impredicative.
We do not need the full set theory, but only the ordinal number theory is sufficient to realize the Universe Polymorphism and Size Types. This is a great benefit for those who do not trust alternative set theory, because the constructive ordinal system of alternative set theory is much easier to verify consistency than alternative set theory itself. But once again, $\mathsf{Ord} \in \mathsf{Ord}$, means "the order type of all the ordinals is a ordinal", seems to be impredicative.
Further, it is unreasonable to think that the Universe Level can be extended indefinitely. From a low criterion, we only need $Type[\![<\Gamma_0]\!]$, and by the principle of ordinal notation, this might even be better set to $Type[\![<\omega]\!]$ as in Coq. From a high criterion, we can expect the existence of an ordinal $\alpha$ such that $Type[\![\alpha]\!]$ is closed for Computable
infinitary predicative formulas (even though we do not have a definition of it).

By the way, the best candidates is the constructive ordinal system of Double extension set theory (Although no one has conducted a study like "Leveloid" to explore what is meant by the double extension of constructivism).
The class WF of all the well-founded relation isn't a NF(U)'s set, this is a disadvantage for Universe Level.
