∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C)
  {Z : CochainComplex (ModuleCat k) ℕ} (h : groupCohomology.inhomogeneousCochains C ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.cochainsMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap (MonoidHom.id G) φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap (MonoidHom.id G) ψ) h)