{A B : Type} (f : A <~> B) (z : A) : ap (transport idmap (path_universe f)^) (transport_path_universe f z) @ transport_path_universe_V f (f z) @ eissect f z = transport_Vp idmap (path_universe f) z. Proof. pattern f. refine (equiv_ind (equiv_path A B) _ _ _); intros p. refine (_ @ ap_transport_Vp_idmap p (path_universe (equiv_path A B p)) (eissect (equiv_path A B) p) z). apply whiskerR. apply concat2. - apply ap. apply transport_path_universe_equiv_path. - apply transport_path_universe_V_equiv_path. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.