fact: Definition equiv_path_universe (A B : Type) : (A <~> B) <~> (A = B) := Build_Equiv _ _ (@path_universe_uncurried A B) isequiv_path_universe.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod