Free loops

module synthetic-homotopy-theory.free-loops where
Imports
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.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-contr-total-Eq-free-loop :
      (α : free-loop X)  is-contr (Σ (free-loop X) (Eq-free-loop α))
    is-contr-total-Eq-free-loop (pair x α) =
      is-contr-total-Eq-structure
        ( λ x α' p  Id (α  p) (p  α'))
        ( is-contr-total-path 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-contr-total-path α))

  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-contr-total-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-contr-total-Eq-free-dependent-loop :
      ( p : free-dependent-loop α P) 
      is-contr (Σ (free-dependent-loop α P) (Eq-free-dependent-loop p))
    is-contr-total-Eq-free-dependent-loop (pair y p) =
      is-contr-total-Eq-structure
        ( λ y' p' q  Id (p  q) ((ap (tr P (loop-free-loop α)) q)  p'))
        ( is-contr-total-path 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-contr-total-path 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-contr-total-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-const :
    free-loop Y  free-dependent-loop α  x  Y)
  compute-free-dependent-loop-const =
    equiv-tot  y  equiv-concat (tr-const (loop-free-loop α) y) y)

  map-compute-free-dependent-loop-const :
    free-loop Y  free-dependent-loop α  x  Y)
  map-compute-free-dependent-loop-const =
    map-equiv compute-free-dependent-loop-const