`{PropResizing} `{Univalence} {A : Ordinal} (a b : A) : a < b <-> ↓a < ↓b. Proof. split. - intros a_b. exists (in_ a a_b). exact (path_initial_segment_simulation out (in_ a a_b)). - intros a_b. assert (a = out (bound a_b)) as ->. { apply (injective initial_segment). rewrite (path_initial_segment_simulation out). apply bound_property. } apply initial_segment_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.