Lemma grinvandmonoidfun (X Y : gr) {f : X → Y} (is : ismonoidfun f) (x : X) : f (x^-1) = (f x)^-1. Proof. apply (grrcan Y (f x)). rewrite <- (pr1 is _ _). rewrite (grlinvax X). rewrite (grlinvax Y). apply (pr2 is). Qed.
Require Import UniMath.MoreFoundations.Subtypes.