∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] (X Y : P.FullSubcategory),
  CategoryTheory.Functor.LaxMonoidal.μ P.ι X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (P.ι.obj X) (P.ι.obj Y))