proposition: Lemma Injection_power {PR : PropResizing} X : IsHSet X -> Injection X (X -> HProp).
proof: Proof. intros HX. set (f (x : X) := fun y => Build_HProp (resize_hprop (x = y))). exists f. intros x x' H. eapply (equiv_resize_hprop _)^-1. change (f x x'). rewrite H. cbn. apply equiv_resize_hprop. reflexivity. Qed.
imports: HoTT(Basics Types TruncType) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card Spaces.Nat.Core)