proposition: Lemma inject_sings : (P + ~ P) -> Injection (X -> HProp) sings.
proof: Proof. intros HP. unshelve eexists. - intros p. exists p. apply tr. now 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.
imports: HoTT(TruncType abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card)