{P : Sort u} →
  {C : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.MonoidalCategory C} →
        {t : CategoryTheory.Mon C} →
          {C' : Type u₁} →
            {inst' : CategoryTheory.Category.{v₁, u₁} C'} →
              {inst'_1 : CategoryTheory.MonoidalCategory C'} →
                {t' : CategoryTheory.Mon C'} →
                  C = C' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → CategoryTheory.Mon.noConfusionType P t t'