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