We present and study the category of formal topologies and
some of its variants.
Two main results are proven.
The first is that, for any inductively generated formal cover,
there exists a formal topology whose cover extends in the
minimal way the given one.
This result is obtained by enhancing the method for the inductive
generation of the cover relation by adding a coinductive generation
of the positivity predicate.
Categorically, this result can be rephrased by saying that inductively
generated formal topologies are coreflective
into inductively generated formal covers.
The second result is that unary formal covers are exponentiable
in the category of inductively generated formal covers and hence,
thanks to the coreflection, unary formal topologies are exponentiable
in the category of inductively generated formal topologies.
From a localic point of view the exponentiability of unary formal
topologies means that algebraic dcpos are
exponentiable in the category of open locales.
But, the coreflection theorem states that open locales are
coreflective in locales and hence, as a consequence of
well-known impredicative results on exponentiable locales,
it allows to prove that locally compact open locales are
exponentiable in the category of open locales.