GCH_injects' (X : HSet) : GCH -> infinite X -> InjectsInto X (HN (Build_HSet (X -> HProp))). Proof. intros gch HX. eapply InjectsInto_trans; try apply tr, Injection_power; try apply X. apply (@Sierpinski_step (Build_HSet (X -> HProp)) HN_bound gch). - apply infinite_inject with X; trivial. apply Injection_power. apply X. - intros n. cbn. rewrite !power_iterated_shift. eapply path_infinite_power. cbn. by apply infinite_power_iterated. - apply HN_inject. 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.