∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {B : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} B], CategoryTheory.Limits.HasZeroObject (CategoryTheory.Functor B C)