X Y := { f : X -> Y | IsInjective f }. Global Instance Injection_refl : Reflexive . Proof. intros X. exists (fun x => x). intros x x'. done. Qed.
Require Import HoTT.Universes.TruncType. Require Import HoTT.Classes.interfaces.abstract_algebra.