We construct the category of uniform spaces, show that the complete separated uniform spaces form a reflective subcategory, and hence possess all limits that uniform spaces do.
TODO: show that uniform spaces actually have all limits!
A (bundled) uniform spaces.
Construct a bundled UniformSpace from the underlying type and the typeclass.
The category instance on UniformSpace.
The forgetful functor from uniform spaces to topological spaces.
A (bundled) complete separated uniform space.
Construct a bundled UniformSpace from the underlying type and the appropriate typeclasses.
The category instance on CpltSepUniformSpace.
The functor turning uniform spaces into complete separated uniform spaces.
The inclusion of any uniform spaces into its completion.
The mate of a morphism from a UniformSpace to a CpltSepUniformSpace.
The completion functor is left adjoint to the forgetful functor.