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 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 = n-Tr-elim (Ξ» _ β 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 n-Tr.inc (merid x)) Ξ» pt β commutesβsquare (ap (refl β_) (remβ .snd _ β sym (remβ .snd _)))))) (conn' .centre) where 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-Tr.inc {n = 3 + n} N β‘ inc S} {A = A} (suc n) (hlevel (2 + 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 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)

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 suspensions1, 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 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.

  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 Its values are either for equal poles or 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 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.

    _ = 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 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 _ _)

opaque
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 β©οΈ