Sections of sheaf over empty set

Stream: Is there code for X?

[Christian Merten]

This must be somewhere

example {X : TopCat} (F : X.Sheaf CommRingCat) :
    Subsingleton (F.presheaf.obj (op ⊥)) :=
  sorry

but I can't find it.

[Christian Merten]

I found it. Its:

example {X : TopCat} (F : X.Sheaf CommRingCat) : Subsingleton (F.presheaf.obj (op ⊥)) :=
  CommRingCat.subsingleton_of_isTerminal F.isTerminalOfEmpty