Lemma isweqinclandsurj {X Y : UU} (f : X -> Y) : isincl f -> issurjective f -> isweq f. Proof. intros Hincl Hsurj. intro y. set (H := make_hProp (iscontr (hfiber f y)) (isapropiscontr _)). apply (Hsurj y H). intro x. simpl. apply iscontraprop1. - apply Hincl. - apply x. Defined.