Definition isEquivalence_to_isweq {X Y} {f:X->Y} : isEquivalence f -> isweq f. Proof. intros i. set (g := isEquivalence_toInverseFunction i). set (p := isEquivalence_toTargetHomotopy i). set (q := isEquivalence_toSourceHomotopy i). set (h := isEquivalence_toAdjointness i). intro y. exists (g y,,p y). intros xe. simple refine (hfibertriangle2 _ _ _ _ _). - exact (! (q (pr1 xe)) @ maponpaths g (pr2 xe)). - induction xe as [x e]; simpl. induction e; simpl. rewrite pathscomp0rid. rewrite maponpathsinv0. rewrite h. now rewrite pathsinv0l. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.