`{Funext} {A : Type} {B C : A -> Type} {a1 a2 : A} {p : a1 = a2} {f : B a1 -> C a1} {g : B a2 -> C a2} : (forall x, DPath C p (f x) (g (p # x))) <~> DPath (fun x => B x -> C x) p f g. Proof. destruct p. apply equiv_path_forall. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.