Definition iscotransresrel {X : UU} (L : hrel X) (P : hsubtype X) (isl : iscotrans L) : iscotrans (resrel L P). Proof. intros. intros x1 x2 x3 r13. apply (isl _ _ _ r13). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.