Localic completion of quasimetric spaces

Abstract

We give a constructive localic account of the completion of quasimetric spaces. In the context of Lawvere's approach, using enriched categories, the points of the completion are flat left modules over the quasimetric space. The completion is a triquotient surjective image of a space of Cauchy sequences and can also be embedded in a continuous depo, the "ball domain". Various examples and constructions are given, including the lower, upper and Vietoris powerlocales, which are completions of finite powerspaces. The exposition uses the language of locales as "topology-free spaces".