open import 1Lab.Path.Groupoid
open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.HIT.Sinfty where


# The Infinite SphereðŸ”—

The $(n+1)$-sphere can be constructed from the $n$-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 $\infty$-sphere.

data Sâˆž : Type where
N S   : Sâˆž
merid : Sâˆž â†’ N â‰¡ S


In classical topology, there are several definitions of the $\infty$-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                        â‰¡âŸ¨ âˆ™-id-l (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 defenition 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 easilly 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
(Î» k â†’ Î» { (i = i0) â†’ N
; (i = i1) â†’ merid N j
; (j = i0) â†’ N
; (j = i1) â†’ merid (pathsSâˆž x k) i})
(merid N (i âˆ§ j))

is-contrSâˆž : is-contr Sâˆž
is-contrSâˆž .centre = N
is-contrSâˆž .paths = pathsSâˆž