{A : Type} {B C : A -> Type} {x1 x2 : A} (p : x1 = x2) (f : B x1 <~> C x1) (y : B x2) : (transport (fun x => B x <~> C x) p f) y = p # (f (p^ # y)). Proof. destruct p; auto. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.