category of metric spaces with ∞ allowed

notation: $\mathbf{Met}_{\infty}$
objects: metric spaces, where the metric is allowed to assume the value $\infty$
morphisms: non-expansive maps $f$ , meaning $d(f(x),f(y)) \leq d(x,y)$ for all $x,y$
Related categories: $\mathbf{Met}_c$ , $\mathbf{Met}$
nLab Link

The fact that we allow $\infty$ means that universal constructions work much better.

Properties from the database

Deduced properties

Properties from the database

Deduced properties*

*This also uses the deduced satisfied properties.

There are 3 properties for which the database doesn't have an answer if they are satisfied or not. Please help to contribute the data!

terminal object: singleton space
initial object: empty metric space
products: direct products with the metric $d(x,y) = \sup_i d_i(x_i,y_i)$
coproducts: disjoint union with the metric that extends the given ones and gives points in different spaces the distance $\infty$