proposition: Lemma isembedding_initial_segment `{PropResizing} `{Univalence} {A : Ordinal} (a b : A) : a < b <-> ↓a < ↓b.
proof: 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.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)