Free loops

module synthetic-homotopy-theory.free-loops where

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