proposition: Lemma monoidfuninvtoinv {X Y : gr} (f : monoidfun X Y) (x : X) : f (grinv X x) = grinv Y (f x).
proof: Proof. intros. apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is (pr2 Y) (f x)))). simpl. change (paths (op (pr1 f (grinv X x)) (pr1 f x)) (op (grinv Y (pr1 f x)) (pr1 f x))). rewrite (grlinvax Y (pr1 f x)). destruct (pr1 (pr2 f) (grinv X x) x). rewrite (grlinvax X x). apply (pr2 (pr2 f)). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids