∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesZeroMorphisms]
  [G.PreservesZeroMorphisms], (F.comp G).PreservesZeroMorphisms