{A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B) : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z := transport_path_universe_V_uncurried (Build_Equiv _ _ f feq) z.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.