Lemma iseqclassresrel {X : UU} (R : hrel X) (P Q : hsubtype X) (is : iseqclass R Q) (is' : ∏ x, Q x -> P x) : iseqclass (resrel R P) (λ x : P, Q (pr1 x)). Proof. intros. split. - set (l1 := pr1 is). generalize l1. clear l1. simpl. apply hinhfun. intro q. split with (make_carrier P (pr1 q) (is' (pr1 q) (pr2 q))). apply (pr2 q). - split. + intros p1 p2 r12 q1. apply ((pr1 (pr2 is)) _ _ r12 q1). + intros p1 p2 q1 q2. apply ((pr2 (pr2 is)) _ _ q1 q2). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.