fact: Definition monaction_equivariant_map {C : category} {M : monoid} {X Y : ob C} (actX : monaction_as_morphism M X) (actY : monaction_as_morphism M Y) : UU := ∑ f : X --> Y, ∏ m, actX m · f = f · actY m.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.PartA UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Additive UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.Categories.HSET.Core