# Homotopy between loop and composite with constant loop

From Topospaces

## Contents

## Statement

### Existential version

Suppose is a point in a topological space and is a loop based at , i.e., is a continuous map from to such that . Suppose is the *constant loop* based at , i.e., the loop that stays at throughout.

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

This statement is essentially the *identity element* part of the proof that the Fundamental group (?) of a based topological space is indeed a group.

### Constructive/explicit version

For a loop based at , the loop is given by:

The homotopy between and is given by:

The loop is given by:

The homotopy between and is given by:

### Graphical version

Here is a pictorial description of the homotopy between and :

Here is a pictorial description of the homotopy between and :