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