Definition isporesrel {X : UU} (L : hrel X) (P : hsubtype X) (isl : ispreorder L) : ispreorder (resrel L P). Proof. intros. apply (make_dirprod (istransresrel L P (pr1 isl)) (isreflresrel L P (pr2 isl))). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.