Definition monaction_functor (Mon : monoid) (C : category) := contr_cat_action (monoid_weq_contr_category Mon) C.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.Categories.HSET.Core.