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