(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Equiv.
Require Import NullHomotopy.
Require Import Homotopy.Suspension.
Require Import Pointed.
Require Import Truncations.
Require Import Spaces.Circle Spaces.TwoSphere.

(** * The spheres, in all dimensions. *)

Local Open Scope pointed_scope.
Local Open Scope trunc_scope.
Local Open Scope path_scope.

Generalizable Variables X A B f g n.

(** ** Definition, by iterated suspension. *)

(** To match the usual indexing for spheres, we have to pad the sequence with a dummy term [Sphere -2]. *)
Fixpoint Sphere (n : trunc_index)
  := match n return Type with
       | -2 => Empty
       | -1 => Empty
       | n'.+1 => Susp (Sphere n')
     end.

(** ** Pointed sphere for non-negative dimensions. *)
Definition psphere (n : nat) : pType := [Sphere n, _].

Arguments Sphere : simpl never.
Arguments psphere : simpl never.

(** ** Explicit equivalences in low dimensions  *)

(** *** [Sphere 0] *)
Definition S0_to_Bool : (Sphere 0) -> Bool.
Sphere 0 -> Bool
Proof.
Sphere 0 -> Bool
  simpl.
Sphere 0 -> Bool apply (Susp_rec true false).
Empty -> true = false intros [].
Defined.

Definition Bool_to_S0 : Bool -> (Sphere 0).
Bool -> Sphere 0
Proof.
Bool -> Sphere 0
  exact (fun b => if b then North else South).
Defined.

Global Instance isequiv_S0_to_Bool : IsEquiv (S0_to_Bool) | 0.
IsEquiv S0_to_Bool
Proof.
IsEquiv S0_to_Bool
  apply isequiv_adjointify with Bool_to_S0.
(fun x : Bool => S0_to_Bool (Bool_to_S0 x)) == idmap
(fun x : Sphere 0 => Bool_to_S0 (S0_to_Bool x)) ==
idmap
  -
(fun x : Bool => S0_to_Bool (Bool_to_S0 x)) == idmap intros [ | ]; exact 1.
  -
(fun x : Sphere 0 => Bool_to_S0 (S0_to_Bool x)) ==
idmap refine (Susp_ind _ 1 1 _).
forall x : Empty,
transport
  (fun y : Susp Empty => Bool_to_S0 (S0_to_Bool y) = y)
  (merid x) 1 = 1 intros [].
Defined.

Definition equiv_S0_Bool : Sphere 0 <~> Bool
  := Build_Equiv _ _ _ isequiv_S0_to_Bool.

Definition ispointed_bool : IsPointed Bool := true.

Definition pBool := [Bool, true].

Definition pequiv_S0_Bool : psphere 0 <~>* pBool
  := @Build_pEquiv' (psphere 0) pBool equiv_S0_Bool 1.

(** In [pmap_from_psphere_iterated_loops] below, we'll use this universal property of [pBool]. *)
Definition pmap_from_bool `{Funext} (X : pType)
  : (pBool ->** X) <~>* X.
H: Funext
X: pType
(pBool ->** X) <~>* X
Proof.
H: Funext
X: pType
(pBool ->** X) <~>* X
  snrapply Build_pEquiv'.
H: Funext
X: pType
(pBool ->** X) <~> X
H: Funext
X: pType
?f pt = pt
  -
H: Funext
X: pType
(pBool ->** X) <~> X refine (_ oE (issig_pmap _ _)^-1%equiv).
H: Funext
X: pType
{f : pBool -> X & f pt = pt} <~> X
    refine (_ oE (equiv_functor_sigma_pb (equiv_bool_rec_uncurried X))^-1%equiv); cbn.
H: Funext
X: pType
{x : X * X & snd x = pt} <~> X
    make_equiv_contr_basedpaths.
  -
H: Funext
X: pType
((equiv_adjointify
    (fun H0 : {x : X * X & snd x = pt} =>
     (fun H1 : X * X =>
      (fun (H2 H3 : X) (_ : snd (H2, H3) = pt) =>
       H2 : X) (fst H1) (snd H1)) H0.1 H0.2)
    (fun H0 : X =>
     ((H0 : X, let H1 := pt in H1) : X * X;
     1%path
     :
     snd ((H0 : X, let H1 := pt in H1) : X * X) = pt)
     :
     {x : X * X & snd x = pt})
    ((fun H0 : X => 1%path)
     :
     (fun H0 : {x : X * X & snd x = pt} =>
      (fun H1 : X * X =>
       (fun (H2 H3 : X) (_ : snd (H2, H3) = pt) =>
        H2 : X) (fst H1) (snd H1)) H0.1 H0.2)
     o (fun H0 : X =>
        ((H0 : X, let H1 := pt in H1) : X * X;
        1%path
        :
        snd ((H0 : X, let H1 := pt in H1) : X * X) =
        pt)
        :
        {x : X * X & snd x = pt}) == idmap)
    ((fun H0 : {x : X * X & snd x = pt} =>
      (fun H1 : X * X =>
       (fun (H2 H3 : X) (H4 : snd (H2, H3) = pt) =>
        paths_ind_r pt
          (fun (y : X) (p : y = pt) =>
           ((H2, let H5 := pt in H5); 1%path) =
           ((H2, y); p)) 1%path H3 H4) (fst H1)
         (snd H1)) H0.1 H0.2)
     :
     (fun H0 : X =>
      ((H0 : X, let H1 := pt in H1) : X * X;
      1%path
      :
      snd ((H0 : X, let H1 := pt in H1) : X * X) = pt)
      :
      {x : X * X & snd x = pt})
     o (fun H0 : {x : X * X & snd x = pt} =>
        (fun H1 : X * X =>
         (fun (H2 H3 : X) (_ : snd (H2, H3) = pt) =>
          H2 : X) (fst H1) (snd H1)) H0.1 H0.2) ==
     idmap)
  :
  {x : X * X & equiv_bool_rec_uncurried X x pt = pt} <~>
  X)
 oE (equiv_functor_sigma_pb
       (equiv_bool_rec_uncurried X))^-1
 oE (issig_pmap pBool X)^-1) pt = pt reflexivity.
Defined.

(** *** [Sphere 1] *)
Definition S1_to_Circle : (Sphere 1) -> Circle.
Sphere 1 -> Circle
Proof.
Sphere 1 -> Circle
  apply (Susp_rec Circle.base Circle.base).
Susp Empty -> Circle.base = Circle.base
  exact (fun x => if (S0_to_Bool x) then loop else 1).
Defined.

Definition Circle_to_S1 : Circle -> (Sphere 1).
Circle -> Sphere 1
Proof.
Circle -> Sphere 1
  apply (Circle_rec _ North).
North = North
  exact (merid North @ (merid South)^).
Defined.

Global Instance isequiv_S1_to_Circle : IsEquiv (S1_to_Circle) | 0.
IsEquiv S1_to_Circle
Proof.
IsEquiv S1_to_Circle
  apply isequiv_adjointify with Circle_to_S1.
(fun x : Circle => S1_to_Circle (Circle_to_S1 x)) ==
idmap
(fun x : Sphere 1 => Circle_to_S1 (S1_to_Circle x)) ==
idmap
  -
(fun x : Circle => S1_to_Circle (Circle_to_S1 x)) ==
idmap refine (Circle_ind _ 1 _).
transport
  (fun x : Circle => S1_to_Circle (Circle_to_S1 x) = x)
  loop 1 = 1
    nrapply transport_paths_FFlr'; apply equiv_p1_1q.
ap S1_to_Circle (ap Circle_to_S1 loop) = loop
    refine (ap _ (Circle_rec_beta_loop _ _ _) @ _).
ap S1_to_Circle (merid North @ (merid South)^) = loop
    refine (ap_pp _ _ (merid South)^ @ _).
ap S1_to_Circle (merid North) @
ap S1_to_Circle (merid South)^ = loop
    refine ((1 @@ ap_V _ _) @ _).
ap S1_to_Circle (merid North) @
(ap S1_to_Circle (merid South))^ = loop
    refine ((_ @@ (ap inverse _)) @ _).
ap S1_to_Circle (merid North) = ?Goal0
ap S1_to_Circle (merid South) = ?Goal2
?Goal0 @ ?Goal2^ = loop 1, 2: nrapply Susp_rec_beta_merid.
(if S0_to_Bool North then loop else 1) @
(if S0_to_Bool South then loop else 1)^ = loop
    simpl.
loop @ 1 = loop
    apply concat_p1.
  -
(fun x : Sphere 1 => Circle_to_S1 (S1_to_Circle x)) ==
idmap refine (Susp_ind (fun x => Circle_to_S1 (S1_to_Circle x) = x)
                     1 (merid South) _); intros x.
x: Susp Empty
transport
  (fun x : Susp (Susp Empty) =>
   Circle_to_S1 (S1_to_Circle x) = x) (merid x) 1 =
merid South
    nrapply transport_paths_FFlr'; symmetry.
x: Susp Empty
1 @ merid x =
ap Circle_to_S1 (ap S1_to_Circle (merid x)) @
merid South
    unfold S1_to_Circle; rewrite (Susp_rec_beta_merid x).
x: Susp Empty
1 @ merid x =
ap Circle_to_S1 (if S0_to_Bool x then loop else 1) @
merid South
    revert x.
forall x : Susp Empty,
1 @ merid x =
ap Circle_to_S1 (if S0_to_Bool x then loop else 1) @
merid South change (Susp Empty) with (Sphere 0).
forall x : Sphere 0,
1 @ merid x =
ap Circle_to_S1 (if S0_to_Bool x then loop else 1) @
merid South
    apply (equiv_ind (S0_to_Bool ^-1)); intros x.
x: Bool
1 @ merid (S0_to_Bool^-1 x) =
ap Circle_to_S1
  (if S0_to_Bool (S0_to_Bool^-1 x) then loop else 1) @
merid South
    case x; simpl.
x: Bool
1 @ merid North = ap Circle_to_S1 loop @ merid South
x: Bool
1 @ merid South = 1 @ merid South
    2: reflexivity.
x: Bool
1 @ merid North = ap Circle_to_S1 loop @ merid South
    lhs nrapply concat_1p.
x: Bool
merid North = ap Circle_to_S1 loop @ merid South
    unfold Circle_to_S1; rewrite Circle_rec_beta_loop.
x: Bool
merid North =
(merid North @ (merid South)^) @ merid South
    symmetry; apply concat_pV_p.
Defined.

Definition equiv_S1_Circle : Sphere 1 <~> Circle
  := Build_Equiv _ _ _ isequiv_S1_to_Circle.

Definition pequiv_S1_Circle : psphere 1 <~>* [Circle, _].
psphere 1 <~>* [Circle, ispointed_Circle]
Proof.
psphere 1 <~>* [Circle, ispointed_Circle]
  srapply Build_pEquiv'.
psphere 1 <~> [Circle, ispointed_Circle]
?f pt = pt
  1: apply equiv_S1_Circle.
equiv_S1_Circle pt = pt
  reflexivity.
Defined.

(** *** [Sphere 2] *)
Definition S2_to_TwoSphere : (Sphere 2) -> TwoSphere.
Sphere 2 -> TwoSphere
Proof.
Sphere 2 -> TwoSphere
  apply (Susp_rec base base).
Susp (Susp Empty) -> base = base
  apply (Susp_rec (idpath base) (idpath base)).
Susp Empty -> 1 = 1
  apply (Susp_rec surf (idpath (idpath base))).
Empty -> surf = 1
  apply Empty_rec.
Defined.

Definition TwoSphere_to_S2 : TwoSphere -> (Sphere 2).
TwoSphere -> Sphere 2
Proof.
TwoSphere -> Sphere 2
  apply (TwoSphere_rec (Sphere 2) North).
1 = 1
  refine (transport (fun x => x = x) (concat_pV (merid North)) _).
merid North @ (merid North)^ =
merid North @ (merid North)^
  refine (((ap (fun u => merid u @ (merid North)^) 
               (merid North @ (merid South)^)))).
Defined.

Definition issect_TwoSphere_to_S2 : S2_to_TwoSphere o TwoSphere_to_S2 == idmap.
S2_to_TwoSphere o TwoSphere_to_S2 == idmap
Proof.
S2_to_TwoSphere o TwoSphere_to_S2 == idmap
  refine (TwoSphere_ind _ 1 _).
1 =
transport2
  (fun x : TwoSphere =>
   S2_to_TwoSphere (TwoSphere_to_S2 x) = x) surf 1 
  rhs_V rapply concat_p1.
1 =
transport2
  (fun x : TwoSphere =>
   S2_to_TwoSphere (TwoSphere_to_S2 x) = x) surf 1 @ 1
  rhs refine (@concat_Ap (base = base) _ _
                          (fun p => (p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))^)
                          (fun x =>
                             (transport_paths_FFlr x 1) 
                               @ ap (fun u => u @ x) (concat_p1 _)
                               @ ap (fun w => _ @ w) (inv_V x)^ 
                               @ (inv_pp _ _)^) 
                          1 1 surf).
1 =
(((transport_paths_FFlr 1 1 @
   ap
     (fun
        u : S2_to_TwoSphere (TwoSphere_to_S2 base) =
            base => u @ 1)
     (concat_p1
        (ap S2_to_TwoSphere (ap TwoSphere_to_S2 1))^)) @
  ap
    (fun w : base = base =>
     (ap S2_to_TwoSphere (ap TwoSphere_to_S2 1))^ @ w)
    (inv_V 1)^) @
 (inv_pp 1^
    (ap S2_to_TwoSphere (ap TwoSphere_to_S2 1)))^) @
ap
  (fun p : base = base =>
   (p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))^)
  surf
  rhs rapply concat_1p.
1 =
ap
  (fun p : base = base =>
   (p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))^)
  surf
  rhs refine (ap_compose (fun p => p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))
                          inverse
                          surf).
1 =
ap inverse
  (ap
     (fun p : base = base =>
      p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))
     surf)
  refine (@ap _ _ (ap inverse) 1 _ _).
1 =
ap
  (fun p : base = base =>
   p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))
  surf
  rhs_V rapply concat2_ap_ap.
1 =
ap inverse surf @@
ap
  (fun u : base = base =>
   ap S2_to_TwoSphere (ap TwoSphere_to_S2 u)) surf
  rhs refine (ap (fun w => inverse2 surf @@ w)
                  (ap_compose (ap TwoSphere_to_S2) (ap S2_to_TwoSphere) surf)).
1 =
inverse2 surf @@
ap (ap S2_to_TwoSphere) (ap (ap TwoSphere_to_S2) surf)
  lhs_V refine (concat_Vp_inverse2 _ _ surf).
(inverse2 surf @@ surf) @ concat_Vp 1 =
inverse2 surf @@
ap (ap S2_to_TwoSphere) (ap (ap TwoSphere_to_S2) surf)
  lhs rapply concat_p1.
inverse2 surf @@ surf =
inverse2 surf @@
ap (ap S2_to_TwoSphere) (ap (ap TwoSphere_to_S2) surf)
  refine (ap (fun p : 1 = 1 => inverse2 surf @@ p) _).
surf =
ap (ap S2_to_TwoSphere) (ap (ap TwoSphere_to_S2) surf)

  symmetry.
ap (ap S2_to_TwoSphere) (ap (ap TwoSphere_to_S2) surf) =
surf lhs refine ((ap (ap (ap S2_to_TwoSphere))
                        (TwoSphere_rec_beta_surf (Sphere 2) North _))).
ap (ap S2_to_TwoSphere)
  (transport (fun x : North = North => x = x)
     (concat_pV (merid North))
     (ap
        (fun u : Susp (Susp Empty) =>
         merid u @ (merid North)^)
        (merid North @ (merid South)^))) = surf
  lhs refine (ap_transport (concat_pV (merid North))
                        (fun z => @ap _ _ _ z z) 
                        (ap (fun u => merid u @ (merid North)^)
                            (merid North @ (merid South)^))).
transport
  (fun z : North = North =>
   ap S2_to_TwoSphere z = ap S2_to_TwoSphere z)
  (concat_pV (merid North))
  (ap (ap S2_to_TwoSphere)
     (ap
        (fun u : Susp (Susp Empty) =>
         merid u @ (merid North)^)
        (merid North @ (merid South)^))) = surf

  lhs_V refine (ap (transport (fun z => ap S2_to_TwoSphere z = ap S2_to_TwoSphere z)
                      (concat_pV (merid North)))
               (ap_compose (fun u => merid u @ (merid North)^) (ap S2_to_TwoSphere)
                           (merid North @ (merid South)^))).
transport
  (fun z : North = North =>
   ap S2_to_TwoSphere z = ap S2_to_TwoSphere z)
  (concat_pV (merid North))
  (ap
     (fun x : Susp (Susp Empty) =>
      ap S2_to_TwoSphere (merid x @ (merid North)^))
     (merid North @ (merid South)^)) = surf
  apply transport_paths_FlFr'; symmetry.
ap
  (fun x : Susp (Susp Empty) =>
   ap S2_to_TwoSphere (merid x @ (merid North)^))
  (merid North @ (merid South)^) @
ap (ap S2_to_TwoSphere) (concat_pV (merid North)) =
ap (ap S2_to_TwoSphere) (concat_pV (merid North)) @
surf
  lhs_V refine (1 @@ ap_pp_concat_pV S2_to_TwoSphere (merid North)).
ap
  (fun x : Susp (Susp Empty) =>
   ap S2_to_TwoSphere (merid x @ (merid North)^))
  (merid North @ (merid South)^) @
(ap_pp S2_to_TwoSphere (merid North) (merid North)^ @
 ((1 @@ ap_V S2_to_TwoSphere (merid North)) @
  concat_pV (ap S2_to_TwoSphere (merid North)))) =
ap (ap S2_to_TwoSphere) (concat_pV (merid North)) @
surf
  lhs_V refine (1 @@ (1 @@ (1 @@
                              (concat_pV_inverse2 (ap S2_to_TwoSphere (merid North))
                                  _
                                  (Susp_rec_beta_merid North))))).
ap
  (fun x : Susp (Susp Empty) =>
   ap S2_to_TwoSphere (merid x @ (merid North)^))
  (merid North @ (merid South)^) @
(ap_pp S2_to_TwoSphere (merid North) (merid North)^ @
 ((1 @@ ap_V S2_to_TwoSphere (merid North)) @
  ((Susp_rec_beta_merid North @@
    inverse2 (Susp_rec_beta_merid North)) @
   concat_pV
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) North)))) =
ap (ap S2_to_TwoSphere) (concat_pV (merid North)) @
surf
  lhs refine (@concat_Ap (Sphere 1) _
                      (fun x => ap S2_to_TwoSphere (merid x @ (merid North)^))
                      (fun x => Susp_rec 1 1 
                                (Susp_rec surf 1 
                                Empty_rec) x 
                                @ 1)
                      (fun x => ap_pp S2_to_TwoSphere (merid x) (merid North)^ 
                                @ ((1 @@ ap_V S2_to_TwoSphere (merid North)) 
                                @ ((Susp_rec_beta_merid x 
                                   @@ inverse2 (Susp_rec_beta_merid North)) 
                                @ 1)))
                      North North (merid North @ (merid South)^)).
(ap_pp S2_to_TwoSphere (merid North) (merid North)^ @
 ((1 @@ ap_V S2_to_TwoSphere (merid North)) @
  ((Susp_rec_beta_merid North @@
    inverse2 (Susp_rec_beta_merid North)) @ 1))) @
ap
  (fun x : Sphere 1 =>
   Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x @ 1)
  (merid North @ (merid South)^) =
ap (ap S2_to_TwoSphere) (concat_pV (merid North)) @
surf f_ap.
ap_pp S2_to_TwoSphere (merid North) (merid North)^ @
((1 @@ ap_V S2_to_TwoSphere (merid North)) @
 ((Susp_rec_beta_merid North @@
   inverse2 (Susp_rec_beta_merid North)) @ 1)) =
ap (ap S2_to_TwoSphere) (concat_pV (merid North))
ap
  (fun x : Sphere 1 =>
   Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x @ 1)
  (merid North @ (merid South)^) = surf
  {
ap_pp S2_to_TwoSphere (merid North) (merid North)^ @
((1 @@ ap_V S2_to_TwoSphere (merid North)) @
 ((Susp_rec_beta_merid North @@
   inverse2 (Susp_rec_beta_merid North)) @ 1)) =
ap (ap S2_to_TwoSphere) (concat_pV (merid North)) rhs_V refine (ap_pp_concat_pV _ _).
ap_pp S2_to_TwoSphere (merid North) (merid North)^ @
((1 @@ ap_V S2_to_TwoSphere (merid North)) @
 ((Susp_rec_beta_merid North @@
   inverse2 (Susp_rec_beta_merid North)) @ 1)) =
ap_pp S2_to_TwoSphere (merid North) (merid North)^ @
((1 @@ ap_V S2_to_TwoSphere (merid North)) @
 concat_pV (ap S2_to_TwoSphere (merid North)))
    exact (1 @@ (1 @@ (concat_pV_inverse2 _ _ _))). }
ap
  (fun x : Sphere 1 =>
   Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x @ 1)
  (merid North @ (merid South)^) = surf
  lhs_V refine (concat2_ap_ap (Susp_rec 1 1 (Susp_rec surf 1
                                         Empty_rec)) 
                         (fun _ => 1) 
                         (merid North @ (merid South)^)).
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid North @ (merid South)^) @@
ap (fun _ : Susp (Susp Empty) => 1)
  (merid North @ (merid South)^) = surf
  lhs refine (ap (fun w => _ @@ w) (ap_const _ _)).
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid North @ (merid South)^) @@ 1 = surf
  lhs rapply whiskerR_p1_1.
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid North @ (merid South)^) = surf
  lhs refine (ap_pp _ (merid North) (merid South)^).
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid North) @
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid South)^ = surf
  rhs_V rapply concat_p1.
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid North) @
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid South)^ = surf @ 1 f_ap.
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid North) = surf
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid South)^ = 1
  -
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid North) = surf exact (Susp_rec_beta_merid North).
  -
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid South)^ = 1 lhs rapply ap_V.
(ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
   (merid South))^ = 1 refine (@inverse2 _ _ _ _ 1 _).
ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
  (merid South) = 1
    exact (Susp_rec_beta_merid South).
Defined.

Definition issect_S2_to_TwoSphere : TwoSphere_to_S2 o S2_to_TwoSphere == idmap.
TwoSphere_to_S2 o S2_to_TwoSphere == idmap
Proof.
TwoSphere_to_S2 o S2_to_TwoSphere == idmap
  intro x.
x: Sphere 2
TwoSphere_to_S2 (S2_to_TwoSphere x) = x
  refine ((Susp_rec_eta_homot (TwoSphere_to_S2 o S2_to_TwoSphere) x) @ _).
x: Sphere 2
Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
  (TwoSphere_to_S2 (S2_to_TwoSphere South))
  (fun x : Susp (Susp Empty) =>
   ap
     (fun x0 : Sphere 2 =>
      TwoSphere_to_S2 (S2_to_TwoSphere x0)) (merid x))
  x = x symmetry.
x: Sphere 2
x =
Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
  (TwoSphere_to_S2 (S2_to_TwoSphere South))
  (fun x : Susp (Susp Empty) =>
   ap
     (fun x0 : Sphere 2 =>
      TwoSphere_to_S2 (S2_to_TwoSphere x0)) (merid x))
  x
  generalize dependent x.
forall x : Sphere 2,
x =
Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
  (TwoSphere_to_S2 (S2_to_TwoSphere South))
  (fun x0 : Susp (Susp Empty) =>
   ap
     (fun x1 : Sphere 2 =>
      TwoSphere_to_S2 (S2_to_TwoSphere x1)) (merid x0))
  x
  refine (Susp_ind _ 1 (merid North)^ _).
forall x : Susp (Susp Empty),
transport
  (fun y : Susp (Susp (Susp Empty)) =>
   y =
   Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
     (TwoSphere_to_S2 (S2_to_TwoSphere South))
     (fun x0 : Susp (Susp Empty) =>
      ap
        (fun x1 : Sphere 2 =>
         TwoSphere_to_S2 (S2_to_TwoSphere x1))
        (merid x0)) y) (merid x) 1 = (merid North)^
  intro x.
x: Susp (Susp Empty)
transport
  (fun y : Susp (Susp (Susp Empty)) =>
   y =
   Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
     (TwoSphere_to_S2 (S2_to_TwoSphere South))
     (fun x : Susp (Susp Empty) =>
      ap
        (fun x0 : Sphere 2 =>
         TwoSphere_to_S2 (S2_to_TwoSphere x0))
        (merid x)) y) (merid x) 1 = (merid North)^
  refine ((transport_paths_FlFr (f := fun y => y) _ _) @ _).
x: Susp (Susp Empty)
((ap idmap (merid x))^ @ 1) @
ap
  (Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
     (TwoSphere_to_S2 (S2_to_TwoSphere South))
     (fun x : Susp (Susp Empty) =>
      ap
        (fun x0 : Sphere 2 =>
         TwoSphere_to_S2 (S2_to_TwoSphere x0))
        (merid x))) (merid x) = (merid North)^
  rewrite_moveR_Vp_p.
x: Susp (Susp Empty)
1 @
ap
  (Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
     (TwoSphere_to_S2 (S2_to_TwoSphere South))
     (fun x : Susp (Susp Empty) =>
      ap
        (fun x0 : Sphere 2 =>
         TwoSphere_to_S2 (S2_to_TwoSphere x0))
        (merid x))) (merid x) =
ap idmap (merid x) @ (merid North)^ refine ((concat_1p _) @ _).
x: Susp (Susp Empty)
ap
  (Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
     (TwoSphere_to_S2 (S2_to_TwoSphere South))
     (fun x : Susp (Susp Empty) =>
      ap
        (fun x0 : Sphere 2 =>
         TwoSphere_to_S2 (S2_to_TwoSphere x0))
        (merid x))) (merid x) =
ap idmap (merid x) @ (merid North)^
  refine (_ @ (ap (fun w => w @ _) (ap_idmap _)^)).
x: Susp (Susp Empty)
ap
  (Susp_rec (TwoSphere_to_S2 (S2_to_TwoSphere North))
     (TwoSphere_to_S2 (S2_to_TwoSphere South))
     (fun x : Susp (Susp Empty) =>
      ap
        (fun x0 : Sphere 2 =>
         TwoSphere_to_S2 (S2_to_TwoSphere x0))
        (merid x))) (merid x) =
merid x @ (merid North)^
  refine ((Susp_rec_beta_merid _) @ _).
x: Susp (Susp Empty)
ap
  (fun x : Sphere 2 =>
   TwoSphere_to_S2 (S2_to_TwoSphere x)) (merid x) =
merid x @ (merid North)^
  path_via (ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x))).
x: Susp (Susp Empty)
ap
  (fun x : Sphere 2 =>
   TwoSphere_to_S2 (S2_to_TwoSphere x)) (merid x) =
ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x))
x: Susp (Susp Empty)
ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x)) =
merid x @ (merid North)^
  {
x: Susp (Susp Empty)
ap
  (fun x : Sphere 2 =>
   TwoSphere_to_S2 (S2_to_TwoSphere x)) (merid x) =
ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x)) apply (ap_compose S2_to_TwoSphere TwoSphere_to_S2 (merid x)). }
x: Susp (Susp Empty)
ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x)) =
merid x @ (merid North)^
  path_via (ap TwoSphere_to_S2 
               (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x)).
x: Susp (Susp Empty)
ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x)) =
ap TwoSphere_to_S2
  (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x)
x: Susp (Susp Empty)
ap TwoSphere_to_S2
  (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x) =
merid x @ (merid North)^ 
  {
x: Susp (Susp Empty)
ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x)) =
ap TwoSphere_to_S2
  (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x) repeat f_ap.
x: Susp (Susp Empty)
ap S2_to_TwoSphere (merid x) =
Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x apply Susp_rec_beta_merid. }
x: Susp (Susp Empty)
ap TwoSphere_to_S2
  (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x) =
merid x @ (merid North)^
  symmetry.
x: Susp (Susp Empty)
merid x @ (merid North)^ =
ap TwoSphere_to_S2
  (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x) generalize dependent x.
forall x : Susp (Susp Empty),
merid x @ (merid North)^ =
ap TwoSphere_to_S2
  (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x) 

  simple refine (Susp_ind _ (concat_pV (merid North)) _ _).
(fun y : Susp (Susp Empty) =>
 merid y @ (merid North)^ =
 ap TwoSphere_to_S2
   (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) y)) South
forall x : Susp Empty,
transport
  (fun y : Susp (Susp Empty) =>
   merid y @ (merid North)^ =
   ap TwoSphere_to_S2
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) y))
  (merid x) (concat_pV (merid North)) = ?H_S
  -
(fun y : Susp (Susp Empty) =>
 merid y @ (merid North)^ =
 ap TwoSphere_to_S2
   (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) y)) South refine (_ @ (concat_pV (merid North))).
merid South @ (merid North)^ =
merid North @ (merid North)^ 
    apply (ap (fun w => merid w @ (merid North)^) (merid South)^).
  -
forall x : Susp Empty,
transport
  (fun y : Susp (Susp Empty) =>
   merid y @ (merid North)^ =
   ap TwoSphere_to_S2
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) y))
  (merid x) (concat_pV (merid North)) =
ap
  (fun w : Susp (Susp Empty) =>
   merid w @ (merid North)^) (merid South)^ @
concat_pV (merid North) intro x.
x: Susp Empty
transport
  (fun y : Susp (Susp Empty) =>
   merid y @ (merid North)^ =
   ap TwoSphere_to_S2
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) y))
  (merid x) (concat_pV (merid North)) =
ap
  (fun w : Susp (Susp Empty) =>
   merid w @ (merid North)^) (merid South)^ @
concat_pV (merid North)
    refine ((transport_paths_FlFr (merid x) (concat_pV (merid North))) @ _).
x: Susp Empty
((ap
    (fun x : Susp (Susp Empty) =>
     merid x @ (merid North)^) (merid x))^ @
 concat_pV (merid North)) @
ap
  (fun x : Susp (Susp Empty) =>
   ap TwoSphere_to_S2
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x))
  (merid x) =
ap
  (fun w : Susp (Susp Empty) =>
   merid w @ (merid North)^) (merid South)^ @
concat_pV (merid North)
    rewrite_moveR_Vp_p.
x: Susp Empty
concat_pV (merid North) @
ap
  (fun x : Susp (Susp Empty) =>
   ap TwoSphere_to_S2
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x))
  (merid x) =
(ap
   (fun x : Susp (Susp Empty) =>
    merid x @ (merid North)^) (merid x) @
 ap
   (fun w : Susp (Susp Empty) =>
    merid w @ (merid North)^) (merid South)^) @
concat_pV (merid North) symmetry.
x: Susp Empty
(ap
   (fun x : Susp (Susp Empty) =>
    merid x @ (merid North)^) (merid x) @
 ap
   (fun w : Susp (Susp Empty) =>
    merid w @ (merid North)^) (merid South)^) @
concat_pV (merid North) =
concat_pV (merid North) @
ap
  (fun x : Susp (Susp Empty) =>
   ap TwoSphere_to_S2
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x))
  (merid x) refine ((dpath_path_lr _ _ _)^-1 _).
x: Susp Empty
transport (fun x : North = North => x = x)
  (concat_pV (merid North))
  (ap
     (fun x : Susp (Susp Empty) =>
      merid x @ (merid North)^) (merid x) @
   ap
     (fun w : Susp (Susp Empty) =>
      merid w @ (merid North)^) (merid South)^) =
ap
  (fun x : Susp (Susp Empty) =>
   ap TwoSphere_to_S2
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x))
  (merid x)
    refine ((ap (transport _ _) (ap_pp _ (merid x) (merid South)^)^) @ _).
x: Susp Empty
transport (fun x : North = North => x = x)
  (concat_pV (merid North))
  (ap
     (fun x : Susp (Susp Empty) =>
      merid x @ (merid North)^)
     (merid x @ (merid South)^)) =
ap
  (fun x : Susp (Susp Empty) =>
   ap TwoSphere_to_S2
     (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x))
  (merid x)
    refine (_ @ (ap_compose (Susp_rec 1 1 
                              (Susp_rec surf 1 
                                Empty_rec)) 
                            (ap TwoSphere_to_S2) (merid x))^).
x: Susp Empty
transport (fun x : North = North => x = x)
  (concat_pV (merid North))
  (ap
     (fun x : Susp (Susp Empty) =>
      merid x @ (merid North)^)
     (merid x @ (merid South)^)) =
ap (ap TwoSphere_to_S2)
  (ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec))
     (merid x))
    refine (_ @ (ap (ap02 TwoSphere_to_S2) (Susp_rec_beta_merid _)^)).
x: Susp Empty
transport (fun x : North = North => x = x)
  (concat_pV (merid North))
  (ap
     (fun x : Susp (Susp Empty) =>
      merid x @ (merid North)^)
     (merid x @ (merid South)^)) =
ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec x)
    symmetry.
x: Susp Empty
ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec x) =
transport (fun x : North = North => x = x)
  (concat_pV (merid North))
  (ap
     (fun x : Susp (Susp Empty) =>
      merid x @ (merid North)^)
     (merid x @ (merid South)^)) generalize dependent x.
forall x : Susp Empty,
ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec x) =
transport (fun x0 : North = North => x0 = x0)
  (concat_pV (merid North))
  (ap
     (fun x0 : Susp (Susp Empty) =>
      merid x0 @ (merid North)^)
     (merid x @ (merid South)^))

    simple refine (Susp_ind _ _ _ _).
(fun y : Susp Empty =>
 ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec y) =
 transport (fun x : North = North => x = x)
   (concat_pV (merid North))
   (ap
      (fun x : Susp (Susp Empty) =>
       merid x @ (merid North)^)
      (merid y @ (merid South)^))) North
(fun y : Susp Empty =>
 ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec y) =
 transport (fun x : North = North => x = x)
   (concat_pV (merid North))
   (ap
      (fun x : Susp (Susp Empty) =>
       merid x @ (merid North)^)
      (merid y @ (merid South)^))) South
forall x : Empty,
transport
  (fun y : Susp Empty =>
   ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec y) =
   transport (fun x0 : North = North => x0 = x0)
     (concat_pV (merid North))
     (ap
        (fun x0 : Susp (Susp Empty) =>
         merid x0 @ (merid North)^)
        (merid y @ (merid South)^))) (merid x) ?H_N =
?H_S
    +
(fun y : Susp Empty =>
 ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec y) =
 transport (fun x : North = North => x = x)
   (concat_pV (merid North))
   (ap
      (fun x : Susp (Susp Empty) =>
       merid x @ (merid North)^)
      (merid y @ (merid South)^))) North refine (TwoSphere_rec_beta_surf _ _ _).
    +
(fun y : Susp Empty =>
 ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec y) =
 transport (fun x : North = North => x = x)
   (concat_pV (merid North))
   (ap
      (fun x : Susp (Susp Empty) =>
       merid x @ (merid North)^)
      (merid y @ (merid South)^))) South refine (_ @ (ap (fun w => transport _ _ (ap _ w))
                      (concat_pV (merid South))^)).
ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec South) =
transport (fun x : North = North => x = x)
  (concat_pV (merid North))
  (ap
     (fun x : Susp (Susp Empty) =>
      merid x @ (merid North)^) 1)
      refine (_ @ (transport_paths_lr _ _)^).
ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec South) =
((concat_pV (merid North))^ @
 ap
   (fun x : Susp (Susp Empty) =>
    merid x @ (merid North)^) 1) @
concat_pV (merid North)
      refine (_ @ (ap (fun w => w @ _) (concat_p1 _)^)).
ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec South) =
(concat_pV (merid North))^ @ concat_pV (merid North)
      refine (concat_Vp _)^.
    +
forall x : Empty,
transport
  (fun y : Susp Empty =>
   ap02 TwoSphere_to_S2 (Susp_rec surf 1 Empty_rec y) =
   transport (fun x0 : North = North => x0 = x0)
     (concat_pV (merid North))
     (ap
        (fun x0 : Susp (Susp Empty) =>
         merid x0 @ (merid North)^)
        (merid y @ (merid South)^))) (merid x)
  (TwoSphere_rec_beta_surf (Sphere 2) North
     (transport (fun x0 : North = North => x0 = x0)
        (concat_pV (merid North))
        (ap
           (fun u : Susp (Susp Empty) =>
            merid u @ (merid North)^)
           (merid North @ (merid South)^)))) =
(((concat_Vp (concat_pV (merid North)))^ @
  ap
    (fun
       w : ap TwoSphere_to_S2
             (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec)
                North) = merid North @ (merid North)^
     => w @ concat_pV (merid North))
    (concat_p1 (concat_pV (merid North))^)^) @
 (transport_paths_lr (concat_pV (merid North))
    (ap
       (fun x0 : Susp (Susp Empty) =>
        merid x0 @ (merid North)^) 1))^) @
ap
  (fun w : North = North =>
   transport (fun x0 : North = North => x0 = x0)
     (concat_pV (merid North))
     (ap
        (fun x0 : Susp (Susp Empty) =>
         merid x0 @ (merid North)^) w))
  (concat_pV (merid South))^ apply Empty_ind.
Defined.

Global Instance isequiv_S2_to_TwoSphere : IsEquiv (S2_to_TwoSphere) | 0.
IsEquiv S2_to_TwoSphere
Proof.
IsEquiv S2_to_TwoSphere
  apply isequiv_adjointify with TwoSphere_to_S2.
(fun x : TwoSphere =>
 S2_to_TwoSphere (TwoSphere_to_S2 x)) == idmap
(fun x : Sphere 2 =>
 TwoSphere_to_S2 (S2_to_TwoSphere x)) == idmap
  -
(fun x : TwoSphere =>
 S2_to_TwoSphere (TwoSphere_to_S2 x)) == idmap apply issect_TwoSphere_to_S2.
  -
(fun x : Sphere 2 =>
 TwoSphere_to_S2 (S2_to_TwoSphere x)) == idmap apply issect_S2_to_TwoSphere.
Defined.

Definition equiv_S2_TwoSphere : Sphere 2 <~> TwoSphere
  := Build_Equiv _ _ _ isequiv_S2_to_TwoSphere.

(** ** Truncation and connectedness of spheres. *)

(** S0 is 0-truncated. *)
Global Instance istrunc_s0 : IsHSet (Sphere 0).
IsHSet (Sphere 0)
Proof.
IsHSet (Sphere 0)
  srapply (istrunc_isequiv_istrunc _ S0_to_Bool^-1).
Defined.

(** S1 is 1-truncated. *)
Global Instance istrunc_s1 `{Univalence} : IsTrunc 1 (Sphere 1).
H: Univalence
IsTrunc 1 (Sphere 1)
Proof.
H: Univalence
IsTrunc 1 (Sphere 1)
  srapply (istrunc_isequiv_istrunc _ S1_to_Circle^-1).
Defined.

Global Instance isconnected_sn n : IsConnected n.+1 (Sphere n.+2).
n: trunc_index
IsConnected (Tr n.+1) (Sphere n.+2)
Proof.
n: trunc_index
IsConnected (Tr n.+1) (Sphere n.+2)
  induction n.
IsConnected (Tr (-1)) (Sphere 0)
n: trunc_index
IHn: IsConnected (Tr n.+1) (Sphere n.+2)
IsConnected (Tr n.+2) (Sphere n.+3)
  {
IsConnected (Tr (-1)) (Sphere 0) srapply contr_inhabited_hprop.
Tr (-1) (Sphere 0)
    apply tr, North. }
n: trunc_index
IHn: IsConnected (Tr n.+1) (Sphere n.+2)
IsConnected (Tr n.+2) (Sphere n.+3)
  apply isconnected_susp.
Defined.

(** ** Truncatedness via spheres  *)

(** We show here that a type is n-truncated if and only if every map from the (n+1)-sphere into it is null-homotopic.  (One direction of this is of course the assertion that the (n+1)-sphere is n-connected.) *)

(** TODO: re-type these lemmas in terms of truncation. *)

Fixpoint allnullhomot_trunc {n : trunc_index} {X : Type} `{IsTrunc n X}
  (f : Sphere n.+1 -> X) {struct n}
: NullHomotopy f.
allnullhomot_trunc: forall (n : trunc_index)
(X : Type),
IsTrunc n X ->
forall f : Sphere n.+1 -> X,
NullHomotopy f
n: trunc_index
X: Type
IsTrunc0: IsTrunc n X
f: Sphere n.+1 -> X
NullHomotopy f
Proof.
allnullhomot_trunc: forall (n : trunc_index)
(X : Type),
IsTrunc n X ->
forall f : Sphere n.+1 -> X,
NullHomotopy f
n: trunc_index
X: Type
IsTrunc0: IsTrunc n X
f: Sphere n.+1 -> X
NullHomotopy f
  destruct n as [ | n'].
allnullhomot_trunc: forall (n : trunc_index)
(X : Type),
IsTrunc n X ->
forall f : Sphere n.+1 -> X,
NullHomotopy f
X: Type
IsTrunc0: Contr X
f: Sphere (-1) -> X
NullHomotopy f
allnullhomot_trunc: forall (n : trunc_index)
(X : Type),
IsTrunc n X ->
forall f : Sphere n.+1 -> X,
NullHomotopy f
n': trunc_index
X: Type
IsTrunc0: IsTrunc n'.+1 X
f: Sphere n'.+2 -> X
NullHomotopy f
  -
allnullhomot_trunc: forall (n : trunc_index)
(X : Type),
IsTrunc n X ->
forall f : Sphere n.+1 -> X,
NullHomotopy f
X: Type
IsTrunc0: Contr X
f: Sphere (-1) -> X
NullHomotopy f exists (center X).
allnullhomot_trunc: forall (n : trunc_index)
(X : Type),
IsTrunc n X ->
forall f : Sphere n.+1 -> X,
NullHomotopy f
X: Type
IsTrunc0: Contr X
f: Sphere (-1) -> X
forall x : Sphere (-1), f x = center X intros [].
  -
allnullhomot_trunc: forall (n : trunc_index)
(X : Type),
IsTrunc n X ->
forall f : Sphere n.+1 -> X,
NullHomotopy f
n': trunc_index
X: Type
IsTrunc0: IsTrunc n'.+1 X
f: Sphere n'.+2 -> X
NullHomotopy f apply nullhomot_susp_from_paths.
allnullhomot_trunc: forall (n : trunc_index)
(X : Type),
IsTrunc n X ->
forall f : Sphere n.+1 -> X,
NullHomotopy f
n': trunc_index
X: Type
IsTrunc0: IsTrunc n'.+1 X
f: Sphere n'.+2 -> X
NullHomotopy
  (fun
     x : match n' with
         | -2 => Empty
         | _.+1 =>
             Susp
               ((fix Sphere 
                 (n : trunc_index) : Type :=
                 match n with
                 | (_.+1 as n').+1 => Susp (Sphere n')
                 | _ => Empty
                 end) n')
         end => ap f (merid x))
    rapply allnullhomot_trunc.
Defined.

Fixpoint istrunc_allnullhomot {n : trunc_index} {X : Type}
  (HX : forall (f : Sphere n.+2 -> X), NullHomotopy f) {struct n}
: IsTrunc n.+1 X.
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
n: trunc_index
X: Type
HX: forall f : Sphere n.+2 -> X, NullHomotopy f
IsTrunc n.+1 X
Proof.
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
n: trunc_index
X: Type
HX: forall f : Sphere n.+2 -> X, NullHomotopy f
IsTrunc n.+1 X
  destruct n as [ | n'].
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
X: Type
HX: forall f : Sphere 0 -> X, NullHomotopy f
IsHProp X
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
n': trunc_index
X: Type
HX: forall f : Sphere n'.+3 -> X, NullHomotopy f
IsTrunc n'.+2 X
  - (* n = -2 *)
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
X: Type
HX: forall f : Sphere 0 -> X, NullHomotopy f
IsHProp X apply hprop_allpath.
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
X: Type
HX: forall f : Sphere 0 -> X, NullHomotopy f
forall x y : X, x = y
    intros x0 x1.
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
X: Type
HX: forall f : Sphere 0 -> X, NullHomotopy f
x0, x1: X
x0 = x1 set (f := (fun b => if (S0_to_Bool b) then x0 else x1)).
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
X: Type
HX: forall f : Sphere 0 -> X, NullHomotopy f
x0, x1: X
f:= fun b : Sphere 0 => if S0_to_Bool b then x0 else x1: Sphere 0 -> X
x0 = x1
    set (n := HX f).
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
X: Type
HX: forall f : Sphere 0 -> X, NullHomotopy f
x0, x1: X
f:= fun b : Sphere 0 => if S0_to_Bool b then x0 else x1: Sphere 0 -> X
n:= HX f: NullHomotopy f
x0 = x1 exact (n.2 North @ (n.2 South)^).
  - (* n ≥ -1 *)
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
n': trunc_index
X: Type
HX: forall f : Sphere n'.+3 -> X, NullHomotopy f
IsTrunc n'.+2 X apply istrunc_S; intros x0 x1.
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
n': trunc_index
X: Type
HX: forall f : Sphere n'.+3 -> X, NullHomotopy f
x0, x1: X
IsTrunc n'.+1 (x0 = x1)
    apply (istrunc_allnullhomot n').
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
n': trunc_index
X: Type
HX: forall f : Sphere n'.+3 -> X, NullHomotopy f
x0, x1: X
forall f : Sphere n'.+2 -> x0 = x1, NullHomotopy f
    intro f.
istrunc_allnullhomot: forall (n : trunc_index)
(X : Type),
(forall f : Sphere n.+2 -> X,
 NullHomotopy f) ->
IsTrunc n.+1 X
n': trunc_index
X: Type
HX: forall f : Sphere n'.+3 -> X, NullHomotopy f
x0, x1: X
f: Sphere n'.+2 -> x0 = x1
NullHomotopy f apply nullhomot_paths_from_susp, HX.
Defined.

(** Iterated loop spaces can be described using pointed maps from spheres.  The [n = 0] case of this is stated using Bool in [pmap_from_bool] above, and the [n = 1] case of this is stated using [Circle] in [pmap_from_circle_loops] in Circle.v. *)
Definition pmap_from_psphere_iterated_loops `{Funext} (n : nat) (X : pType)
  : (psphere n ->** X) <~>* iterated_loops n X.
H: Funext
n: nat
X: pType
(psphere n ->** X) <~>* iterated_loops n X
Proof.
H: Funext
n: nat
X: pType
(psphere n ->** X) <~>* iterated_loops n X
  induction n as [|n IHn]; simpl.
H: Funext
X: pType
(psphere 0 ->** X) <~>* X
H: Funext
n: nat
X: pType
IHn: (psphere n ->** X) <~>* iterated_loops n X
(psphere n.+1 ->** X) <~>* loops (iterated_loops n X)
  -
H: Funext
X: pType
(psphere 0 ->** X) <~>* X exact (pmap_from_bool X o*E pequiv_pequiv_precompose pequiv_S0_Bool^-1* ).
  -
H: Funext
n: nat
X: pType
IHn: (psphere n ->** X) <~>* iterated_loops n X
(psphere n.+1 ->** X) <~>* loops (iterated_loops n X) refine (emap loops IHn o*E _).
H: Funext
n: nat
X: pType
IHn: (psphere n ->** X) <~>* iterated_loops n X
(psphere n.+1 ->** X) <~>* loops (psphere n ->** X)
    refine (_ o*E loop_susp_adjoint (psphere n) _).
H: Funext
n: nat
X: pType
IHn: (psphere n ->** X) <~>* iterated_loops n X
(psphere n ->** loops X) <~>* loops (psphere n ->** X)
    symmetry; apply equiv_loops_ppforall.
Defined.