Associativity of Join, and lots more

theories/Basics/PathGroupoids.v

@@ -78,6 +78,15 @@ Definition concat_1p {A : Type} {x y : A} (p : x = y) :
   :=
   match p with idpath => 1 end.
 
+(** It's common to need to use both. *)
+Definition concat_p1_1p {A : Type} {x y : A} (p : x = y)
+  : p @ 1 = 1 @ p
+  := concat_p1 p @ (concat_1p p)^.
+
+Definition concat_1p_p1 {A : Type} {x y : A} (p : x = y)
+  : 1 @ p = p @ 1
+  := concat_1p p @ (concat_p1 p)^.
+
 (** Concatenation is associative. *)
 Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
   p @ (q @ r) = (p @ q) @ r :=
@@ -437,7 +446,7 @@ Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y
   (ap f q) @ (p y) = (p x) @ (ap g q)
   :=
   match q with
-    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+    | idpath => concat_1p_p1 _
   end.
 
 (* A useful variant of concat_Ap. *)
@@ -453,7 +462,7 @@ Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A}
   (ap f q) @ (p y) = (p x) @ q
   :=
   match q with
-    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+    | idpath => concat_1p_p1 _
   end.
 
 (* The corresponding variant of concat_A1p. *)
@@ -468,7 +477,7 @@ Definition concat_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A}
   (p x) @ (ap f q) =  q @ (p y)
   :=
   match q as i in (_ = y) return (p x @ ap f i = i @ p y) with
-    | idpath => concat_p1 _ @ (concat_1p _)^
+    | idpath => concat_p1_1p _
   end.
 
 (** Naturality with other paths hanging around. *)
@@ -479,7 +488,7 @@ Definition concat_pA_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
   (r @ ap f q) @ (p y @ s) = (r @ p x) @ (ap g q @ s).
 Proof.
   destruct q, s; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -490,7 +499,7 @@ Definition concat_pA_p {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
   (r @ ap f q) @ p y = (r @ p x) @ ap g q.
 Proof.
   destruct q; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -501,8 +510,7 @@ Definition concat_A_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
   (ap f q) @ (p y @ s) = (p x) @ (ap g q @ s).
 Proof.
   destruct q, s; cbn.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
+  apply concat_1p.
 Defined.
 
 Definition concat_pA1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
@@ -512,7 +520,7 @@ Definition concat_pA1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
   (r @ ap f q) @ (p y @ s) = (r @ p x) @ (q @ s).
 Proof.
   destruct q, s; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -523,7 +531,7 @@ Definition concat_pp_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
   (r @ p x) @ (ap g q @ s) = (r @ q) @ (p y @ s).
 Proof.
   destruct q, s; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -534,7 +542,7 @@ Definition concat_pA1_p {A : Type} {f : A -> A} (p : forall x, f x = x)
   (r @ ap f q) @ p y = (r @ p x) @ q.
 Proof.
   destruct q; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -545,8 +553,7 @@ Definition concat_A1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
   (ap f q) @ (p y @ s) = (p x) @ (q @ s).
 Proof.
   destruct q, s; cbn.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
+  apply concat_1p.
 Defined.
 
 Definition concat_pp_A1 {A : Type} {g : A -> A} (p : forall x, x = g x)
@@ -556,7 +563,7 @@ Definition concat_pp_A1 {A : Type} {g : A -> A} (p : forall x, x = g x)
   (r @ p x) @ ap g q = (r @ q) @ p y.
 Proof.
   destruct q; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -567,8 +574,7 @@ Definition concat_p_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
   p x @ (ap g q @ s) = q @ (p y @ s).
 Proof.
   destruct q, s; simpl.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
+  symmetry; apply concat_1p.
 Defined.
 
 (** Some coherence lemmas for functoriality *)
@@ -814,7 +820,7 @@ Definition concat_AT {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
   {z w : P x} (r : p = q) (s : z = w)
   : ap (transport P p) s  @  transport2 P r w
     = transport2 P r z  @  ap (transport P q) s
-  := match r with idpath => (concat_p1 _ @ (concat_1p _)^) end.
+  := match r with idpath => (concat_p1_1p _) end.
 
 (* TODO: What should this be called? *)
 Lemma ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x) :
@@ -1048,7 +1054,7 @@ Definition cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
 (** Whiskering and identity paths. *)
 
 Definition whiskerR_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
-  (concat_p1 p) ^ @ whiskerR h 1 @ concat_p1 q = h
+  (concat_p1 p)^ @ whiskerR h 1 @ concat_p1 q = h
   :=
   match h with idpath =>
     match p with idpath =>

theories/Colimits/Coeq.v

@@ -91,7 +91,9 @@ Proof.
     srapply Coeq_ind; intros b.
     1: cbn;reflexivity.
     cbn.
-    abstract (rewrite transport_paths_FlFr, concat_p1, Coeq_rec_beta_cglue, concat_Vp; reflexivity).
+    nrapply transport_paths_FlFr'.
+    apply equiv_p1_1q.
+    nrapply Coeq_rec_beta_cglue.
   - intros [h q]; srapply path_sigma'.
     + reflexivity.
     + cbn.
@@ -134,8 +136,8 @@ 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.
-  rewrite transport_paths_FlFr.
-  rewrite concat_p1; apply moveR_Vp; rewrite concat_p1.
+  nrapply transport_paths_FlFr'.
+  apply equiv_p1_1q; symmetry.
   rewrite ap_compose.
   rewrite !functor_coeq_beta_cglue, !ap_pp, functor_coeq_beta_cglue.
   rewrite <- !ap_compose. cbn.

theories/Colimits/Colimit.v

@@ -138,9 +138,9 @@ Proof.
     srapply Colimit_ind.
     1: reflexivity.
     intros ????; cbn.
-    rewrite transport_paths_FlFr.
-    rewrite Colimit_rec_beta_colimp.
-    hott_simpl. }
+    nrapply transport_paths_FlFr'.
+    apply equiv_p1_1q.
+    apply Colimit_rec_beta_colimp. }
   { intros [].
     srapply path_cocone.
     1: reflexivity.
@@ -166,17 +166,16 @@ Proof.
     srapply path_cocone.
     1: reflexivity.
     intros i j f x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
+    apply equiv_p1_1q.
     apply Colimit_rec_beta_colimp.
   - intro f.
     apply path_forall.
     srapply Colimit_ind.
     1: reflexivity.
     intros i j g x; simpl.
-    rewrite transport_paths_FlFr.
-    rewrite Colimit_rec_beta_colimp.
-    refine (ap (fun x => concat x _) (concat_p1 _) @ _).
-    apply concat_Vp.
+    nrapply (transport_paths_FlFr' (g:=f)).
+    apply equiv_p1_1q.
+    apply Colimit_rec_beta_colimp.
 Defined.
 
 Global Instance iscolimit_colimit `{Funext} {G : Graph} (D : Diagram G)

theories/Colimits/Colimit_Coequalizer.v

@@ -70,9 +70,10 @@ Section Coequalizer.
       end.
       + reflexivity.
       + intros b; simpl.
-        rewrite transport_paths_FlFr.
-        rewrite Coeq_rec_beta_cglue.
-        hott_simpl.
+        nrapply (transport_paths_FlFr' (g:=F)).
+        apply equiv_p1_1q.
+        refine (Coeq_rec_beta_cglue _ _ _ _ @ _).
+        apply concat_p1.
   Defined.
 
   Definition equiv_Coeq_Coequalizer `{Funext}

theories/Colimits/Colimit_Pushout.v

@@ -142,12 +142,13 @@ Section PO.
         apply ap, eisretr.
       + reflexivity.
       + intro a; cbn.
-        rewrite transport_paths_FlFr, ap_idmap.
-        rewrite ap_compose, PO_rec_beta_pp.
+        nrapply transport_paths_FFlr'.
+        refine (concat_p1 _ @ _).
+        rewrite PO_rec_beta_pp.
         rewrite eisadj.
         destruct (eissect f a); cbn.
-        rewrite concat_1p, concat_p1.
-        apply concat_Vp.
+        rewrite concat_p1.
+        symmetry; apply concat_Vp.
     - cbn; reflexivity.
   Defined.
 
@@ -191,11 +192,10 @@ Section is_PO_pushout.
         srapply Pushout_ind; cbn.
         1,2: reflexivity.
         intro a; cbn.
-        rewrite transport_paths_FlFr, concat_p1.
-        rewrite Pushout_rec_beta_pglue.
-        eapply moveR_Vp.
-        unfold popp'.
-        by rewrite 2 concat_p1.
+        nrapply transport_paths_FlFr'; apply equiv_p1_1q.
+        unfold popp'; cbn.
+        refine (_ @ concat_p1 _).
+        nrapply Pushout_rec_beta_pglue.
   Defined.
 
   Definition equiv_pushout_PO : Pushout f g <~> PO f g.

theories/Colimits/Pushout.v

@@ -108,8 +108,8 @@ Proof.
     + intros b; reflexivity.
     + intros c; reflexivity.
     + intros a; cbn.
-      abstract (rewrite transport_paths_FlFr, Pushout_rec_beta_pglue;
-                rewrite concat_p1; apply concat_Vp).
+      nrapply transport_paths_FlFr'; apply equiv_p1_1q.
+      nrapply Pushout_rec_beta_pglue.
   - intros [[pushb pushc] pusha]; unfold pushout_unrec; cbn.
     srefine (path_sigma' _ _ _).
     + srefine (path_prod' _ _); reflexivity.
@@ -308,12 +308,12 @@ Section EquivSigmaPushout.
       + reflexivity.
       + reflexivity.
       + intros [x a].
-        rewrite transport_paths_FlFr.
-        rewrite ap_idmap, concat_p1.
-        apply moveR_Vp. rewrite concat_p1.
-        rewrite ap_compose.
-        rewrite esp2_beta_pglue, esp1_beta_pglue.
-        reflexivity.
+        refine (transport_paths_FFlr _ _ @ _).
+        refine (concat_p1 _ @@ 1 @ _).
+        apply moveR_Vp; symmetry.
+        refine (concat_p1 _ @ _).
+        refine (ap _ (esp2_beta_pglue _ _) @ _).
+        apply esp1_beta_pglue.
     - intros [x a]; revert a.
       srefine (Pushout_ind _ _ _ _); cbn.
       + reflexivity.

theories/Cubical/PathSquare.v

@@ -111,11 +111,10 @@ Section PathSquaresFromPaths.
     {p p' : a00 = a10} {q q' : a00 = a01}.
 
   Definition equiv_sq_G1  : p = p' <~> PathSquare p p' 1 1
-    := sq_path oE (equiv_concat_lr (concat_p1 _)^ (concat_1p _))^-1.
+    := sq_path oE equiv_p1_1q.
 
   Definition equiv_sq_1G : q = q' <~> PathSquare 1 1 q q'
-    := sq_path oE (equiv_concat_lr (concat_1p _)^ (concat_p1 _))^-1
-      oE equiv_path_inverse _ _.
+    := sq_path oE equiv_1p_q1 oE equiv_path_inverse _ _.
 
 End PathSquaresFromPaths.
 

theories/Diagrams/Cocone.v

@@ -109,7 +109,7 @@ Section FunctorialityCocone.
     srapply path_cocone; intro i.
     1: reflexivity.
     intros j g x; simpl.
-    refine (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
+    apply equiv_p1_1q, ap_idmap.
   Defined.
 
   Definition cocone_postcompose_comp {D : Diagram G}
@@ -120,7 +120,7 @@ Section FunctorialityCocone.
     srapply path_cocone; intro i.
     1: reflexivity.
     intros j h x; simpl.
-    refine (concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
+    apply equiv_p1_1q, ap_compose.
   Defined.
 
   (** ** Precomposition for cocones *)
@@ -149,7 +149,7 @@ Section FunctorialityCocone.
     intro C; srapply path_cocone; simpl.
     1: reflexivity.
     intros; simpl.
-    refine (concat_p1 _).
+    apply concat_p1.
   Defined.
 
   Definition cocone_precompose_comp {D1 D2 D3 : Diagram G}
@@ -161,7 +161,7 @@ Section FunctorialityCocone.
     srapply path_cocone.
     1: reflexivity.
     intros i j g x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
+    apply equiv_p1_1q.
     unfold CommutativeSquares.comm_square_comp.
     refine (concat_p_pp _ _ _ @ _).
     apply ap10, ap.
@@ -183,7 +183,7 @@ Section FunctorialityCocone.
     srapply path_cocone; intro i.
     1: reflexivity.
     intros j g x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
+    apply equiv_p1_1q.
     etransitivity.
     + apply ap_pp.
     + apply ap10, ap.

theories/Diagrams/Cone.v

@@ -106,7 +106,7 @@ Section FunctorialityCone.
     srapply path_cone; intro i.
     1: reflexivity.
     intros j g x; simpl.
-    refine (concat_p1 _ @ (concat_1p _)^).
+    apply concat_p1_1p.
   Defined.
 
   Definition cone_precompose_comp {D : Diagram G}
@@ -117,7 +117,7 @@ Section FunctorialityCone.
     srapply path_cone; intro i.
     1: reflexivity.
     intros j h x; simpl.
-    refine (concat_p1 _ @ (concat_1p _)^).
+    apply concat_p1_1p.
   Defined.
 
   (** ** Postcomposition for cones *)
@@ -157,7 +157,7 @@ Section FunctorialityCone.
     srapply path_cone.
     1: reflexivity.
     intros i j g x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
+    apply equiv_p1_1q.
     unfold CommutativeSquares.comm_square_comp.
     refine (_ @ concat_p_pp _ _ _).
     apply ap.
@@ -177,8 +177,7 @@ Section FunctorialityCone.
     srapply path_cone; intro i.
     1: reflexivity.
     intros j g x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
-    reflexivity.
+    apply concat_p1_1p.
   Defined.
 
   (** The postcomposition with a diagram equivalence is an equivalence. *)