{A B} (f : A -> B) (feq : B -> IsEquiv f) : IsEquiv f. Proof. apply isequiv_contr_map. intros b. pose (feq b); exact _. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.