This file defines Locale, the category of locales. This is the opposite of the category of frames.
The category of locales.
Construct a bundled Locale from a Frame.
The forgetful functor from Top to Locale which forgets that the space has "enough points".