∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep k G} {B : Rep k H} (f : G →* H)
  (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) {Z : ModuleCat k} (h : (groupHomology.shortComplexH2 B).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ f φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 B).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.i
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap₂ f φ) h)