`(f : A -> B) `{IsEquiv A B f} : path_universe (f^-1) = (path_universe f)^ := path_universe_V_uncurried (Build_Equiv A B f _).
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.