{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} →
                  [SizeOf V] → [SizeOf C] → [SizeOf D] → CategoryTheory.GradedNatTrans A F G → ℕ