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