Let K be a simplicial complex, and let $α_1$ and $α_2$ be edge paths. Suppose that $α_1$ and $α_2$ are homotopic relative to their endpoints. Show that $α_1$ and $α_2$ are equivalent as edge paths.
(where we've defined paths to be equivalent if they can be obtained from one another by a finite sequence of the following moves or their reverse, where the $a_i$ in the descriptions of the rules are the sequence of vertices the edge path follows:
$(0)$ replacing $. . . , a_{i−1}, a_i , . . .$ by $. . . , a_{i−1}, . . .$ provided $a_{i−1} = a_i$ ;
$(1)$ replacing $. . . , a_{i−1}, a_i , a_{i+1}, . . . $ by $. . . , a_{i−1}, . . . ,$ provided $a_{i−1} = a_{i+1}$;
(2) replacing $. . . , a_{i−1}, a_i , a_{i+1}, . . .$ by $. . . , a_{i−1}, a_{i+1}, . . .,$ provided {$a_{i−1}, a_i , a_{i+1}$} span a 2-simplex of $K$.
Here's a diagram showing what (1) and (2) look like)
I've shown in a similar question that the group of equivalence classes edge loops based at a point is isomorphic to the fundamental group of the realisation $|K|$ of $K$ based at a point, which shows that any homotopic edge loops are equivalent, but I don't know how to modify the approach in this case, since the equivalence classes of edge paths don't form a group in the same way so I can't employ the same strategy.
UPDATE: I've put a bit more thought into it, and here's where I'm at:
If I let $I_{(n)}$ be the triangulation of $I=[0, 1]$ with $n$ 1-simplices, each of length $1/n$, then I can regard an edge path of length $n$ as a simplicial map $I_{(n)}\rightarrow K$, which defines a mapping
$f:$ {equivalence classes of edge paths in $K$ with endpoints $x, y$} $\rightarrow $ {homotopy classes of paths in $|K|$ with endpoints $x, y$}.
If I can show that $f$ is injective - that if $f([α_1])=f([α_2])$ then $[α_1]=[α_2]$ then I'm done.
The trouble is there's no identity because I'm not mapping into a group, so I need to show this directly, and I'm not sure how.
Any help would be appreciated.
First, you can work with the fundamental group, because certain statements about path homotopies can be translated into fundamental group statements, even for paths which are not closed. For example, given two paths $\alpha_1,\alpha_2 : I \to K$ with the same initial endpoints $p = \alpha_1(0)=\alpha_2(0)$ and the same terminal endpoints $q = \alpha_1(1)=\alpha_2(1)$, $\alpha_1$ and $\alpha_1$ are path homotopic if and only if the closed path $\alpha_1 * \bar\alpha_2$ represents the identity element of the fundamental group $\pi_1(K,p)$.
Thus, the statement you are trying to prove is equivalent to the statement that a closed edge path in $K$ based at a vertex $p$ represents the identity if and only if it is equivalent as an edge path to the trivial edge path at $p$.
What you need next is a theorem that is usually expressed in far greater generality, namely for a CW complex. This theorem gives an explicit presentation of the fundamental group $\pi_1(K,p)$.
To describe the presentation first choose a maximal tree $T$ in the 1-skeleton $K^{(1)}$. List the remaining edges of $K^{(1)}-T$ as $E_i$, and choose an orientation of each $E_i$.
The generating set of the presentation consists of one element $g_i$ for each $1$-cell $E_i$, where $g_i$ is the homotopy class of the following path: starting from $p$, in the maximal tree take the unique edge path from $p$ to the initial endpoint of $E_i$; then concatenate with $E_i$; and then concatenate with the unique edge path from the terminal endpoint of $E_i$ back through the maximal tree back to $p$.
The relation set of the presentation contains one relation for each $2$-cell. In your situation where a 2-cell is a simplex, go around the simplex and write its edges as $E_{i_1},E_{i_2},E_{i_3}$. The relator is obtained by writing $g_{i_1} g_{i_2} g_{i_3}$ except that if $E_{i_j}$ is actually contained in the maximal tree then you just skip $g_{i_j}$.
With that, you should be able to put the pieces together to prove the statement you want.
Let me add that the one textbook I know which does a good job of both the simplicial complex situation of your question and the general theory of fundamental group is Spanier's "Algebraic Topology".