(epif : isepi f) (monof : ismono f) : IsEquiv f. Proof. pose proof (@isepi_issurj _ _ _ f epif) as surjf. pose proof (isinj_ismono _ monof) as injf. pose proof (unique_choice (fun y x => f x = y) _ (fun y => (@center _ (surjf y), atmost1P_isinj injf y))) as H_unique_choice. apply (isequiv_adjointify _ H_unique_choice.1). - intro. apply H_unique_choice.2. - intro. apply injf. apply H_unique_choice.2. Defined.
Require Import HoTT.Basics. Require Import Types.Universe. Require Import HSet. Require Import HIT.epi HIT.unique_choice.