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')?