Timings for Spheres.v

(* -*- mode: coq; mode: visual-line -*- *)

Require Import Basics Types.

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.

Proof.

  simpl.

 apply (Susp_rec true false).

 intros [].

Defined.

Definition Bool_to_S0 : Bool -> (Sphere 0).

Proof.

  exact (fun b => if b then North else South).

Defined.

Global Instance isequiv_S0_to_Bool : IsEquiv (S0_to_Bool) | 0.

Proof.

  apply isequiv_adjointify with Bool_to_S0.

  -

 intros [ | ]; exact 1.

  -

 refine (Susp_ind _ 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.

Proof.

  snrapply Build_pEquiv'.

  -

 refine (_ oE (issig_pmap _ _)^-1%equiv).

    refine (_ oE (equiv_functor_sigma_pb (equiv_bool_rec_uncurried X))^-1%equiv); cbn.

    make_equiv_contr_basedpaths.

  -

 reflexivity.

Defined.

(** *** [Sphere 1] *)

Definition S1_to_Circle : (Sphere 1) -> Circle.

Proof.

  apply (Susp_rec Circle.base Circle.base).

  exact (fun x => if (S0_to_Bool x) then loop else 1).

Defined.

Definition Circle_to_S1 : Circle -> (Sphere 1).

Proof.

  apply (Circle_rec _ North).

  exact (merid North @ (merid South)^).

Defined.

Global Instance isequiv_S1_to_Circle : IsEquiv (S1_to_Circle) | 0.

Proof.

  apply isequiv_adjointify with Circle_to_S1.

  -

 refine (Circle_ind _ 1 _).

    nrapply transport_paths_FFlr'; apply equiv_p1_1q.

    refine (ap _ (Circle_rec_beta_loop _ _ _) @ _).

    refine (ap_pp _ _ (merid South)^ @ _).

    refine ((1 @@ ap_V _ _) @ _).

    refine ((_ @@ (ap inverse _)) @ _).

 1, 2: nrapply Susp_rec_beta_merid.

    simpl.

    apply concat_p1.

  -

 refine (Susp_ind (fun x => Circle_to_S1 (S1_to_Circle x) = x)
                     1 (merid South) _); intros x.

    nrapply transport_paths_FFlr'; symmetry.

    unfold S1_to_Circle; rewrite (Susp_rec_beta_merid x).

    revert x.

 change (Susp Empty) with (Sphere 0).

    apply (equiv_ind (S0_to_Bool ^-1)); intros x.

    case x; simpl.

    2: reflexivity.

    lhs nrapply concat_1p.

    unfold Circle_to_S1; rewrite Circle_rec_beta_loop.

    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, _].

Proof.

  srapply Build_pEquiv'.

  1: apply equiv_S1_Circle.

  reflexivity.

Defined.

(** *** [Sphere 2] *)

Definition S2_to_TwoSphere : (Sphere 2) -> TwoSphere.

Proof.

  apply (Susp_rec base base).

  apply (Susp_rec (idpath base) (idpath base)).

  apply (Susp_rec surf (idpath (idpath base))).

  apply Empty_rec.

Defined.

Definition TwoSphere_to_S2 : TwoSphere -> (Sphere 2).

Proof.

  apply (TwoSphere_rec (Sphere 2) North).

  refine (transport (fun x => x = x) (concat_pV (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.

Proof.

  refine (TwoSphere_ind _ 1 _).

 
  rhs_V rapply concat_p1.

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

  rhs rapply concat_1p.

  rhs refine (ap_compose (fun p => p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))
                          inverse
                          surf).

  refine (@ap _ _ (ap inverse) 1 _ _).

  rhs_V rapply concat2_ap_ap.

  rhs refine (ap (fun w => inverse2 surf @@ w)
                  (ap_compose (ap TwoSphere_to_S2) (ap S2_to_TwoSphere) surf)).

  lhs_V refine (concat_Vp_inverse2 _ _ surf).

  lhs rapply concat_p1.

  refine (ap (fun p : 1 = 1 => inverse2 surf @@ p) _).

  symmetry.

 lhs refine ((ap (ap (ap S2_to_TwoSphere))
                        (TwoSphere_rec_beta_surf (Sphere 2) North _))).

  lhs refine (ap_transport (concat_pV (merid North))
                        (fun z => @ap _ _ _ z z) 
                        (ap (fun u => merid u @ (merid North)^)
                            (merid North @ (merid South)^))).

  
  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)^))).

  apply transport_paths_FlFr'; symmetry.

  lhs_V refine (1 @@ ap_pp_concat_pV S2_to_TwoSphere (merid North)).

  lhs_V refine (1 @@ (1 @@ (1 @@
                              (concat_pV_inverse2 (ap S2_to_TwoSphere (merid North))
                                  _
                                  (Susp_rec_beta_merid North))))).

  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)^)).

 f_ap.

  {

 rhs_V refine (ap_pp_concat_pV _ _).

    exact (1 @@ (1 @@ (concat_pV_inverse2 _ _ _))).

 }

  lhs_V refine (concat2_ap_ap (Susp_rec 1 1 (Susp_rec surf 1
                                         Empty_rec)) 
                         (fun _ => 1) 
                         (merid North @ (merid South)^)).

  lhs refine (ap (fun w => _ @@ w) (ap_const _ _)).

  lhs rapply whiskerR_p1_1.

  lhs refine (ap_pp _ (merid North) (merid South)^).

  rhs_V rapply concat_p1.

 f_ap.

  -

 exact (Susp_rec_beta_merid North).

  -

 lhs rapply ap_V.

 refine (@inverse2 _ _ _ _ 1 _).

    exact (Susp_rec_beta_merid South).

Defined.

Definition issect_S2_to_TwoSphere : TwoSphere_to_S2 o S2_to_TwoSphere == idmap.

Proof.

  intro x.

  refine ((Susp_rec_eta_homot (TwoSphere_to_S2 o S2_to_TwoSphere) x) @ _).

 symmetry.

  generalize dependent x.

  refine (Susp_ind _ 1 (merid North)^ _).

  intro x.

  refine ((transport_paths_FlFr (f := fun y => y) _ _) @ _).

  rewrite_moveR_Vp_p.

 refine ((concat_1p _) @ _).

  refine (_ @ (ap (fun w => w @ _) (ap_idmap _)^)).

  refine ((Susp_rec_beta_merid _) @ _).

  path_via (ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x))).

  {

 apply (ap_compose S2_to_TwoSphere TwoSphere_to_S2 (merid x)).

 }

  path_via (ap TwoSphere_to_S2 
               (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x)).

 
  {

 repeat f_ap.

 apply Susp_rec_beta_merid.

 }

  symmetry.

 generalize dependent x.

 

  simple refine (Susp_ind _ (concat_pV (merid North)) _ _).

  -

 refine (_ @ (concat_pV (merid North))).

 
    apply (ap (fun w => merid w @ (merid North)^) (merid South)^).

  -

 intro x.

    refine ((transport_paths_FlFr (merid x) (concat_pV (merid North))) @ _).

    rewrite_moveR_Vp_p.

 symmetry.

 refine ((dpath_path_lr _ _ _)^-1 _).

    refine ((ap (transport _ _) (ap_pp _ (merid x) (merid South)^)^) @ _).

    refine (_ @ (ap_compose (Susp_rec 1 1 
                              (Susp_rec surf 1 
                                Empty_rec)) 
                            (ap TwoSphere_to_S2) (merid x))^).

    refine (_ @ (ap (ap02 TwoSphere_to_S2) (Susp_rec_beta_merid _)^)).

    symmetry.

 generalize dependent x.

    
    simple refine (Susp_ind _ _ _ _).

    +

 refine (TwoSphere_rec_beta_surf _ _ _).

    +

 refine (_ @ (ap (fun w => transport _ _ (ap _ w))
                      (concat_pV (merid South))^)).

      refine (_ @ (transport_paths_lr _ _)^).

      refine (_ @ (ap (fun w => w @ _) (concat_p1 _)^)).

      refine (concat_Vp _)^.

    +

 apply Empty_ind.

Defined.

Global Instance isequiv_S2_to_TwoSphere : IsEquiv (S2_to_TwoSphere) | 0.

Proof.

  apply isequiv_adjointify with TwoSphere_to_S2.

  -

 apply issect_TwoSphere_to_S2.

  -

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

Proof.

  srapply (istrunc_isequiv_istrunc _ S0_to_Bool^-1).

Defined.

(** S1 is 1-truncated. *)

Global Instance istrunc_s1 `{Univalence} : IsTrunc 1 (Sphere 1).

Proof.

  srapply (istrunc_isequiv_istrunc _ S1_to_Circle^-1).

Defined.

Global Instance isconnected_sn n : IsConnected n.+1 (Sphere n.+2).

Proof.

  induction n.

  {

 srapply contr_inhabited_hprop.

    apply tr, North.

 }

  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.

Proof.

  destruct n as [ | n'].

  -

 exists (center X).

 intros [].

  -

 apply nullhomot_susp_from_paths.

    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.

Proof.

  destruct n as [ | n'].

  -

 (* n = -2 *)

apply hprop_allpath.

    intros x0 x1.

 set (f := (fun b => if (S0_to_Bool b) then x0 else x1)).

    set (n := HX f).

 exact (n.2 North @ (n.2 South)^).

  -

 (* n ≥ -1 *)

apply istrunc_S; intros x0 x1.

    apply (istrunc_allnullhomot n').

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

Proof.

  induction n as [|n IHn]; simpl.

  -

 exact (pmap_from_bool X o*E pequiv_pequiv_precompose pequiv_S0_Bool^-1* ).

  -

 refine (emap loops IHn o*E _).

    refine (_ o*E loop_susp_adjoint (psphere n) _).

    symmetry; apply equiv_loops_ppforall.

Defined.