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