Varieties of quantitative algebras as categories

Varieties of quantitative algebras of Mardare, Panangaden and Plotkin are characterized as certain categories enriched over metric spaces. We introduce the concept of a procongruence (a metric-enriched analogue of a congruence) and the corresponding proexact categories. Varieties of quantitative algebras are precisely the metric-enriched proexact categories with a provarietal generator. This means an abstractly finite, strong generator whose hom-functor preserves proregular epimorphisms.