∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {A : C} [inst_2 : SizeOf C] (toPrepathObject : HomotopicalAlgebra.PrepathObject A)
  (weakEquivalence_ι :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrepathObject.ι)
      HomotopicalAlgebra.PathObject.weakEquivalence_ι._autoParam),
  sizeOf { toPrepathObject := toPrepathObject, weakEquivalence_ι := weakEquivalence_ι } =
    1 + sizeOf toPrepathObject + sizeOf weakEquivalence_ι