# The loop homotopy on the circle

```agda
module synthetic-homotopy-theory.loop-homotopy-circle where
```

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.negated-equality
open import foundation.negation
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps

open import synthetic-homotopy-theory.circle
```

</details>

## Idea

The
{{#concept "loop homotopy" Disambiguation="on the circle type" Agda=loop-htpy-๐•Šยน}}
on the [circle](synthetic-homotopy-theory.circle.md) is the family of
[equalities](foundation-core.identity-types.md)

```text
  loop-htpy-๐•Šยน : (x : ๐•Šยน) โ†’ x ๏ผ x
```

defined by [transporting](foundation-core.transport-along-identifications.md)
along the loop of the circle. This [homotopy](foundation-core.homotopies.md) is
distinct from the constant homotopy and has winding number 1.

## Definitions

### The loop homotopy on the circle

```agda
loop-htpy-๐•Šยน : (x : ๐•Šยน) โ†’ x ๏ผ x
loop-htpy-๐•Šยน =
  function-apply-dependent-universal-property-๐•Šยน
    ( eq-value id id)
    ( loop-๐•Šยน)
    ( map-compute-dependent-identification-eq-value-id-id
      ( loop-๐•Šยน)
      ( loop-๐•Šยน)
      ( loop-๐•Šยน)
      ( refl))

compute-base-loop-htpy-๐•Šยน : loop-htpy-๐•Šยน base-๐•Šยน ๏ผ loop-๐•Šยน
compute-base-loop-htpy-๐•Šยน =
  base-dependent-universal-property-๐•Šยน
    ( eq-value id id)
    ( loop-๐•Šยน)
    ( map-compute-dependent-identification-eq-value-id-id
      ( loop-๐•Šยน)
      ( loop-๐•Šยน)
      ( loop-๐•Šยน)
      ( refl))
```

## Properties

### The loop homotopy on the circle is nontrivial

```agda
abstract
  is-not-refl-ev-base-loop-htpy-๐•Šยน : loop-htpy-๐•Šยน base-๐•Šยน โ‰  refl
  is-not-refl-ev-base-loop-htpy-๐•Šยน p =
    is-nontrivial-loop-๐•Šยน (inv compute-base-loop-htpy-๐•Šยน โˆ™ p)

is-nontrivial-loop-htpy-๐•Šยน' : ยฌ (loop-htpy-๐•Šยน ~ refl-htpy)
is-nontrivial-loop-htpy-๐•Šยน' H =
  is-not-refl-ev-base-loop-htpy-๐•Šยน (H base-๐•Šยน)

is-nontrivial-loop-htpy-๐•Šยน : loop-htpy-๐•Šยน โ‰  refl-htpy
is-nontrivial-loop-htpy-๐•Šยน =
  nonequal-ฮ  loop-htpy-๐•Šยน refl-htpy base-๐•Šยน is-not-refl-ev-base-loop-htpy-๐•Šยน
```