{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.AddMon C} → (hom : M.X ⟶ N.X) → [isAddMonHom_hom : CategoryTheory.IsAddMonHom hom] → M.Hom N