{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} →
                  (app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X) →
                    (∀ (X Y : C),
                        CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y))
                              (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y))
                            (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))) →
                      CategoryTheory.GradedNatTrans A F G