proposition: Lemma equiv_path_equiv {A B : Type} (e1 e2 : A <~> B) : (e1 = e2 :> (A -> B)) <~> (e1 = e2 :> (A <~> B)).
proof: 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.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths