proposition: Lemma path_Ordinal `{Univalence} (A B : Ordinal) : forall f : A <~> B, (forall a a' : A, a < a' <-> f a < f a') -> A = B.
proof: Proof. intros f H0. apply equiv_path_Ordinal. exists f. exact H0. Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)