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