Definition fiber_binopeqrel {X Y : monoid} (f : monoidfun X Y) : binopeqrel X. Proof. use make_binopeqrel. - exact (same_fiber_eqrel f). - use make_isbinophrel; intros ? ? ? same; refine (monoidfunmul _ _ _ @ _ @ !monoidfunmul _ _ _). + apply maponpaths. exact same. + apply (maponpaths (λ z, z * f c)). exact same. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.