hartogs_number' : Ordinal. Proof. set (carrier := {B : Ordinal@{A _} & card B <= card A}). set (relation := fun (B C : carrier) => B.1 < C.1). exists carrier relation. snrapply (isordinal_simulation pr1). 1-4: exact _. - apply isinj_embedding, (mapinO_pr1 (Tr (-1))). - constructor. + intros a a' a_a'. exact a_a'. + intros [B small_B] C C_B; cbn in *. apply tr. unshelve eexists (C; _); cbn; auto. revert small_B. srapply Trunc_rec. intros [f isinjective_f]. apply tr. destruct C_B as [b ->]. exists (fun '(x; x_b) => f x); cbn. intros [x x_b] [y y_b] fx_fy. apply path_sigma_hprop; cbn. apply (isinjective_f x y). exact fx_fy. 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.