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