{A B} (f : A -> B) (P : B -> Type) {x y : A} (p : x = y) {u : P (f x)} {v : P (f y)} : DPath (fun x => P (f x)) p u v <~> DPath P (ap f p) u v := dp_compose' f P (idpath (ap f p)).
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.