fact: Definition OrderedSet := ∑ X:Poset, istotal (posetRelation X).
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions