Update theories/Cubical/DPath.v

Co-authored-by: Dan Christensen <[email protected]>

theories/Cubical/DPath.v

@@ -27,8 +27,7 @@ Defined.
 (** We have reflexivity for DPaths, this helps coq guess later *)
 Definition dp_id {A} {P : A -> Type} {a : A} {x : P a} : DPath P 1 x x := 1%path.
 
-(** Althought 1%dpath is definitionally 1%path, coq cannot guess this so it helps
-   to have 1 be a dpath before hand. *)
+(** Although [1%dpath] is definitionally [1%path], coq cannot guess this so it helps to have [1] be a dpath beforehand. *)
 Notation "1" := dp_id : dpath_scope.
 
 (** DPath induction *)