In homotopy type theory, or dependent type theories more generally, there is a "top-level" type called the universe, generally denoted Type. So for a concrete example, I could describe having 3 types: Nats, Reals, 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')  ?

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