Theorem isweqezmaphf {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (ye : hfiber g z) : isweq (ezmaphf f g z ye). Proof. intros. set (ff := ezmaphf f g z ye). set (gg := invezmaphf f g z ye). assert (egf : ∏ xe : _ , (gg (ff xe)) = xe). induction ye as [ y e ]. induction e. intro xe. apply (hfibertriangle2 f (gg (ff xe)) xe (idpath (pr1 xe))). induction xe as [ x ex ]. simpl in ex. induction ex. simpl. apply idpath. assert (efg : ∏ xee' : _ , (ff (gg xee')) = xee'). induction ye as [ y e ]. induction e. intro xee'. assert (hint : (ff (gg xee')) = (ffgg f g (g y) (make_hfiber g y (idpath _)) xee')). induction xee' as [ xe e' ]. induction xe as [ x e ]. apply idpath. apply (pathscomp0 hint (homotffggid _ _ _ _ xee')). apply (isweq_iso _ _ egf efg). Defined.