module Homotopy.Space.Sphere where

The -1 and 0 spheres🔗

In classical topology, the topological space is typically defined as the subspace of consisting of all points at unit distance from the origin. We see from this definition that the is the discrete two point space and that the sphere is the empty subspace 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


The spheres of higher dimension can be defined inductively: that is, suspending the constructs the

The spheres are essentially indexed by the natural numbers, except that we want to start at instead of To remind ourselves of this, we name our spheres with a superscript

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 :

SuspS⁰≡S¹ : Sⁿ⁻¹ 2  
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 we have a single point constructor and a loop. Geometrically, we can picture morphing Sⁿ⁻¹ 2 into 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  
  SuspS⁰→S¹ N = base
  SuspS⁰→S¹ S = base
  SuspS⁰→S¹ (merid N i) = base
  SuspS⁰→S¹ (merid S i) = loop i

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ⁿ⁻¹ 2
  S¹→SuspS⁰ base = N
  S¹→SuspS⁰ (loop i) = (merid S  sym (merid N)) 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 S  sym (merid N)) ≡⟨ ap-∙ SuspS⁰→S¹ (merid S) (sym (merid N))
      loop  refl                             ≡⟨ ∙-idr _ 
      loop                                    )
  iso-pf .linv N = refl
  iso-pf .linv S = merid N
  iso-pf .linv (merid N i) j = merid N (i  j)
  iso-pf .linv (merid S i) j = hcomp ( i   j) λ where
    k (k = i0)  merid S i
    k (i = i0)  N
    k (i = i1)  merid N (j  ~ k)
    k (j = i0)  ∙-filler (merid S) (sym (merid N)) k i
    k (j = i1)  merid S i