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