∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} [inst_3 : SizeOf C] [inst_4 : SizeOf J]
  [inst_5 : (a : J) → SizeOf (I a)] (base : k.fst ⟶ l.fst) (hom : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base) =
        CategoryTheory.CategoryStruct.comp hom ((P l.fst).ι.app l.snd))
      CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam),
  sizeOf { base := base, hom := hom, w := w } = 1 + sizeOf base + sizeOf hom + sizeOf w