{P : Sort u} →
  {C : Type u_1} →
    {D : Type u_2} →
      {inst : CategoryTheory.Category.{v_1, u_1} C} →
        {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
          {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
            {t : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D} →
              {C' : Type u_1} →
                {D' : Type u_2} →
                  {inst' : CategoryTheory.Category.{v_1, u_1} C'} →
                    {inst'_1 : CategoryTheory.Category.{v_2, u_2} D'} →
                      {inst'_2 : CategoryTheory.MonoidalCategoryStruct C'} →
                        {t' : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C' D'} →
                          C = C' →
                            D = D' →
                              inst ≍ inst' →
                                inst_1 ≍ inst'_1 →
                                  inst_2 ≍ inst'_2 →
                                    t ≍ t' →
                                      CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.noConfusionType P t t'