# The loop homotopy on the circle

Content created by Fredrik Bakke.

Created on 2024-06-04.

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

Imports
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


## Idea

The loop homotopy on the circle is the family of equalities

  loop-htpy-𝕊¹ : (x : 𝕊¹) → x ＝ x


defined by transporting along the loop of the circle. This homotopy is distinct from the constant homotopy and has winding number 1.

## Definitions

### The loop homotopy on the circle

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

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-𝕊¹