# Universal Property of suspensions of pointed types

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

Created on 2023-08-28.

module synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types where
Imports
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

## Idea

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)
where

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 =
pointed-equiv-loop-pointed-identity
( 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-map-pointed-equiv
( 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

X →∗ Ω (suspension-Pointed-Type X)
pointed-map-loop-pointed-identity-suspension ∘∗
pointed-map-concat-meridian-suspension

type-Pointed-Type X  type-Ω (suspension-Pointed-Type X)

suspension (type-Ω X)  type-Pointed-Type X
map-inv-is-equiv
( up-suspension (type-Pointed-Type X))
( point-Pointed-Type X , point-Pointed-Type X , id)

pair (suspension (type-Ω X)) (north-suspension) →∗ X
compute-north-cogap-suspension
( 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)
where

(suspension-Pointed-Type X →∗ Y)  (X →∗ Ω Y)

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

(X →∗ Ω Y)  (suspension-Pointed-Type X →∗ Y)
cogap-suspension
( suspension-structure-map-into-Ω
( type-Pointed-Type X)
( Y)
( map-pointed-map f∗))
compute-north-cogap-suspension
( 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)
where

(suspension-Pointed-Type X →∗ Y)  (X →∗ Ω Y)
( 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