∀ (C : Type u),
  CategoryTheory.FreeMonoidalCategory.tensorFunc C =
    {
      obj := fun X =>
        CategoryTheory.Discrete.functor fun n =>
          CategoryTheory.MonoidalCategoryStruct.tensorObj
            (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n }) X,
      map := fun {X Y} f =>
        CategoryTheory.Discrete.natTrans fun x =>
          CategoryTheory.MonoidalCategoryStruct.whiskerLeft
            (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := x.as }) f,
      map_id := ⋯, map_comp := ⋯ }