HoTT.Spaces.Spheres.v.alectryon.json

From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
Require Import WildCat.Equiv.
Require Import Homotopy.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.

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
  snapply 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.

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
    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
    lhs napply Susp_rec_beta_zigzag.(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 snapply Susp_ind_FFlr; simpl.North = North
North = South
forall x : Susp Empty,
ap Circle_to_S1 (ap S1_to_Circle (merid x)) @ ?Goal0 = ?Goal @ merid x
    1: reflexivity.North = South
forall x : Susp Empty,
ap Circle_to_S1 (ap S1_to_Circle (merid x)) @ ?Goal = 1 @ merid x
    1: exact (merid South).forall x : Susp Empty,
ap Circle_to_S1 (ap S1_to_Circle (merid x)) @ merid South = 1 @ merid x
    intro x.x: Susp Empty
ap Circle_to_S1 (ap S1_to_Circle (merid x)) @ merid South = 1 @ merid x
    unfold S1_to_Circle; rewrite (Susp_rec_beta_merid x).x: Susp Empty
ap Circle_to_S1 (if S0_to_Bool x then loop else 1) @ merid South =
1 @ merid x
    revert x.forall x : Susp Empty,
ap Circle_to_S1 (if S0_to_Bool x then loop else 1) @ merid South =
1 @ merid x change (Susp Empty) with (Sphere 0).forall x : Sphere 0,
ap Circle_to_S1 (if S0_to_Bool x then loop else 1) @ merid South =
1 @ merid x
    apply (equiv_ind (S0_to_Bool ^-1)); intros x.x: Bool
ap Circle_to_S1 (if S0_to_Bool (S0_to_Bool^-1 x) then loop else 1) @
merid South = 1 @ merid (S0_to_Bool^-1 x)
    case x; simpl.x: Bool
ap Circle_to_S1 loop @ merid South = 1 @ merid North
x: Bool
1 @ merid South = 1 @ merid South
    2: reflexivity.x: Bool
ap Circle_to_S1 loop @ merid South = 1 @ merid North
    rhs napply concat_1p.x: Bool
ap Circle_to_S1 loop @ merid South = merid North
    unfold Circle_to_S1; rewrite Circle_rec_beta_loop.x: Bool
(merid North @ (merid South)^) @ merid South = merid North
    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: exact 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
  exact 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)^
  exact (((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 exact (@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 exact (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 exact (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 exact (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 exact (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
  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_ap_concat_pV _ _ _ (Susp_rec_beta_merid North)).ap
  (fun x : Susp (Susp Empty) => ap S2_to_TwoSphere (merid x @ (merid North)^))
  (merid North @ (merid South)^) @
(ap_pV (Susp_rec base base (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec)))
   (merid North) (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
  simpl.ap
  (fun x : Susp (Susp Empty) => ap S2_to_TwoSphere (merid x @ (merid North)^))
  (merid North @ (merid South)^) @
(ap_pV (Susp_rec base base (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec)))
   (merid North) (merid North) @
 ((Susp_rec_beta_merid North @@ inverse2 (Susp_rec_beta_merid North)) @ 1)) =
ap (ap S2_to_TwoSphere) (concat_pV (merid North)) @ surf
  lhs exact (concat_Ap (fun x => ap_pV S2_to_TwoSphere (merid x) (merid North)
                                  @ ((Susp_rec_beta_merid x
                                        @@ inverse2 (Susp_rec_beta_merid North))
                                       @ 1))
               (merid North @ (merid South)^)).(ap_pV S2_to_TwoSphere (merid North) (merid North) @
 ((Susp_rec_beta_merid North @@ inverse2 (Susp_rec_beta_merid North)) @ 1)) @
ap
  (fun x : Susp (Susp Empty) =>
   Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x @
   (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) North)^)
  (merid North @ (merid South)^) =
ap (ap S2_to_TwoSphere) (concat_pV (merid North)) @ surf
  f_ap.ap_pV S2_to_TwoSphere (merid North) (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 : Susp (Susp Empty) =>
   Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x @
   (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) North)^)
  (merid North @ (merid South)^) =
surf
  1: exact (ap_ap_concat_pV _ _ _ (Susp_rec_beta_merid North)).ap
  (fun x : Susp (Susp Empty) =>
   Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x @
   (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) North)^)
  (merid North @ (merid South)^) =
surf
  lhs_V exact (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 nrefine (ap (fun w => _ @@ w) (ap_const _ _)).ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec)) (merid North @ (merid South)^) @@
1 = surf
  lhs napply whiskerR_p1_1.ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec)) (merid North @ (merid South)^) =
surf
  rhs_V napply concat_p1.ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec)) (merid North @ (merid South)^) =
surf @ 1
  napply Susp_rec_beta_zigzag.
Defined. (* A bit slow, ~0.2s. *)

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_homotopic (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 x0 : Susp (Susp Empty) =>
   ap (fun x1 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x1)) (merid x0))
  x =
x symmetry.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
  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 x0 : Susp (Susp Empty) =>
      ap (fun x1 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x1))
        (merid x0))
     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 x0 : Susp (Susp Empty) =>
      ap (fun x1 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x1))
        (merid x0)))
  (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 x0 : Susp (Susp Empty) =>
      ap (fun x1 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x1))
        (merid x0)))
  (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 x0 : Susp (Susp Empty) =>
      ap (fun x1 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x1))
        (merid x0)))
  (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 x0 : Susp (Susp Empty) =>
      ap (fun x1 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x1))
        (merid x0)))
  (merid x) =
merid x @ (merid North)^
  refine ((Susp_rec_beta_merid _) @ _).x: Susp (Susp Empty)
ap (fun x0 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x0)) (merid x) =
merid x @ (merid North)^
  path_via (ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x))).x: Susp (Susp Empty)
ap (fun x0 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x0)) (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 x0 : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x0)) (merid x) =
ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x)) exact (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)^ 
    exact (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 x0 : Susp (Susp Empty) => merid x0 @ (merid North)^) (merid x))^ @
 concat_pV (merid North)) @
ap
  (fun x0 : Susp (Susp Empty) =>
   ap TwoSphere_to_S2 (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x0))
  (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 x0 : Susp (Susp Empty) =>
   ap TwoSphere_to_S2 (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x0))
  (merid x) =
(ap (fun x0 : Susp (Susp Empty) => merid x0 @ (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 x0 : Susp (Susp Empty) => merid x0 @ (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 x0 : Susp (Susp Empty) =>
   ap TwoSphere_to_S2 (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x0))
  (merid x) refine ((dpath_path_lr _ _ _)^-1 _).x: Susp Empty
transport (fun x0 : North = North => x0 = x0) (concat_pV (merid North))
  (ap (fun x0 : Susp (Susp Empty) => merid x0 @ (merid North)^) (merid x) @
   ap (fun w : Susp (Susp Empty) => merid w @ (merid North)^) (merid South)^) =
ap
  (fun x0 : Susp (Susp Empty) =>
   ap TwoSphere_to_S2 (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x0))
  (merid x)
    refine ((ap (transport _ _) (ap_pp _ (merid x) (merid South)^)^) @ _).x: Susp Empty
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)^)) =
ap
  (fun x0 : Susp (Susp Empty) =>
   ap TwoSphere_to_S2 (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x0))
  (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 x0 : North = North => x0 = x0) (concat_pV (merid North))
  (ap (fun x0 : Susp (Susp Empty) => merid x0 @ (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 x0 : North = North => x0 = x0) (concat_pV (merid North))
  (ap (fun x0 : Susp (Susp Empty) => merid x0 @ (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 x0 : North = North => x0 = x0) (concat_pV (merid North))
  (ap (fun x0 : Susp (Susp Empty) => merid x0 @ (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 exact (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.

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 exact issect_TwoSphere_to_S2.
  -(fun x : Sphere 2 => TwoSphere_to_S2 (S2_to_TwoSphere x)) == idmap exact 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. *)
Instance istrunc_s0 : IsHSet (Sphere 0).IsHSet (Sphere 0)
Proof.IsHSet (Sphere 0)
  exact (istrunc_isequiv_istrunc _ S0_to_Bool^-1).
Defined.

(** S1 is 1-truncated. *)
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.

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)
  exact 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 (n0 : trunc_index) (X0 : Type),
IsTrunc n0 X0 -> forall f0 : Sphere n0.+1 -> X0, NullHomotopy f0
n: trunc_index
X: Type
IsTrunc0: IsTrunc n X
f: Sphere n.+1 -> X
NullHomotopy f
Proof.allnullhomot_trunc: forall (n0 : trunc_index) (X0 : Type),
IsTrunc n0 X0 -> forall f0 : Sphere n0.+1 -> X0, NullHomotopy f0
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) (X0 : Type),
IsTrunc n X0 -> forall f0 : Sphere n.+1 -> X0, NullHomotopy f0
X: Type
IsTrunc0: Contr X
f: Sphere (-1) -> X
NullHomotopy f
allnullhomot_trunc: forall (n : trunc_index) (X0 : Type),
IsTrunc n X0 -> forall f0 : Sphere n.+1 -> X0, NullHomotopy f0
n': trunc_index
X: Type
IsTrunc0: IsTrunc n'.+1 X
f: Sphere n'.+2 -> X
NullHomotopy f
  -allnullhomot_trunc: forall (n : trunc_index) (X0 : Type),
IsTrunc n X0 -> forall f0 : Sphere n.+1 -> X0, NullHomotopy f0
X: Type
IsTrunc0: Contr X
f: Sphere (-1) -> X
NullHomotopy f exists (center X).allnullhomot_trunc: forall (n : trunc_index) (X0 : Type),
IsTrunc n X0 -> forall f0 : Sphere n.+1 -> X0, NullHomotopy f0
X: Type
IsTrunc0: Contr X
f: Sphere (-1) -> X
forall x : Sphere (-1), f x = center X intros [].
  -allnullhomot_trunc: forall (n : trunc_index) (X0 : Type),
IsTrunc n X0 -> forall f0 : Sphere n.+1 -> X0, NullHomotopy f0
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) (X0 : Type),
IsTrunc n X0 -> forall f0 : Sphere n.+1 -> X0, NullHomotopy f0
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'0).+1 => Susp (Sphere n'0)
                   | _ => 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 (n0 : trunc_index) (X0 : Type),
(forall f : Sphere n0.+2 -> X0, NullHomotopy f) -> IsTrunc n0.+1 X0
n: trunc_index
X: Type
HX: forall f : Sphere n.+2 -> X, NullHomotopy f
IsTrunc n.+1 X
Proof.istrunc_allnullhomot: forall (n0 : trunc_index) (X0 : Type),
(forall f : Sphere n0.+2 -> X0, NullHomotopy f) -> IsTrunc n0.+1 X0
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) (X0 : Type),
(forall f : Sphere n.+2 -> X0, NullHomotopy f) -> IsTrunc n.+1 X0
X: Type
HX: forall f : Sphere 0 -> X, NullHomotopy f
IsHProp X
istrunc_allnullhomot: forall (n : trunc_index) (X0 : Type),
(forall f : Sphere n.+2 -> X0, NullHomotopy f) -> IsTrunc n.+1 X0
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) (X0 : Type),
(forall f : Sphere n.+2 -> X0, NullHomotopy f) -> IsTrunc n.+1 X0
X: Type
HX: forall f : Sphere 0 -> X, NullHomotopy f
IsHProp X apply hprop_allpath.istrunc_allnullhomot: forall (n : trunc_index) (X0 : Type),
(forall f : Sphere n.+2 -> X0, NullHomotopy f) -> IsTrunc n.+1 X0
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) (X0 : Type),
(forall f : Sphere n.+2 -> X0, NullHomotopy f) -> IsTrunc n.+1 X0
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) (X0 : Type),
(forall f0 : Sphere n.+2 -> X0, NullHomotopy f0) -> IsTrunc n.+1 X0
X: Type
HX: forall f0 : Sphere 0 -> X, NullHomotopy f0
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 (n0 : trunc_index) (X0 : Type),
(forall f0 : Sphere n0.+2 -> X0, NullHomotopy f0) -> IsTrunc n0.+1 X0
X: Type
HX: forall f0 : Sphere 0 -> X, NullHomotopy f0
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) (X0 : Type),
(forall f : Sphere n.+2 -> X0, NullHomotopy f) -> IsTrunc n.+1 X0
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) (X0 : Type),
(forall f : Sphere n.+2 -> X0, NullHomotopy f) -> IsTrunc n.+1 X0
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) (X0 : Type),
(forall f : Sphere n.+2 -> X0, NullHomotopy f) -> IsTrunc n.+1 X0
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) (X0 : Type),
(forall f0 : Sphere n.+2 -> X0, NullHomotopy f0) -> IsTrunc n.+1 X0
n': trunc_index
X: Type
HX: forall f0 : Sphere n'.+3 -> X, NullHomotopy f0
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.