{D : Type u_1} →
  {D' : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} D} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C} →
              {inst_3 : CategoryTheory.MonoidalCategory C} →
                {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} →
                  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} →
                    {P : Sort u} →
                      {μₗ :
                          (c : C) →
                            (d : D) →
                              CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ⟶
                                F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)} →
                        {μₗ_naturality_left :
                            autoParam
                              (∀ {c c' : C} (f : c ⟶ c') (d : D),
                                CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d))
                                    (μₗ c' d) =
                                  CategoryTheory.CategoryStruct.comp (μₗ c d)
                                    (F.map
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)))
                              CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left._autoParam} →
                          {μₗ_naturality_right :
                              autoParam
                                (∀ (c : C) {d d' : D} (f : d ⟶ d'),
                                  CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
                                        (F.map f))
                                      (μₗ c d') =
                                    CategoryTheory.CategoryStruct.comp (μₗ c d)
                                      (F.map
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)))
                                CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right._autoParam} →
                            {μₗ_associativity :
                                autoParam
                                  (∀ (c c' : C) (d : D),
                                    CategoryTheory.CategoryStruct.comp
                                        (μₗ (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
                                        (F.map
                                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'
                                              d).hom) =
                                      CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'
                                            (F.obj d)).hom
                                        (CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
                                            (μₗ c' d))
                                          (μₗ c
                                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))))
                                  CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity._autoParam} →
                              {μₗ_unitality :
                                  autoParam
                                    (∀ (d : D),
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
                                            (F.obj d)).hom =
                                        CategoryTheory.CategoryStruct.comp
                                          (μₗ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d)
                                          (F.map
                                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
                                                d).hom))
                                    CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality._autoParam} →
                                {μₗ' :
                                    (c : C) →
                                      (d : D) →
                                        CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ⟶
                                          F.obj
                                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)} →
                                  {μₗ_naturality_left' :
                                      autoParam
                                        (∀ {c c' : C} (f : c ⟶ c') (d : D),
                                          CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f
                                                (F.obj d))
                                              (μₗ' c' d) =
                                            CategoryTheory.CategoryStruct.comp (μₗ' c d)
                                              (F.map
                                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                                  f d)))
                                        CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left._autoParam} →
                                    {μₗ_naturality_right' :
                                        autoParam
                                          (∀ (c : C) {d d' : D} (f : d ⟶ d'),
                                            CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
                                                  c (F.map f))
                                                (μₗ' c d') =
                                              CategoryTheory.CategoryStruct.comp (μₗ' c d)
                                                (F.map
                                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
                                                    c f)))
                                          CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right._autoParam} →
                                      {μₗ_associativity' :
                                          autoParam
                                            (∀ (c c' : C) (d : D),
                                              CategoryTheory.CategoryStruct.comp
                                                  (μₗ' (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
                                                  (F.map
                                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso
                                                        c c' d).hom) =
                                                CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso
                                                      c c' (F.obj d)).hom
                                                  (CategoryTheory.CategoryStruct.comp
                                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
                                                      c (μₗ' c' d))
                                                    (μₗ' c
                                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
                                                        c' d))))
                                            CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity._autoParam} →
                                        {μₗ_unitality' :
                                            autoParam
                                              (∀ (d : D),
                                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
                                                      (F.obj d)).hom =
                                                  CategoryTheory.CategoryStruct.comp
                                                    (μₗ' (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d)
                                                    (F.map
                                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
                                                          d).hom))
                                              CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality._autoParam} →
                                          { μₗ := μₗ, μₗ_naturality_left := μₗ_naturality_left,
                                                μₗ_naturality_right := μₗ_naturality_right,
                                                μₗ_associativity := μₗ_associativity, μₗ_unitality := μₗ_unitality } =
                                              { μₗ := μₗ', μₗ_naturality_left := μₗ_naturality_left',
                                                μₗ_naturality_right := μₗ_naturality_right',
                                                μₗ_associativity := μₗ_associativity', μₗ_unitality := μₗ_unitality' } →
                                            (μₗ ≍ μₗ' → P) → P