∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep k H} {B : Rep k G} (f : G →* H)
  (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupCohomology.cocycles₁ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ 1)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₁ f φ) h)