∀ {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) (x : ↥(groupHomology.cycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.map f φ 2))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H2π A)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H2π B))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ f φ)) x)