`{Funext} {D : Type} {A : Type} {B : D -> A -> Type} {t1 t2 : D} {d : t1 = t2} {f : forall x, B t1 x} {g : forall x, B t2 x} : (forall x, DPath (fun t => B t x) d (f x) (g x)) <~> DPath (fun t => forall x, B t x) d f g. Proof. destruct d. apply equiv_path_forall. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.