Show that a skeletal dagger **Cost**-category is an
extended metric space.

We already know that a **Cost**-category is a Lawvere
metric space. We only need to prove that the distance function
of such metric space is symmetric and that
implies
.

The first condition is proved by appealing to the dagger condition.
Since
is a **Cost**-functor,
. Dually,
. Thus, since the ordering on the extended real is a total
order, we can deduce that
. This is true for all objects
and
in
.

The second condition is proved by appealing to skeletality. Suppose . Symmetry tells us that . Then, and . Then, by the skeletality condition.