Definition eqrelabgrdiff (X : abmonoid) : @eqrel (abmonoiddirprod X X) := make_eqrel _ (iseqrelabgrdiff X).
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.