~ (exists f : hartogs_number -> A, IsInjective f). Proof. cbn. intros [f Hf]. cbn in f. assert (HN : card hartogs_number <= card A). { apply tr. by exists f. } transparent assert (HNO : hartogs_number'). { exists hartogs_number. apply HN. } apply (ordinal_initial hartogs_number' HNO). eapply (transitive_Isomorphism hartogs_number' hartogs_number). - apply isomorphism_inverse. unfold hartogs_number. exact (resize_ordinal_iso hartogs_number' hartogs_number_carrier hartogs_equiv). - assert (Isomorphism hartogs_number ↓hartogs_number) by apply isomorphism_to_initial_segment. eapply transitive_Isomorphism. 1: exact X. unshelve eexists. + srapply equiv_adjointify. * intros [a Ha % equiv_smalltype]. unshelve eexists. -- exists a. transitivity (card hartogs_number). ++ nrapply le_Cardinal_lt_Ordinal; apply Ha. ++ apply HN. -- apply equiv_smalltype. cbn. exact Ha. * intros [[a Ha] H % equiv_smalltype]. exists a. apply equiv_smalltype. apply H. * intro a. apply path_sigma_hprop. apply path_sigma_hprop. reflexivity. * intro a. apply path_sigma_hprop. reflexivity. + reflexivity. Defined.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card. From HoTT.Sets Require Import Ordinals Powers.