A predicative completion of a uniform space (Q424538)

In this contribution to the constructive theory of uniform spaces, having pointed out their perceived problems with the Bridges-Vîţă notion of \textit{uniform space}, the authors introduce a new, predicative notion, built on a base of entourages. They then show how, in the subsystem CZF\(^{-}\) of the constructive set theory CZF, one can construct a completion of their kind of uniform space.