Vtyjkyuk

Let $p:Xrightarrow Y$ a covering map, $a,b : Irightarrow Y$ are relatively homotopic to each other: $a simeq_partial I b $ (denoting $F:Itimes[0,1] rightarrow Y$ the homotopy between $a$ and $b$). The lifts $tildea , tildeb$ satisfies $tildea(0)=tildeb(0)$. I wish to prove that $tildea(1) = tildeb(1)$ and $tildea simeq tildeb$.

For $tildea(1) = tildeb(1)$ I tried to show by using the homotopy lifting property of $F$, and use the homotopy $G:Itimes [0,1] rightarrow X$ satisfies: $G_0 = tildea$ and $pcirc G_t =F_t$. Then I took two approaches:

1. Show the existence of a lift $gamma$ of $b$ such that $gamma(0) = tildea(0)$ and $gamma(1) = tildea(1)$ then from path lifting uniqueness $gamma$ must be equal to $tildeb$.


2. Show that $G_1$ and $tildeb$ agree in one point and then by theorem they agree on all points. Yet this approach (which I didn't succeeded to prove), just satisfies the fact $tildea simeq tildeb$ but as fat as I understand doesn't promise $tildea(1) = tildeb(1)$.

This post is very similar, relating to loops which are lifted to the same base point:
Are the lifts of homotopic curves necessarily homotopic?

Let $tilde a,tilde b:Irightarrow X$ be lifts of $a,b:Irightarrow Y$ satisfying $pcirc tilde a=a$, $pcirc tilde b=b$, and let $F_t:asimeq_partial Ib:Irightarrow Y$ be a relative homotopy satisfying $F(s,0)=a(s)$, $F(s,1)=b(s)$, $F(0,t)=a(0)=b(0)$ and $F(1,t)=a(1)=b(1)$. Now apply the HELP lemma in the diagram

$requireAMScd$
beginCD
0times Icup Itimes partial I@>G'>> X\
@Vi V V @VVpV\
Itimes I @>F>> Y
endCD$requireAMScd$

where $G'(s,0)=tilde a(s)$, $G'(s,1)=tilde b(s)$, $G'(0,t)=tilde a(0)=tilde b(0)$. Note that $pcirc G'=Fcirc i$. From the data the HELP lemma gives a map $G:Itimes Irightarrow X$ satisfying

$$G(s,0)=tilde a (s),quad G(s,1)=tilde b(s),quad G(0,t)=tilde a(0)=tilde b(0),quad pcirc G(s,t)=F(s,t).$$

In particular $p(G(s,1))=p(tilde a(1))=p(tilde b(1))=F(s,1)=a(0)=b(0)$, so the assignment $smapsto G(s,1)$ is a path in $X$ contained in the fibre over $a(0)=b(0)$, going from $tilde a(0)$ and ending at $tilde b(0)$. Since the covering projection has discrete fibres such a path must be constant.

Hence $tilde a(1)=tilde b(1)$, and $G:tilde asimeq_partial Itilde b$ is a relative homotopy.