proposition: Lemma hartogs_number_no_injection : ~ (exists f : hartogs_number -> A, IsInjective f).
proof: Proof. cbn. intros [f Hf]. cbn in f. assert (HN : card hartogs_number <= card A). { apply tr. now 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_resize_hprop]. unshelve eexists. -- exists a. transitivity (card hartogs_number). ++ nrapply le_Cardinal_lt_Ordinal; apply Ha. ++ apply HN. -- apply equiv_resize_hprop. cbn. exact Ha. * intros [[a Ha] H % equiv_resize_hprop]. exists a. apply equiv_resize_hprop. apply H. * intro a. apply path_sigma_hprop. apply path_sigma_hprop. reflexivity. * intro a. apply path_sigma_hprop. reflexivity. + reflexivity. Defined.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card) HoTT.Sets(Ordinals Powers)