{A B : Type} (e1 e2 : A <~> B) : (e1 = e2 :> (A -> B)) <~> (e1 = e2 :> (A <~> B)). Proof. equiv_via ((issig_equiv A B) ^-1 e1 = (issig_equiv A B) ^-1 e2). 2: symmetry; apply equiv_ap; refine _. exact (equiv_path_sigma_hprop ((issig_equiv A B)^-1 e1) ((issig_equiv A B)^-1 e2)). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.