module Homotopy.Space.Suspension.Properties where

Properties of suspensionsπŸ”—


This section contains the aforementioned proof that suspension increases the connectedness of a space.

  : βˆ€ {β„“} {A : Type β„“} n
  β†’ is-n-connected A n β†’ is-n-connected (Susp A) (suc n)
Susp-is-connected 0 a-conn = inc N
Susp-is-connected 1 a-conn = βˆ₯-βˆ₯-out! do
  pt ← a-conn
  pure $ is-connectedβˆ™β†’is-connected Ξ» where
    N           β†’ inc refl
    S           β†’ inc (sym (merid pt))
    (merid x i) β†’ is-propβ†’pathp (Ξ» i β†’ βˆ₯_βˆ₯.squash {A = merid x i ≑ N})
      (inc refl) (inc (sym (merid pt))) i
Susp-is-connected {A = A} (suc (suc n)) a-conn =
    (Ξ» _ β†’ is-n-connected (Susp A) (3 + n))
    (λ _ → is-prop→is-hlevel-suc {n = suc n} (hlevel 1))
    (Ξ» x β†’ contr (inc N) (n-Tr-elim _ (Ξ» _ β†’ is-hlevel-suc (2 + n) (n-Tr-is-hlevel (2 + n) _ _))
      (Susp-elim _ refl (ap (merid x)) Ξ» pt β†’
        commutesβ†’square (ap (refl βˆ™_) (remβ‚‚ .snd _ βˆ™ sym (remβ‚‚ .snd _))))))
    (conn' .centre)
    conn' : is-contr (n-Tr A (2 + n))
    conn' = is-n-connected-Tr (1 + n) a-conn

    rem₁ : is-equiv Ξ» b a β†’ b
    rem₁ = is-n-connectedβ†’n-type-const
      {B = {n = 3 + n} N ≑ inc S} {A = A}
      (suc n) (hlevel (2 + n)) a-conn

    remβ‚‚ : Ξ£ (inc N ≑ inc S) (Ξ» p β†’ βˆ€ x β†’ ap (merid x) ≑ p)
    remβ‚‚ = _ , Ξ» x β†’ sym (rem₁ .is-eqv _ .centre .snd) $β‚š x

As a direct corollary, the is (remember that our indices are offset by 2).

Sⁿ⁻¹-is-connected : βˆ€ n β†’ is-n-connected (Sⁿ⁻¹ n) n
Sⁿ⁻¹-is-connected zero = _
Sⁿ⁻¹-is-connected (suc n) = Susp-is-connected n (Sⁿ⁻¹-is-connected n)


While there is no similarly pleasant characterisation of the truncatedness of suspensions1, we can give a few special cases.

First, the suspension of a contractible type is contractible.

  : βˆ€ {β„“} {A : Type β„“}
  β†’ is-contr A β†’ is-contr (Susp A)
Susp-is-contr c .centre = N
Susp-is-contr c .paths N = refl
Susp-is-contr c .paths S = merid (c .centre)
Susp-is-contr c .paths (merid a i) j = hcomp (βˆ‚ i ∨ βˆ‚ j) Ξ» where
  k (k = i0) β†’ merid (c .centre) (i ∧ j)
  k (i = i0) β†’ N
  k (j = i0) β†’ N
  k (i = i1) β†’ merid (c .centre) j
  k (j = i1) β†’ merid (c .paths a k) i

Notice the similarity with the proof that the is contractible: that argument is essentially a recursive version of this one, since is its own suspension.

Going up a level, we do not have that the suspension of a proposition is a proposition (think of the suspension of but we do have that the suspension of a proposition is a set.

module _ {β„“} {A : Type β„“} (prop : is-prop A) where

We start by defining a helper induction principle: in order to map out of it suffices to give values at the four poles, and, assuming holds, a square over the meridians with the given corners.

    : βˆ€ {β„“} {B : Susp A β†’ Susp A β†’ Type β„“}
    β†’ (bnn : B N N) (bns : B N S)
    β†’ (bsn : B S N) (bss : B S S)
    β†’ ((a : A) β†’ (i j : I) β†’ B (merid a i) (merid a j)
        [ _ ↦ (Ξ» { (i = i0) (j = i0) β†’ bnn
                 ; (i = i0) (j = i1) β†’ bns
                 ; (i = i1) (j = i0) β†’ bsn
                 ; (i = i1) (j = i1) β†’ bss }) ])
    β†’ βˆ€ a b β†’ B a b
  Susp-prop-elimΒ² bnn bns bsn bss bm = Susp-elim _
    (Susp-elim _ bnn bns Ξ» a j β†’ outS (bm a i0 j))
    (Susp-elim _ bsn bss Ξ» a j β†’ outS (bm a i1 j))
    Ξ» a β†’ funextP (Susp-elim _
      (Ξ» i β†’ outS (bm a i i0))
      (Ξ» i β†’ outS (bm a i i1))
      (subst-prop prop a (Ξ» j i β†’ outS (bm a i j))))

Then, we use the usual machinery of identity systems: we define a type family of β€œcodes” of equality for Its values are either for equal poles or for different poles, and we fill the square using univalence.

    Code : Susp A β†’ Susp A β†’ Type β„“
    Code = Susp-prop-elim² (Lift _ ⊀) A A (Lift _ ⊀)
      Ξ» a i j β†’ inS (double-connection (sym (Aβ‰‘βŠ€ a)) (Aβ‰‘βŠ€ a) i j)
        Aβ‰‘βŠ€ : A β†’ A ≑ Lift _ ⊀
        Aβ‰‘βŠ€ a = ua (prop-ext prop (hlevel 1) _ (Ξ» _ β†’ a))

We’ve defined a reflexive family of propositions:

    Code-is-prop : βˆ€ a b β†’ is-prop (Code a b)
    Code-is-prop = Susp-elim-prop (Ξ» _ β†’ hlevel 1)
      (Susp-elim-prop (Ξ» _ β†’ hlevel 1) (hlevel 1) prop)
      (Susp-elim-prop (Ξ» _ β†’ hlevel 1) prop (hlevel 1))

    Code-refl : βˆ€ a β†’ Code a a
    Code-refl = Susp-elim-prop (Ξ» a β†’ Code-is-prop a a) _ _

Thus all that remains is to prove that it implies equality. At the poles, we can use refl and merid.

    decode : βˆ€ a b β†’ Code a b β†’ a ≑ b
    decode = Susp-prop-elimΒ²
      (Ξ» _ β†’ refl)          (Ξ» c β†’ merid c)
      (Ξ» c β†’ sym (merid c)) (Ξ» _ β†’ refl)

This time, if holds, we have to fill a cube with the given four edges:

Notice that we have two different meridians: comes from our assumption that holds, whereas comes from the function out of codes we’re trying to build. If and were the same, we could simply fill this cube by interpolating between and along However, we can take a shortcut: since we’ve assumed holds, and is a proposition, then is contractible, and we’ve shown that the suspension of a contractible type is contractible, so we can trivially extend our partial system to fill the desired cube!

      λ a i j → is-contr→extend
        (Ξ -is-hlevel 0 (Ξ» _ β†’ Path-is-hlevel 0
          (Susp-is-contr (is-propβˆ™β†’is-contr prop a))))
        (βˆ‚ i ∧ βˆ‚ j) _

This concludes the proof that is a set with

    Code-ids : is-identity-system Code Code-refl
    Code-ids = set-identity-system Code-is-prop (decode _ _)

    Susp-prop-is-set : is-set (Susp A)
    Susp-prop-is-set = identity-system→hlevel 1 Code-ids Code-is-prop

  Susp-prop-path : Path (Susp A) N S ≃ A
  Susp-prop-path = identity-system-gives-path Code-ids e⁻¹

  1. for instance, while the circle is a groupoid, its suspension, the 2-sphere, is not for any β†©οΈŽ