proposition: Theorem CH_LEM : (Injection X sings -> Injection sings (X -> HProp) -> ~ (Injection sings X) -> InjectsInto (X -> HProp) sings) -> P \/ ~ P.
proof: 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). now rewrite H. - exists (@proj1 _ _). now apply injective_proj1. - intros H. assert (HP' : ~ ~ (P + ~ P)). { intros HP. apply HP. right. intros p. apply HP. now left. } apply HP'. intros HP % inject_sings. clear HP'. apply Cantor_inj with X. now eapply (Injection_trans _ _ _ HP). - intros [i Hi]. destruct (Cantor_sing (fun p => @proj1 _ _ (i p))) as [p HP]. + intros x y H % injective_proj1. now apply Hi. + destruct (i p) as [q Hq]; cbn in *. eapply merely_destruct; try apply Hq. intros [H|H]; [destruct (HP H)|now apply tr]. Qed.
imports: HoTT(TruncType abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card)