A prometric on a set is a family of functions such that
is a -filter, i.e.
For every and , we have .
For any there exists an such that for all we have
For every , there is an with for all .
If we drop the final condition, we obtain a quasi-prometric. We can also consider extended prometrics in which the can take the value .
A base for a prometric is a collection satisfying all these axioms except -closure; the -closure of a prometric base is a prometric. Any single pseudometric, and in fact any gauge, constitutes a base for a prometric.
Of course a prometric space is a space equipped with a prometric, and likewise for a quasi-prometric space.
A short map between prometric spaces and is a function such that for every , we have . We write for the category of prometric spaces and short maps.
If the prometrics of and are presented by bases, then this is equivalent to saying that for any basic on , there is a basic on such that for all . Thus, for metric spaces and gauge spaces considered as prometric spaces, this reduces to the usual notion of short map (i.e. distance-decreasing map). Hence the category of gauge spaces and short maps is included as a full subcategory of .
Since includes the categories of metric spaces and uniform spaces (disjointly), so does . Likewise, since includes the category of topological spaces (disjointly from metric and uniform spaces), so does .
The collection of such is a base for a prometric on . The short maps between such prometric spaces are precisely the uniformly continuous ones, so this defines another embedding of into . The full image of this embedding consists precisely of those prometric spaces generated by a base of -valued functions. Note that replacing by any other positive real number defines a different embedding of into .
Conversely, every prometric induces a uniformity, where the entourages are the sets
In this way every short map induces a uniformly continuous map as well. This operation is compatible with the above inclusion of , as well as with the inclusion of .
As observed by Lawvere, an (extended quasi pseudo) metric space is a category enriched over . In other words, it is a monoid (or monad) in the bicategory of matrices with values in this monoidal category. Analogously, an (extended quasi) prometric space is a monoid in the bicategory whose hom-categories are the categories of pro-objects in the hom-categories of .