Definition prabgrdiff (X : abmonoid) : X → X → abgrdiff X := λ x x' : X, setquotpr (eqrelabgrdiff X) (x ,, x').
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.