{A B : Type} (f : A <~> B) (z : A) : transport (fun X:Type => X) (path_universe_uncurried f) z = f z. Proof. revert f. equiv_intro (equiv_path A B) p. exact (ap (fun s => transport idmap s z) (eissect _ p)). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.