A predicative completion of a uniform space

We give a predicative construction of a completion of a uniform space in the constructive Zermelo–Fraenkel set theory.