Add pmap_from_psphere_iterated_loops, and needed lemmas

theories/Homotopy/HSpace/Moduli.v

@@ -80,7 +80,7 @@ Lemma equiv_pmap_hspace `{Funext} {A : pType}
   (a : A) `{IsHSpace A} `{!IsEquiv (hspace_op a)}
   : (A ->* A) <~> (A ->* [A,a]).
 Proof.
-  apply equiv_pequiv_postcompose.
+  nrapply pequiv_pequiv_postcompose.
   rapply pequiv_hspace_left_op.
 Defined.
 
@@ -131,7 +131,7 @@ Proof.
   refine (_ oE equiv_iscohhspace_psect A).
   refine (_ oE (equiv_pequiv_pslice_psect _ _ _ hspace_ev_trivialization^*)^-1%equiv).
   refine (_ oE equiv_psect_psnd (A:=[A ->* A, pmap_idmap])).
-  refine (equiv_pequiv_postcompose _); symmetry.
+  refine (pequiv_pequiv_postcompose _); symmetry.
   rapply pequiv_hspace_left_op.
 Defined.
 

theories/Pointed/pEquiv.v

@@ -102,13 +102,24 @@ Proof.
   symmetry; apply peisretr.
 Defined.
 
-Definition equiv_pequiv_precompose `{Funext} {A B C : pType} (f : A <~>* B)
-  : (B ->* C) <~> (A ->* C)
-  := equiv_precompose_cat_equiv f.
+Definition pequiv_pequiv_precompose `{Funext} {A B C : pType} (f : A <~>* B)
+  : (B ->** C) <~>* (A ->** C).
+Proof.
+  srapply Build_pEquiv'.
+  - exact (equiv_precompose_cat_equiv f).
+  - (* By using [pelim f], we can avoid [Funext] in this part of the proof. *)
+    cbn; unfold "o*", point_pforall; cbn.
+    by pelim f.
+Defined.
 
-Definition equiv_pequiv_postcompose `{Funext} {A B C : pType} (f : B <~>* C)
-  : (A ->* B) <~> (A ->* C)
-  := equiv_postcompose_cat_equiv f.
+Definition pequiv_pequiv_postcompose `{Funext} {A B C : pType} (f : B <~>* C)
+  : (A ->** B) <~>* (A ->** C).
+Proof.
+  srapply Build_pEquiv'.
+  - exact (equiv_postcompose_cat_equiv f).
+  - cbn; unfold "o*", point_pforall; cbn.
+    by pelim f.
+Defined.
 
 Proposition equiv_pequiv_inverse `{Funext} {A B : pType}
   : (A <~>* B) <~> (B <~>* A).

theories/Pointed/pSect.v

@@ -30,7 +30,7 @@ Definition equiv_pequiv_pslice_psect `{Funext} {A B C : pType}
   : pSect f <~> pSect g.
 Proof.
   srapply equiv_functor_sigma'.
-  1: exact (equiv_pequiv_postcompose t).
+  1: exact (pequiv_pequiv_postcompose t).
   intro s; cbn.
   apply equiv_phomotopy_concat_l.
   refine ((pmap_compose_assoc _ _ _)^* @* _).

theories/Pointed/pSusp.v

@@ -3,6 +3,7 @@ Require Import Types.
 Require Import Pointed.Core.
 Require Import Pointed.Loops.
 Require Import Pointed.pTrunc.
+Require Import Pointed.pEquiv.
 Require Import Homotopy.Suspension.
 Require Import Homotopy.Freudenthal.
 Require Import Truncations.
@@ -241,25 +242,30 @@ Qed.
 (** Now we can finally construct the adjunction equivalence. *)
 
 Definition loop_susp_adjoint `{Funext} (A B : pType)
-  : (psusp A ->* B) <~> (A ->* loops B).
+  : (psusp A ->** B) <~>* (A ->** loops B).
 Proof.
-  refine (equiv_adjointify
-            (fun f => fmap loops f o* loop_susp_unit A)
-            (fun g => loop_susp_counit B o* fmap psusp g) _ _).
-  - intros g. apply path_pforall.
-    refine (pmap_prewhisker _ (fmap_comp loops _ _) @* _).
-    refine (pmap_compose_assoc _ _ _ @* _).
-    refine (pmap_postwhisker _ (loop_susp_unit_natural g)^* @* _).
-    refine ((pmap_compose_assoc _ _ _)^* @* _).
-    refine (pmap_prewhisker g (loop_susp_triangle1 B) @* _).
-    apply pmap_postcompose_idmap.
-  - intros f. apply path_pforall.
-    refine (pmap_postwhisker _ (fmap_comp psusp _ _) @* _).
-    refine ((pmap_compose_assoc _ _ _)^* @* _).
-    refine (pmap_prewhisker _ (loop_susp_counit_natural f)^* @* _).
-    refine (pmap_compose_assoc _ _ _ @* _).
-    refine (pmap_postwhisker f (loop_susp_triangle2 A) @* _).
-    apply pmap_precompose_idmap.
+  snrapply Build_pEquiv'.
+  - refine (equiv_adjointify
+              (fun f => fmap loops f o* loop_susp_unit A)
+              (fun g => loop_susp_counit B o* fmap psusp g) _ _).
+    + intros g. apply path_pforall.
+      refine (pmap_prewhisker _ (fmap_comp loops _ _) @* _).
+      refine (pmap_compose_assoc _ _ _ @* _).
+      refine (pmap_postwhisker _ (loop_susp_unit_natural g)^* @* _).
+      refine ((pmap_compose_assoc _ _ _)^* @* _).
+      refine (pmap_prewhisker g (loop_susp_triangle1 B) @* _).
+      apply pmap_postcompose_idmap.
+    + intros f. apply path_pforall.
+      refine (pmap_postwhisker _ (fmap_comp psusp _ _) @* _).
+      refine ((pmap_compose_assoc _ _ _)^* @* _).
+      refine (pmap_prewhisker _ (loop_susp_counit_natural f)^* @* _).
+      refine (pmap_compose_assoc _ _ _ @* _).
+      refine (pmap_postwhisker f (loop_susp_triangle2 A) @* _).
+      apply pmap_precompose_idmap.
+  - apply path_pforall.
+    unfold equiv_adjointify, equiv_fun.
+    nrapply (pmap_prewhisker _ fmap_loops_pconst @* _).
+    rapply cat_zero_l.
 Defined.
 
 (** And its naturality is easy. *)

theories/Spaces/BAut.v

@@ -276,14 +276,14 @@ Section ClassifyingMaps.
     : (Y ->* pBAut@{u v} F) <~> { p : { q : pSlice Y & forall y:Y, merely (hfiber q.2 y <~> F) } &
                                       pfiber p.1.2 <~>* F }
     := (equiv_sigma_pfibration_O (subuniverse_merely_equiv F))
-         oE equiv_pequiv_postcompose pequiv_pbaut_typeOp.
+         oE pequiv_pequiv_postcompose pequiv_pbaut_typeOp.
 
   (** When [Y] is connected, pointed maps into [pBAut F] correspond to maps into the universe sending the base point to [F]. *)
   Proposition equiv_pmap_pbaut_type_p `{Univalence}
               {Y : pType@{u}} {F : Type@{u}} `{IsConnected 0 Y}
     : (Y ->* pBAut F) <~> (Y ->* [Type@{u}, F]).
   Proof.
-    refine (_ oE equiv_pequiv_postcompose pequiv_pbaut_typeOp).
+    refine (_ oE pequiv_pequiv_postcompose pequiv_pbaut_typeOp).
     rapply equiv_pmap_typeO_type_connected.
   Defined.
 

theories/Spaces/Circle.v

@@ -1,5 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
+Require Import Pointed.Core Pointed.Loops Pointed.pEquiv.
 Require Import HSet.
 Require Import Spaces.Pos Spaces.Int.
 Require Import Colimits.Coeq.
@@ -8,6 +9,7 @@ Require Import Cubical.DPath.
 
 (** * Theorems about the [Circle]. *)
 
+Local Open Scope pointed_scope.
 Local Open Scope path_scope.
 
 Generalizable Variables X A B f g n.
@@ -77,6 +79,8 @@ Defined.
 (** The [Circle] is pointed by [base]. *)
 Global Instance ispointed_Circle : IsPointed Circle := base.
 
+Definition pCircle : pType := [Circle, base].
+
 (** ** The loop space of the [Circle] is the Integers [Int]
 
   This is the encode-decode style proof a la Licata-Shulman. *)
@@ -257,13 +261,25 @@ Proof.
     srapply Circle_ind.
     + reflexivity.
     + unfold Circle_rec_uncurried; cbn.
-      rewrite transport_paths_FlFr.
-      rewrite Circle_rec_beta_loop.
-      rewrite concat_p1; apply concat_Vp.
+      apply transport_paths_FlFr'.
+      apply equiv_p1_1q.
+      apply Circle_rec_beta_loop.
   - intros [b p]; apply ap.
     apply Circle_rec_beta_loop.
 Defined.
 
 Definition equiv_Circle_rec `{Funext} (P : Type)
   : {b : P & b = b} <~> (Circle -> P)
   := Build_Equiv _ _ _ (isequiv_Circle_rec_uncurried P).
+
+(** A pointed version of the universal property of the circle. *)
+Definition pmap_from_circle_loops `{Funext} (X : pType)
+  : (pCircle ->** X) <~>* loops X.
+Proof.
+  snrapply Build_pEquiv'.
+  - refine (_ oE (issig_pmap _ _)^-1%equiv).
+    equiv_via { xp : { x : X & x = x } & xp.1 = pt }.
+    2: make_equiv_contr_basedpaths.
+    exact ((equiv_functor_sigma_pb (equiv_Circle_rec X)^-1%equiv)).
+  - simpl.  apply ap_const.
+Defined.

theories/Spaces/Spheres.v

@@ -1,5 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
+Require Import WildCat.Equiv.
 Require Import NullHomotopy.
 Require Import Homotopy.Suspension.
 Require Import Pointed.
@@ -53,6 +54,24 @@ 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.
@@ -287,3 +306,14 @@ Proof.
     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.

theories/Types/Bool.v

@@ -117,6 +117,9 @@ Section BoolForall.
   Defined.
 End BoolForall.
 
+Definition equiv_bool_rec_uncurried `{Funext} (P : Type) : P * P <~> (Bool -> P)
+  := (equiv_bool_forall_prod (fun _ => P))^-1%equiv.
+
 (** ** The type [Bool <~> Bool] is equivalent to [Bool]. *)
 
 (** The nonidentity equivalence is negation (the flip). *)