Definition setwith2binopquot {X : setwith2binop} (R : twobinopeqrel X) : setwith2binop. Proof. exists (setquotinset R). set (qt := setquot R). set (qtset := setquotinset R). assert (iscomp1 : iscomprelrelfun2 R R (@op1 X)) by apply (pr1 (iscomp2binoptransrel (pr1 R) (eqreltrans _) (pr2 R))). set (qtop1 := setquotfun2 R R (@op1 X) iscomp1). assert (iscomp2 : iscomprelrelfun2 R R (@op2 X)) by apply (pr2 (iscomp2binoptransrel (pr1 R) (eqreltrans _) (pr2 R))). set (qtop2 := setquotfun2 R R (@op2 X) iscomp2). simpl. exact (qtop1 ,, qtop2). Defined.