{A B : Type} {e1 e2 : A <~> B} : (e1 = e2 :> (A -> B)) -> (e1 = e2 :> (A <~> B)) := equiv_path_equiv e1 e2. Global Instance isequiv_path_equiv {A B : Type} {e1 e2 : A <~> B} : IsEquiv (@ _ _ e1 e2) := equiv_isequiv (equiv_path_equiv e1 e2). Global Instance isequiv_ap_equiv_fun {A B : Type} (e1 e2 : A <~> B) : IsEquiv (ap (x:=e1) (y:=e2) (@equiv_fun A B)). Proof. snrapply isequiv_homotopic. - exact (equiv_path_equiv e1 e2)^-1%equiv. - exact _. - intro p. exact (ap_compose (fun v => (equiv_fun v; equiv_isequiv v)) pr1 p)^. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.