Lemma isaprop_isPartialOrder {X : hSet} (R : hrel X) : isaprop (isPartialOrder R). Proof. intros. unfold isPartialOrder. apply isapropdirprod. { apply isaprop_ispreorder. } { apply isaprop_isantisymm. } Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.