{X : TopCat} →
  {F : TopCat.Presheaf CommRingCat X} →
    {motive : F.SubmonoidPresheaf → Sort u} →
      ((obj : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ↑(F.obj U)) →
          (map :
              ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
                obj U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (obj V)) →
            motive { obj := obj, map := map }) →
        (t : F.SubmonoidPresheaf) → motive t