hartogs_number_carrier <~> hartogs_number'. Proof. apply equiv_inverse. unshelve eexists. - intros a. exists (uni_fix (hartogs_number'_injection.1 a)). apply equiv_smalltype, tr. exists a. reflexivity. - snrapply isequiv_surj_emb. + apply BuildIsSurjection. intros [X HX]. eapply merely_destruct. * eapply equiv_smalltype, 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. by apply hartogs_number'_injection.2. Qed.
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.