# Suspension Structures

```agda
module synthetic-homotopy-theory.suspension-structures where
```

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-identifications
open import foundation.constant-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-systems
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.unit-type
open import foundation.universal-property-unit-type
open import foundation.universe-levels
open import foundation.whiskering-identifications-concatenation

open import synthetic-homotopy-theory.cocones-under-spans
```

</details>

## Idea

The suspension of `X` is the [pushout](synthetic-homotopy-theory.pushouts.md) of
the span `unit <-- X --> unit`. A
[cocone under such a span](synthetic-homotopy-theory.dependent-cocones-under-spans.md)
is called a `suspension-cocone`. Explicitly, a suspension cocone with nadir `Y`
consists of functions

```text
f : unit → Y
g : unit → Y
```

and a homotopy

```text
h : (x : X) → (f ∘ (terminal-map X)) x = (g ∘ (terminal-map X)) x
```

Using the
[universal property of the unit type](foundation.universal-property-unit-type.md),
we can characterize suspension cocones as equivalent to a selection of "north"
and "south" poles

```text
north , south : Y
```

and a meridian function

```text
meridian : X → north = south
```

We call this type of structure `suspension-structure`.

## Definition

### Suspension cocones on a type

```agda
suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2)  UU (l1  l2)
suspension-cocone X Y = cocone (terminal-map X) (terminal-map X) Y
```

### Suspension structures on a type

```agda
module _
  {l1 l2 : Level} (X : UU l1) (Y : UU l2)
  where

  suspension-structure : UU (l1  l2)
  suspension-structure = Σ Y  N  Σ Y  S  (x : X)  N  S))

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

  north-suspension-structure : suspension-structure X Y  Y
  north-suspension-structure c = pr1 c

  south-suspension-structure : suspension-structure X Y  Y
  south-suspension-structure c = (pr1  pr2) c

  meridian-suspension-structure :
    (c : suspension-structure X Y) 
    X  north-suspension-structure c  south-suspension-structure c
  meridian-suspension-structure c = (pr2  pr2) c
```

## Properties

### Equivalence between suspension structures and suspension cocones

```agda
module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
  where

  suspension-cocone-suspension-structure :
    suspension-structure X Y  suspension-cocone X Y
  pr1 (suspension-cocone-suspension-structure (N , S , merid)) = point N
  pr1 (pr2 (suspension-cocone-suspension-structure (N , S , merid))) = point S
  pr2 (pr2 (suspension-cocone-suspension-structure (N , S , merid))) = merid

  suspension-structure-suspension-cocone :
    suspension-cocone X Y  suspension-structure X Y
  pr1 (suspension-structure-suspension-cocone (N , S , merid)) = N star
  pr1 (pr2 (suspension-structure-suspension-cocone (N , S , merid))) = S star
  pr2 (pr2 (suspension-structure-suspension-cocone (N , S , merid))) = merid

  is-equiv-suspension-cocone-suspension-structure :
    is-equiv suspension-cocone-suspension-structure
  is-equiv-suspension-cocone-suspension-structure =
    is-equiv-is-invertible
      ( suspension-structure-suspension-cocone)
      ( refl-htpy)
      ( refl-htpy)

  is-equiv-suspension-structure-suspension-cocone :
    is-equiv suspension-structure-suspension-cocone
  is-equiv-suspension-structure-suspension-cocone =
    is-equiv-is-invertible
      ( suspension-cocone-suspension-structure)
      ( refl-htpy)
      ( refl-htpy)

  equiv-suspension-structure-suspension-cocone :
    suspension-structure X Y  suspension-cocone X Y
  pr1 equiv-suspension-structure-suspension-cocone =
    suspension-cocone-suspension-structure
  pr2 equiv-suspension-structure-suspension-cocone =
    is-equiv-suspension-cocone-suspension-structure

  equiv-suspension-cocone-suspension-structure :
    suspension-cocone X Y  suspension-structure X Y
  pr1 equiv-suspension-cocone-suspension-structure =
    suspension-structure-suspension-cocone
  pr2 equiv-suspension-cocone-suspension-structure =
    is-equiv-suspension-structure-suspension-cocone
```

#### Characterization of equalities in `suspension-structure`

```agda
module _
  {l1 l2 : Level} {X : UU l1} {Z : UU l2}
  where

  htpy-suspension-structure :
    (c c' : suspension-structure X Z)  UU (l1  l2)
  htpy-suspension-structure c c' =
    Σ ( north-suspension-structure c  north-suspension-structure c')
      ( λ p 
        Σ ( south-suspension-structure c  south-suspension-structure c')
          ( λ q 
            ( x : X) 
            ( meridian-suspension-structure c x  q) 
            ( p  meridian-suspension-structure c' x)))

  north-htpy-suspension-structure :
    {c c' : suspension-structure X Z} 
    htpy-suspension-structure c c' 
    north-suspension-structure c  north-suspension-structure c'
  north-htpy-suspension-structure = pr1

  south-htpy-suspension-structure :
    {c c' : suspension-structure X Z} 
    htpy-suspension-structure c c' 
    south-suspension-structure c  south-suspension-structure c'
  south-htpy-suspension-structure = pr1  pr2

  meridian-htpy-suspension-structure :
    {c c' : suspension-structure X Z} 
    (h : htpy-suspension-structure c c') 
    ( x : X) 
    coherence-square-identifications
      ( north-htpy-suspension-structure h)
      ( meridian-suspension-structure c x)
      ( meridian-suspension-structure c' x)
      ( south-htpy-suspension-structure h)
  meridian-htpy-suspension-structure = pr2  pr2

  extensionality-suspension-structure :
    (c c' : suspension-structure X Z) 
    (c  c')  (htpy-suspension-structure c c')
  extensionality-suspension-structure (N , S , merid) =
    extensionality-Σ
      ( λ y p 
        Σ (S  pr1 y)  q  (x : X)  (merid x  q)  (p  pr2 y x)))
      ( refl)
      ( refl , right-unit-htpy)
      ( λ z  id-equiv)
      ( extensionality-Σ
        ( λ H q  (x : X)  (merid x  q)  H x)
        ( refl)
        ( right-unit-htpy)
        ( λ z  id-equiv)
        ( λ H  equiv-concat-htpy right-unit-htpy H ∘e equiv-funext))

module _
  {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c c' : suspension-structure X Z}
  where

  htpy-eq-suspension-structure : (c  c')  htpy-suspension-structure c c'
  htpy-eq-suspension-structure =
    map-equiv (extensionality-suspension-structure c c')

  eq-htpy-suspension-structure : htpy-suspension-structure c c'  (c  c')
  eq-htpy-suspension-structure =
    map-inv-equiv (extensionality-suspension-structure c c')

module _
  {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c : suspension-structure X Z}
  where

  refl-htpy-suspension-structure : htpy-suspension-structure c c
  pr1 refl-htpy-suspension-structure = refl
  pr1 (pr2 refl-htpy-suspension-structure) = refl
  pr2 (pr2 refl-htpy-suspension-structure) = right-unit-htpy

  is-refl-refl-htpy-suspension-structure :
    refl-htpy-suspension-structure  htpy-eq-suspension-structure refl
  is-refl-refl-htpy-suspension-structure = refl

  extensionality-suspension-structure-refl-htpy-suspension-structure :
    eq-htpy-suspension-structure refl-htpy-suspension-structure  refl
  extensionality-suspension-structure-refl-htpy-suspension-structure =
    is-injective-equiv
      ( extensionality-suspension-structure c c)
      ( is-section-map-inv-equiv
        ( extensionality-suspension-structure c c)
        ( refl-htpy-suspension-structure))

module _
  {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c : suspension-structure X Z}
  where

  ind-htpy-suspension-structure :
    { l : Level}
    ( P :
      (c' : suspension-structure X Z)  htpy-suspension-structure c c'  UU l) 
    ( P c refl-htpy-suspension-structure) 
    ( c' : suspension-structure X Z)
    ( H : htpy-suspension-structure c c') 
    P c' H
  ind-htpy-suspension-structure P =
    pr1
      ( is-identity-system-is-torsorial
        ( c)
        ( refl-htpy-suspension-structure)
        ( is-contr-equiv
          ( Σ (suspension-structure X Z)  c'  c  c'))
          ( inv-equiv
            ( equiv-tot (extensionality-suspension-structure c)))
          ( is-torsorial-Id c))
        ( P))
```

#### The action of paths of the projections have the expected effect

```agda
module _
  {l1 l2 : Level} {X : UU l1} {Z : UU l2} (c : suspension-structure X Z)
  where

  ap-pr1-eq-htpy-suspension-structure :
    (c' : suspension-structure X Z) (H : htpy-suspension-structure c c') 
    (ap (pr1) (eq-htpy-suspension-structure H))  (pr1 H)
  ap-pr1-eq-htpy-suspension-structure =
    ind-htpy-suspension-structure
      ( λ c' H  (ap (pr1) (eq-htpy-suspension-structure H))  (pr1 H))
      ( ap
        ( ap pr1)
        ( is-retraction-map-inv-equiv
          ( extensionality-suspension-structure c c)
          ( refl)))

  ap-pr1∘pr2-eq-htpy-suspension-structure :
    (c' : suspension-structure X Z) (H : htpy-suspension-structure c c') 
    (ap (pr1  pr2) (eq-htpy-suspension-structure H))  ((pr1  pr2) H)
  ap-pr1∘pr2-eq-htpy-suspension-structure =
    ind-htpy-suspension-structure
      ( λ c' H 
        ap (pr1  pr2) (eq-htpy-suspension-structure H)  (pr1  pr2) H)
      ( ap
        ( ap (pr1  pr2))
        ( is-retraction-map-inv-equiv
          ( extensionality-suspension-structure c c)
          ( refl)))
```

### Characterization of equalities in `htpy-suspension-structure`

```agda
module _
  {l1 l2 : Level} {X : UU l1} {Z : UU l2}
  {c c' : suspension-structure X Z}
  where

  htpy-in-htpy-suspension-structure :
    htpy-suspension-structure c c' 
    htpy-suspension-structure c c'  UU (l1  l2)
  htpy-in-htpy-suspension-structure (n , s , h) (n' , s' , h') =
    Σ ( n  n')
      ( λ p 
        Σ ( s  s')
          ( λ q 
            (x : X) 
            coherence-square-identifications
              ( h x)
              ( left-whisker-concat
                ( meridian-suspension-structure c x)
                ( q))
              ( right-whisker-concat
                ( p)
                ( meridian-suspension-structure c' x))
              ( h' x)))

  extensionality-htpy-suspension-structure :
    (h h' : htpy-suspension-structure c c') 
      (h  h')  htpy-in-htpy-suspension-structure h h'
  extensionality-htpy-suspension-structure (n , s , h) =
    extensionality-Σ
      ( λ y p 
        Σ ( s  pr1 y)
          ( λ q 
            (x : X) 
            coherence-square-identifications
              ( h x)
              ( left-whisker-concat
                ( meridian-suspension-structure c x)
                ( q))
              ( right-whisker-concat
                ( p)
                ( meridian-suspension-structure c' x))
              ( pr2 y x)))
      ( refl)
      ( refl , inv-htpy right-unit-htpy)
      ( λ n'  id-equiv)
      ( extensionality-Σ
        ( λ h' q 
          (x : X) 
          coherence-square-identifications
            ( h x)
            ( left-whisker-concat (meridian-suspension-structure c x) q)
            ( right-whisker-concat
              ( refl)
              ( meridian-suspension-structure c' x))
            ( h' x))
        ( refl)
        ( inv-htpy right-unit-htpy)
        ( λ q  id-equiv)
        ( λ h' 
          ( inv-equiv (equiv-concat-htpy' h' (right-unit-htpy))) ∘e
          ( equiv-inv-htpy h h') ∘e
          ( equiv-funext {f = h} {g = h'})))

  north-htpy-in-htpy-suspension-structure :
    {h h' : htpy-suspension-structure c c'} 
    htpy-in-htpy-suspension-structure h h' 
    ( north-htpy-suspension-structure h) 
    ( north-htpy-suspension-structure h')
  north-htpy-in-htpy-suspension-structure = pr1

  south-htpy-in-htpy-suspension-structure :
    {h h' : htpy-suspension-structure c c'} 
    htpy-in-htpy-suspension-structure h h' 
    ( south-htpy-suspension-structure h) 
    ( south-htpy-suspension-structure h')
  south-htpy-in-htpy-suspension-structure = pr1  pr2

  meridian-htpy-in-htpy-suspension-structure :
    {h h' : htpy-suspension-structure c c'} 
    (H : htpy-in-htpy-suspension-structure h h') 
    (x : X) 
      coherence-square-identifications
        ( meridian-htpy-suspension-structure h x)
        ( left-whisker-concat
          ( meridian-suspension-structure c x)
          ( south-htpy-in-htpy-suspension-structure H))
        ( right-whisker-concat
          ( north-htpy-in-htpy-suspension-structure H)
          ( meridian-suspension-structure c' x))
        ( meridian-htpy-suspension-structure h' x)
  meridian-htpy-in-htpy-suspension-structure = pr2  pr2

module _
  {l1 l2 : Level} {X : UU l1} {Z : UU l2}
  {c c' : suspension-structure X Z} {h h' : htpy-suspension-structure c c'}
  where

  htpy-eq-htpy-suspension-structure :
    h  h'  htpy-in-htpy-suspension-structure h h'
  htpy-eq-htpy-suspension-structure =
    map-equiv (extensionality-htpy-suspension-structure h h')

  eq-htpy-in-htpy-suspension-structure :
    htpy-in-htpy-suspension-structure h h'  h  h'
  eq-htpy-in-htpy-suspension-structure =
    map-inv-equiv (extensionality-htpy-suspension-structure h h')
```