redefine DPath as transport and cleanup proofs

theories/Algebra/AbGroups/Abelianization.v

@@ -87,7 +87,6 @@ Section Abel.
     1: apply a.
     intros [[x y] z].
     refine (transport_compose _ _ _ _ @ _).
-    srapply dp_path_transport^-1%equiv.
     apply c.
   Defined.
 
@@ -96,9 +95,8 @@ Section Abel.
     `{forall x, IsHSet (P x)}(a : forall x, P (ab x))
     (c : forall x y z, DPath P (ab_comm x y z)
       (a (x * (y * z))) (a (x * (z * y))))
-    (x y z : G) : dp_apD (Abel_ind P a c) (ab_comm x y z) = c x y z.
+    (x y z : G) : apD (Abel_ind P a c) (ab_comm x y z) = c x y z.
   Proof.
-    apply dp_apD_path_transport.
     refine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _).
     rapply Coeq_ind_beta_cglue.
   Defined.
@@ -117,8 +115,7 @@ Section Abel.
     (a : forall x, P (ab x)) : forall (x : Abel), P x.
   Proof.
     srapply (Abel_ind _ a).
-    intros; apply dp_path_transport.
-    apply path_ishprop.
+    intros; apply path_ishprop.
   Defined.
 
   (** And its recursion version. *)

theories/Algebra/Groups/FreeProduct.v

@@ -242,7 +242,6 @@ Section FreeProduct.
     snrapply Coeq_ind.
     1: exact e.
     intro a.
-    nrapply dp_path_transport^-1%equiv.
     destruct a as [ [ [ [a | a ] | a] | a ] | a ].
     + destruct a as [[[x h1] h2] y].
       apply dp_compose.
@@ -267,7 +266,7 @@ Section FreeProduct.
   Proof.
     srapply amal_type_ind.
     1: exact e.
-    all: intros; apply dp_path_transport, path_ishprop.
+    all: intros; apply path_ishprop.
   Defined.
 
   (** From which we can derive the non-dependent eliminator / recursion principle *)

theories/Colimits/Coeq.v

@@ -54,25 +54,6 @@ Proof.
   rapply GraphQuotient_rec_beta_gqglue.
 Defined.
 
-Definition Coeq_ind_dp {B A f g} (P : @Coeq B A f g -> Type)
-  (coeq' : forall a, P (coeq a))
-  (cglue' : forall b, DPath P (cglue b) (coeq' (f b)) (coeq' (g b)))
-  : forall w, P w.
-Proof.
-  srapply (Coeq_ind P coeq'); intros b.
-  apply dp_path_transport^-1, cglue'.
-Defined.
-
-Definition Coeq_ind_dp_beta_cglue {B A f g} (P : @Coeq B A f g -> Type)
-  (coeq' : forall a, P (coeq a))
-  (cglue' : forall b, DPath P (cglue b) (coeq' (f b)) (coeq' (g b)))
-  (b : B)
-  : dp_apD (Coeq_ind_dp P coeq' cglue') (cglue b) = cglue' b.
-Proof.
-  apply dp_apD_path_transport.
-  srapply Coeq_ind_beta_cglue.
-Defined.
-
 (** ** Universal property *)
 
 Definition Coeq_unrec {B A} (f g : B -> A) {P}

theories/Colimits/GraphQuotient.v

@@ -116,7 +116,6 @@ Section Flattening.
   Lemma equiv_dp_dgraphquotient (x y : A) (s : R x y) (a : F x) (b : F y)
     : DPath DGraphQuotient (gqglue s) a b <~> (e x y s a = b).
   Proof.
-    refine (_ oE dp_path_transport^-1).
     refine (equiv_concat_l _^ _).
     apply transport_DGraphQuotient.
   Defined.
@@ -132,21 +131,17 @@ Section Flattening.
     snrapply GraphQuotient_ind.
     1: exact Qgq.
     intros a b s.
-    apply equiv_dp_path_transport.
     apply dp_forall.
     intros x y.
     srapply (equiv_ind (equiv_dp_dgraphquotient a b s x y)^-1).
     intros q.
     destruct q.
-    apply equiv_dp_path_transport.
     refine (transport2 _ _ _ @ Qgqglue a b s x).
     refine (ap (path_sigma_uncurried DGraphQuotient _ _) _).
     snrapply path_sigma.
     1: reflexivity.
-    apply moveR_equiv_V.
-    simpl; f_ap.
-    lhs rapply concat_p1.
-    rapply inv_V.
+    lhs nrapply concat_p1.
+    apply inv_V.
   Defined.
 
   (** Rather than use [flatten_ind] to define [flatten_rec] we reprove this simple case. This means we can later reason about it and derive the computation rules easily. The full computation rule for [flatten_ind] takes some work to derive and is not actually needed. *)

theories/Colimits/MappingCylinder.v

@@ -33,41 +33,24 @@ Section MappingCylinder.
             (cylb : forall b, P (cyr b))
             (cylg : forall a, DPath P (cyglue a) (cyla a) (cylb (f a))).
 
-    Definition Cyl_ind_dp : forall c, P c.
-    Proof.
-      srapply Pushout_ind.
-      - apply cyla.
-      - apply cylb.
-      - intros a; apply dp_path_transport^-1, cylg.
-    Defined.
-
-    Definition Cyl_ind_dp_beta_cyglue (a : A)
-      : dp_apD Cyl_ind_dp (cyglue a) = cylg a.
-    Proof.
-      unfold Cyl_ind_dp.
-      refine ((dp_path_transport_apD _ _)^ @ _).
-      apply moveR_equiv_M.
-      rapply Pushout_ind_beta_pglue.
-    Defined.
+    Definition Cyl_ind : forall c, P c
+      := Pushout_ind _ cyla cylb cylg.
+
+    Definition Cyl_ind_beta_cyglue (a : A)
+      : apD Cyl_ind (cyglue a) = cylg a
+      := Pushout_ind_beta_pglue _ _ _ _ _.
 
   End CylInd.
 
   Section CylRec.
     Context {P : Type} (cyla : A -> P) (cylb : B -> P) (cylg : cyla == cylb o f).
 
-    Definition Cyl_rec : Cyl f -> P.
-    Proof.
-      srapply Pushout_rec.
-      - apply cyla.
-      - apply cylb.
-      - apply cylg.
-    Defined.
+    Definition Cyl_rec : Cyl f -> P
+      := Pushout_rec _ cyla cylb cylg.
 
     Definition Cyl_rec_beta_cyglue (a : A)
-      : ap Cyl_rec (cyglue a) = cylg a.
-    Proof.
-      rapply Pushout_rec_beta_pglue.
-    Defined.
+      : ap Cyl_rec (cyglue a) = cylg a
+      := Pushout_rec_beta_pglue _ _ _ _ _.
 
   End CylRec.
 
@@ -82,7 +65,7 @@ Section MappingCylinder.
       + exact f.
       + exact idmap.
       + reflexivity.
-    - srapply Cyl_ind_dp.
+    - srapply Cyl_ind.
       + intros a; cbn.
         symmetry; apply cyglue.
       + intros b; reflexivity.