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+1} \to \Type_{k}$ 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$ would contain a type isomorphic to itself, namely $f(\Type_k)$, and that is all that is needed for the usual paradox to occur.

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.

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_2$ 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+1} \to \Type_{k}$ 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$ would contain a type isomorphic to itself, namely $f(\Type_k)$, and that is all that is needed for the usual paradox to occur.

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+1} \to \Type_{k}$ 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$ would contain a type isomorphic to itself, namely $f(\Type_k)$, and that is all that is needed for the usual paradox to occur.