  We give geometric characterisations of patch and Lawson topologies in the
context of predicative point-free topology using the constructive notion of
located subset. We present the patch topology of a stably locally compact
formal topology by a geometric theory whose models are the points of the given
topology that are located, and the Lawson topology of a continuous lattice by a
geometric theory whose models are the located subsets of the given lattice. We
also give a predicative presentation of the frame of perfect nuclei on a stably
locally compact formal topology, and show that it is essentially the same as
our geometric presentation of the patch topology. Moreover, the construction of
Lawson topologies naturally induces a monad on the category of compact regular
formal topologies, which is shown to be isomorphic to the Vietoris monad.
