{C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v', u'} D] →
      [inst_1 : CategoryTheory.MonoidalCategory D] →
        (f : C → D) →
          (X Y : CategoryTheory.FreeMonoidalCategory C) →
            (X ⟶ Y) →
              (CategoryTheory.FreeMonoidalCategory.projectObj f X ⟶ CategoryTheory.FreeMonoidalCategory.projectObj f Y)