# Homotopy between constant loop and composite of loop with inverse

## Contents

## Statement

### Existential version

Suppose is a point in a topological space . Suppose is a loop based at , i.e., is a continuous map from the closed unit interval to such that . Denote by the loop defined as . Denote by the constant loop at the point .

Denote by the composition of loops by concatenation. Then, the loops and are both homotopic to .

Note that since , it suffices to show that is homotopic to .

This is the *inverses* part of the proof that the Fundamental group (?) of a based topological space is indeed a group.

### Constructive/explicit version

We note that , so we have:

The map to which we want to homotope this is:

The homotopy is given by:

### Graphical version

Here is a pictorial description of the homotopy:

### Uniform version

Suppose is a based topological space. Let be the loop space. Consider the following two maps from to itself:

and:

Then, the maps and are homotopic maps.