∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal],
  F.mapAddGrp =
    { obj := fun A => { X := F.obj A.X, addGrp := CategoryTheory.Functor.addGrpObjObj },
      map := fun {X Y} f => CategoryTheory.AddGrp.homMk' (F.mapAddMon.map f.hom), map_id := ⋯, map_comp := ⋯ }