Definition isTotalOrder {X : hSet} (R : hrel X) : hProp := make_hProp (isPartialOrder R × istotal R) (isapropdirprod _ _ (isaprop_isPartialOrder R) (isaprop_istotal R)).
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.