# Identity types and universes

Let us consider Martin-Löf type theory with a cumulative hierarchy of universes $$\mathcal{U}_0\colon\mathcal{U}_1\colon\ldots$$ If $$A, B\colon \mathcal{U}_i$$, we can form an identity type $$A=_{\mathcal{U}_i} B:\mathcal{U}_i$$. Using the axiom of cumulative hierarchy, we can derive $$A, B:\mathcal{U}_{i+1}$$, so we have also an identity type $$A=_{\mathcal{U}_{i+1}}B$$. Assuming the Univalence axiom (for all the universes), they are both equivalent to a type of equivalences $$(A\simeq B)$$, which has nothing to do with universe issues. What can we say about the relationship between types $$A=_{\mathcal{U}_i} B$$ and $$A=_{\mathcal{U}_{i+1}} B$$ without the Univalence axiom?

In general cummulative universes are a bit nasty. To see what is really going on, at the very least it makes sense to have explicit lifting maps $$\mathsf{lift}_{i,j} : \mathcal{U}_i \to \mathcal{U}_j$$ for $$i \leq j$$. With these in place, your question is: how do the types $$\mathsf{lift}_{i,i+1}(A =_{\mathcal{U}_i} B)$$ and $$(\mathsf{lift}_{i,i+1} A) =_{\mathcal{U}_{i+1}}(\mathsf{lift}_{i,i+1} B)$$ relate? The answer is: unless we make further assumptions, we cannot show them to be equivalent. In fact, when type theory is given with explicit $$\mathsf{lift}_{i,j}$$ maps, we include judgemental equalities which say "lifting maps commute with type constructions", such as, for $$i < j$$, $$\mathsf{lift}_{i,j}(A =_{\mathcal{U}_i} B) \equiv (\mathsf{lift}_{i,j} A =_{\mathcal{U}_{j}} \mathsf{lift}_{i,j} B).$$ These sorts of details are usually skipped in informal presentations of type theory. In particular the HoTT book is a bit sloppy on this point. (But the formalizations of HoTT in Coq, Agda and Lean are not.)
The induction principle for $$=_{U_{i+1}}$$ gives you a map $$(A=_{U_{i+1}}B)\rightarrow (A=_{U_i}B)$$.
In HoTT without univalence, there is no map $$(A=_{U_i}B)\rightarrow (A=_{U_{i+1}}B)$$: indeed, you could assume the univalence axiom only for universe $$U_i$$. In that case, $$A\simeq B$$ gives you by univalence an inhabitant of $$A=_{U_i}B$$, but not of $$A=_{U_{i+1}}B$$: with the rules of the theory, the inhabitants of the identity types $$=_{U_{i+1}}$$ can only take the form $$refl_A$$.