∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [inst_1 : SizeOf C] (J : C)
  (injective : autoParam (CategoryTheory.Injective J) CategoryTheory.InjectivePresentation.injective._autoParam)
  (f : X ⟶ J) (mono : autoParam (CategoryTheory.Mono f) CategoryTheory.InjectivePresentation.mono._autoParam),
  sizeOf { J := J, injective := injective, f := f, mono := mono } =
    1 + sizeOf J + sizeOf injective + sizeOf f + sizeOf mono