{UA : Univalence} {PR : PropResizing} {LEM : ExcludedMiddle} : GCH -> Choice_type. Proof. intros gch. apply WO_AC. intros X. apply tr. exists (hartogs_number (Build_HSet (Build_HSet (nat + X) -> HProp))). unshelve eapply (@GCH_injects UA LEM PR hartogs_number _ 3 _ X gch). - intros Y. intros H. eapply merely_destruct; try apply H. apply hartogs_number_no_injection. - intros Y. apply tr. apply hartogs_number_injection. Qed.
From HoTT Require Import TruncType ExcludedMiddle abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card. From HoTT Require Import Equiv.BiInv. From HoTT Require Import HIT.unique_choice. From HoTT.Sets Require Import Ordinals Hartogs Powers GCH AC.