{A B : Type} (f g : A <~> B) : (f == g) <~> (path_universe f = path_universe g). Proof. refine (_ oE equiv_path_arrow f g). refine (_ oE equiv_path_equiv f g). exact (equiv_ap (equiv_path A B)^-1 _ _). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.