∀ (k G : Type u_1) [inst : CommRing k] [inst_1 : Monoid G] ⦃X Y : ModuleCat k⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((Rep.trivialFunctor k G).comp (Rep.coinvariantsFunctor k G)).map f)
      (Rep.desc (CategoryTheory.CategoryStruct.id ((Rep.trivialFunctor k G).obj Y))) =
    CategoryTheory.CategoryStruct.comp (Rep.desc (CategoryTheory.CategoryStruct.id ((Rep.trivialFunctor k G).obj X)))
      ((CategoryTheory.Functor.id (ModuleCat k)).map f)