(X : HSet) : GCH -> InjectsInto X (HN (Build_HSet (Build_HSet (nat + X) -> HProp))). Proof. intros gch. eapply InjectsInto_trans with (nat + X). - apply tr. exists inr. intros x y. apply path_sum_inr. - apply '; trivial. exists inl. intros x y. apply path_sum_inl. 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.