# Free loops

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-07-29.

module synthetic-homotopy-theory.free-loops where

Imports
open import foundation.action-on-identifications-functions
open import foundation.constant-type-families
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.universe-levels


## Idea

A free loop in a type X consists of a point x : X and an identification x ＝ x. The type of free loops in X is equivalent to the type of maps 𝕊¹ → X.

## Definitions

### Free loops

free-loop : {l1 : Level} (X : UU l1) → UU l1
free-loop X = Σ X (λ x → x ＝ x)

module _
{l1 : Level} {X : UU l1}
where

base-free-loop : free-loop X → X
base-free-loop = pr1

loop-free-loop : (α : free-loop X) → base-free-loop α ＝ base-free-loop α
loop-free-loop = pr2


### Free dependent loops

module _
{l1 l2 : Level} {X : UU l1} (α : free-loop X) (P : X → UU l2)
where

free-dependent-loop : UU l2
free-dependent-loop =
Σ ( P (base-free-loop α)) (λ p₀ → tr P (loop-free-loop α) p₀ ＝ p₀)

base-free-dependent-loop : free-dependent-loop → P (base-free-loop α)
base-free-dependent-loop = pr1

loop-free-dependent-loop :
(β : free-dependent-loop) →
( tr P (loop-free-loop α) (base-free-dependent-loop β)) ＝
( base-free-dependent-loop β)
loop-free-dependent-loop = pr2


## Properties

### Characterization of the identity type of the type of free loops

module _
{l1 : Level} {X : UU l1}
where

Eq-free-loop : (α α' : free-loop X) → UU l1
Eq-free-loop (pair x α) α' =
Σ (Id x (base-free-loop α')) (λ p → Id (α ∙ p) (p ∙ (loop-free-loop α')))

refl-Eq-free-loop : (α : free-loop X) → Eq-free-loop α α
pr1 (refl-Eq-free-loop (pair x α)) = refl
pr2 (refl-Eq-free-loop (pair x α)) = right-unit

Eq-eq-free-loop : (α α' : free-loop X) → Id α α' → Eq-free-loop α α'
Eq-eq-free-loop α .α refl = refl-Eq-free-loop α

abstract
is-torsorial-Eq-free-loop :
(α : free-loop X) → is-torsorial (Eq-free-loop α)
is-torsorial-Eq-free-loop (pair x α) =
is-torsorial-Eq-structure
( is-torsorial-Id x)
( pair x refl)
( is-contr-is-equiv'
( Σ (Id x x) (λ α' → Id α α'))
( tot (λ α' α → right-unit ∙ α))
( is-equiv-tot-is-fiberwise-equiv
( λ α' → is-equiv-concat right-unit α'))
( is-torsorial-Id α))

abstract
is-equiv-Eq-eq-free-loop :
(α α' : free-loop X) → is-equiv (Eq-eq-free-loop α α')
is-equiv-Eq-eq-free-loop α =
fundamental-theorem-id
( is-torsorial-Eq-free-loop α)
( Eq-eq-free-loop α)


### Characterization of the identity type of free dependent loops

module _
{l1 l2 : Level} {X : UU l1} (α : free-loop X) (P : X → UU l2)
where

Eq-free-dependent-loop : (p p' : free-dependent-loop α P) → UU l2
Eq-free-dependent-loop (pair y p) p' =
Σ ( Id y (base-free-dependent-loop α P p'))
( λ q →
( p ∙ q) ＝
( ( ap (tr P (loop-free-loop α)) q) ∙
( loop-free-dependent-loop α P p')))

refl-Eq-free-dependent-loop :
(p : free-dependent-loop α P) → Eq-free-dependent-loop p p
pr1 (refl-Eq-free-dependent-loop (pair y p)) = refl
pr2 (refl-Eq-free-dependent-loop (pair y p)) = right-unit

Eq-free-dependent-loop-eq :
( p p' : free-dependent-loop α P) → Id p p' → Eq-free-dependent-loop p p'
Eq-free-dependent-loop-eq p .p refl = refl-Eq-free-dependent-loop p

abstract
is-torsorial-Eq-free-dependent-loop :
( p : free-dependent-loop α P) → is-torsorial (Eq-free-dependent-loop p)
is-torsorial-Eq-free-dependent-loop (pair y p) =
is-torsorial-Eq-structure
( is-torsorial-Id y)
( pair y refl)
( is-contr-is-equiv'
( Σ (Id (tr P (loop-free-loop α) y) y) (λ p' → Id p p'))
( tot (λ p' α → right-unit ∙ α))
( is-equiv-tot-is-fiberwise-equiv
( λ p' → is-equiv-concat right-unit p'))
( is-torsorial-Id p))

abstract
is-equiv-Eq-free-dependent-loop-eq :
(p p' : free-dependent-loop α P) →
is-equiv (Eq-free-dependent-loop-eq p p')
is-equiv-Eq-free-dependent-loop-eq p =
fundamental-theorem-id
( is-torsorial-Eq-free-dependent-loop p)
( Eq-free-dependent-loop-eq p)

eq-Eq-free-dependent-loop :
(p p' : free-dependent-loop α P) →
Eq-free-dependent-loop p p' → Id p p'
eq-Eq-free-dependent-loop p p' =
map-inv-is-equiv (is-equiv-Eq-free-dependent-loop-eq p p')


### The type of free dependent loops in a constant family of types is equivalent to the type of ordinary free loops

module _
{l1 l2 : Level} {X : UU l1} (α : free-loop X) (Y : UU l2)
where

compute-free-dependent-loop-constant-type-family :
free-loop Y ≃ free-dependent-loop α (λ x → Y)
compute-free-dependent-loop-constant-type-family =
equiv-tot
( λ y → equiv-concat (tr-constant-type-family (loop-free-loop α) y) y)

map-compute-free-dependent-loop-constant-type-family :
free-loop Y → free-dependent-loop α (λ x → Y)
map-compute-free-dependent-loop-constant-type-family =
map-equiv compute-free-dependent-loop-constant-type-family