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