Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?

Question

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

Answer 1

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.

Answer 2

We usually assume that universes are closed under all type constructions. So, Type$_0$ contains Nats, Reals, Complex; Type$_1$ contains Nats, Reals, Complex, and Type$_0$; Type$_2$ contains Nats, Reals, Complex, Type$_0$, and Type$_1$; and so on.

Even if we define a type theory, where the only term of type Type$_{k+1}$ is Type$_k$, we cannot prove that Type$_1$ isomorphic to Type$_2$. The problem is that we know that Type$_1$ contains Type$_0$, but we do not know that it is the only term of this type. We just do not have rules from which that would follow. This is a general philosophy of Martin-Löf's type theories: universes should be open; we know which types they contain, but we do not know that they are the only types in these universes.

It is possible to define closed universes, but we need to do this carefully. We cannot say that Type$_0$ is a type with three elements (Nats, Reals, Complex) since this implies that it is a set, and tihs contradicts the univalence axiom. I describe a simple (and not very interesting) way to do this correcly. We can define a closed universe as a subuniverse of an open universe. First, we define a predicate $P : \mathrm{Type}_0 \to \mathrm{Prop}$. For example, we can take $$P(A) = \| (A = \mathrm{Nats}) + (A = \mathrm{Reals}) + (A = \mathrm{Complex}) \|.$$ Then $\sum\limits_{A : \mathrm{Type}_0} P(A)$ is a "universe" which contains these three types and all paths (and higher paths) between them.

Answer 3

The Univalence axiom states that homotopy equivalent types are equal. That doesn't mean the hierarchy is collapsible: that would require judgemental and not Leibniz equality. The very point of HoTT is that equal objects are still non-trivially equal and in general too different to recklessly identify them.

Anyway, that doesn't apply to the type hierarchy because the universes are not equivalent: you cannot construct a map $Type_{k+1} \to Type_k$ because $Type_k : Type_{k+1}$ but $Type_k \not\in Type_k$ and there is no other element to map it.

Also note that $Type_{k+1}$ can have many more other elements. The exact forms depend on your rules of universe labelling, but at least there should be types like $Real$ or $Type_k \to Nat$ or $Nat \to Type_k \to 2$.