Ordinal <~> { R : { A : Type & Relation A } & IsOrdinal _ R.2 }. Proof. transitivity { A : Type & { R : Relation A & IsOrdinal A R } }. { symmetry. issig. } apply equiv_sigma_assoc'. Defined.
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.