module Homotopy.Space.Sinfty where
The infinite sphere🔗
The can be constructed from the 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
data S∞ : Type where N S : S∞ merid : S∞ → N ≡ S
In classical topology, there are several definitions of the
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∞