∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type u_4}
  (U : I → C) (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) (c : T ⟶ U k),
  CategoryTheory.PresheafOfGroups.OneCochain.ev 1 i j a b * CategoryTheory.PresheafOfGroups.OneCochain.ev 1 j k b c =
    CategoryTheory.PresheafOfGroups.OneCochain.ev 1 i k a c