more transport_paths lemmas

theories/Colimits/Coeq.v

@@ -84,7 +84,8 @@ Proof.
   unfold pointwise_paths.
   nrapply (Coeq_ind _ (fun _ => 1)).
   intros b.
-  apply transport_paths_FlFr', equiv_p1_1q.
+  transport_paths FlFr.
+  apply equiv_p1_1q.
   symmetry; nrapply Coeq_rec_beta_cglue.
 Defined.
 
@@ -135,7 +136,7 @@ Proof.
     srapply Coeq_ind; intros b.
     1: cbn;reflexivity.
     cbn.
-    nrapply transport_paths_FlFr'.
+    transport_paths FlFr.
     apply equiv_p1_1q.
     nrapply Coeq_rec_beta_cglue.
   - intros [h q]; srapply path_sigma'.
@@ -176,7 +177,7 @@ Proof.
   snrapply Coeq_ind.
   1: reflexivity.
   intros b.
-  nrapply transport_paths_Flr'.
+  transport_paths Flr.
   apply moveR_pM.
   nrapply functor_coeq_beta_cglue.
 Defined.
@@ -192,7 +193,7 @@ Definition functor_coeq_compose {B A f g B' A' f' g' B'' A'' f'' g''}
   == functor_coeq h' k' p' q' o functor_coeq h k p q.
 Proof.
   refine (Coeq_ind _ (fun a => 1) _); cbn; intros b.
-  nrapply transport_paths_FlFr'.
+  transport_paths FlFr.
   apply equiv_p1_1q; symmetry.
   rewrite ap_compose.
   rewrite !functor_coeq_beta_cglue, !ap_pp, functor_coeq_beta_cglue.
@@ -212,7 +213,7 @@ Definition functor_coeq_homotopy {B A f g B' A' f' g'}
 : functor_coeq h k p q == functor_coeq h' k' p' q'.
 Proof.
   refine (Coeq_ind _ (fun a => ap coeq (s a)) _); cbn; intros b.
-  apply transport_paths_FlFr'.
+  transport_paths FlFr.
   rewrite !functor_coeq_beta_cglue.
   Open Scope long_path_scope.
   rewrite 2 ap_V.
@@ -357,7 +358,7 @@ Section CoeqRec2.
         cbn.
         apply cgluel.
       + intros b'.
-        nrapply (transport_paths_FlFr' (cglue b')).
+        transport_paths (transport_paths_FlFr (cglue b')).
         lhs nrapply (_ @@ 1).
         1: apply Coeq_rec_beta_cglue.
         rhs nrapply (1 @@ _).
@@ -705,7 +706,7 @@ Section Flattening.
     - snrapply Coeq_ind.
       1: reflexivity.
       intros [b pf]; cbn.
-      nrapply transport_paths_FFlr'; apply equiv_p1_1q.
+      transport_paths FFlr; apply equiv_p1_1q.
       rewrite Coeq_rec_beta_cglue.
       lhs nrapply cdepdescent_rec_beta_cglue.
       nrapply concat_p1.
@@ -715,7 +716,7 @@ Section Flattening.
       + by intros a pa.
       + intros b pf; cbn.
         lhs nrapply transportDD_is_transport.
-        nrapply transport_paths_FFlr'; apply equiv_p1_1q.
+        transport_paths FFlr; apply equiv_p1_1q.
         rewrite <- (concat_p1 (transport_fam_cdescent_cglue _ _ _)).
         rewrite cdepdescent_rec_beta_cglue. (* This needs to be in the form [transport_fam_cdescent_cglue Pe r pa @ p] to work, and the other [@ 1] introduced comes in handy as well. *)
         lhs nrapply (ap _ (concat_p1 _)).

theories/Colimits/Colimit.v

@@ -145,7 +145,7 @@ Proof.
   snrapply Colimit_ind.
   - simpl. exact h_obj.
   - cbn beta; intros i j g x.
-    nrapply (transport_paths_FlFr' (colimp i j g x)).
+    transport_paths FlFr.
     lhs nrapply (Colimit_rec_beta_colimp _ _ _ _ _ _ @@ 1).
     apply h_comm.
 Defined.

theories/Colimits/Colimit_Coequalizer.v

@@ -69,8 +69,8 @@ Section Coequalizer.
         | [|- ?G == _ ] => simple refine (Coeq_ind (fun w => G w = F w) _ _)
       end.
       + reflexivity.
-      + intros b; simpl.
-        nrapply (transport_paths_FlFr' (g:=F)).
+      + intros b.
+        transport_paths FlFr; simpl.
         apply equiv_p1_1q.
         refine (Coeq_rec_beta_cglue _ _ _ _ @ _).
         apply concat_p1.

theories/Colimits/Colimit_Flattening.v

@@ -134,12 +134,12 @@ Section Flattening.
       funext y.
       set (L := cocone_extends Z (cocone_postcompose cocone_E' f)).
       refine (transport_forall _ _ _ @ _).
-      nrapply (transport_paths_FlFr' (f:=fun y0 => L (_; y0))).
+      transport_paths (transport_paths_FlFr (f:=fun y0 => L (_; y0))).
       lhs nrapply concat_p1.
       lhs_V nrapply concat_1p.
       refine (_^ @@ 1).
       lhs rapply (transportD_is_transport E' (fun w => L w = f w)).
-      nrapply transport_paths_FlFr'; apply equiv_p1_1q.
+      transport_paths FlFr; apply equiv_p1_1q.
       rewrite ap_path_sigma.
       rewrite Colimit_ind_beta_colimp.
       rewrite ap10_path_forall.

theories/Colimits/Colimit_Pushout.v

@@ -138,7 +138,7 @@ Section PO.
         apply ap, eisretr.
       + reflexivity.
       + intro a; cbn.
-        nrapply transport_paths_FFlr'.
+        transport_paths FFlr.
         refine (concat_p1 _ @ _).
         rewrite PO_rec_beta_pp.
         rewrite eisadj.
@@ -192,7 +192,7 @@ Section is_PO_pushout.
         srapply Pushout_ind; cbn.
         1,2: reflexivity.
         intro a; cbn beta.
-        nrapply transport_paths_FlFr'; apply equiv_p1_1q.
+        transport_paths FlFr; apply equiv_p1_1q.
         unfold popp'; cbn.
         rhs_V nrapply concat_p1.
         nrapply Pushout_rec_beta_pglue.
@@ -223,7 +223,7 @@ Section is_PO_pushout.
     snrapply Pushout_ind.
     1, 2: reflexivity.
     intro a; cbn beta.
-    nrapply transport_paths_FlFr'; apply equiv_p1_1q.
+    transport_paths FlFr; apply equiv_p1_1q.
     lhs exact (Pushout_rec_beta_pglue P pushb pushc pusha a).
     symmetry.
     lhs nrapply (ap_compose equiv_pushout_PO _ (pglue a)).

theories/Colimits/GraphQuotient.v

@@ -303,7 +303,7 @@ Section Flattening.
       1: reflexivity.
       intros [a x] [b y] [r pr]; cbn in r, pr; cbn.
       destruct pr.
-      nrapply transport_paths_FFlr'; apply equiv_p1_1q.
+      transport_paths FFlr; apply equiv_p1_1q.
       rewrite GraphQuotient_rec_beta_gqglue.
       lhs nrapply gqdepdescent_rec_beta_gqglue.
       nrapply concat_p1.
@@ -313,7 +313,7 @@ Section Flattening.
       + by intros a pa.
       + intros a b r pa; cbn.
         lhs nrapply transportDD_is_transport.
-        nrapply transport_paths_FFlr'; apply equiv_p1_1q.
+        transport_paths FFlr; apply equiv_p1_1q.
         rewrite <- (concat_p1 (transport_fam_gqdescent_gqglue _ _ _)).
         rewrite gqdepdescent_rec_beta_gqglue. (* This needs to be in the form [transport_fam_gqdescent_gqglue Pe r pa @ p] to work, and the other [@ 1] introduced comes in handy as well. *)
         lhs nrapply (ap _ (concat_p1 _)).
@@ -369,15 +369,21 @@ Proof.
   exact r.
 Defined.
 
+Definition functor_gq_beta_gqglue {A B : Type} (f : A -> B)
+  {R : A -> A -> Type} {S : B -> B -> Type}
+  (e : forall a b, R a b -> S (f a) (f b))
+  {a b : A} (s : R a b)
+  : ap (functor_gq f e) (gqglue s) = gqglue (e a b s)
+  := GraphQuotient_rec_beta_gqglue _ _ _ _ _.
+
 Lemma functor_gq_idmap {A : Type} {R : A -> A -> Type}
   : functor_gq (A:=A) (B:=A) (S:=R) idmap (fun a b r => r) == idmap.
 Proof.
   snrapply GraphQuotient_ind.
   1: reflexivity.
   intros a b r.
-  nrapply (transport_paths_FlFr' (gqglue r)).
+  transport_paths Flr.
   apply equiv_p1_1q.
-  rhs nrapply ap_idmap.
   nrapply GraphQuotient_rec_beta_gqglue.
 Defined.
 
@@ -388,14 +394,13 @@ Lemma functor_gq_compose {A B C : Type} (f : A -> B) (g : B -> C)
 Proof.
   snrapply GraphQuotient_ind.
   1: reflexivity.
-  intros a b s.
-  nrapply (transport_paths_FlFr' (gqglue s)).
+  intros a b s; cbn beta.
+  transport_paths FFlFr.
   apply equiv_p1_1q.
-  lhs nrapply (ap_compose (functor_gq f e) (functor_gq g e') (gqglue s)).
   lhs nrapply ap.
-  1: apply GraphQuotient_rec_beta_gqglue.
-  lhs nrapply GraphQuotient_rec_beta_gqglue.
-  exact (GraphQuotient_rec_beta_gqglue _ _ _ _ s)^.
+  1: apply functor_gq_beta_gqglue.
+  rhs nrapply (functor_gq_beta_gqglue (g o f)).
+  nrapply (functor_gq_beta_gqglue g).
 Defined.
 
 Lemma functor2_gq {A B : Type} (f f' : A -> B)
@@ -409,12 +414,12 @@ Proof.
   - simpl; intro.
     apply ap.
     apply p.
-  - intros a b s.
-    nrapply (transport_paths_FlFr' (gqglue s)).
-    rhs nrefine (1 @@ _).
-    2: apply GraphQuotient_rec_beta_gqglue.
-    lhs nrefine (_ @@ 1).
-    1: apply GraphQuotient_rec_beta_gqglue.
+  - intros a b s; simpl.
+    transport_paths (transport_paths_FlFr (gqglue s)).
+    rhs nrapply whiskerL.
+    2: nrapply functor_gq_beta_gqglue.
+    lhs nrapply whiskerR.
+    1: nrapply functor_gq_beta_gqglue.
     apply moveL_Mp.
     symmetry.
     destruct (q a b s).

theories/Colimits/Pushout.v

@@ -98,7 +98,7 @@ Proof.
   snrapply Pushout_ind.
   1, 2: reflexivity.
   intro a; cbn beta.
-  apply transport_paths_FlFr'.
+  transport_paths FlFr.
   apply equiv_p1_1q.
   nrapply Pushout_rec_beta_pglue.
 Defined.
@@ -217,7 +217,7 @@ Proof.
   1,2: reflexivity.
   simpl.
   intros a.
-  nrapply transport_paths_Flr'.
+  transport_paths Flr.
   nrapply moveR_pM.
   nrapply functor_pushout_beta_pglue.
 Defined.
@@ -845,7 +845,7 @@ Section Flattening.
     - snrapply Pushout_ind.
       1, 2: reflexivity.
       intros [a pf]; cbn.
-      nrapply transport_paths_FFlr'; apply equiv_p1_1q.
+      transport_paths FFlr; apply equiv_p1_1q.
       rewrite Pushout_rec_beta_pglue.
       lhs nrapply podepdescent_rec_beta_pglue.
       nrapply concat_p1.
@@ -856,7 +856,7 @@ Section Flattening.
       + by intros c pc.
       + intros a pf; cbn.
         lhs nrapply transportDD_is_transport.
-        nrapply transport_paths_FFlr'; apply equiv_p1_1q.
+        transport_paths FFlr; apply equiv_p1_1q.
         rewrite <- (concat_p1 (transport_fam_podescent_pglue _ _ _)).
         rewrite podepdescent_rec_beta_pglue. (* This needs to be in the form [transport_fam_podescent_gqglue Pe r pa @ p] to work, and the other [@ 1] introduced comes in handy as well. *)
         lhs nrapply (ap _ (concat_p1 _)).

theories/Colimits/SpanPushout.v

@@ -77,7 +77,7 @@ Proof.
   snrapply spushout_ind.
   1,2: reflexivity.
   intros x y q; cbn beta.
-  snrapply transport_paths_FFlFr'.
+  transport_paths FFlFr.
   apply equiv_p1_1q.
   lhs nrapply ap.
   1: nrapply spushout_rec_beta_spglue.
@@ -92,7 +92,7 @@ Proof.
   snrapply spushout_ind.
   1,2: reflexivity.
   intros x y q; cbn.
-  snrapply transport_paths_Flr'.
+  transport_paths Flr.
   apply equiv_p1_1q.
   nrapply spushout_rec_beta_spglue.
 Defined.
@@ -114,7 +114,7 @@ Proof.
   - intros y; cbn.
     exact (ap (spushr Q') (k y)).
   - intros x y q.
-    snrapply transport_paths_FlFr'.
+    transport_paths FlFr.
     lhs nrapply whiskerR.
     1: apply spushout_rec_beta_spglue.
     rhs nrapply whiskerL.

theories/Homotopy/ClassifyingSpace.v

@@ -375,9 +375,8 @@ Section HSpace_bg.
     snrapply ClassifyingSpace_ind_hprop.
     1: exact _.
     simpl.
-    nrapply (transport_paths_FFlr' (g := idmap)).
+    transport_paths Flr.
     apply equiv_p1_1q.
-    lhs nrapply ap_idmap.
     nrapply ClassifyingSpace_rec_beta_bloop.
   Defined.
 

theories/Homotopy/Join/Core.v

@@ -52,7 +52,7 @@ Section Join.
   Proof.
     snrapply (Join_ind _ Hl Hr).
     intros a b.
-    nrapply transport_paths_FlFr'.
+    transport_paths FlFr.
     apply Hglue.
   Defined.
 
@@ -64,7 +64,7 @@ Section Join.
   Proof.
     snrapply (Join_ind _ Hl Hr).
     intros a b.
-    nrapply transport_paths_Flr'.
+    transport_paths Flr.
     apply Hglue.
   Defined.
 
@@ -77,7 +77,7 @@ Section Join.
   Proof.
     snrapply (Join_ind _ Hl Hr).
     intros a b.
-    nrapply transport_paths_FFlr'.
+    transport_paths FFlr.
     apply Hglue.
   Defined.
 
@@ -90,7 +90,7 @@ Section Join.
   Proof.
     snrapply (Join_ind _ Hl Hr).
     intros a b; cbn beta.
-    nrapply transport_paths_FFlFr'.
+    transport_paths FFlFr.
     apply Hglue.
   Defined.
 
@@ -103,7 +103,7 @@ Section Join.
   Proof.
     snrapply (Join_ind _ Hl Hr).
     intros a b; cbn beta.
-    nrapply transport_paths_FlFFr'.
+    transport_paths FlFFr.
     apply Hglue.
   Defined.
 
@@ -116,7 +116,7 @@ Section Join.
   Proof.
     snrapply (Join_ind _ Hl Hr).
     intros a b; cbn beta.
-    nrapply transport_paths_FFlFFr'.
+    transport_paths FFlFFr.
     apply Hglue.
   Defined.
 

theories/Homotopy/Join/JoinSusp.v

@@ -29,8 +29,8 @@ Proof.
   snrapply (isequiv_adjointify _ (susp_to_join A)).
   - snrapply Susp_ind.
     1,2: reflexivity.
-    intros a.
-    apply (transport_paths_FFlr' (f:=susp_to_join A)).
+    intros a; cbn beta.
+    transport_paths FFlr.
     apply equiv_p1_1q.
     lhs nrapply (ap _ _); [nrapply Susp_rec_beta_merid | ].
     lhs nrapply (ap_pp _ _ (jglue false a)^).

theories/Homotopy/Join/TriJoin.v

@@ -405,6 +405,15 @@ Proof.
   apply s.
 Defined.
 
+(** We need to explicitly reason about the proof given by [transport_paths FlFr] so we give it a name here. *)
+Local Definition transport_paths_FlFr' {A B : Type} {f g : A -> B} {x1 x2 : A}
+  (p : x1 = x2) (q : f x1 = g x1) (r : (f x2) = (g x2))
+  (h : (ap f p) @ r = q @ (ap g p))
+  : transport (fun x => f x = g x) p q = r.
+Proof.
+  by transport_paths FlFr.
+Defined.
+
 (** This lemma handles the path algebra in the last goal of the next result. *)
 Local Definition isinj_trijoin_rec_inv_helper {J P : Type} {f g : J -> P}
   {a b c : J} {ab : a = b} {ac : a = c} {bc : b = c} {abc : ab @ bc = ac}

theories/Homotopy/Smash.v

@@ -231,10 +231,10 @@ Definition Smash_ind_FlFr {A B : pType} {P : Type} (f g : Smash A B -> P)
 Proof.
   snrapply (Smash_ind Hsm Hl Hr).
   - intros a.
-    nrapply transport_paths_FlFr'.
+    transport_paths FlFr.
     exact (Hgluel a).
   - intros b.
-    nrapply transport_paths_FlFr'.
+    transport_paths FlFr.
     exact (Hgluer b).
 Defined.
 
@@ -248,11 +248,11 @@ Definition Smash_ind_FFlr {A B : pType} {P : Type}
   : g o f == idmap.
 Proof.
   snrapply (Smash_ind Hsm Hl Hr).
-  - intros a.
-    nrapply (transport_paths_FFlr' (f := f) (g := g)).
+  - intros a; cbn beta.
+    transport_paths FFlr.
     exact (Hgluel a).
-  - intros b.
-    nrapply (transport_paths_FFlr' (f := f) (g := g)).
+  - intros b; cbn beta.
+    transport_paths FFlr.
     exact (Hgluer b).
 Defined.