∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C]
  (toPresheafedSpace : AlgebraicGeometry.PresheafedSpace C) (IsSheaf : toPresheafedSpace.presheaf.IsSheaf),
  sizeOf { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf } = 1 + sizeOf toPresheafedSpace