dpath_forall' {A : Type } (P : A -> Type) (Q: sig P -> Type) {x y : A} (h : x = y) (f : forall p, Q (x ; p)) (g : forall p, Q (y ; p)) : (forall p, transport Q (path_sigma P (x ; p) (y; _) h 1) (f p) = g (h # p)) <~> (forall p, transportD P (fun x => fun p => Q ( x ; p)) h p (f p) = g (transport P h p)). Proof. destruct h. apply 1%equiv. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.