`{Univalence} `{PropResizing} {X : Type} (F : X -> Ordinal) : forall x, F x <= limit F. Proof. set (f := fun x : {i : X & F i} => ↓x.2). intros x. unfold le, le_on_Ordinal. exists (fun u => factor1 f (x; u)). split. - intros u v u_v. change (smalltype (f (x; u) < f (x; v))). apply equiv_smalltype. apply isembedding_initial_segment. exact u_v. - intros u. nrefine (image_ind_prop f _ _). 1: exact _. intros a a_u. change (smalltype (f a < f (x; u))) in a_u. apply equiv_smalltype in a_u. apply tr. exists (out (bound a_u)). split. + apply initial_segment_property. + apply (isinjective_factor2 f); simpl. change (factor2 f (factor1 f ?A)) with (f A). unfold f. rewrite (path_initial_segment_simulation out). symmetry. apply bound_property. Qed.
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.