open import 1Lab.Path.Reasoning
open import 1Lab.Prelude

open import Data.Nat.Properties
open import Data.Nat.Base

open import Homotopy.Space.Suspension.Properties
open import Homotopy.Space.Suspension
open import Homotopy.Connectedness
open import Homotopy.Truncation
open import Homotopy.Loopspace
open import Homotopy.Wedge

module Homotopy.Space.Suspension.Freudenthal where

Freudenthal suspension theorem🔗

The merid constructor of the suspension $\Sigma A$ generates a path between the north and south poles, rather than a loop on either pole. If $A$ is pointed¹, then we can “correct” the meridian generated by an element $x:A$ by composing with the inverse of the meridian at the basepoint, to properly get an element in the loop space $\Omega \Sigma A\text{.}$ Moreover, since $\mathrm{merid}{a}_0\cdot \mathrm{merid}{a_0}^{-1}$ is $\mathrm{refl}\text{,}$ this is a pointed map which we will call $\sigma :A{\to }_{\ast }\Omega \Sigma A\text{.}$ If we’re considering $A$ based at some other point $x:A\text{,}$ we will write ${\sigma }_x$ to indicate this.

suspend∙ : ∀ {ℓ} (A : Type∙ ℓ) → A →∙ Ω¹ (Σ¹ A)
suspend∙ (_ , a₀) .fst x = merid x ∙ sym (merid a₀)
suspend∙ (_ , a₀) .snd   = ∙-invr (merid a₀)

suspend : ∀ {ℓ} (A : Type∙ ℓ) → ⌞ A ⌟ → Path ⌞ Σ¹ A ⌟ north north
suspend A∙ x = suspend∙ A∙ .fst x

The Freudenthal suspension theorem gives a bound on the failure of this map to be an isomorphism. Precisely, it says that if $A$ is $n\text{-}$connected with $n\ge 2$ then the suspension map $\sigma :A\to \Omega \Sigma A$ is $2(n-1)\text{-connected.}$ As a corollary, it induces an equivalence of $2(n-1)\text{-}$truncations $$\Vert A{\Vert }_{2(n-1)}\simeq \Vert \Omega \Sigma A{\Vert }_{2(n-1)}\text{.}$$

-- this line is unfortunately long but layout stacking doesn't work
-- unless it's all together like this :(
module freudenthal {ℓ} (A∙@(A , a₀) : Type∙ ℓ) (n : Nat) (conn : is-n-connected A ( + n)) (let 2n = (suc n) + (suc n)) where
  ∥_∥₂ₙ : ∀ {ℓ} → Type ℓ → Type ℓ
  ∥ A ∥₂ₙ = n-Tr A 2n

The proof we present is natively cubical, but the outline is the same as the HoTT book proof (2013, sec. 8.6): we will define a family code over a point $x:\Sigma A$ and path $p:x\equiv \mathrm{north}\text{,}$ satisfying $$\begin{array}{rl}\mathrm{code}(\mathrm{north},p)& =\Vert {\sigma }^{\ast }(p){\Vert }_{2(n-1)}\\ \mathrm{code}(\mathrm{south},p)& =\Vert {\mathrm{merid}}^{\ast }(p){\Vert }_{2(n-1)}\text{,}\end{array}$$ and then show that $\mathrm{code}(\mathrm{south},p)$ is contractible at each $p\text{.}$ We will start by giving a family of equivalences $i_a\text{,}$ over $a:A\text{,}$ between the truncated fibres $\Vert {\sigma }^{\ast }(p){\Vert }_{2(n-1)}$ and $\Vert {\sigma }_a^{\ast }(p){\Vert }_{2(n-1)}$ over some $p:\mathrm{north}\equiv \mathrm{north}\text{.}$ We start by constructing such a fibre under the assumptions that $a,b:A$ and $q:\sigma (b)=p\text{.}$ By the wedge connectivity lemma, it will suffice to do so when $a=a_0$ and $b=a_0\text{,}$ as long as our constructions agree when $a=a_0=b\text{.}$ When $b=a_0\text{,}$ we can show $${\sigma }_a(a)=\mathrm{merid}a\cdot (\mathrm{merid}a{)}^{-1}=\mathrm{refl}=\mathrm{merid}{a}_0\cdot (\mathrm{merid}{a}_0{)}^{-1}=p\text{,}$$ with the final step by our assumption of $q\text{;}$ and when $a=a_0$ we are immediately done. To show that these agree, we simply have to prove that the round-trip between $\mathrm{refl}$ is the identity when $a=a_0\text{,}$ but we can easily arrange for those steps to cancel in this case.

  module wc (p : north ≡ north) =
    Wedge {A∙ = A∙} {A∙} {λ a b → suspend A∙ b ≡ p → ∥ fibre (suspend (A , a)) p ∥₂ₙ}
      n n conn conn (λ x y → hlevel 2n)
      (λ a q → inc (a , ∙-invr (merid a) ∙ sym (∙-invr (merid a₀)) ∙ q))
      (λ a q → inc (a , q))
      (funext λ x → ap (λ e → n-Tr.inc {n = 2n} (a₀ , e))
        (∙-cancell (sym (∙-invr (merid a₀))) x))

By truncation recursion, we can extend this to the function $i_a$ between fibres we promised. Since being an equivalence is a proposition and $A$ is $(2+n)\text{-connected,}$ it will suffice to show that $i_{a_0}$ is an equivalence; but in this case $i$ is the identity, so we are done.

  fwd : ∀ p a → ∥ fibre (suspend A∙) p ∥₂ₙ → ∥ fibre (suspend (A , a)) p ∥₂ₙ
  fwd = elim! wc.elim

  fwd-is-equiv : ∀ p a → is-equiv (fwd p a)

  fwd-is-equiv p a .is-eqv =
    let
      eqv = relative-n-type-const
        (λ a → ∀ t → is-contr (fibre (fwd p a) t))
        (λ _ → a₀) (suc n) (point-is-n-connected a₀ n conn)
        (λ x → hlevel (suc n))

      it : ∀ a (t : n-Tr (fibre (suspend A∙) p) 2n)
          → is-contr (fibre (fwd p a₀) t)
      it = elim! λ _ x q →
        subst (λ e → is-contr (fibre e (inc (x , q)))) {x = id} {y = _}
          (funext (elim! λ x → sym ∘ happly (wc.β₂ p x)))
          Singleton'-is-contr
    in Equiv.from (_ , eqv) it a

We can then use this equivalence to define the code family. Here is when cubical type theory allows a significant simplification over book HoTT: we can directly glue our equivalence along a dependent identification interpolate between suspend and merid, as in the diagram below (where we write $i$ for inv and $\phi$ for interpolate).

Constructing this dependent identification is very easy, and so everything falls together as usual.

  interpolate
    : ∀ {ℓ} {A : Type ℓ} (a : A)
    → PathP (λ i → A → north ≡ merid a i) (suspend (A , a)) merid
  interpolate a i x j = ∙-filler (merid x) (sym (merid a)) (~ i) j

  code : (y : Susp A) → north ≡ y → Type ℓ
  code north p = ∥ fibre (suspend A∙) p ∥₂ₙ
  code south p = ∥ fibre merid p        ∥₂ₙ
  code (merid a i) p = Glue ∥ fibre (interpolate a i) p ∥₂ₙ λ where
    (i = i0) → ∥ fibre (suspend A∙) p ∥₂ₙ , fwd p a , fwd-is-equiv p a
    (i = i1) → ∥ fibre merid p        ∥₂ₙ , id≃

By path induction, each $\mathrm{code}(y,p)$ is inhabited. We will now show that each $\mathrm{code}(\mathrm{south},p)$ is contractible, with centre the encoding of $p\text{.}$ By truncation induction we can assume we have $a:A$ and $r:\mathrm{merid}a=p\text{,}$ and by path induction on $r$ we can assume $p$ is $\mathrm{merid}a\text{,}$ so that our goal is showing $\mathrm{encode}(\mathrm{south},\mathrm{merid}a)$ is $(a,\mathrm{refl})\text{.}$ This is a simple, if tedious, calculation.

  encode : (y : Susp A) (p : north ≡ y) → code y p
  encode y = J code (inc (a₀ , ∙-invr (merid a₀)))

  encode-paths : ∀ p (c : ∥ fibre merid p ∥₂ₙ) → encode south p ≡ c
  encode-paths p = elim! λ a → J (λ p r → encode south p ≡ inc (a , r))
    let
      gp i = n-Tr (fibre (interpolate a i) (λ j → merid a (i ∧ j))) 2n

      rem₁ =
        wc.elim refl a a₀ (∙-invr (merid a₀))
          ≡⟨ happly (wc.β₁ refl a) (∙-invr (merid a₀)) ⟩≡
        inc (a , ∙-invr (merid a) ∙ sym (∙-invr (merid a₀)) ∙ ∙-invr (merid a₀))
          ≡⟨ ap (λ e → n-Tr.inc (a , e)) (∙-elimr (∙-invl (∙-invr (merid a₀)))) ⟩≡
        inc (a , ∙-invr (merid a))
          ∎

      rem₂ =
        transport gp (fwd refl a (inc (a₀ , ∙-invr (merid a₀))))
          ≡⟨ ap (transport gp) rem₁ ⟩≡
        transport gp (inc (a , ∙-invr (merid a)))
          ≡⟨ from-pathp {A = λ i → gp i} (λ i → inc (a , λ j k → ∙-invr-filler (merid a) j k (~ i))) ⟩≡
        inc (a , refl) ∎
    in rem₂

By definition, this proof shows that $\mathrm{merid}$ is an $2(n-1)$ connected map, because the $2(n-1)\text{-truncations}$ of its fibres are contractible. We have also essentially already shown our main theorem, since we have an identification between the fibres of merid and those of suspend.

  merid-is-n-connected : is-n-connected-map merid 2n
  merid-is-n-connected x = n-connected.from (n + suc n) record
    { centre = encode south x
    ; paths  = encode-paths x
    }

module
  _ {ℓ} {A∙@(A , a₀) : Type∙ ℓ} (n : Nat) (conn : is-n-connected A ( + n)) where

  open freudenthal A∙ n conn

  suspend-is-n-connected : is-n-connected-map (suspend A∙) (suc n + suc n)
  suspend-is-n-connected = transport
    (λ i → is-n-connected-map (λ z → interpolate a₀ (~ i) z) (suc n + suc n))
    merid-is-n-connected

  freudenthal-equivalence
    : n-Tr∙ A∙ (suc n + suc n) ≃∙ n-Tr∙ (Ωⁿ  (Σ¹ A∙)) (suc n + suc n)
  freudenthal-equivalence .fst .fst = _
  freudenthal-equivalence .fst .snd = is-n-connected-map→is-equiv-tr
    _ _ suspend-is-n-connected
  freudenthal-equivalence .snd = ap n-Tr.inc (∙-invr (merid a₀))