`{Univalence} (A B : Ordinal) : forall f : A <~> B, (forall a a' : A, a < a' <-> f a < f a') -> A = B. Proof. intros f H0. apply equiv_path_Ordinal. exists f. exact H0. 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.