Theorem isweq_iso {X Y : UU} (f : X -> Y) (g : Y -> X) (egf: ∏ x : X, g (f x) = x) (efg: ∏ y : Y, f (g y) = y) : isweq f. Proof. intros. unfold isweq. intro y. assert (X0 : iscontr (hfiber (f ∘ g) y)). assert (efg' : ∏ y : Y, y = f (g y)). { intro y0. apply pathsinv0. apply (efg y0). } apply (iscontrhfiberl2 (idfun _) (f ∘ g) efg' y (idisweq Y y)). apply (iscontrhfiberl1 g f egf y). apply X0. Defined.