∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T}
  [CategoryTheory.Limits.HasLimitsOfShape J A] [CategoryTheory.Limits.PreservesLimitsOfShape J G],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.StructuredArrow X G)