{P : Sort u} →
  {V : Type v} →
    {inst : CategoryTheory.Category.{w, v} V} →
      {inst_1 : CategoryTheory.MonoidalCategory V} →
        {C : Type u₁} →
          {inst_2 : CategoryTheory.EnrichedCategory V C} →
            {D : Type u₂} →
              {inst_3 : CategoryTheory.EnrichedCategory V D} →
                {A : CategoryTheory.Center V} →
                  {F G : CategoryTheory.EnrichedFunctor V C D} →
                    {t : CategoryTheory.GradedNatTrans A F G} →
                      {V' : Type v} →
                        {inst' : CategoryTheory.Category.{w, v} V'} →
                          {inst'_1 : CategoryTheory.MonoidalCategory V'} →
                            {C' : Type u₁} →
                              {inst'_2 : CategoryTheory.EnrichedCategory V' C'} →
                                {D' : Type u₂} →
                                  {inst'_3 : CategoryTheory.EnrichedCategory V' D'} →
                                    {A' : CategoryTheory.Center V'} →
                                      {F' G' : CategoryTheory.EnrichedFunctor V' C' D'} →
                                        {t' : CategoryTheory.GradedNatTrans A' F' G'} →
                                          V = V' →
                                            inst ≍ inst' →
                                              inst_1 ≍ inst'_1 →
                                                C = C' →
                                                  inst_2 ≍ inst'_2 →
                                                    D = D' →
                                                      inst_3 ≍ inst'_3 →
                                                        A ≍ A' →
                                                          F ≍ F' →
                                                            G ≍ G' →
                                                              t ≍ t' →
                                                                CategoryTheory.GradedNatTrans.noConfusionType P t t'