Definition pullback_binopeqrel {X Y : setwithbinop} (f : binopfun X Y) (R : binopeqrel Y) : binopeqrel X. Proof. use make_binopeqrel. - use make_eqrel. + intros x x'. exact (R (f x) (f x')). + apply iseqrelconstr. * intros x1 x2 x3 r1 r2. exact (eqreltrans R _ _ _ r1 r2). * intro x. exact (eqrelrefl R _). * intros x x' r. exact (eqrelsymm R _ _ r). - apply make_isbinophrel; simpl; intros x1 x2 x3 r; rewrite !binopfunisbinopfun. + exact (binopeqrel_resp_left R _ r). + exact (binopeqrel_resp_right R _ r). Defined.