∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (D : Type u₂)
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D],
  CategoryTheory.Functor.mapAddMonFunctor C D =
    { obj := fun F => F.mapAddMon,
      map := fun {X Y} α => { app := fun A => CategoryTheory.AddMon.Hom.mk' (α.hom.app A.X) ⋯ ⋯, naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }