{A B : Type} (f : A <~> B) : path_universe_uncurried f^-1 = (path_universe_uncurried f)^. Proof. revert f. equiv_intro ((equiv_path_universe A B)^-1) p. simpl. transitivity (p^). 2: exact (inverse2 (eisretr (equiv_path_universe A B) p)^). transitivity (path_universe_uncurried (equiv_path B A p^)). - by refine (ap _ (equiv_path_V A B p)^). - by refine (eissect (equiv_path B A) p^). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.