proposition: Lemma atmost1P_isinj (injf : isinj f) : forall y : Y, atmost1P (fun x => f x = y).
proof: Proof. unfold isinj, atmost1P in *. intros. apply injf. path_induction. reflexivity. Defined.
imports: HoTT.Basics Types.Universe HSet HIT.epi HIT.unique_choice