{C : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} C} →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        {inst_1 : CategoryTheory.Category.{v', u'} J} →
          {X : C} → [SizeOf C] → [(a : C) → SizeOf (P a)] → [SizeOf J] → P.ColimitOfShape J X → ℕ