# 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-๐ยน ```