Require Import Types Basics Pointed Truncations.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HSpace Suspension ExactSequence HomotopyGroup.
Require Import WildCat.Core WildCat.Universe WildCat.Equiv Modalities.ReflectiveSubuniverse Modalities.Descent.
Require Import HSet Spaces.Nat.Core.
Require Import Homotopy.Join Colimits.Pushout.

Local Open Scope pointed_scope.
Local Open Scope trunc_scope.
Local Open Scope mc_mult_scope.


(** * The Hopf construction *)

(** We define the Hopf construction associated to a left-invertible H-space, and use it to prove that H-spaces satisfy a strengthened version of Freudenthal's theorem (see [freudenthal_hspace] below). *)

(** The Hopf construction associated to a left-invertible H-space (Definition 8.5.6 in the HoTT book). *)
Definition hopf_construction `{Univalence} (X : pType)
  `{IsHSpace X} `{forall a, IsEquiv (a *.)}
  : pFam (psusp X).
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
pFam (psusp X)
Proof.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
pFam (psusp X)
  srapply Build_pFam.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
psusp X -> Type
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
?pfam_pr1 pt
  -
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
psusp X -> Type apply (Susp_rec (Y:=Type) X X).
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
X -> X = X
    exact (fun x => path_universe (x *.)).
  -
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
Susp_rec X X (fun x : X => path_universe (sg_op x)) pt simpl.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
X exact pt.
Defined.

(** *** Total space of the Hopf construction *)

(** The total space of the Hopf construction on [Susp X] is the join of [X] with itself. Note that we need both left and right multiplication to be equivalences. This is true when [X] is a 0-connected H-space for example. (This is lemma 8.5.7 in the HoTT book). *)
Definition pequiv_hopf_total_join `{Univalence} (X : pType)
  `{IsHSpace X} `{forall a, IsEquiv (a *.)} `{forall a, IsEquiv (.* a)}
  : psigma (hopf_construction X) <~>* pjoin X X.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
psigma (hopf_construction X) <~>* pjoin X X
Proof.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
psigma (hopf_construction X) <~>* pjoin X X
  snrapply Build_pEquiv'.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
psigma (hopf_construction X) <~> pjoin X X
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
?f pt = pt
  {
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
psigma (hopf_construction X) <~> pjoin X X refine (_ oE equiv_pushout_flatten (f := const_tt X) (g := const_tt X)
      (Unit_ind (pointed_type X)) (Unit_ind (pointed_type X))
      (fun x => Build_Equiv _ _ (x *.) (H1 x))).
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
Pushout
  (functor_sigma (const_tt X) (fun a : X => idmap))
  (functor_sigma (const_tt X)
     (fun a : X =>
      {|
        equiv_fun := sg_op a; equiv_isequiv := H1 a
      |})) <~> pjoin X X
    snrapply equiv_pushout.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
{H : X & Unit_ind X (const_tt X H)} <~> X * X
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
{x : _ & Unit_ind X x} <~> X
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
{x : _ & Unit_ind X x} <~> X
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
?eB o functor_sigma (const_tt X) (fun a : X => idmap) ==
fst o ?eA
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
?eC
o functor_sigma (const_tt X)
    (fun a : X =>
     {| equiv_fun := sg_op a; equiv_isequiv := H1 a |}) ==
snd o ?eA
    (* The equivalence [{x : X & X} <~> X * X] that we need sends [(x; y) to (y, x*y)]. *)
    {
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
{H : X & Unit_ind X (const_tt X H)} <~> X * X cbn.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
{_ : X & X} <~> X * X refine (equiv_sigma_prod0 _ _ oE _ oE equiv_sigma_symm0 _ _).
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
{_ : X & X} <~> {_ : X & X}
      snrapply equiv_functor_sigma_id.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
forall a : X,
(fun _ : X => pointed_type X) a <~>
(fun _ : X => pointed_type X) a
      intros x.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
x: X
(fun _ : X => pointed_type X) x <~>
(fun _ : X => pointed_type X) x
      exact (Build_Equiv _ _ (.* x) _). }
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
{x : _ & Unit_ind X x} <~> X
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
{x : _ & Unit_ind X x} <~> X
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
?eB o functor_sigma (const_tt X) (fun a : X => idmap) ==
fst
o (equiv_sigma_prod0 X X
   oE equiv_functor_sigma_id
        (fun x : X =>
         {|
           equiv_fun := fun y : X => y * x;
           equiv_isequiv := H2 x
         |}) oE equiv_sigma_symm0 X X
   :
   {H : X & Unit_ind X (const_tt X H)} <~> X * X)
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
?eC
o functor_sigma (const_tt X)
    (fun a : X =>
     {| equiv_fun := sg_op a; equiv_isequiv := H1 a |}) ==
snd
o (equiv_sigma_prod0 X X
   oE equiv_functor_sigma_id
        (fun x : X =>
         {|
           equiv_fun := fun y : X => y * x;
           equiv_isequiv := H2 x
         |}) oE equiv_sigma_symm0 X X
   :
   {H : X & Unit_ind X (const_tt X H)} <~> X * X)
    1,2: rapply (equiv_contr_sigma (Unit_ind (pointed_type X))).
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
equiv_contr_sigma (Unit_ind X)
o functor_sigma (const_tt X) (fun a : X => idmap) ==
fst
o (equiv_sigma_prod0 X X
   oE equiv_functor_sigma_id
        (fun x : X =>
         {|
           equiv_fun := fun y : X => y * x;
           equiv_isequiv := H2 x
         |}) oE equiv_sigma_symm0 X X
   :
   {H : X & Unit_ind X (const_tt X H)} <~> X * X)
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
equiv_contr_sigma (Unit_ind X)
o functor_sigma (const_tt X)
    (fun a : X =>
     {| equiv_fun := sg_op a; equiv_isequiv := H1 a |}) ==
snd
o (equiv_sigma_prod0 X X
   oE equiv_functor_sigma_id
        (fun x : X =>
         {|
           equiv_fun := fun y : X => y * x;
           equiv_isequiv := H2 x
         |}) oE equiv_sigma_symm0 X X
   :
   {H : X & Unit_ind X (const_tt X H)} <~> X * X)
    1,2: reflexivity. }
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
H2: forall a : X, IsEquiv (fun y : X => y * a)
(equiv_pushout
   (equiv_sigma_prod0 X X
    oE equiv_functor_sigma_id
         (fun x : X =>
          {|
            equiv_fun := fun y : X => y * x;
            equiv_isequiv := H2 x
          |}) oE equiv_sigma_symm0 X X
    :
    {H : X & Unit_ind X (const_tt X H)} <~> X * X)
   (equiv_contr_sigma (Unit_ind X))
   (equiv_contr_sigma (Unit_ind X))
   (fun x0 : {_ : X & X} => 1%path)
   (fun x0 : {_ : X & X} => 1%path)
 oE equiv_pushout_flatten (Unit_ind X) (Unit_ind X)
      (fun x : X =>
       {|
         equiv_fun := sg_op x; equiv_isequiv := H1 x
       |})) pt = pt
  reflexivity.
Defined. 

(** ** Miscellaneous lemmas and corollaries about the Hopf construction *)

Lemma transport_hopf_construction `{Univalence} {X : pType}
  `{IsHSpace X} `{forall a, IsEquiv (a *.)}
  : forall x y : X, transport (hopf_construction X) (merid x) y = x * y.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
forall x y : X,
transport (hopf_construction X) (merid x) y = x * y
Proof.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
forall x y : X,
transport (hopf_construction X) (merid x) y = x * y
  intros x y.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x, y: X
transport (hopf_construction X) (merid x) y = x * y
  transport_to_ap.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x, y: X
transport idmap (ap (hopf_construction X) (merid x)) y =
x * y
  refine (ap (fun z => transport idmap z y) _ @ _).
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x, y: X
ap (hopf_construction X) (merid x) = ?Goal
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x, y: X
transport idmap ?Goal y = x * y
  1: apply Susp_rec_beta_merid.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x, y: X
transport idmap (path_universe (sg_op x)) y = x * y
  apply transport_path_universe.
Defined.

(** The connecting map associated to the Hopf construction of [X] is a retraction of [loop_susp_unit X] (Proposition 2.19 in https://arxiv.org/abs/2301.02636v1). *)
Proposition hopf_retraction `{Univalence} (X : pType)
  `{IsHSpace X} `{forall a, IsEquiv (a *.)}
  : connecting_map_family (hopf_construction X) o* loop_susp_unit X
    ==* pmap_idmap.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
connecting_map_family (hopf_construction X)
o* loop_susp_unit X ==* pmap_idmap
Proof.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
connecting_map_family (hopf_construction X)
o* loop_susp_unit X ==* pmap_idmap
  nrapply hspace_phomotopy_from_homotopy.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
IsHSpace
  [hopf_construction X pt,
  dpoint (hopf_construction X)]
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
connecting_map_family (hopf_construction X)
o* loop_susp_unit X == pmap_idmap
  1: assumption.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
connecting_map_family (hopf_construction X)
o* loop_susp_unit X == pmap_idmap
  intro x; cbn.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x: X
transport
  (Susp_rec X X (fun x : X => path_universe (sg_op x)))
  (merid x @ (merid pt)^) pt = x
  refine (transport_pp _ _ _ _ @ _); unfold dpoint.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x: X
transport
  (Susp_rec X X (fun x : X => path_universe (sg_op x)))
  (merid pt)^
  (transport
     (Susp_rec X X
        (fun x : X => path_universe (sg_op x)))
     (merid x) pt) = x
  apply moveR_transport_V.
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x: X
transport
  (Susp_rec X X (fun x : X => path_universe (sg_op x)))
  (merid x) pt =
transport
  (Susp_rec X X (fun x : X => path_universe (sg_op x)))
  (merid pt) x
  refine (transport_hopf_construction _ _
            @ _ @ (transport_hopf_construction _ _)^).
H: Univalence
X: pType
H0: IsHSpace X
H1: forall a : X, IsEquiv (sg_op a)
x: X
x * pt = pt * x
  exact (right_identity _ @ (left_identity _)^).
Defined.

(** It follows from [hopf_retraction] and Freudenthal's theorem that [loop_susp_unit] induces an equivalence on [Pi (2n+1)] for [n]-connected H-spaces (with n >= 0). Note that [X] is automatically left-invertible. *)
Proposition isequiv_Pi_connected_hspace `{Univalence}
  {n : nat} (X : pType) `{IsConnected n X}
  `{IsHSpace X}
  : IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X)).
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X))
Proof.
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X))
  nrapply isequiv_surj_emb.
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
IsConnMap (Tr (-1))
  (fmap (pPi (n + n).+1) (loop_susp_unit X))
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
IsEmbedding (fmap (pPi (n + n).+1) (loop_susp_unit X))
  -
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
IsConnMap (Tr (-1))
  (fmap (pPi (n + n).+1) (loop_susp_unit X)) apply issurj_pi_connmap.
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
IsConnMap (Tr (n + n)%nat) (loop_susp_unit X)
    destruct n.
H: Univalence
X: pType
H0: IsConnected (Tr 0%nat) X
H1: IsHSpace X
IsConnMap (Tr (0 + 0)%nat) (loop_susp_unit X)
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr (n.+1)%nat) X
H1: IsHSpace X
IsConnMap (Tr (n.+1 + n.+1)%nat) (loop_susp_unit X)
    +
H: Univalence
X: pType
H0: IsConnected (Tr 0%nat) X
H1: IsHSpace X
IsConnMap (Tr (0 + 0)%nat) (loop_susp_unit X) by apply (conn_map_loop_susp_unit (-1)).
    +
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr (n.+1)%nat) X
H1: IsHSpace X
IsConnMap (Tr (n.+1 + n.+1)%nat) (loop_susp_unit X) rewrite <- trunc_index_add_nat_add.
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr (n.+1)%nat) X
H1: IsHSpace X
IsConnMap (Tr (n +2+ n)) (loop_susp_unit X)
      by apply (conn_map_loop_susp_unit).
  -
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
IsEmbedding (fmap (pPi (n + n).+1) (loop_susp_unit X)) pose (is0connected_isconnected n.-2 _).
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
i:= is0connected_isconnected n.-2 X: IsConnected (Tr 0) X
IsEmbedding (fmap (pPi (n + n).+1) (loop_susp_unit X))
    nrapply isembedding_pi_psect.
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr n) X
H1: IsHSpace X
i:= is0connected_isconnected n.-2 X: IsConnected (Tr 0) X
?Goal o* loop_susp_unit X ==* pmap_idmap
    apply hopf_retraction.
Defined.

(** By Freudenthal, [loop_susp_unit] induces an equivalence on lower homotopy groups as well, so it is a (2n+1)-equivalence.  We formalize it below with [m = n-1], and allow [n] to start at [-1].  We prove it using a more general result about reflective subuniverses, [OO_inverts_conn_map_factor_conn_map], but one could also use homotopy groups and the truncated Whitehead theorem. *)
Definition freudenthal_hspace' `{Univalence}
  {m : trunc_index} (X : pType) `{IsConnected m.+1 X}
  `{IsHSpace X} `{forall a, IsEquiv (a *.)}
  : O_inverts (Tr (m +2+ m).+1) (loop_susp_unit X).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
O_inverts (Tr (m +2+ m).+1) (loop_susp_unit X)
Proof.
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
O_inverts (Tr (m +2+ m).+1) (loop_susp_unit X)
  set (r:=connecting_map_family (hopf_construction X)).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
O_inverts (Tr (m +2+ m).+1) (loop_susp_unit X)
  nrapply (OO_inverts_conn_map_factor_conn_map _ (m +2+ m) _ r).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
Tr (m +2+ m) <<< Tr (m +2+ m).+1
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
O_leq (Tr (m +2+ m).+1) (Sep (Tr (m +2+ m)))
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
IsConnMap (Tr (m +2+ m).+1)
  (fun x : X => r (loop_susp_unit X x))
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
IsConnMap (Tr (m +2+ m)) (loop_susp_unit X)
  2, 4: exact _.
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
Tr (m +2+ m) <<< Tr (m +2+ m).+1
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
IsConnMap (Tr (m +2+ m).+1)
  (fun x : X => r (loop_susp_unit X x))
  1: apply O_lex_leq_Tr.
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
IsConnMap (Tr (m +2+ m).+1)
  (fun x : X => r (loop_susp_unit X x))
  rapply (conn_map_homotopic _ equiv_idmap (r o loop_susp_unit X)).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
1%equiv == (fun x : X => r (loop_susp_unit X x))
  symmetry.
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+1) X
H1: IsHSpace X
H2: forall a : X, IsEquiv (sg_op a)
r:= connecting_map_family (hopf_construction X): loops (psusp X) ->*
[hopf_construction X pt,
dpoint (hopf_construction X)]
(fun x : X => r (loop_susp_unit X x)) == 1%equiv
  nrapply hopf_retraction.
Defined.

(** Note that we don't really need the assumption that [X] is left-invertible in the previous result; for [m >= -1], it follows from connectivity.  And for [m = -2], the conclusion is trivial. Here we state the version for [m >= -1] without left-invertibility. *)
Definition freudenthal_hspace `{Univalence}
  {m : trunc_index} (X : pType) `{IsConnected m.+2 X}
  `{IsHSpace X}
  : O_inverts (Tr (m.+1 +2+ m.+1).+1) (loop_susp_unit X).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+2) X
H1: IsHSpace X
O_inverts (Tr (m.+1 +2+ m.+1).+1) (loop_susp_unit X)
Proof.
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+2) X
H1: IsHSpace X
O_inverts (Tr (m.+1 +2+ m.+1).+1) (loop_susp_unit X)
  pose (is0connected_isconnected m _).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+2) X
H1: IsHSpace X
i:= is0connected_isconnected m X: IsConnected (Tr 0) X
O_inverts (Tr (m.+1 +2+ m.+1).+1) (loop_susp_unit X)
  exact (freudenthal_hspace' (m:=m.+1) X).
Defined.

(** Here we give a generalization of a result from Eilenberg-MacLane Spaces in Homotopy Type Theory, Dan Licata and Eric Finster.  Their version corresponds to [m = -2] in our version.  Their encode-decode proof was formalized in this library in EMSpace.v until this shorter and more general approach was found. *)
Definition licata_finster `{Univalence}
  {m : trunc_index} (X : pType) `{IsConnected m.+2 X}
  (k := (m.+1 +2+ m.+1).+1) `{IsHSpace X} `{IsTrunc k X}
  : X <~>* pTr k (loops (psusp X)).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+2) X
k:= (m.+1 +2+ m.+1).+1: trunc_index
H1: IsHSpace X
IsTrunc0: IsTrunc k X
X <~>* pTr k (loops (psusp X))
Proof.
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+2) X
k:= (m.+1 +2+ m.+1).+1: trunc_index
H1: IsHSpace X
IsTrunc0: IsTrunc k X
X <~>* pTr k (loops (psusp X))
  refine (_ o*E pequiv_ptr (n:=k)).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+2) X
k:= (m.+1 +2+ m.+1).+1: trunc_index
H1: IsHSpace X
IsTrunc0: IsTrunc k X
pTr k X <~>* pTr k (loops (psusp X))
  nrefine (pequiv_O_inverts k (loop_susp_unit X)).
H: Univalence
m: trunc_index
X: pType
H0: IsConnected (Tr m.+2) X
k:= (m.+1 +2+ m.+1).+1: trunc_index
H1: IsHSpace X
IsTrunc0: IsTrunc k X
O_inverts (Tr k) (loop_susp_unit X)
  rapply freudenthal_hspace.
Defined.

(** Since [loops X] is an H-space, the Hopf construction provides a map [Join (loops X) (loops X) -> Susp (loops X)].  We show that this map is equivalent to the fiber of [loop_susp_counit X : Susp (loops X) -> X] over the base point, up to the automorphism of [Susp (loops X)] induced by inverting loops. *)
Definition pequiv_pfiber_loops_susp_counit_join `{Univalence} (X : pType)
  : pfiber (loop_susp_counit X) <~>* pjoin (loops X) (loops X).
H: Univalence
X: pType
pfiber (loop_susp_counit X) <~>*
pjoin (loops X) (loops X)
Proof.
H: Univalence
X: pType
pfiber (loop_susp_counit X) <~>*
pjoin (loops X) (loops X)
  snrefine (pequiv_hopf_total_join (loops X) o*E _).
H: Univalence
X: pType
pfiber (loop_susp_counit X) <~>*
psigma (hopf_construction (loops X))
H: Univalence
X: pType
IsHSpace (loops X)
H: Univalence
X: pType
forall a : loops X, IsEquiv (sg_op a)
H: Univalence
X: pType
forall a : loops X, IsEquiv (fun y : loops X => y * a)
  2: rapply ishspace_loops.
H: Univalence
X: pType
pfiber (loop_susp_counit X) <~>*
psigma (hopf_construction (loops X))
H: Univalence
X: pType
forall a : loops X, IsEquiv (sg_op a)
H: Univalence
X: pType
forall a : loops X, IsEquiv (fun y : loops X => y * a)
  2,3: exact _.
H: Univalence
X: pType
pfiber (loop_susp_counit X) <~>*
psigma (hopf_construction (loops X))
  snrapply Build_pEquiv'.
H: Univalence
X: pType
pfiber (loop_susp_counit X) <~>
psigma (hopf_construction (loops X))
H: Univalence
X: pType
?f pt = pt
  {
H: Univalence
X: pType
pfiber (loop_susp_counit X) <~>
psigma (hopf_construction (loops X)) snrapply equiv_functor_sigma'.
H: Univalence
X: pType
psusp (loops X) <~> psusp (loops X)
H: Univalence
X: pType
forall a : psusp (loops X),
(fun x : psusp (loops X) => loop_susp_counit X x = pt)
  a <~> hopf_construction (loops X) (?f a)
    1: exact (emap psusp (equiv_path_inverse _ _)).
H: Univalence
X: pType
forall a : psusp (loops X),
(fun x : psusp (loops X) => loop_susp_counit X x = pt)
  a <~>
hopf_construction (loops X)
  (emap psusp (equiv_path_inverse pt pt) a)
    snrapply Susp_ind; hnf.
H: Univalence
X: pType
loop_susp_counit X North = pt <~>
hopf_construction (loops X)
  (emap psusp (equiv_path_inverse pt pt) North)
H: Univalence
X: pType
loop_susp_counit X South = pt <~>
hopf_construction (loops X)
  (emap psusp (equiv_path_inverse pt pt) South)
H: Univalence
X: pType
forall x : loops X,
transport
  (fun y : Susp (loops X) =>
   loop_susp_counit X y = pt <~>
   hopf_construction (loops X)
     (emap psusp (equiv_path_inverse pt pt) y))
  (merid x) ?Goal = ?Goal0
    1,2: reflexivity.
H: Univalence
X: pType
forall x : loops X,
transport
  (fun y : Susp (loops X) =>
   loop_susp_counit X y = pt <~>
   hopf_construction (loops X)
     (emap psusp (equiv_path_inverse pt pt) y))
  (merid x) 1%equiv = 1%equiv
    intros p.
H: Univalence
X: pType
p: loops X
transport
  (fun y : Susp (loops X) =>
   loop_susp_counit X y = pt <~>
   hopf_construction (loops X)
     (emap psusp (equiv_path_inverse pt pt) y))
  (merid p) 1%equiv = 1%equiv
    nrapply path_equiv.
H: Univalence
X: pType
p: loops X
transport
  (fun y : Susp (loops X) =>
   loop_susp_counit X y = pt <~>
   hopf_construction (loops X)
     (emap psusp (equiv_path_inverse pt pt) y))
  (merid p) 1%equiv = 1%equiv
    funext q.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport
  (fun y : Susp (loops X) =>
   loop_susp_counit X y = pt <~>
   hopf_construction (loops X)
     (emap psusp (equiv_path_inverse pt pt) y))
  (merid p) 1%equiv q = 1%equiv q
    simpl.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport
  (fun y : Susp (pt = pt) =>
   Susp_rec pt pt idmap y = pt <~>
   Susp_rec (pt = pt) (pt = pt)
     (fun x : pt = pt => path_universe (sg_op x))
     (functor_susp inverse y)) (merid p) 1%equiv q = q
    lhs rapply (transport_equiv (merid p) _ q).
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport
  (fun x : Susp (loops X) =>
   Susp_rec (pt = pt) (pt = pt)
     (fun x0 : pt = pt => path_universe (sg_op x0))
     (functor_susp inverse x)) (merid p)
  (1%equiv
     (transport
        (fun x : Susp (loops X) =>
         Susp_rec pt pt idmap x = pt) (merid p)^ q)) =
q
    simpl.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport
  (fun x : Susp (pt = pt) =>
   Susp_rec (pt = pt) (pt = pt)
     (fun x0 : pt = pt => path_universe (sg_op x0))
     (functor_susp inverse x)) (merid p)
  (transport
     (fun x : Susp (pt = pt) =>
      Susp_rec pt pt idmap x = pt) (merid p)^ q) = q
    lhs nrapply ap.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport
  (fun x : Susp (pt = pt) =>
   Susp_rec pt pt idmap x = pt) (merid p)^ q = ?Goal
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport
  (fun x : Susp (pt = pt) =>
   Susp_rec (pt = pt) (pt = pt)
     (fun x0 : pt = pt => path_universe (sg_op x0))
     (functor_susp inverse x)) (merid p) ?Goal = q
    {
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport
  (fun x : Susp (pt = pt) =>
   Susp_rec pt pt idmap x = pt) (merid p)^ q = ?Goal lhs nrapply transport_paths_Fl.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
(ap (Susp_rec pt pt idmap) (merid p)^)^ @ q = ?Goal
      nrapply whiskerR.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
(ap (Susp_rec pt pt idmap) (merid p)^)^ = ?Goal0
      {
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
(ap (Susp_rec pt pt idmap) (merid p)^)^ = ?Goal0 lhs nrapply (ap inverse (ap_V _ _)).
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
((ap (Susp_rec pt pt idmap) (merid p))^)^ = ?Goal0
        lhs rapply inv_V.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
ap (Susp_rec pt pt idmap) (merid p) = ?Goal0
        apply Susp_rec_beta_merid. } }
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport
  (fun x : Susp (pt = pt) =>
   Susp_rec (pt = pt) (pt = pt)
     (fun x0 : pt = pt => path_universe (sg_op x0))
     (functor_susp inverse x)) (merid p) (p @ q) = q
    lhs nrapply (transport_idmap_ap _ (merid p)).
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport idmap
  (ap
     (fun x : Susp (pt = pt) =>
      Susp_rec (pt = pt) (pt = pt)
        (fun x0 : pt = pt => path_universe (sg_op x0))
        (functor_susp inverse x)) (merid p)) (p @ q) =
q
    lhs nrapply (transport2 idmap).
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
ap
  (fun x : Susp (pt = pt) =>
   Susp_rec (pt = pt) (pt = pt)
     (fun x0 : pt = pt => path_universe (sg_op x0))
     (functor_susp inverse x)) (merid p) = ?Goal
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport idmap ?Goal (p @ q) = q
    {
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
ap
  (fun x : Susp (pt = pt) =>
   Susp_rec (pt = pt) (pt = pt)
     (fun x0 : pt = pt => path_universe (sg_op x0))
     (functor_susp inverse x)) (merid p) = ?Goal lhs nrapply ap_compose.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
ap
  (Susp_rec (pt = pt) (pt = pt)
     (fun x : pt = pt => path_universe (sg_op x)))
  (ap (functor_susp inverse) (merid p)) = ?Goal
      lhs nrapply ap.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
ap (functor_susp inverse) (merid p) = ?Goal1
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
ap
  (Susp_rec (pt = pt) (pt = pt)
     (fun x : pt = pt => path_universe (sg_op x)))
  ?Goal1 = ?Goal
      1: apply functor_susp_beta_merid.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
ap
  (Susp_rec (pt = pt) (pt = pt)
     (fun x : pt = pt => path_universe (sg_op x)))
  (merid p^) = ?Goal
      apply Susp_rec_beta_merid. }
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
transport idmap (path_universe (sg_op p^)) (p @ q) = q
    lhs nrapply transport_path_universe.
H: Univalence
X: pType
p: loops X
q: loop_susp_counit X South = pt
p^ * p @ q = q
    apply concat_V_pp. }
H: Univalence
X: pType
equiv_functor_sigma'
  (emap psusp (equiv_path_inverse pt pt))
  (Susp_ind
     (fun y : Susp (loops X) =>
      (fun x : psusp (loops X) =>
       loop_susp_counit X x = pt) y <~>
      hopf_construction (loops X)
        (emap psusp (equiv_path_inverse pt pt) y))
     (1%equiv
      :
      (fun y : Susp (loops X) =>
       (fun x : psusp (loops X) =>
        loop_susp_counit X x = pt) y <~>
       hopf_construction (loops X)
         (emap psusp (equiv_path_inverse pt pt) y))
        North)
     (1%equiv
      :
      (fun y : Susp (loops X) =>
       (fun x : psusp (loops X) =>
        loop_susp_counit X x = pt) y <~>
       hopf_construction (loops X)
         (emap psusp (equiv_path_inverse pt pt) y))
        South)
     ((fun p : loops X =>
       path_equiv
         (path_forall
            (transport
               (fun y : Susp (loops X) =>
                loop_susp_counit X y = pt <~>
                hopf_construction (loops X)
                  (emap psusp
                     (equiv_path_inverse pt pt) y))
               (merid p) 1%equiv) 1%equiv
            ((fun q : loop_susp_counit X South = pt =>
              transport_equiv (merid p) 1 q @
              (ap
                 (transport
                    (fun x : ... =>
                     Susp_rec (...) (...) (...) (...))
                    (merid p))
                 (transport_paths_Fl (merid p)^ q @
                  whiskerR (ap inverse ... @ (...)) q) @
               (transport_idmap_ap
                  (fun x : ... =>
                   Susp_rec (...) (...) (...) (...))
                  (merid p) (p @ q) @
                (transport2 idmap (... @ ...) (p @ q) @
                 (transport_path_universe ... ... @
                  concat_V_pp p q)))
               :
               transport
                 (fun x : Susp (...) =>
                  Susp_rec (pt = pt) (pt = pt)
                    (fun ... => path_universe ...)
                    (functor_susp inverse x))
                 (merid p)
                 (1%equiv
                    (transport (... => ...) (merid p)^
                       q)) = q)
              :
              transport
                (fun y : Susp (loops X) =>
                 loop_susp_counit X y = pt <~>
                 hopf_construction (loops X)
                   (emap psusp
                      (equiv_path_inverse pt pt) y))
                (merid p) 1%equiv q = 1%equiv q)
             :
             transport
               (fun y : Susp (loops X) =>
                loop_susp_counit X y = pt <~>
                hopf_construction (loops X)
                  (emap psusp
                     (equiv_path_inverse pt pt) y))
               (merid p) 1%equiv == 1%equiv)))
      :
      forall x : loops X,
      transport
        (fun y : Susp (loops X) =>
         (fun x0 : psusp (loops X) =>
          loop_susp_counit X x0 = pt) y <~>
         hopf_construction (loops X)
           (emap psusp (equiv_path_inverse pt pt) y))
        (merid x)
        (1%equiv
         :
         (fun y : Susp (loops X) =>
          (fun x0 : psusp (loops X) =>
           loop_susp_counit X x0 = pt) y <~>
          hopf_construction (loops X)
            (emap psusp (equiv_path_inverse pt pt) y))
           North) =
      (1%equiv
       :
       (fun y : Susp (loops X) =>
        (fun x0 : psusp (loops X) =>
         loop_susp_counit X x0 = pt) y <~>
        hopf_construction (loops X)
          (emap psusp (equiv_path_inverse pt pt) y))
         South))) pt = pt
  reflexivity.
Defined.

(** As a corollary we get 2n-connectivity of [loop_susp_counit X] for an n-connected [X]. *)
Global Instance conn_map_loop_susp_counit `{Univalence}
  {n : trunc_index} (X : pType) `{IsConnected n.+1 X}
  : IsConnMap (n +2+ n) (loop_susp_counit X).
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) (loop_susp_counit X)
Proof.
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) (loop_susp_counit X)
  destruct n.
H: Univalence
X: pType
H0: IsConnected (Tr (-1)) X
IsConnMap (Tr (-2 +2+ -2)) (loop_susp_counit X)
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
IsConnMap (Tr (n.+1 +2+ n.+1)) (loop_susp_counit X)
  -
H: Univalence
X: pType
H0: IsConnected (Tr (-1)) X
IsConnMap (Tr (-2 +2+ -2)) (loop_susp_counit X) intro x; hnf; exact _.
  -
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
IsConnMap (Tr (n.+1 +2+ n.+1)) (loop_susp_counit X) snrapply (conn_point_elim (-1)).
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
IsConnected (Tr 0) X
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
forall a : X,
IsHProp
  ((fun a0 : X =>
    IsConnected (Tr (n.+1 +2+ n.+1))
      (hfiber (loop_susp_counit X) a0)) a)
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
(fun a : X =>
 IsConnected (Tr (n.+1 +2+ n.+1))
   (hfiber (loop_susp_counit X) a)) pt
    +
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
IsConnected (Tr 0) X exact (isconnected_pred_add' n 0 _).
    +
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
forall a : X,
IsHProp
  ((fun a0 : X =>
    IsConnected (Tr (n.+1 +2+ n.+1))
      (hfiber (loop_susp_counit X) a0)) a) exact _.
    +
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
(fun a : X =>
 IsConnected (Tr (n.+1 +2+ n.+1))
   (hfiber (loop_susp_counit X) a)) pt nrapply (isconnected_equiv' _ _ (pequiv_pfiber_loops_susp_counit_join X)^-1).
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+2) X
IsConnected (Tr (n.+1 +2+ n.+1))
  (pjoin (loops X) (loops X))
      nrapply isconnected_join; exact _.
Defined.