proposition: Lemma hartogs_equiv : hartogs_number_carrier <~> hartogs_number'.
proof: Proof. apply equiv_inverse. unshelve eexists. - intros a. exists (uni_fix (hartogs_number'_injection.1 a)). apply equiv_resize_hprop, tr. exists a. reflexivity. - snrapply isequiv_surj_emb. + apply BuildIsSurjection. intros [X HX]. eapply merely_destruct. * eapply equiv_resize_hprop, HX. * intros [a <-]. cbn. apply tr. exists a. cbn. apply ap. apply path_ishprop. + apply isembedding_isinj_hset. intros a b. intros H % pr1_path. cbn in H. specialize (injective_uni_fix (hartogs_number'_injection.1 a) (hartogs_number'_injection.1 b)). intros H'. apply H' in H. now apply hartogs_number'_injection.2. Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card) HoTT.Sets(Ordinals Powers)