Definition istransresrel {X : UU} (L : hrel X) (P : hsubtype X) (isl : istrans L) : istrans (resrel L P). Proof. intros. intros x1 x2 x3 r12 r23. apply (isl _ (pr1 x2) _ r12 r23). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.