`{PropResizing} {A : Type} {R : Lt A} `{IsOrdinal A R} (a : A) : Ordinal. Proof. srefine {| ordinal_carrier := {b : A & smalltype (b < a)} ; ordinal_relation := fun x y => x.1 < y.1 |}; try exact _. srapply (isordinal_simulation pr1). - unfold lt. exact _. - exact _. - exact _. - constructor. + intros x y x_y. exact x_y. + intros b a' a'_b; cbn in *. apply tr. assert (b_a : b.1 < a). { exact ((equiv_smalltype _) b.2). } srapply exist. { exists a'. apply equiv_smalltype. exact (transitivity a'_b b_a). } cbn. split. * exact a'_b. * reflexivity. Defined.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Colimits.Quotient. From HoTT Require Import HSet.