Identity types and universes
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 &lt; 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.)