In homotopy type theory, or dependent type theories more generally, there is a "top-level" type called the universe, generally denoted $\newcommand{\type}{\mathtt{Type}}\type$. So for a concrete example, I could describe having 3 types: $\mathtt{Nat}$, $\mathtt{Real}$, $\mathtt{Complex}$ and the type of those types would be $\type$, hence my universe contains 3 types. Now in order to avoid Russel-like paradoxes, there is a need for a hierarchy of 'universe types' such that my universe should be called $\type\_k$ ('Type at level $k$') and then the type of that type would be $\type\_{k+1}$, and so on and so on. But types $\type\_{k+1}$, $\type\_{k+2}$, and so forth all only "contain" a single term $\type\_k : \type\_{k+1}$, namely the type from the 'previous level,' so aren't they all isomorphic types, and by the univalence axiom in HoTT, equivalent, and thus 'collapsable' back down to just to the single universe type $\type$ ('level 1')?



Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?
This question is about type theory in general and is not specific to homotopy type theory. $\newcommand{\Type}{\mathtt{Type}}$


The thing you are missing is that **a universe $\Type\_k$ contains very many types**, not just one as you claim. Each $\mathtt{Type}\_k$ is closed under type forming operations $\times$, $+$, $\Sigma$, $\Pi$, etc. For example, $\Type\_3$ contains $\Type\_2 \times \Type\_2$ and $\Type\_2 \to \Type\_2$, and if $A : \Type\_3$ and $B : A \to \Type\_3$ then $\prod\_{x : A} B(x) : \Type\_3$, and so on.


In case that the type universes are **cummulative** (so that if $A : \Type\_k$ then $A : \Type\_{k+1}$) we also get types like $\mathtt{Bool}$ and $\mathtt{Nat}$ in every type universe.


This still leaves open the question as to whether $\mathtt{Type}\_k$ could be isomorphic to $\mathtt{Type}\_{k+1}$. The answer is *no*, they are not isomorphic. If we had an isomorphism $f : \Type\_{k} \to \Type\_{k+1}$ we could derive one of the usual paradoxes, such as the variant of Buralli-Forti paradox found by Girard in the original Martin-Löf type theory (which had $\Type : \Type)$. Indeed, $\Type\_{k+1}$ would contain a type isomorphic to itself, namely $\Type\_k$, and that is all that is needed for the usual paradox to occur.


