∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D],
  CategoryTheory.instHasZeroMorphismsMon = CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject