∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C}
  (α : X.Hom Y) (β : Y.Hom Z),
  AlgebraicGeometry.PresheafedSpace.comp α β =
    { base := CategoryTheory.CategoryStruct.comp α.base β.base,
      c := CategoryTheory.CategoryStruct.comp β.c ((TopCat.Presheaf.pushforward C β.base).map α.c) }