Definition binopeqrelabgrdiff (X : abmonoid) : binopeqrel (abmonoiddirprod X X) := make_binopeqrel (eqrelabgrdiff X) (isbinophrelabgrdiff X).
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.