I am reading the HoTT book and have question regarding the following:
Lemma 2.3.2 : (Path lifting property). Let $P : A → U$ be a type family over A and assume we have $u : P(x)$ for some $x : A$. Then for any $p : x = y$, we have $lift(u, p) : (x, u) = (y, p_∗(u))$ in $∑_{(x:A)} P(x)$, such that $pr_1(lift(u, p)) = p$.
On page 73, the last paragraph says this implies:
Any path from $u : P(x)$ to $v : P(y)$ lying over p should factor through $lift(u, p)$, essentially uniquely, by a path from $p_∗(u)$ to $v$ lying entirely in the fiber $P(y)$. Thus, up to equivalence, it makes sense to define “a path from $u$ to $v$ lying over $p : x = y$” to mean a path $p_∗(u) = v$ in $P(y)$.
I am confused how the lemma above implies "Any path from $u : P(x)$ to $v : P(y)$ lying over p should factor through $lift(u, p)$, essentially uniquely, by a path from $p_∗(u)$ to $v$ lying entirely in the fiber $P(y)$". If I got it correct, this statement will translate to: For any path $q:(x,u)=(y,v)$ for $u\in P(x),v\in P(y)$ such that $p_1(q)=p$, exists a unique path $r:(y,p_*(u))=(y,v)$ such that $q=lift(u,p)\cdot r$, could someone please tell me why does this holds from the lemma?
Thank you for any attempt of help!