{A B : Type} {f g : A <~> B} (p q : f == g) : (p == q) <~> (path2_universe p = path2_universe q). Proof. refine (_ oE equiv_path_forall p q). refine (_ oE equiv_ap (equiv_path_arrow f g) p q). refine (_ oE equiv_ap (equiv_path_equiv f g) _ _). unfold path2_universe, equiv_path2_universe. simpl. refine (equiv_ap (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.