∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G) [inst_2 : A.IsTrivial],
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 0) (groupHomology.H0IsoOfIsTrivial A).hom =
    (groupHomology.cyclesIso₀ A).hom