Definition abgrdiffinv (X : abmonoid) : abgrdiffcarrier X → abgrdiffcarrier X := setquotfun (hrelabgrdiff X) (eqrelabgrdiff X) (abgrdiffinvint X) (abgrdiffinvcomp X).
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.