open import 1Lab.Prelude

module Homotopy.Space.Sinfty where

The infinite sphere🔗

The $(n+1)\text{-sphere}$ can be constructed from the $n\text{-sphere}$ via suspension. By writing a recursive HIT, we can define a type which is its own suspension. It stands to reason that this definition is a good candidate for being considered the infinitary limit of the process of iterated suspension and is thus referred to as the $\infty \text{-sphere.}$

data S∞ : Type where
  N S   : S∞
  merid : S∞ → N ≡ S

In classical topology, there are several definitions of the $\infty \text{-sphere.}$ However, independently of the approach taken, the resulting space is always contractible. In Homotopy Type Theory, then, the only meaningful statement that can be made of S∞ is that it is contractible. We prove this in two different ways.

The Book HoTT approach🔗

open is-contr

private
  pathsS∞' : (x : S∞) → N ≡ x
  pathsS∞' N = refl
  pathsS∞' S = merid N
  pathsS∞' (merid x i) =

First we reduce the problem from constructing a dependent path over (λ i → N ≡ merid x i) from refl to merid N to the problem of constructing a path in N ≡ S from transport (λ j → N ≡ merid x j) refl to merid N.

    to-pathp {A = λ j → N ≡ merid x j}

The proof goes as follows: by the characterisation of transport in path types the LHS is identified with refl ∙ merid x. We get rid of the refl and then a a path between merid x and merid N can be obtained from applying merid to the recursive call pathsS∞' x.

      (transport (λ j → N ≡ merid x j) refl ≡⟨ subst-path-right refl (merid x) ⟩≡
      refl ∙ merid x                        ≡⟨ ∙-idl (merid x) ⟩≡
      merid x                               ≡⟨ ap merid (sym (pathsS∞' x)) ⟩≡
      merid N                               ∎) i

is-contrS∞' : is-contr S∞
is-contrS∞' .centre = N
is-contrS∞' .paths = pathsS∞'

The cubical approach🔗

The cubical approach essentially accomplishes the same thing as the previous proof, without using any helper lemmas, by way of drawing a slightly clever cube. The case of the definition for the higher constructor requires a square in which two of the sides are merid N and merid x. We start with a square in which both of these sides are merid N (specifically merid N (i ∧ j)), and then construct a cube in which one of the faces morphs merid N into merid x. This is something that we can easily do since we have a path N ≡ x via the recursive call pathsS∞ x.

private
  pathsS∞ : (x : S∞) → N ≡ x
  pathsS∞ N = refl
  pathsS∞ S = merid N
  pathsS∞ (merid x i) j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → merid N (i ∧ j)
    k (i = i0) → N
    k (j = i0) → N
    k (i = i1) → merid N j
    k (j = i1) → merid (pathsS∞ x k) i

is-contrS∞ : is-contr S∞
is-contrS∞ .centre = N
is-contrS∞ .paths = pathsS∞