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.)

StackExchange Computer Science Q#104103, answer score: 3