(X : HSet) n : GCH -> infinite X -> powfix X -> InjectsInto (HN X) (power_iterated X n) -> InjectsInto X (HN X). Proof. intros gch H1 H2 Hi. induction n. - by apply HN_ninject in Hi. - destruct (gch (Build_HSet (power_iterated X n)) (Build_HSet (power_iterated X n + HN X))) as [H|H]. + by apply infinite_power_iterated. + apply tr. exists inl. intros x x'. apply path_sum_inl. + eapply InjectsInto_trans. * apply InjectsInto_sum; try apply Hi. apply tr, Injection_power. exact _. * cbn. specialize (H2 (S n)). cbn in H2. rewrite H2. apply tr, Injection_refl. + apply IHn. eapply InjectsInto_trans; try apply H. apply tr. exists inr. intros x y. apply path_sum_inr. + apply InjectsInto_trans with (power_iterated X (S n)); try apply tr, Injection_power_iterated. cbn. apply (Cantor_injects_injects H). rewrite (H2 n). apply tr, Injection_refl. 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.