`{PropResizing} `{Univalence} (A : Ordinal) : A < successor A. Proof. exists (inr tt). srapply path_Ordinal. - srapply equiv_adjointify. + intros a. srapply in_. * exact (inl a). * exact tt. + intros [[a | []] Ha]; cbn in *. * exact a. * apply equiv_smalltype in Ha. destruct Ha. + intros [[a | []] Ha]. * unfold in_. cbn. f_ap. assert (IsHProp (smalltype Unit)) by exact _. apply path_ishprop. * destruct (equiv_smalltype _ Ha). + intros a. reflexivity. - cbn. intros a a'. reflexivity. 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.