fact: Definition path_universe_compose {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.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod