Lemma isweqimplimpl {X Y : UU} (f : X -> Y) (g : Y -> X) (isx : isaprop X) (isy : isaprop Y) : isweq f. Proof. intros. assert (isx0: ∏ x : X, paths (g (f x)) x) by (intro; apply proofirrelevance; apply isx). assert (isy0 : ∏ y : Y, paths (f (g y)) y) by (intro; apply proofirrelevance; apply isy). apply (isweq_iso f g isx0 isy0). Defined.