Definition issymmresrel {X : UU} (L : hrel X) (P : hsubtype X) (isl : issymm L) : issymm (resrel L P). Proof. intros. intros x1 x2 r12. apply isl. apply r12. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.