# Hausdorff completion of uniform spaces

I'm working on constructing a completion of uniform spaces. As far as possible I'd like to follow the construction in the case of metric spaces that uses equivalence classes of Cauchy sequences because that seems most natural to me... despite Bourbaki and other authors not bothering with equivalence classes. Here's what I've tried:

Let $$X$$ be a uniform space and let $$\hat{X}$$ be the collection of all Cauchy proper filters on $$X$$.

• Let $$\mathcal{F}, \mathcal{G}$$ be Cauchy proper filters on $$X$$. For each entourage $$U$$ of $$X$$, we say that $$\mathcal{F}$$ and $$\mathcal{G}$$ are $$U$$-close if they have a $$U$$-small set in common.
• Cauchy proper filters $$\mathcal{F}, \mathcal{G}$$ on $$X$$ are equivalent if $$\mathcal{F}$$ and $$\mathcal{G}$$ are $$U$$-close for every entourage $$U$$ of $$X$$. This is an equivalence relation, so we can replace $$\hat{X}$$ by the quotient space.

Next we need to make $$\hat{X}$$ a uniform space by giving it a uniformity.

• For any $$[\mathcal{F}], [\mathcal{G}] \in \hat{X}$$, we say that $$[\mathcal{F}]$$ and $$[\mathcal{G}]$$ are $$U$$-close if $$\mathcal{F}$$ and $$\mathcal{G}$$ have a $$U$$-small set in common.
• Let $$U^*$$ be the collection of all pairs of equivalence classes that are $$U$$-close; then $$\{\,U^* \mid \text{U is an entourage of X}\,\}$$ forms a uniformity base on $$\hat{X}$$.

Since this is about equivalence classes, I should need to check well-definedness right? Is this what I need to check?

Q: Suppose $$\mathcal{F}_1, \mathcal{F}_2$$ are representatives of $$[\mathcal{F}]$$ and $$\mathcal{G}_1, \mathcal{G}_2$$ are representatives of $$[\mathcal{G}]$$. Fix an entourage $$U$$ of $$X$$; then $$\mathcal{F}_1$$ and $$\mathcal{G}_1$$ are $$U$$-close if and only if $$\mathcal{F}_2$$ and $$\mathcal{G}_2$$ are $$U$$-close.

Note: let $$U$$ be an entourage of $$X$$. We say that $$A \subseteq X$$ is $$U$$-small if $$A \times A$$ is a subset of $$U$$.