Lemma incl_injectivity {X Y : UU} (f : X -> Y) : isincl f ≃ isInjective f. Proof. intros. apply weqimplimpl. - apply isweqonpathsincl. - apply isinclweqonpaths. - apply isapropisincl. - apply isaprop_isInjective. Defined.