Definition isInjectiveFunction {X Y : hSet} (f : X -> Y) : hProp. Proof. intros. exists (∏ (x x': X), f x = f x' -> x = x'). abstract ( intros; apply impred; intro x; apply impred; intro y; apply impred; intro e; apply setproperty) using isaprop_isInjectiveFunction. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.