Category of metric spaces and non-expansive maps ($\mathbf{Met}$)

The category $\mathbf{Met}$ has metric spaces as objects and maps $f$ satisfying $d(fx,fy)\le d(x,y)$ as morphisms. Its binary product uses the maximum metric.

A non-expansive map between metric spaces is a function $f$ such that $d(fx,fy)\le d(x,y)$.

The category ${\mathbf{Met}}_b$ is the full subcategory on bounded metric spaces. It has finite products: the terminal space is a singleton and

For bounded metric spaces $X,Y$, let $[X,Y]$ be the set of non-expansive maps and defineWhenever $\bar{d}$ satisfies the triangle inequality, it is a metric and makes $[X,-]$ right adjoint to $-\times X$ in ${\mathbf{Met}}_b$.

A metric space $X$ is interpolating when $d(x,y)=r+s$ implies that some $z$ satisfies $d(x,z)=r$ and $d(z,y)=s$. Interpolation makes the metric exponential candidate satisfy the triangle inequality, so every bounded interpolating metric space is an exponentiable object of ${\mathbf{Met}}_b$.

The quotient metric is the largest metric on a quotient set for which the quotient map is non-expansive. It is obtained by taking infima of lengths of chains that may jump freely within equivalence classes.