{A B C : Type} (f : A <~> B) (g : B <~> C) : path_universe_uncurried (equiv_compose g f) = path_universe_uncurried f @ path_universe_uncurried g. Proof. revert f. equiv_intro (equiv_path A B) f. revert g. equiv_intro (equiv_path B C) g. refine ((ap path_universe_uncurried (equiv_path_pp f g))^ @ _). refine (eta_path_universe (f @ g) @ _). apply concat2; symmetry; apply eta_path_universe. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.