module Homotopy.Space.Sinfty where
The Infinite Sphere🔗
The -sphere can be constructed from the -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 conisdered the infinitary limit of the process of iterated suspension and is thus referred to as the -sphere.
data S∞ : Type where N S : S∞ merid : S∞ → N ≡ S
In classical topology, there are several definitions of the
-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 acomplishes 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∞