X Y := merely (Injection X Y). Global Instance InjectsInto_refl : Reflexive . Proof. intros X. apply tr. reflexivity. Qed.
Require Import HoTT.Universes.TruncType. Require Import HoTT.Classes.interfaces.abstract_algebra.