(P + ~ P) -> Injection (X -> HProp) sings. Proof. intros HP. unshelve eexists. - intros p. exists p. apply tr. by right. - intros p q. intros H. change p with ((exist (fun r => sing r \/ (P + ~ P)) p (tr (inr HP))).1). rewrite H. cbn. reflexivity. Qed.
From HoTT Require Import TruncType abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card.