Lemma isbinopquotrel {X : setwithbinop} (R : binopeqrel X) {L : hrel X} (is : iscomprelrel R L) (isl : isbinophrel L) : @isbinophrel (setwithbinopquot R) (quotrel is). Proof. unfold isbinophrel. split. - assert (int : ∏ (a b c : setwithbinopquot R), isaprop (quotrel is a b → quotrel is (op c a) (op c b))). { intros a b c. apply impred. intro. apply (pr2 (quotrel is _ _)). } apply (setquotuniv3prop R (λ a b c, make_hProp _ (int a b c))). exact (pr1 isl). - assert (int : ∏ (a b c : setwithbinopquot R), isaprop (quotrel is a b → quotrel is (op a c) (op b c))). { intros a b c. apply impred. intro. apply (pr2 (quotrel is _ _)). } apply (setquotuniv3prop R (λ a b c, make_hProp _ (int a b c))). exact (pr2 isl). Defined.