{PR : PropResizing} X : IsHSet X -> Injection X (X -> HProp). Proof. intros HX. set (f (x : X) := fun y => Build_HProp (smalltype (x = y))). exists f. intros x x' H. eapply equiv_smalltype. change (f x x'). rewrite H. cbn. apply equiv_smalltype. reflexivity. Qed.
From HoTT Require Import Basics Types TruncType. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card Spaces.Nat.Core.