∀ (k : Type u_1) {G H : Type u_1} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (X : Rep k G), Rep.coindMap φ (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (Rep.coind φ X)