I want to prove the square lemma:
Let $F: I \times I \rightarrow X$ continuous. Let $a(s)=F(s,0)$, $b(t)=F(1,t)$, $c(t)=F(0,t)$, $d(s)=F(s,1)$. Then $a * b \sim c*d$
Here $I=[0,1]$, $X$ is any topological space, $*$ denotes path composition and $\sim$ path homotopy.
I'm stuck in my attempt of proof, any suggestion is welcome!
So, let $\phi: I^2 \rightarrow B^2$ be a homeomorphism between the square $I^2$ and the unit disk $B^2$, and let $\tilde{F}= F \circ \phi$. I define $\tilde{f}$, $\tilde{F}$ restricted to $\mathbb{S}^1$: it is a continuous map into $X$ and therefore it is the circle representative for $f=\tilde{f} \circ w$, where $w: I \rightarrow \mathbb{S}^1$, $w(s)= e^{2 \pi i s}$.
Now $\tilde{f}$ can be extended to a continuous map from the disk into $X$, therefore $f$ is path homotopic to its base point.
The proof would be complete if I could show $f \sim (a*b)*\overline{(c*d)}$, where the bar denotes the reverse path. I guess that supposing that $\phi$ maps $\mathbb{S}^1$ to $\partial (I\times I)$ could get me unstuck...
Thanks in advance!
There is a completely explicit way to construct a path homotopy from the path $p = (a * b) * \overline{(c * d)}$ to a constant path. The idea of the construction is to exploit the fact that the path $p$ factors through a closed path in the square, and every closed path in the square is path homotopic to a constant.
To be precise, let $A(s)=(s,0)$, $B(t)=(1,t)$, $C(t)=(0,t)$, $D(s)=(s,1)$. Clearly $q = (A * B) * \overline{(C * D)}$ is a closed path in $I \times I$. And clearly we have $p = F \circ q$. Here is a path homotopy from $q$ to the constant path at $(0,0)$: $$H(u,v) = v \cdot q(u) \quad \text{(That is, multiply the vector $q(u) \in \mathbb R \times \mathbb R$ times the scalar $v$.)} $$ It follows that $F \circ H$ is a path homotopy from $p$ to the constant path at $F(0,0)$.