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