Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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).
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) merid
Proof.
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) merid
  snrapply cancelL_equiv_conn_map.
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
Type
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
North = South <~> ?C
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) (?g o merid)
  2: {
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
North = South <~> ?C refine (equiv_ap' (B:=SPushout (fun (u v : Unit) => X)) _ North South).
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
Susp X <~> SPushout (unit_name (unit_name X))
       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)). }
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n))
  (equiv_ap'
     (equiv_pushout
        (equiv_contr_sigma (fun _ : Unit * Unit => X))^-1
        1 1 (fun x : X => 1) (fun x : X => 1)) North
     South o merid)
  refine (conn_map_homotopic _ _ _ _
                             (blakers_massey n n (fun (u v:Unit) => X) tt tt)).
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
spglue (unit_name (unit_name X)) ==
(fun x : X =>
 equiv_ap'
   (equiv_pushout
      (equiv_contr_sigma (fun _ : Unit * Unit => X))^-1
      1 1 (fun x0 : X => 1) (fun x0 : X => 1)) North
   South (merid x))
  intros x.
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
x: X
spglue (unit_name (unit_name X)) x =
equiv_ap'
  (equiv_pushout
     (equiv_contr_sigma (fun _ : Unit * Unit => X))^-1
     1 1 (fun x : X => 1) (fun x : X => 1)) North
  South (merid 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)^).
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
x: X
spglue (unit_name (unit_name X)) x =
(ap pushl 1 @
 pglue
   (((equiv_contr_sigma (fun _ : Unit * Unit => X))^-1)%equiv
      x)) @ ap pushr 1^
  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.