(Injection X sings -> Injection sings (X -> HProp) -> ~ (Injection sings X) -> InjectsInto (X -> HProp) sings) -> P \/ ~ P. Proof. intros ch. eapply merely_destruct; try apply ch. - unshelve eexists. + intros x. exists (hpaths x). apply tr. left. exists x. reflexivity. + intros x y. intros H % pr1_path. cbn in H. change (hpaths x y). by rewrite H. - exists (@proj1 _ _). by apply injective_proj1. - intros H. assert (HP' : ~ ~ (P + ~ P)). { intros HP. apply HP. right. intros p. apply HP. by left. } apply HP'. intros HP % inject_sings. clear HP'. apply Cantor_inj with X. by eapply (Injection_trans _ _ _ HP). - intros [i Hi]. destruct (Cantor_sing (fun p => @proj1 _ _ (i p))) as [p HP]. + intros x y H % injective_proj1. by apply Hi. + destruct (i p) as [q Hq]; cbn in *. eapply merely_destruct; try apply Hq. intros [H|H]; [destruct (HP H)|by apply tr]. Qed.
From HoTT Require Import TruncType abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card.