changed '@D' notation to '@Dp'

theories/Basics/Notations.v

@@ -172,7 +172,7 @@ Reserved Notation "s ^v$" (at level 20).
 Reserved Infix "@@h" (at level 30).
 Reserved Infix "@@v" (at level 30).
 Reserved Infix "@lr" (at level 30).
-Reserved Notation "x '@D' y"  (at level 20).
+Reserved Notation "x '@Dp' y"  (at level 20).
 Reserved Notation "x '@Dr' y" (at level 20).
 Reserved Notation "x '@Dl' y" (at level 20).
 Reserved Notation "x '^D'" (at level 3).

theories/Cubical/DPath.v

@@ -109,7 +109,7 @@ Proof.
   exact concat.
 Defined.
 
-Notation "x '@D' y" := (dp_concat x y) : dpath_scope.
+Notation "x '@Dp' y" := (dp_concat x y) : dpath_scope.
 
 (* Concatenation of dependent paths with non-dependent paths *)
 Definition dp_concat_r {A} {P : A -> Type} {a0 a1}
@@ -143,7 +143,7 @@ Notation "x '^D'" := (dp_inverse x) : dpath_scope.
 (* dp_apD distributes over concatenation *)
 Definition dp_apD_pp (A : Type) (P : A -> Type) (f : forall a, P a)
   {a0 a1 a2 : A} (p : a0 = a1) (q : a1 = a2)
-  : dp_apD f (p @ q) = (dp_apD f p) @D (dp_apD f q).
+  : dp_apD f (p @ q) = (dp_apD f p) @Dp (dp_apD f q).
 Proof.
   by destruct p, q.
 Defined.
@@ -158,7 +158,7 @@ Defined.
 (* dp_const preserves concatenation *)
 Definition dp_const_pp {A B : Type} {a0 a1 a2 : A}
   {p : a0 = a1} {q : a1 = a2} {x y z : B} (r : x = y) (s : y = z)
-  : dp_const (p:=p @ q) (r @ s) = (dp_const (p:=p) r) @D (dp_const (p:=q) s).
+  : dp_const (p:=p @ q) (r @ s) = (dp_const (p:=p) r) @Dp (dp_const (p:=q) s).
 Proof.
   by destruct p,q.
 Defined.
@@ -169,28 +169,28 @@ Section DGroupoid.
     {b0 : P a0} {b1 : P a1} {dp : DPath P p b0 b1}.
 
   Definition dp_concat_p1
-    : DPath (fun t => DPath _ t _ _) (concat_p1 _) (dp @D 1) dp.
+    : DPath (fun t => DPath _ t _ _) (concat_p1 _) (dp @Dp 1) dp.
   Proof.
     destruct p.
     apply concat_p1.
   Defined.
 
   Definition dp_concat_1p
-    : DPath (fun t => DPath _ t _ _) (concat_1p _) (1 @D dp) dp.
+    : DPath (fun t => DPath _ t _ _) (concat_1p _) (1 @Dp dp) dp.
   Proof.
     destruct p.
     apply concat_1p.
   Defined.
 
   Definition dp_concat_Vp
-    : DPath (fun t => DPath _ t _ _) (concat_Vp _) (dp^D @D dp) 1.
+    : DPath (fun t => DPath _ t _ _) (concat_Vp _) (dp^D @Dp dp) 1.
   Proof.
     destruct p.
     apply concat_Vp.
   Defined.
 
   Definition dp_concat_pV
-    : DPath (fun t => DPath _ t _ _) (concat_pV _) (dp @D dp^D) 1.
+    : DPath (fun t => DPath _ t _ _) (concat_pV _) (dp @Dp dp^D) 1.
   Proof.
     destruct p.
     apply concat_pV.
@@ -204,15 +204,15 @@ Section DGroupoid.
 
     Definition dp_concat_pp_p
       : DPath (fun t => DPath _ t _ _) (concat_pp_p _ _ _)
-        ((dp @D dq) @D dr) (dp @D (dq @D dr)).
+        ((dp @Dp dq) @Dp dr) (dp @Dp (dq @Dp dr)).
     Proof.
       destruct p, q, r.
       apply concat_pp_p.
     Defined.
 
     Definition dp_concat_p_pp
       : DPath (fun t => DPath _ t _ _) (concat_p_pp _ _ _)
-        (dp @D (dq @D dr)) ((dp @D dq) @D dr).
+        (dp @Dp (dq @Dp dr)) ((dp @Dp dq) @Dp dr).
     Proof.
       destruct p, q, r.
       apply concat_p_pp.

theories/Cubical/DPathSquare.v

@@ -56,7 +56,7 @@ Definition equiv_ds_dpath {A} (P : A -> Type) {a00 a10 a01 a11 : A}
   (s : px0 @ p1x = p0x @ px1) {b00 b10 b01 b11}
   {qx0 : DPath P px0 b00 b10} {qx1 : DPath P px1 b01 b11}
   {q0x : DPath P p0x b00 b01} {q1x : DPath P p1x b10 b11}
-  : DPath (fun p => DPath P p b00 b11) s (qx0 @D q1x) (q0x @D qx1)
+  : DPath (fun p => DPath P p b00 b11) s (qx0 @Dp q1x) (q0x @Dp qx1)
     <~> DPathSquare P (sq_path s) qx0 qx1 q0x q1x.
 Proof.
   set (s' := sq_path s).

theories/Homotopy/ClassifyingSpace.v

@@ -59,7 +59,7 @@ Module Export ClassifyingSpace.
       (bbase' : P bbase)
       (bloop' : forall x, DPath P (bloop x) bbase' bbase')
       (bloop_pp' : forall x y,  DPathSquare P (sq_G1 (bloop_pp x y))
-        (bloop' (x * y)) ((bloop' x) @D (bloop' y)) 1 1) x : P x
+        (bloop' (x * y)) ((bloop' x) @Dp (bloop' y)) 1 1) x : P x
       := match x with
             bbase => (fun _ _ => bbase')
          end bloop' bloop_pp'.
@@ -70,7 +70,7 @@ Module Export ClassifyingSpace.
      `{forall x, IsTrunc 1 (P x)}
       (bbase' : P bbase) (bloop' : forall x, DPath P (bloop x) bbase' bbase')
       (bloop_pp' : forall x y,  DPathSquare P (sq_G1 (bloop_pp x y))
-        (bloop' (x * y)) ((bloop' x) @D (bloop' y)) 1 1) (x : G)
+        (bloop' (x * y)) ((bloop' x) @Dp (bloop' y)) 1 1) (x : G)
       : dp_apD (ClassifyingSpace_ind P bbase' bloop' bloop_pp') (bloop x)
         = bloop' x.
     Proof. Admitted.

theories/Homotopy/Smash.v

@@ -118,7 +118,7 @@ Section Smash.
     (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
     (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (a b : X)
     : dp_apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel' a b)
-    = (Pgl a) @D ((Pgl b)^D).
+    = (Pgl a) @Dp ((Pgl b)^D).
   Proof.
     unfold gluel'.
     rewrite dp_apD_pp, dp_apD_V.
@@ -130,7 +130,7 @@ Section Smash.
     (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
     (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (a b : Y)
     : dp_apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer' a b)
-    = (Pgr a) @D ((Pgr b)^D).
+    = (Pgr a) @Dp ((Pgr b)^D).
   Proof.
     unfold gluer'.
     rewrite dp_apD_pp, dp_apD_V.
@@ -142,7 +142,7 @@ Section Smash.
     (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
     (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (a : X) (b : Y)
     : dp_apD (Smash_ind Psm Pl Pr Pgl Pgr) (glue a b)
-    = ((Pgl a) @D ((Pgl pt)^D)) @D ((Pgr pt) @D ((Pgr b)^D)).
+    = ((Pgl a) @Dp ((Pgl pt)^D)) @Dp ((Pgr pt) @Dp ((Pgr b)^D)).
   Proof.
     by rewrite dp_apD_pp, Smash_ind_beta_gluel', Smash_ind_beta_gluer'.
   Qed.