Merge pull request #2259 from jdchristensen/ap_pV-zigzag

Add ap_pV and things related to suspensions and joins

Author: jdchristensen

theories/Basics/PathGroupoids.v

@@ -1135,6 +1135,16 @@ Definition inverse2 {A : Type} {x y : A} {p q : x = y} (h : p = q)
   : p^ = q^
 := ap inverse h.
 
+(** Two common combinations of [ap_pp] and [ap_V]. *)
+
+Definition ap_pV {A B : Type} (f : A -> B) {a0 a1 a0' : A} (p : a0 = a1) (q : a0' = a1)
+  : ap f (p @ q^) = ap f p @ (ap f q)^
+  := ap_pp f p q^ @ (1 @@ ap_V f q).
+
+Definition ap_Vp {A B : Type} (f : A -> B) {a0 a1 a1' : A} (p : a0 = a1) (q : a0 = a1')
+  : ap f (p^ @ q) = (ap f p)^ @ ap f q
+  := ap_pp f p^ q @ (ap_V f p @@ 1).
+
 (** Some higher coherences *)
 
 Lemma ap_pp_concat_p1 {A B} (f : A -> B) {a b : A} (p : a = b)
@@ -1149,15 +1159,14 @@ Proof.
   destruct p; reflexivity.
 Defined.
 
-Lemma ap_pp_concat_pV {A B} (f : A -> B) {x y : A} (p : x = y)
-: ap_pp f p p^ @ ((1 @@ ap_V f p) @ concat_pV (ap f p))
-  = ap (ap f) (concat_pV p).
+Lemma ap_pV_concat_pV {A B} (f : A -> B) {x y : A} (p : x = y)
+  : ap_pV f p p @ concat_pV (ap f p) = ap (ap f) (concat_pV p).
 Proof.
   destruct p; reflexivity.
 Defined.
 
-Lemma ap_pp_concat_Vp {A B} (f : A -> B) {x y : A} (p : x = y)
-: ap_pp f p^ p @ ((ap_V f p @@ 1) @ concat_Vp (ap f p))
+Lemma ap_Vp_concat_Vp {A B} (f : A -> B) {x y : A} (p : x = y)
+  : ap_Vp f p p @ concat_Vp (ap f p)
   = ap (ap f) (concat_Vp p).
 Proof.
   destruct p; reflexivity.
@@ -1175,6 +1184,17 @@ Proof.
   destruct r, p; reflexivity.
 Defined.
 
+(** Often [ap_pV_concat_pV] is combined with [concat_pV_inverse2] using a beta rule for [ap f p].  This and several above are best read from right-to-left, and the name here reflects the right-hand-side. *)
+Definition ap_ap_concat_pV {A B} (f : A -> B) {x y : A} (p : x = y)
+  (q : f x = f y) (r : ap f p = q)
+  : ap_pV f p p @ ((r @@ inverse2 r) @ concat_pV q) = ap (ap f) (concat_pV p)
+  := (1 @@ concat_pV_inverse2 _ q r) @ ap_pV_concat_pV f p.
+
+Definition ap_ap_concat_Vp {A B} (f : A -> B) {x y : A} (p : x = y)
+  (q : f x = f y) (r : ap f p = q)
+  : ap_Vp f p p @ ((inverse2 r @@ r) @ concat_Vp q) = ap (ap f) (concat_Vp p)
+  := (1 @@ concat_Vp_inverse2 _ q r) @ ap_Vp_concat_Vp f p.
+
 (** *** Whiskering *)
 
 Definition whiskerL {A : Type} {x y z : A} (p : x = y)

theories/Homotopy/Join/Core.v

@@ -143,6 +143,26 @@ End Join.
 Arguments joinl {A B}%_type_scope _ , [A] B _.
 Arguments joinr {A B}%_type_scope _ , A [B] _.
 
+(** ** Zigzags in joins *)
+
+(** These paths are very common, so we give them names. *)
+Definition zigzag {A B : Type} (a a' : A) (b : B)
+  : joinl a = joinl a'
+  := jglue a b @ (jglue a' b)^.
+
+Definition zagzig {A B : Type} (a : A) (b b' : B)
+  : joinr b = joinr b'
+  := (jglue a b)^ @ jglue a b'.
+
+(** And we give a beta rule for zigzags. *)
+Definition Join_rec_beta_zigzag {A B P : Type} (P_A : A -> P)
+  (P_B : B -> P) (P_g : forall a b, P_A a = P_B b) a a' b
+  : ap (Join_rec P_A P_B P_g) (zigzag a a' b) = P_g a b @ (P_g a' b)^.
+Proof.
+  lhs napply ap_pV.
+  exact (Join_rec_beta_jglue _ _ _ a b @@ inverse2 (Join_rec_beta_jglue _ _ _ a' b)).
+Defined.
+
 (** * [Join_rec] gives an equivalence of 0-groupoids
 
   We now prove many things about [Join_rec], for example, that it is an equivalence of 0-groupoids from the [JoinRecData] that we define next.  The framework we use is a bit elaborate, but it parallels the framework used in TriJoin.v, where careful organization is essential. *)
@@ -404,6 +424,22 @@ Proof.
   exact (isnat (join_rec_natequiv A B) g f).
 Defined.
 
+(** We restate the previous two results using [Join_rec] for convenience. *)
+Definition Join_rec_homotopic (A B : Type) {P : Type}
+  (fl  : A -> P) (fr  : B -> P) (fg  : forall a b, fl  a = fr  b)
+  (fl' : A -> P) (fr' : B -> P) (fg' : forall a b, fl' a = fr' b)
+  (hl : forall a, fl a = fl' a)
+  (hr : forall b, fr b = fr' b)
+  (hg : forall a b, fg a b @ hr b = hl a @ fg' a b)
+  : Join_rec fl fr fg == Join_rec fl' fr' fg'
+  := fmap join_rec (Build_JoinRecPath _ _ _
+      {| jl:=fl; jr:=fr; jg:=fg |} {| jl:=fl'; jr:=fr'; jg:=fg' |} hl hr hg).
+
+Definition Join_rec_nat (A B : Type) {P Q : Type} (g : P -> Q)
+  (fl : A -> P) (fr : B -> P) (fg : forall a b, fl a = fr b)
+  : Join_rec (g o fl) (g o fr) (fun a b => ap g (fg a b)) == g o Join_rec fl fr fg
+  := join_rec_nat _ _ g {| jl:=fl; jr:=fr; jg:=fg |}.
+
 (** * Various types of equalities between paths in joins *)
 
 (** Naturality squares for given paths in [A] and [B]. *)
@@ -448,7 +484,7 @@ Section Triangle.
   Defined.
 
   Definition triangle_h' {a a' : A} (b : B) (p : a = a')
-    : jglue a b @ (jglue a' b)^ = ap joinl p.
+    : zigzag a a' b = ap joinl p.
   Proof.
     destruct p.
     apply concat_pV.
@@ -462,7 +498,7 @@ Section Triangle.
   Defined.
 
   Definition triangle_v' (a : A) {b b' : B} (p : b = b')
-    : (jglue a b)^ @ jglue a b' = ap joinr p.
+    : zagzig a b b' = ap joinr p.
   Proof.
     destruct p.
     apply concat_Vp.
@@ -488,7 +524,7 @@ Section Diamond.
     := PathSquare (jglue a b) (jglue a' b')^ (jglue a b') (jglue a' b)^.
 
   Definition diamond_h {a a' : A} (b b' : B) (p : a = a')
-    : jglue a b @ (jglue a' b)^ = jglue a b' @ (jglue a' b')^.
+    : zigzag a a' b = zigzag a a' b'.
   Proof.
     destruct p.
     exact (concat_pV _ @ (concat_pV _)^).
@@ -501,7 +537,7 @@ Section Diamond.
   Defined.
 
   Definition diamond_v (a a' : A) {b b' : B} (p : b = b')
-    : jglue a b @ (jglue a' b)^ = jglue a b' @ (jglue a' b')^.
+    : zigzag a a' b = zigzag a a' b'.
   Proof.
     by destruct p.
   Defined.
@@ -546,6 +582,11 @@ Section FunctorJoin.
     : ap (functor_join f g) (jglue a b) = jglue (f a) (g b)
     := join_rec_beta_jg _ a b.
 
+  Definition functor_join_beta_zigzag {A B C D : Type} (f : A -> C) (g : B -> D)
+    (a a' : A) (b : B)
+    : ap (functor_join f g) (zigzag a a' b) = zigzag (f a) (f a') (g b)
+    := Join_rec_beta_zigzag _ _ _ a a' b.
+
   Definition functor_join_compose {A B C D E F}
     (f : A -> C) (g : B -> D) (h : C -> E) (i : D -> F)
     : functor_join (h o f) (i o g) == functor_join h i o functor_join f g.

theories/Homotopy/Join/JoinSusp.v

@@ -20,8 +20,7 @@ Defined.
 Definition susp_to_join (A : Type) : Susp A -> Join Bool A.
 Proof.
   srapply (Susp_rec (joinl true) (joinl false)).
-  intros a.
-  exact (jglue _ a @ (jglue _ a)^).
+  exact (zigzag true false).
 Defined.
 
 Instance isequiv_join_to_susp (A : Type) : IsEquiv (join_to_susp A).
@@ -33,10 +32,7 @@ Proof.
     transport_paths FFlr.
     apply equiv_p1_1q.
     lhs napply (ap _ _); [napply Susp_rec_beta_merid | ].
-    lhs napply (ap_pp _ _ (jglue false a)^).
-    lhs nrefine (_ @@ _).
-    1: lhs napply ap_V; napply (ap inverse).
-    1,2: napply Join_rec_beta_jglue.
+    lhs napply (Join_rec_beta_zigzag _ _ _ true false a).
     apply concat_p1.
   - srapply (Join_ind_FFlr (join_to_susp A)); cbn beta.
     1: intros [|]; reflexivity.
@@ -45,10 +41,10 @@ Proof.
     lhs nrefine (ap _ _ @@ 1).
     1: napply Join_rec_beta_jglue.
     destruct b.
-    all: rhs napply concat_1p.
-    + lhs nrefine (_ @@ 1); [napply Susp_rec_beta_merid | ].
+    + rhs napply concat_1p.
+      lhs nrefine (_ @@ 1); [napply Susp_rec_beta_merid | ].
       apply concat_pV_p.
-    + apply concat_1p.
+    + reflexivity.
 Defined.
 
 Definition equiv_join_susp (A : Type) : Join Bool A <~> Susp A

theories/Homotopy/Smash.v

@@ -181,10 +181,9 @@ Section Smash.
     (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a b : X)
     : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a b) = Pgl a @ (Pgl b)^.
   Proof.
-    lhs napply ap_pp.
+    lhs napply ap_pV.
     f_ap.
     1: apply Smash_rec_beta_gluel.
-    lhs napply ap_V.
     apply inverse2.
     apply Smash_rec_beta_gluel.
   Defined.
@@ -193,10 +192,9 @@ Section Smash.
     (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a b : Y)
     : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer' a b) = Pgr a @ (Pgr b)^.
   Proof.
-    lhs napply ap_pp.
+    lhs napply ap_pV.
     f_ap.
     1: apply Smash_rec_beta_gluer.
-    lhs napply ap_V.
     apply inverse2.
     apply Smash_rec_beta_gluer.
   Defined.

theories/Homotopy/Suspension.v

@@ -120,6 +120,39 @@ Proof.
   srapply Pushout_rec_beta_pglue.
 Defined.
 
+Definition Susp_rec_beta_zigzag {X Y : Type}
+  {H_N H_S : Y} {H_merid : X -> H_N = H_S} (x x' : X)
+  : ap (Susp_rec H_N H_S H_merid) (merid x @ (merid x')^) = H_merid x @ (H_merid x')^.
+Proof.
+  lhs napply ap_pV.
+  exact (Susp_rec_beta_merid x @@ inverse2 (Susp_rec_beta_merid x')).
+Defined.
+
+(** A variant of [Susp_ind_FlFr] specifically for two functions both defined using [Susp_rec]. *)
+Definition Susp_rec_homotopic {X Y : Type} (N S N' S' : Y)
+  (f : X -> N = S) (f' : X -> N' = S')
+  (p : N = N') (q : S = S') (H : forall x, f x @ q = p @ f' x)
+  : Susp_rec N S f == Susp_rec N' S' f'.
+Proof.
+  snapply Susp_ind_FlFr.
+  - exact p.
+  - exact q.
+  - intro x.
+    lhs napply (Susp_rec_beta_merid x @@ 1).
+    rhs napply (1 @@ Susp_rec_beta_merid x).
+    apply H.
+Defined.
+
+(** And the special case where the two functions agree definitionally on [North] and [South]. *)
+Definition Susp_rec_homotopic' {X Y : Type} (N S : Y)
+  (f g : X -> N = S) (H : f == g)
+  : Susp_rec N S f == Susp_rec N S g.
+Proof.
+  snapply Susp_rec_homotopic.
+  1, 2: reflexivity.
+  intro x; apply equiv_p1_1q, H.
+Defined.
+
 (** ** Eta-rule. *)
 
 (** The eta-rule for suspension states that any function out of a suspension is equal to one defined by [Susp_ind] in the obvious way. We give it first in a weak form, producing just a pointwise equality, and then turn this into an actual equality using [Funext]. *)

theories/Homotopy/Wedge.v

@@ -338,8 +338,7 @@ Proof.
       change (?t = _) with (t = loop_susp_unit X x).
       lhs napply (ap_compose (psusp_pinch X)).
       lhs napply (ap _ (psusp_pinch_beta_merid x)).
-      lhs napply ap_pp.
-      lhs napply (ap (fun x => _ @ x) (ap_V _ _)).
+      lhs napply ap_pV.
       apply moveR_pV.
       rhs napply (whiskerL _ (wedge_rec_beta_wglue _ _)).
       lhs napply ap_pp.
@@ -369,8 +368,7 @@ Proof.
       change (?t = _) with (t = loop_susp_unit X x).
       lhs napply (ap_compose (psusp_pinch X)).
       lhs napply (ap _ (psusp_pinch_beta_merid x)).
-      lhs napply ap_pp.
-      lhs napply (ap (fun x => _ @ x) (ap_V _ _)).
+      lhs napply ap_pV.
       apply moveR_pV.
       rhs napply (whiskerL _ (wedge_rec_beta_wglue _ _)).
       lhs napply ap_pp.

theories/Pointed/pSusp.v

@@ -150,30 +150,30 @@ Definition loop_susp_unit_natural {X Y : pType} (f : X ->* Y)
   ==* fmap loops (fmap psusp f) o* loop_susp_unit X.
 Proof.
   pointed_reduce.
-  simple refine (Build_pHomotopy _ _); cbn.
+  snapply Build_pHomotopy; cbn.
   - intros x; symmetry.
-    refine (concat_1p _@ (concat_p1 _ @ _)).
-    refine (ap_pp (Susp_rec North South (merid o f))
-                  (merid x) (merid (point X))^ @ _).
-    refine ((1 @@ ap_V _ _) @ _).
+    lhs napply concat_1p; lhs napply concat_p1.
+    lhs napply (ap_pV _ (merid x) (merid point0)).
     exact (Susp_rec_beta_merid _ @@ inverse2 (Susp_rec_beta_merid _)).
-  - cbn. apply moveL_pV. rewrite !inv_pp, !concat_pp_p, concat_1p; symmetry.
-    apply moveL_Vp.
-    refine (concat_pV_inverse2 _ _ (Susp_rec_beta_merid (point X)) @ _).
-    apply moveL_Vp, moveL_Vp.
-    refine (ap_pp_concat_pV _ _ @ _).
-    apply moveL_Vp, moveL_Vp.
-    rewrite concat_p1_1, concat_1p_1.
-    cbn; symmetry.
-    refine (concat_p1 _ @ _).
-    refine (ap_compose
-      (fun p' => (ap (Susp_rec North South (merid o f))) p' @ 1)
-      (fun p' => 1 @ p')
-      (concat_pV (merid (point X))) @ _).
-    apply ap.
-    exact (ap_compose (ap (Susp_rec North South (merid o f)))
-      (fun p' => p' @ 1) _).
-Qed.
+  - cbn. apply moveL_pV.
+    rhs napply concat_1p.
+    apply moveR_Vp.
+    lhs napply concat_p1.
+    (* Handle the [ap ... (1 @ q)] part. *)
+    lhs napply (ap_compose (fun p => ap _ p @ 1) _ (concat_pV _)).
+    lhs_V napply concat_1p_1.
+    rhs napply concat_pp_p.
+    apply whiskerL.
+    (* Handle the [ap ... (q @ 1)] part. *)
+    lhs napply (ap_compose _ (fun q => q @ 1) (concat_pV _)).
+    lhs_V napply concat_p1_1.
+    rhs napply concat_pp_p.
+    apply whiskerL.
+    (* Finish it off. *)
+    symmetry.
+    lhs napply concat_pp_p.
+    exact (ap_ap_concat_pV _ _ _ (Susp_rec_beta_merid point0)).
+Defined.
 
 Definition loop_susp_counit (X : pType) : psusp (loops X) ->* X
   :=  Build_pMap (psusp (loops X)) X (Susp_rec (point X) (point X) idmap) 1.
@@ -202,25 +202,23 @@ Definition loop_susp_triangle1 (X : pType)
   : fmap loops (loop_susp_counit X) o* loop_susp_unit (loops X)
   ==* pmap_idmap.
 Proof.
-  simple refine (Build_pHomotopy _ _).
+  (* This proof has a lot of overlap with [loop_susp_unit_natural]. Can a common lemma be factored out? *)
+  snapply Build_pHomotopy.
   - intros p; cbn.
-    refine (concat_1p _ @ (concat_p1 _ @ _)).
-    refine (ap_pp (Susp_rec (point X) (point X) idmap)
-                  (merid p) (merid (point (point X = point X)))^ @ _).
-    refine ((1 @@ ap_V _ _) @ _).
-    refine ((Susp_rec_beta_merid p
-      @@ inverse2 (Susp_rec_beta_merid (point (loops X)))) @ _).
-    exact (concat_p1 _).
-  - apply moveL_pV. destruct X as [X x]; cbn; unfold point.
-    apply whiskerR.
-    rewrite (concat_pV_inverse2
-               (ap (Susp_rec x x idmap) (merid 1))
-               1 (Susp_rec_beta_merid 1)).
-    rewrite (ap_pp_concat_pV (Susp_rec x x idmap) (merid 1)).
-    rewrite ap_compose, (ap_compose _ (fun p => p @ 1)).
-    rewrite concat_1p_1; apply ap.
-    apply concat_p1_1.
-Qed.
+    lhs napply concat_1p; lhs napply concat_p1.
+    lhs napply (ap_pV _ (merid p) _).
+    lhs napply (Susp_rec_beta_merid _ @@ inverse2 (Susp_rec_beta_merid _)).
+    apply concat_p1.
+  - simpl.
+    do 2 rhs napply concat_p1.
+    rhs napply (ap_compose (fun p => ap _ p @ 1) _ (concat_pV _)).
+    rhs_V napply (concat_1p_1 _ _).
+    apply whiskerL.
+    rhs napply (ap_compose _ (fun q => q @ 1) (concat_pV _)).
+    rhs_V napply concat_p1_1.
+    apply whiskerL.
+    exact (ap_ap_concat_pV _ _ _ (Susp_rec_beta_merid pt)).
+Defined. (* A bit slow, ~0.9s. *)
 
 Definition loop_susp_triangle2 (X : pType)
   : loop_susp_counit (psusp X) o* fmap psusp (loop_susp_unit X)