{A B C : Type} (f : A <~> B) (g : B <~> C) : path_universe (g o f) = path_universe f @ path_universe g := path_universe_compose_uncurried f g.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.