Definition abgrshombinop_rinvax {X Y : abgr} (f : monoidfun X Y) : @abmonoidshombinop X Y f (abgrshombinop_inv f) = unelmonoidfun X Y.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.