∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F}
  [inst_2 : SizeOf J] [inst_3 : SizeOf C] (isLimit : CategoryTheory.Limits.IsLimit B.toCone)
  (isColimit : CategoryTheory.Limits.IsColimit B.toCocone),
  sizeOf { isLimit := isLimit, isColimit := isColimit } = 1 + sizeOf isLimit + sizeOf isColimit