Cubical.HITs.Susp.Base

module Cubical.HITs.Susp.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Pointed

open import Cubical.Data.Unit
open import Cubical.Data.Bool
open import Cubical.Data.Empty
open import Cubical.Data.Nat

open import Cubical.HITs.S1
open import Cubical.HITs.S2.Base
open import Cubical.HITs.S3

open Iso

private
  variable
    ℓ ℓ' : Level

data Susp (A : Type ℓ) : Type ℓ where
  north : Susp A
  south : Susp A
  merid : (a : A) → north ≡ south

Susp∙ : (A : Type ℓ) → Pointed ℓ
Susp∙ A = Susp A , north

-- induced function
suspFun : {A : Type ℓ} {B : Type ℓ'} (f : A → B)
       → Susp A → Susp B
suspFun f north = north
suspFun f south = south
suspFun f (merid a i) = merid (f a) i

-- pointed version
suspFun∙ : {A : Type ℓ} {B : Type ℓ'} (f : A → B)
       → Susp∙ A →∙ Susp∙ B
fst (suspFun∙ f) = suspFun f
snd (suspFun∙ f) = refl

suspFun↑ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → (b : B)
  → ((a : A) → Path B b b)
  → Susp A → B
suspFun↑ b f north = b
suspFun↑ b f south = b
suspFun↑ b f (merid a i) = f a i

-- Iterated suspensions
Susp^ : ℕ → Type ℓ → Type ℓ
Susp^ 0 X = X
Susp^ (suc n) X = Susp^ n (Susp X)

Susp^' : ℕ → Type ℓ → Type ℓ
Susp^' zero x = x
Susp^' (suc n) x = Susp (Susp^' n x)

Susp^'≡Susp^ : (n : ℕ) {A : Type ℓ} → Susp^' n A ≡ Susp^ n A
Susp^'≡Susp^ zero {A = A} = refl
Susp^'≡Susp^ (suc n) {A = A} = lem n ∙ Susp^'≡Susp^ n {A = Susp A}
  where
  lem : (n : ℕ) → Susp (Susp^' n A) ≡ Susp^' n (Susp A)
  lem zero = refl
  lem (suc n) = cong Susp (lem n)

UnitIsoSuspUnit : Iso Unit (Susp Unit)
fun UnitIsoSuspUnit _ = north
inv UnitIsoSuspUnit _ = tt
sec UnitIsoSuspUnit north = refl
sec UnitIsoSuspUnit south = merid tt
sec UnitIsoSuspUnit (merid tt j) k = merid tt (j ∧ k)
ret UnitIsoSuspUnit _ = refl

Unit≃SuspUnit : Unit ≃ Susp Unit
Unit≃SuspUnit = isoToEquiv UnitIsoSuspUnit

BoolIsoSusp⊥ : Iso Bool (Susp ⊥)
fun BoolIsoSusp⊥ = λ {true  → north; false → south}
inv BoolIsoSusp⊥ = λ {north → true;  south → false}
sec BoolIsoSusp⊥ = λ {north → refl;  south → refl}
ret BoolIsoSusp⊥  = λ {true  → refl;  false → refl}

Bool≃Susp⊥ : Bool ≃ Susp ⊥
Bool≃Susp⊥ = isoToEquiv BoolIsoSusp⊥

SuspBool : Type₀
SuspBool = Susp Bool

SuspBool→S¹ : SuspBool → S¹
SuspBool→S¹ north = base
SuspBool→S¹ south = base
SuspBool→S¹ (merid false i) = loop i
SuspBool→S¹ (merid true i)  = base

S¹→SuspBool : S¹ → SuspBool
S¹→SuspBool base     = north
S¹→SuspBool (loop i) = (merid false ∙ sym (merid true)) i

SuspBool→S¹→SuspBool : (x : SuspBool) → Path _ (S¹→SuspBool (SuspBool→S¹ x)) x
SuspBool→S¹→SuspBool north = refl
SuspBool→S¹→SuspBool south = merid true
SuspBool→S¹→SuspBool (merid false i) j = hcomp (λ k → (λ { (j = i1) → merid false i
                                                         ; (i = i0) → north
                                                         ; (i = i1) → merid true (j ∨ ~ k)}))
                                               (merid false i)
SuspBool→S¹→SuspBool (merid true i) j = merid true (i ∧ j)

S¹→SuspBool→S¹ : (x : S¹) → SuspBool→S¹ (S¹→SuspBool x) ≡ x
S¹→SuspBool→S¹ base       = refl
S¹→SuspBool→S¹ (loop i) j = hfill (λ k → λ { (i = i0) → base
                                           ; (i = i1) → base })
                                  (inS (loop i)) (~ j)

S¹IsoSuspBool : Iso S¹ SuspBool
fun S¹IsoSuspBool      = S¹→SuspBool
inv S¹IsoSuspBool      = SuspBool→S¹
sec S¹IsoSuspBool = SuspBool→S¹→SuspBool
ret S¹IsoSuspBool  = S¹→SuspBool→S¹

S¹≃SuspBool : S¹ ≃ SuspBool
S¹≃SuspBool = isoToEquiv S¹IsoSuspBool

S¹≡SuspBool : S¹ ≡ SuspBool
S¹≡SuspBool = ua S¹≃SuspBool

-- Now the sphere

SuspS¹ : Type₀
SuspS¹ = Susp S¹

SuspS¹→S² : SuspS¹ → S²
SuspS¹→S² north = base
SuspS¹→S² south = base
SuspS¹→S² (merid base i) = base
SuspS¹→S² (merid (loop j) i) = surf i j

meridian-contraction : I → I → I → SuspS¹
meridian-contraction i j l = hfill (λ k → λ { (i = i0) → north
                                            ; (i = i1) → merid base (~ k)
                                            ; (j = i0) → merid base (~ k ∧ i)
                                            ; (j = i1) → merid base (~ k ∧ i) })
                                   (inS (merid (loop j) i)) l

S²→SuspS¹ : S² → SuspS¹
S²→SuspS¹ base = north
S²→SuspS¹ (surf i j) = meridian-contraction i j i1

S²→SuspS¹→S² : ∀ x → SuspS¹→S² (S²→SuspS¹ x) ≡ x
S²→SuspS¹→S² base k = base
S²→SuspS¹→S² (surf i j) k = SuspS¹→S² (meridian-contraction i j (~ k))

SuspS¹→S²→SuspS¹ : ∀ x → S²→SuspS¹ (SuspS¹→S² x) ≡ x
SuspS¹→S²→SuspS¹ north k = north
SuspS¹→S²→SuspS¹ south k = merid base k
SuspS¹→S²→SuspS¹ (merid base j) k = merid base (k ∧ j)
SuspS¹→S²→SuspS¹ (merid (loop j) i) k = meridian-contraction i j (~ k)

S²IsoSuspS¹ : Iso S² SuspS¹
fun S²IsoSuspS¹      = S²→SuspS¹
inv S²IsoSuspS¹      = SuspS¹→S²
sec S²IsoSuspS¹ = SuspS¹→S²→SuspS¹
ret S²IsoSuspS¹  = S²→SuspS¹→S²

S²≃SuspS¹ : S² ≃ SuspS¹
S²≃SuspS¹ = isoToEquiv S²IsoSuspS¹

S²≡SuspS¹ : S² ≡ SuspS¹
S²≡SuspS¹ = ua S²≃SuspS¹

-- And the 3-sphere

SuspS² : Type₀
SuspS² = Susp S²

SuspS²→S³ : SuspS² → S³
SuspS²→S³ north = base
SuspS²→S³ south = base
SuspS²→S³ (merid base i) = base
SuspS²→S³ (merid (surf j k) i) = surf i j k

meridian-contraction-2 : I → I → I → I → SuspS²
meridian-contraction-2 i j k l = hfill (λ m → λ { (i = i0) → north
                                                ; (i = i1) → merid base (~ m)
                                                ; (j = i0) → merid base (~ m ∧ i)
                                                ; (j = i1) → merid base (~ m ∧ i)
                                                ; (k = i0) → merid base (~ m ∧ i)
                                                ; (k = i1) → merid base (~ m ∧ i) })
                                       (inS (merid (surf j k) i)) l

S³→SuspS² : S³ → SuspS²
S³→SuspS² base = north
S³→SuspS² (surf i j k) = meridian-contraction-2 i j k i1

S³→SuspS²→S³ : ∀ x → SuspS²→S³ (S³→SuspS² x) ≡ x
S³→SuspS²→S³ base l = base
S³→SuspS²→S³ (surf i j k) l = SuspS²→S³ (meridian-contraction-2 i j k (~ l))

SuspS²→S³→SuspS² : ∀ x → S³→SuspS² (SuspS²→S³ x) ≡ x
SuspS²→S³→SuspS² north l = north
SuspS²→S³→SuspS² south l = merid base l
SuspS²→S³→SuspS² (merid base j) l = merid base (l ∧ j)
SuspS²→S³→SuspS² (merid (surf j k) i) l = meridian-contraction-2 i j k (~ l)

S³IsoSuspS² : Iso S³ SuspS²
fun S³IsoSuspS²      = S³→SuspS²
inv S³IsoSuspS²      = SuspS²→S³
sec S³IsoSuspS² = SuspS²→S³→SuspS²
ret S³IsoSuspS²  = S³→SuspS²→S³

S³≃SuspS² : S³ ≃ SuspS²
S³≃SuspS² = isoToEquiv S³IsoSuspS²

S³≡SuspS² : S³ ≡ SuspS²
S³≡SuspS² = ua S³≃SuspS²

IsoType→IsoSusp : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Iso A B → Iso (Susp A) (Susp B)
fun (IsoType→IsoSusp is) north = north
fun (IsoType→IsoSusp is) south = south
fun (IsoType→IsoSusp is) (merid a i) = merid (fun is a) i
inv (IsoType→IsoSusp is) north = north
inv (IsoType→IsoSusp is) south = south
inv (IsoType→IsoSusp is) (merid a i) = merid (inv is a) i
sec (IsoType→IsoSusp is) north = refl
sec (IsoType→IsoSusp is) south = refl
sec (IsoType→IsoSusp is) (merid a i) j = merid (sec is a j) i
ret (IsoType→IsoSusp is) north = refl
ret (IsoType→IsoSusp is) south = refl
ret (IsoType→IsoSusp is) (merid a i) j = merid (ret is a j) i

IsoSuspS²SuspSuspS¹ : Iso (Susp S²) (Susp (Susp S¹))
IsoSuspS²SuspSuspS¹ = IsoType→IsoSusp S²IsoSuspS¹

IsoS³S3 : Iso S³ (Susp (Susp S¹))
IsoS³S3 = compIso S³IsoSuspS² IsoSuspS²SuspSuspS¹