{PR : PropResizing} {UA : Univalence} : GCH -> (forall P : HProp, P \/ ~ P). Proof. intros gch P. eapply (CH_LEM (Build_HSet nat)); try exact _. intros H1 H2 H3. pose (sings := { p : nat -> HProp | sing (Build_HSet nat) p \/ (P + ~ P) }). destruct (gch (Build_HSet nat) (Build_HSet sings)) as [H|H]. - cbn. exists idmap. apply isinj_idmap. - apply tr. apply H1. - apply tr. apply H2. - apply Empty_rec. eapply merely_destruct; try apply H. apply H3. - apply H. Qed.
From HoTT Require Import TruncType abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card.