equiv_dp_compose' {A B} (f : A -> B) (P : B -> Type) {x y : A} {p : x = y} {q : f x = f y} (r : ap f p = q) {u : P (f x)} {v : P (f y)} : DPath (fun x => P (f x)) p u v <~> DPath P q u v. Proof. by destruct r, p. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.