open import 1Lab.HIT.Suspension open import 1Lab.Path.Groupoid open import 1Lab.Univalence open import 1Lab.HIT.S1 open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type module 1Lab.HIT.Sphere where

# The -1 and 0 Spheresš

In classical topology, the *topological space* $S^n$ is typically defined as the subspace of $\bb{R}^{n+1}$ consisting of all points at unit distance from the origin. We see from this definition that the $0$-sphere is the discrete two point space $\{-1, 1\} \subset \bb{R}$, and that the $-1$ sphere is the empty subspace $\varnothing \subset \{0\}$. We will recycle existing types and define:

Sā»Ā¹ : Type Sā»Ā¹ = ā„ Sā° : Type Sā° = Bool

We note that `Sā°`

may be identified with `Susp Sā»Ā¹`

. Since the pattern matching checker can prove that `merid x i`

is impossible when `x : ā„`

, the case for this constructor does not need to be written, this makes the proof look rather tautologous.

open is-iso SuspSā»Ā¹āSā° : Susp Sā»Ā¹ ā” Sā° SuspSā»Ā¹āSā° = ua (SuspSā»Ā¹āSā° , is-isoāis-equiv iso-pf) where SuspSā»Ā¹āSā° : Susp Sā»Ā¹ ā Sā° SuspSā»Ā¹āSā° N = true SuspSā»Ā¹āSā° S = false Sā°āSuspSā»Ā¹ : Sā° ā Susp Sā»Ā¹ Sā°āSuspSā»Ā¹ true = N Sā°āSuspSā»Ā¹ false = S iso-pf : is-iso SuspSā»Ā¹āSā° iso-pf .inv = Sā°āSuspSā»Ā¹ iso-pf .rinv false = refl iso-pf .rinv true = refl iso-pf .linv N = refl iso-pf .linv S = refl

# n-Spheresš

The spheres of higher dimension can be defined inductively: $S^{n + 1} = \Sigma S^n$, that is, suspending the $n$-sphere constructs the $n+1$-sphere.

The spheres are essentially indexed by the natural numbers, except that we want to start at $-1$ instead of $0$. To remind ourselves of this, we name our spheres with a superscript $^{n-1}$:

Sāæā»Ā¹ : Nat ā Type Sāæā»Ā¹ zero = Sā»Ā¹ Sāæā»Ā¹ (suc n) = Susp (Sāæā»Ā¹ n)

A slightly less trivial example of definitions lining up is the verification that `Sāæā»Ā¹ 2`

is equivalent to our previous definition of `SĀ¹`

:

SuspSā°āSĀ¹ : Sāæā»Ā¹ 2 ā” SĀ¹ SuspSā°āSĀ¹ = ua (SuspSā°āSĀ¹ , is-isoāis-equiv iso-pf) where

In `Sāæā»Ā¹ 2`

, we have two point constructors joined by two paths, while in `SĀ¹`

we have a single point constructor and a loop. Geometrically, we can picture a morphing `Sāæā»Ā¹ 2`

into `SĀ¹`

by squashing one of the meridians down to a point, thus bringing `N`

and `S`

together. This intuition leads to a definition:

SuspSā°āSĀ¹ : Sāæā»Ā¹ 2 ā SĀ¹ SuspSā°āSĀ¹ N = base SuspSā°āSĀ¹ S = base SuspSā°āSĀ¹ (merid N i) = loop i SuspSā°āSĀ¹ (merid S i) = base

In the other direction, we send `base`

to `N`

, and then need to send `loop`

to some path `N ā” N`

. Since this map should define an equivalence, we make it such that loop wraps around the space `Sāæ 2`

by way of traversing both meridians.

SĀ¹āSuspSā° : SĀ¹ ā Sāæā»Ā¹ 2 SĀ¹āSuspSā° base = N SĀ¹āSuspSā° (loop i) = (merid N ā sym (merid S)) i

##
We then verify that these maps are inverse equivalences. One of the steps involves a slightly tricky `hcomp`

, although this can be avoided by working with transports instead of dependent paths, and then by using lemmas on transport in pathspaces.

iso-pf : is-iso SuspSā°āSĀ¹ iso-pf .inv = SĀ¹āSuspSā° iso-pf .rinv base = refl iso-pf .rinv (loop i) = ap (Ī» p ā p i) (ap SuspSā°āSĀ¹ (merid N ā sym (merid S)) ā”āØ ap-comp-path SuspSā°āSĀ¹ (merid N) (sym (merid S))ā©ā” loop ā refl ā”āØ ā-id-r loop ā©ā” loop ā) iso-pf .linv N = refl iso-pf .linv S = merid S iso-pf .linv (merid N i) j = hcomp (Ī» k ā Ī» { (i = i0) ā N ; (i = i1) ā merid S (j āØ ~ k) ; (j = i0) ā ā-filler (merid N) (sym (merid S)) k i ; (j = i1) ā merid N i}) (merid N i) iso-pf .linv (merid S i) j = merid S (i ā§ j)