∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.Full] [G.Faithful] (J : Type u')
  [inst_4 : CategoryTheory.Category.{v', u'} J] [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.HasExactColimitsOfShape J C]
  [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.HasExactColimitsOfShape J D