Library HoTT.Homotopy.Freudenthal

Require Import Basics.
Require Import Types.
Require Import Colimits.Pushout.
Require Import Colimits.SpanPushout.
Require Import HoTT.Truncations.
Require Import Homotopy.Suspension.
Require Import Homotopy.BlakersMassey.

The Freudenthal Suspension Theorem

The Freudenthal suspension theorem is a fairly trivial corollary of the Blakers-Massey theorem. The only real work is to relate the span-pushout that we used for Blakers-Massey to the naive pushout that we used to define suspension.

Local Definition freudenthal' `{Univalence} (n : trunc_index)
           (X : Type) `{IsConnected n .+1 X}
  : IsConnMap (n +2+ n) (@merid X).
Proof.
  snrapply cancelL_equiv_conn_map.
  2: { refine (equiv_ap' (B:=SPushout (fun (u v : Unit) ⇒ X)) _ North South).
       exact (equiv_pushout (equiv_contr_sigma (fun _ : Unit × Unit ⇒ X))^-1
                            (equiv_idmap Unit) (equiv_idmap Unit)
                            (fun x : X ⇒ idpath) (fun x : X ⇒ idpath)). }
  refine (conn_map_homotopic _ _ _ _
                             (blakers_massey n n (fun (u v:Unit) ⇒ X) tt tt)).
  intros x.
  refine (_ @ (equiv_pushout_pglue
                 (equiv_contr_sigma (fun _ : Unit × Unit ⇒ X))^-1
                 (equiv_idmap Unit) (equiv_idmap Unit)
                 (fun x : X ⇒ idpath) (fun x : X ⇒ idpath) x)^).
  exact ((concat_p1 _ @ concat_1p _)^).
Defined.

Definition freudenthal@{u v | u < v} := Eval unfold freudenthal' in @freudenthal'@{u u u u u v u u u u u}.

Global Existing Instance freudenthal.