∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {S : C} {W X Y Z : CategoryTheory.PreZeroHypercover S}
  (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)