proposition: Lemma isaprop_isInjective {X Y : UU} (f : X -> Y) : isaprop (isInjective f).
proof: Proof. intros. unfold isInjective. apply impred; intro. apply impred; intro. apply isapropisweq. Defined.
imports: UniMath.Foundations.PartC