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âˆž