Presheaves on PUnit

Presheaves on PUnit satisfy sheaf condition iff its value at empty set is a terminal object.

theorem TopCat.Presheaf.isSheaf_of_isTerminal_of_indiscrete {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (hind : X.str = ⊤) (F : Presheaf C X) (it : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥))) : F.IsSheaf

theorem TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (hind : X.str = ⊤) (F : Presheaf C X) : F.IsSheaf ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥)))

theorem TopCat.Presheaf.isSheaf_on_punit_of_isTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] (F : Presheaf C ↧PUnit.{u_1 + 1}) (it : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥))) : F.IsSheaf

theorem TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] (F : Presheaf C ↧PUnit.{u_1 + 1}) : F.IsSheaf ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥)))