(injf : IsInjective f) : forall y : Y, atmost1P (fun x => f x = y). Proof. intros y x x' p q. apply (injective f). exact (p @ q^). Defined.
Require Import HoTT.Basics. Require Import Types.Universe. Require Import HSet. Require Import HIT.epi HIT.unique_choice.