{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {motive : AlgebraicGeometry.PresheafedSpace C → Sort u_2} →
      ((carrier : TopCat) →
          (presheaf : TopCat.Presheaf C carrier) → motive { carrier := carrier, presheaf := presheaf }) →
        (t : AlgebraicGeometry.PresheafedSpace C) → motive t