Path-Lifting in HoTT

Lemma 2.3.2 of the HoTT book defines a kind of path-lifting for "fibrations" (ie type families):

The proof is left as an exercise, but I'm struggling to understand what the last propositional equality means. The main body of the lemma is straightforward; indeed, by induction on $$p$$ we may assume $$p\equiv\text{refl}_x$$, and then take $$\text{lift}(u, \text{refl}_x)\equiv \text{refl}_{(x, u)}$$. Since $$(\text{refl}_x)_*\equiv \text{id}_{P(x)}$$ this is evidently well-typed, and hence by the induction principle will induce the desired function $$\text{lift}:\Pi_{u:P(x)}\Pi_{p:x=_A y}(x, u)=(y, p_*(u))$$. (Though really to be very formal I think we would want to first define $$\text{lift}':\Pi_{p:x=_A y}\Pi_{u:P(x)}(x, u)=(y, p_*(u))$$ by induction and then define $$\text{lift}$$ by swapping the arguments in $$\text{lift}'$$.) In any case this is fine to me. But I don't see why it now makes sense to apply $$\text{pr}_1$$ to $$\text{lift}(u, p)$$...

Surely to reason about such an application we would need the identity type $$(x, u)=_{\Sigma_{(z:A)}P(z)}(y, p_*(u))$$ to be somehow (judgementally equal to?) a dependent sum type; it would have to be of shape $$\Sigma_{x=_A y}B$$, but I am not sure what to substitute in for $$B$$. Intuitively we would want $$B$$ to be a (dependent) "space of paths" between $$u$$ and $$p_*(u)$$ (parametrized by the first coordinate $$p$$), but since $$u:P(x)$$ and $$p_*(u):P(y)$$ it is not clear how to make sense of such a space. Even if there were a suitable choice for $$B$$, I don't see how to make such an identification formal; surely an identity type and a dependent sum type cannot be judgmentally equal. Can anyone help clear up this confusion?

We will often write $$\mathrm{ap}_f(p)$$ as simply $$f(p)$$
and this is an instance of that. $$\mathrm{pr}_1(\mathrm{lift}(u, p)) \equiv \mathrm{ap}_{pr_1}(\mathrm{lift}(u, p)): \mathrm{pr}_1(x, u) = \mathrm{pr}_1(y, p_*(u))$$.