∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep k G} {B : Rep k H} {C : Rep k K} (f : G →* H) (g : H →* K) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B)
  (ψ : B ⟶ (Action.res (ModuleCat k) g).obj C),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap f φ) (groupHomology.chainsMap g ψ) =
    groupHomology.chainsMap (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Action.res (ModuleCat k) f).map ψ))