{A B:Type} (C : A -> B -> Type) (x1 x2:A) (p:x1=x2) (f:forall (y1:B), C x1 y1) (g:forall (y2:B), C x2 y2) : (forall (y1:B), transport (fun x => C x y1) p (f y1) = g y1) <~> (transport (fun x => forall y:B, C x y) p f = g). Proof. destruct p. apply equiv_path_forall. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids