proposition: Theorem GCH_LEM {PR : PropResizing} {UA : Univalence} : GCH -> (forall P : HProp, P \/ ~ P).
proof: 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.
imports: HoTT(TruncType abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card)