Statement
Existential version
Suppose
is a topological space,
is a point in
, and
are loops based at
with the property that
is homotopic to
(as a loop based at
) and
is homotopic to
(again, as a loop based at
). Then,
is homotopic to
.
Constructive/explicit version
More explicitly, suppose
is a homotopy from
to
. In other words,
is a continuous map (where
is the circle, viewed as
with endpoints identified, and
is the closed unit interval) having the following properties:


(here
is the chosen basepoint of the circle from which we're mapping). This says that the loop always remains based on
.
Similarly, suppose
is a continuous map having the following properties:


(here
is the chosen basepoint of the circle). This says that the loop always remains based on
.
Then, we can consider the following homotopy from
to
:
We can think of
as
.
Graphical version
The pictures below describe the explicit construction. Note that the geometric shapes shown in these pictures can be thought of as the sources of the respective maps to
, with the additional caveat that the boundary vertical lines map to the point
. (The same pictures, without the collapse of boundaries, work to establish the homotopy between composites of homotopic paths).
The homotopy
between
and
is a map from a filled unit square, where the restrictions of the map to the bottom and top sides of the square are
and
respectively. The left and right sides map to the point
:
The homotopy
between
and
is a map from a filled unit square, where the restrictions of the map to the bottom and top sides of the square are
and
respectively. The left and right sides map to the point
:
These homotopies are composed by concatenation, as shown below. Both
and
need to be scaled by a factor of
for the concatenated homotopy to fit in a unit square: