Universal Property of suspensions of pointed types

Content created by Fredrik Bakke, Egbert Rijke and Raymond Baker.

Created on 2023-08-28.
Last modified on 2024-03-14.

module synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types where
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import structured-types.pointed-equivalences
open import structured-types.pointed-maps
open import structured-types.pointed-types

open import synthetic-homotopy-theory.functoriality-loop-spaces
open import synthetic-homotopy-theory.loop-spaces
open import synthetic-homotopy-theory.suspensions-of-pointed-types
open import synthetic-homotopy-theory.suspensions-of-types


The suspension of a pointed type enjoys an additional universal property, on top of the universal property associtated with being a suspension. This universal property is packaged in an adjunction: the suspension construction on pointed types is left adjoint to the loop space construction.

The unit and counit of the adjunction

module _
  {l1 : Level} (X : Pointed-Type l1)

  pointed-equiv-loop-pointed-identity-suspension :
    ( pair
      ( north-suspension  south-suspension)
      ( meridian-suspension (point-Pointed-Type X))) ≃∗
    ( Ω (suspension-Pointed-Type X))
  pointed-equiv-loop-pointed-identity-suspension =
      ( suspension-Pointed-Type X)
      ( meridian-suspension (point-Pointed-Type X))

  pointed-map-loop-pointed-identity-suspension :
    ( pair
      ( north-suspension  south-suspension)
      ( meridian-suspension (point-Pointed-Type X))) →∗
    Ω (suspension-Pointed-Type X)
  pointed-map-loop-pointed-identity-suspension =
      ( pointed-equiv-loop-pointed-identity-suspension)

  pointed-map-concat-meridian-suspension :
    X →∗
    ( pair
      ( north-suspension  south-suspension)
      ( meridian-suspension (point-Pointed-Type X)))
  pr1 pointed-map-concat-meridian-suspension = meridian-suspension
  pr2 pointed-map-concat-meridian-suspension = refl

  pointed-map-unit-suspension-loop-adjunction :
    X →∗ Ω (suspension-Pointed-Type X)
  pointed-map-unit-suspension-loop-adjunction =
    pointed-map-loop-pointed-identity-suspension ∘∗

  map-unit-suspension-loop-adjunction :
    type-Pointed-Type X  type-Ω (suspension-Pointed-Type X)
  map-unit-suspension-loop-adjunction =
    map-pointed-map pointed-map-unit-suspension-loop-adjunction

  map-counit-suspension-loop-adjunction :
    suspension (type-Ω X)  type-Pointed-Type X
  map-counit-suspension-loop-adjunction =
      ( up-suspension (type-Pointed-Type X))
      ( point-Pointed-Type X , point-Pointed-Type X , id)

  pointed-map-counit-suspension-loop-adjunction :
    pair (suspension (type-Ω X)) (north-suspension) →∗ X
  pr1 pointed-map-counit-suspension-loop-adjunction =
  pr2 pointed-map-counit-suspension-loop-adjunction =
      ( point-Pointed-Type X , point-Pointed-Type X , id)

The transposing maps of the adjunction

module _
  {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)

  transpose-suspension-loop-adjunction :
    (suspension-Pointed-Type X →∗ Y)  (X →∗ Ω Y)
  transpose-suspension-loop-adjunction f∗ =
    pointed-map-Ω f∗ ∘∗ pointed-map-unit-suspension-loop-adjunction X

module _
  {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)

  inv-transpose-suspension-loop-adjunction :
    (X →∗ Ω Y)  (suspension-Pointed-Type X →∗ Y)
  pr1 (inv-transpose-suspension-loop-adjunction f∗) =
      ( suspension-structure-map-into-Ω
        ( type-Pointed-Type X)
        ( Y)
        ( map-pointed-map f∗))
  pr2 (inv-transpose-suspension-loop-adjunction f∗) =
      ( suspension-structure-map-into-Ω
        ( type-Pointed-Type X)
        ( Y)
        ( map-pointed-map f∗))

We now show these maps are inverses of each other.

The transposing equivalence between pointed maps out of the suspension of X and pointed maps into the loop space of Y

module _
  {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)

  equiv-transpose-suspension-loop-adjunction :
    (suspension-Pointed-Type X →∗ Y)  (X →∗ Ω Y)
  equiv-transpose-suspension-loop-adjunction =
    ( left-unit-law-Σ-is-contr
      ( is-torsorial-Id (point-Pointed-Type Y))
      ( point-Pointed-Type Y , refl)) ∘e
    ( inv-associative-Σ
      ( type-Pointed-Type Y)
      ( λ z  point-Pointed-Type Y  z)
      ( λ t 
        Σ ( type-Pointed-Type X  point-Pointed-Type Y  pr1 t)
          ( λ f  f (point-Pointed-Type X)  pr2 t))) ∘e
    ( equiv-tot  y1  equiv-left-swap-Σ)) ∘e
    ( associative-Σ
      ( type-Pointed-Type Y)
      ( λ y1  type-Pointed-Type X  point-Pointed-Type Y  y1)
      ( λ z 
        Σ ( point-Pointed-Type Y  pr1 z)
          ( λ x  pr2 z (point-Pointed-Type X)  x))) ∘e
    ( inv-right-unit-law-Σ-is-contr
      ( λ z  is-torsorial-Id (pr2 z (point-Pointed-Type X)))) ∘e
    ( left-unit-law-Σ-is-contr
      ( is-torsorial-Id' (point-Pointed-Type Y))
      ( point-Pointed-Type Y , refl)) ∘e
    ( equiv-right-swap-Σ) ∘e
    ( equiv-Σ-equiv-base
      ( λ c  pr1 c  point-Pointed-Type Y)
      ( equiv-up-suspension))

The equivalence in the suspension-loop space adjunction is pointed

This remains to be shown. #702

Recent changes