∀ (k G : Type u_1) [inst : CommRing k] [inst_1 : Monoid G] (X : Rep k G),
  CategoryTheory.CategoryStruct.comp
      ((Rep.coinvariantsFunctor k G).map
        ({ app := fun X => { hom := (Rep.coinvariantsMk k G).app X, comm := ⋯ }, naturality := ⋯ }.app X))
      ({ app := fun X => Rep.desc (CategoryTheory.CategoryStruct.id ((Rep.trivialFunctor k G).obj X)),
            naturality := ⋯ }.app
        ((Rep.coinvariantsFunctor k G).obj X)) =
    CategoryTheory.CategoryStruct.id ((Rep.coinvariantsFunctor k G).obj X)