`{Univalence} `{PropResizing} {X : Type} (F : X -> Ordinal) : Ordinal. Proof. set (f := fun x : {i : X & F i} => ↓x.2). set (carrier := image f : Type@{i}). set (relation := fun A B : carrier => smalltype (factor2 f A < factor2 f B) : Type@{i}). exists carrier relation. snrapply (isordinal_simulation (factor2 f)). 1-4: exact _. - apply isinjective_factor2. - constructor. + intros x x' x_x'. unfold lt, relation. apply equiv_smalltype in x_x'. exact x_x'. + nrefine (image_ind_prop f _ _). 1: exact _. intros a. change (factor2 f (class_of _ a)) with (f a). intros B B_fa. apply tr. exists (factor1 f (a.1; out (bound B_fa))). unfold lt, relation. change (factor2 f (factor1 f ?A)) with (f A). unfold f. assert (↓(out (bound B_fa)) = B) as ->. { rewrite (path_initial_segment_simulation out). symmetry. apply bound_property. } split. * apply equiv_smalltype. exact B_fa. * 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.