proposition: Lemma lt_successor `{PropResizing} `{Univalence} (A : Ordinal) : A < successor A.
proof: 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_resize_hprop in Ha. destruct Ha. + intros [[a | []] Ha]. * unfold in_. cbn. f_ap. assert (IsHProp (resize_hprop Unit)) by exact _. apply path_ishprop. * destruct ((equiv_resize_hprop _)^-1 Ha). + intros a. reflexivity. - cbn. intros a a'. reflexivity. Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)