{A : Type} {x1 x2 y : A} (p : x1 = x2) (q : x1 = y) r : p^ @ q = r <~> DPath (fun x => x = y) p q r. Proof. apply equiv_concat_l, transport_paths_l. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.