open import 1Lab.Path.Cartesian
open import 1Lab.Prelude

open import Data.Set.Truncation

open import Homotopy.Connectedness.Automation
open import Homotopy.Space.Suspension
open import Homotopy.Connectedness
open import Homotopy.Space.Sphere
open import Homotopy.Truncation
open import Homotopy.Base

module Homotopy.Space.Suspension.Properties where

Properties of suspensions🔗

Connectedness🔗

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

Susp-is-connected
  : ∀ {ℓ} {A : Type ℓ} n
  → is-n-connected A n → is-n-connected (Susp A) (suc n)
Susp-is-connected  a-conn = inc N
Susp-is-connected  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 =
  n-Tr-elim
    (λ _ → is-n-connected (Susp A) ( + n))
    (λ _ → is-prop→is-hlevel-suc {n = suc n} (hlevel ))
    (λ x → contr (inc N) (n-Tr-elim _ (λ _ → is-hlevel-suc ( + n) (n-Tr-is-hlevel ( + n) _ _))
      (Susp-elim _ refl (ap n-Tr.inc (merid x)) λ pt →
        commutes→square (ap (refl ∙_) (rem₂ .snd _ ∙ sym (rem₂ .snd _))))))
    (conn' .centre)
  where
    conn' : is-contr (n-Tr A ( + n))
    conn' = is-n-connected-Tr ( + n) a-conn

    rem₁ : is-equiv λ b a → b
    rem₁ = is-n-connected→n-type-const
      {B = n-Tr.inc {n =  + n} N ≡ inc S} {A = A}
      (suc n) (hlevel ( + n)) a-conn

    rem₂ : Σ (inc N ≡ inc S) (λ p → ∀ x → ap n-Tr.inc (merid x) ≡ p)
    rem₂ = _ , λ x → sym (rem₁ .is-eqv _ .centre .snd) $ₚ x

As a direct corollary, the $n\text{-sphere}$ is $(n-1)\text{-connected}$ (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)

instance
  Connected-Susp : ∀ {ℓ} {A : Type ℓ} {n} → ⦃ Connected A n ⦄ → Connected (Susp A) (suc n)
  Connected-Susp {n = n} ⦃ conn-instance c ⦄ = conn-instance (Susp-is-connected n c)

Truncatedness🔗

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

First, the suspension of a contractible type is contractible.

Susp-is-contr
  : ∀ {ℓ} {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 $\infty \text{-sphere}$ is contractible: that argument is essentially a recursive version of this one, since $S^{\infty }$ 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 $\perp \text{),}$ 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 $\Sigma A\times \Sigma A\text{,}$ it suffices to give values at the four poles, and, assuming $A$ holds, a square over the meridians with the given corners.

  Susp-prop-elim²
    : ∀ {ℓ} {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 $\Sigma A\text{.}$ Its values are either $\top$ for equal poles or $A$ for different poles, and we fill the square using univalence.

  private
    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)
      where
        A≡⊤ : A → A ≡ Lift _ ⊤
        A≡⊤ a = ua (prop-ext prop (hlevel ) _ (λ _ → 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 )
      (Susp-elim-prop (λ _ → hlevel ) (hlevel ) prop)
      (Susp-elim-prop (λ _ → hlevel ) prop (hlevel ))

    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.

    _ = I-interp

    decode : ∀ a b → Code a b → a ≡ b
    decode = Susp-prop-elim²
      (λ _ → refl)          (λ c → merid c)
      (λ c → sym (merid c)) (λ _ → refl)

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

Notice that we have two different meridians: $a$ comes from our assumption that $A$ holds, whereas $c$ comes from the function out of codes we’re trying to build. If $a$ and $c$ were the same, we could simply fill this cube by interpolating between $i$ and $j$ along $k\text{.}$ However, we can take a shortcut: since we’ve assumed $A$ holds, and $A$ is a proposition, then $A$ 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  (λ _ → Path-is-hlevel 
          (Susp-is-contr (is-prop∙→is-contr prop a))))
        (∂ i ∧ ∂ j) _

This concludes the proof that $\Sigma A$ is a set with $(N\equiv S)\simeq A\text{.}$

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

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

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