Sequences suffice for pointfree uniform completions

TL;DR

This paper shows that in pointfree topology, uniform locale completions can be achieved using Cauchy sequences, simplifying the process compared to traditional methods involving filters or nets in general uniform spaces.

Contribution

It demonstrates that the uniform completion of locales can be obtained as a quotient of a locale of Cauchy sequences, streamlining the completion process in pointfree topology.

Findings

Uniform locale completions are obtainable via Cauchy sequences.

The approach simplifies the completion process compared to classical methods.

The method provides a quotient construction for uniform locales.

Abstract

Completions of metric spaces are usually constructed using Cauchy sequences. However, this does not work for general uniform spaces, where Cauchy filters or nets must be used instead. The situation in pointfree topology is more straightforward: the correct completion of uniform locales can indeed be obtained as a quotient of a locale of Cauchy sequences.