The implication $\eqref{comm2} \Rightarrow \eqref{comm1}$ is similar.

[Commutative bialgebra]
A $\tupl{F, G}$-bialgebra $(A,a,b)$ is commutative if it satisfies either of the
equivalent conditions of Proposition <ref>.

In the case the functors $F$ and $G$ admit dense sets of pre-operations, commutativity for their bialgebras
can be more conveniently expressed in the following way.

Let $\mathcal{D}$ and $\mathcal{E}$ be dense sets of pre-operations for $F$ and $G$, respectively.
A $\tupl{F, G}$-bialgebra $(A,a,b)$ is commutative iff it satisfies either of the
equivalent conditions:

For all $g \in \mathcal{D}$, $a^g$ is a $G$-homomorphism;

For all $h \in \mathcal{E}$, $b^h$ is a $F$-homomorphism.

The equivalence of the statements (<ref>), (<ref>) follows as
in Proposition <ref>, by using the density of $\D$ and $\E$ in lieu of
Proposition <ref>.

Assume $(A,a,b)$ is a commutative $\tupl{F, G}$-bialgebra. Then, (<ref>)
follows trivially because, $\mathcal{D}$ is a subset of pre-operations of $F$.
For the converse implication, assume (<ref>) and let $h \in \Op[G](w)$ for some
$w \in \cat{V}$. We want to show that

\begin{equation*}
\begin{tikzcd}
F A^w \arrow[r, "\bar{a}"] \arrow[d, "F(b^h)"']
& A^w  \arrow[d, "b^h"] \\
\Sigma A \arrow[r, "a"] & A
\end{tikzcd}
\end{equation*}

commutes, where $(A,a)^{w} = (A^{w}, \bar{a})$.
By density of $\mathcal{D}$, it suffices to show that for all $v$-ary pre-operation $g \in \mathcal{D}$,
$b^h \circ \bar{a}^g = a^g \circ (b^h)^{v}$.
This follows by

\begin{equation*}
\begin{tikzcd}
(A^w)^v \arrow[rr, "\bar{a}^g"] \arrow[rd, "\chi", bend left=10] \arrow[dd, "(b^h)^v"'] & & A^w \arrow[dd, "b^h"] \\
& (A^v)^w \arrow[lu, "\chi^{-1}", bend left=10]
\arrow[ru, "(a^g)^w"', near start] \arrow[ld, "\bar{b}^h"', near start] \\
A^v \arrow[rr, "a^g"] & & A
\end{tikzcd}
\end{equation*}

which commutes by Proposition <ref>, (<ref>), definition of $a^g$, and naturality of

Let $(T,\eta,\mu)$ be a strong monad on $\cat{V}$.
Note that, as $T$ is a strong functor and the EM-algebras for $T$ are closed under powers of
$\cat{V}$-objects, all the results and definitions given in this section extends to EM-algebras for $T$.

Let $T$, $T'$ be two strong monads on $\cat{V}$.
A Eilenberg-Moore $\tupl{T, T'}$-bialgebra is a triple $(A, a, a')$ consisting of an object
$A \in \cat{V}$ with both a EM $T$-algebra structure $a \colon TA \to A$ and a
EM $T'$-algebra structure $a' \colon T'A \to A$.  We say that a EM $\tupl{T, T'}$-bialgebra $(A,a,b)$
is commutative if it is so as a $\tupl{T, T'}$-bialgebra for the functors $T,T'$.

We denote by $\biEMAlg{T}{T'}$ the category of EM $\tupl{T, T'}$-bialgebras and
by $\comAlg{T}{T'}$, the full subcategory of the commutative EM
$\tupl{T, T'}$-bialgebras.

[Tensor of monads]
If the forgetful functor $\comAlg{T}{T'} \to \cat{V}$ has left adjoint, then the
monad induced by the adjunction is the tensor of $T, T'$, denoted $T \otimes T'$.

Note that the tensor of monads does not necessarily exist
(see [10] for counterexamples).
However, when it does $T \otimes T' \iso T' \otimes T$,
as the categories of commutative biagebras
$\comAlg{T}{T'}$ and $\comAlg{T'}{T}$ are isomorphic.

§.§ Tensor of Quantitative Theories

In this section, we develop the theory for the tensor of quantitative equational theories.
The main result is that the free monad on the tensor of two
theories is the tensor of the monads on the theories. In the proof given, we use
the fact that the quantitative theories are basic, as this allows us to exploit the correspondence between the algebras of a theory $\U$ and the EM-algebras of the monad $T_{\U}$ (Theorem <ref>).

Let $\Sigma$, $\Sigma'$ be two disjoint signatures.  Following Freyd [15] (and [20]),
we define the tensor of two quantitative equational theories $\U$, $\U'$ of
respective types $\Sigma$ and $\Sigma'$, written $\U \otimes \U'$, as the
smallest quantitative theory containing $\U$, $\U'$ and the quantitative equations

\begin{equation}
\vdash f( g(x^{1}_{1}, \dots, x^{1}_{m}), \dots, g(x^{n}_{1}, \dots, x^{n}_{m}) )
=_0  g( f(x^{1}_{1}, \dots, x^{n}_{1}), \dots, f(x^{1}_{m}, \dots, x^{n}_{m}) ) \,,
\label{eq:communtativeEq}
\end{equation}

for all $f \colon n \in \Sigma$ and $g \colon m \in \Sigma'$, expressing that the operations of one theory commute with the operations of the other.

§.§.§ Density of Symbolic Pre-operations

Towards our main result, we identify a dense set of pre-operations for the free monads on
quantitative equational theories which, in turn, will give us a simpler characterization
for commutative bialgebras for these monads ( Proposition <ref>).

First notice that any signature
functor $\Sigma = \coprod_{f {:} n \in \Sigma} Id^n$ in $\Met$ is strong, as
it is the coproduct of the strong functors $Id^n \iso (-)^{\underline{n}}$,
where $\underline{n} \in \Met$ denotes the set
$\ens{1, \dots, n}$ equipped with the discrete extended metric assigning infinite
distance to distinct elements.

Moreover, the injections $\inj_f \colon (-)^{\underline{n}} \nat \Sigma$ are strong natural
transformations, hence they are $\underline{n}$-ary pre-operations of $\Sigma$ ( Definition <ref>).

$\mathcal{S}_\Sigma = \{ \inj_f  \mid f \colon n \in \Sigma \}$ is a dense set of pre-operations of $\Sigma$.

Let $(A,a), (B,b)$ be $\Sigma$-algebras in $\Met$ and $h \colon A \to B$ a non-expansive map.
We want to prove the equivalence of

$f$ is a $\Sigma$-homomorphisms from $(A,a)$ to $(B,b)$;

For every $f \colon n \in \Sigma$, $h \circ a^{\inj_f} = b^{\inj_f} \circ h^v$.

$\eqref{symb1} \Rightarrow \eqref{symb2}$ follows by definition of $a^{\inj_f}$, $b^{\inj_f}$ and naturality
of $\inj_f \colon (-)^{\underline{n}} \nat \Sigma$. The implication
$\eqref{symb2} \Rightarrow \eqref{symb1}$ follows by the universality of the coproduct, as
$\Sigma =  \coprod_{f {:} n \in \Sigma} Id^n$.

In the following, the pre-operations in $\mathcal{S}_\Sigma$ will be called symbolic, and to simplify the
notation, for any $f \colon n \in \Sigma$ and $\Sigma$-algebra $(A,a)$, we write $a^f$ instead of $a^{\inj_f}$.

Now we turn to study the pre-operations of the monad $T_{\U}$, for a quantitative equational theory $\U$
of type $\Sigma$. First notice that the monad $T_{\U}$ is strong, with strength

\begin{equation*}
\zeta_{X,Y} \colon X \mprod T_{\U}Y \to T_{\U}(X \mprod Y)
\end{equation*}

obtained by uncurrying the unique map $h_{X,Y}$ that, by Theorem <ref>,
makes the following diagram commute

\begin{equation*}
\begin{tikzcd}
Y \arrow[rd, "\beta_{X,Y}"', near start, bend right] \arrow[r, "\eta^{\U}_Y"] & [-3ex]
T_{\U}Y \arrow[d, dashed, "h_{X,Y}"']
& [5ex] \Sigma T_{\U}Y \arrow[l, "\psi^{\U}_Y"'] \arrow[d,"\Sigma h_{X,Y}"] \\
& (T_{\U}(X \mprod Y))^X & \Sigma (T_{\U}(X \mprod Y))^X
\arrow[l, "\psi^{\U}_{(T(X \mprod Y))^X}"']
\end{tikzcd}
\end{equation*}

where $\beta_{X,Y}$ is the currying of
$\eta^{\U}_{X \mprod Y} \colon X \mprod Y \to T_{\U}(X \mprod Y)$.

Since a monad is strong iff both its unit and multiplication are strong natural transformations,
both $\eta^{\U}$, $\mu^{\U}$ are strong.
Moreover, also $\psi^{\U} \colon \Sigma T_{\U} \nat T_{\U}$ is strong.

Thus any pre-operation $g \in \Op[\Sigma](v)$ can be tuned into
a pre-operation of $T_{\U}$ as the composite

\begin{equation*}
(-)^{v} \xrightarrow{\,g\,} \Sigma
\xrightarrow{\,\Sigma \eta^{\U}\,} \Sigma T_{\U}
\xrightarrow{\,\psi^{\U}\,} T_{\U} \,.
\end{equation*}

In particular, when the theory $\U$ is basic, by Theorem <ref>,
the above composition allows us to turn any dense set of pre-operations of $\Sigma$ into a dense set of
pre-operations of $T_{\U}$.

Let $\U$ be a basic quantitative theory of type $\Sigma$ and $\mathcal{D}$ a dense set of pre-operations of $\Sigma$. Then $\{ \psi^{\U} \circ \Sigma \eta^{\U} \circ g \mid g \in \mathcal{D} \}$ is a dense set of pre-operations of $T_{\U}$.

$(A,a), (B,b)$ be $T_{\U}$-algebras and $h \colon A \to B$ a non-expansive map.
We want to prove the equivalence of

$h$ is a $T_{\U}$-homomorphism from $(A,a)$ to $(B,b)$;

For every $v$-ary pre-operation $g \in \mathcal{D}$,
$h \circ a^{(\psi^{\U} \circ \Sigma \eta^{\U} \circ g)} = b^{(\psi^{\U} \circ \Sigma \eta^{\U} \circ g)} \circ h^v$.

$\eqref{symbterm1} \Rightarrow \eqref{symbterm2}$ follows by
definition of $a^{(\psi^{\U} \circ \Sigma \eta^{\U} \circ g)}$, $b^{(\psi^{\U} \circ \Sigma \eta^{\U} \circ g)}$
and naturality of $\psi^{\U} \circ \Sigma \eta^{\U} \circ g$.
For the converse implication, recall that the isomorphism of categories from Theorem <ref>,
maps a $T_{\U}$-algebra $(A,a)$ to
the $\Sigma$-algebra $(A, a \circ \psi^{\U}_A \circ \Sigma\eta^{\U}_A)$ and morphisms essentially to themselves.
Thus $\eqref{symbterm2} \Rightarrow \eqref{symbterm1}$ follows by density of $\mathcal{D}$
and definition of $a^{(\psi^{\U} \circ \Sigma \eta^{\U} \circ g)}$, $b^{(\psi^{\U} \circ \Sigma \eta^{\U} \circ g)}$.

When $\U$ is a basic theory, by combining Propositions <ref> and <ref>, we easily obtain a dense set of pre-operations also for
the monad $T_{\U}$.

$\mathcal{S}_{T_{\U}} = \{ \psi^{\U} \circ \Sigma \eta^{\U} \circ \inj_f \mid f \colon n \in \Sigma \}$ is a dense set of pre-operations of $T_{\U}$, whenever $\U$ is a basic quantitative equational theory.

Also the pre-operations in $\mathcal{S}_{T_{\U}}$ will be called symbolic and we simplify the notation
by writing $a^{\tupl{f}}$ instead of $a^{(\psi^{\U} \circ \Sigma \eta^{\U} \circ \inj_f)}$, for $f \colon n \in \Sigma$ and $(A,a) \in \Alg{T_{\U}}$.

As an immediate consequence of Corollary <ref> and Proposition <ref>, we obtain the following simpler characterization for commutative $\tupl{T_{\U}, T_{\U'}}$-bialgebras.

Let $\U$, $\U'$ be basic quantitative theories respectively of type $\Sigma$, $\Sigma'$.
A $\tupl{T_{\U}, T_{\U'}}$-bialgebra $(A,a,b)$ is commutative iff
it satisfies either of the equivalent conditions

For all $f \colon n \in \Sigma$, $a^{\tupl{f}}$ is a $T_{\U'}$-homomorphism;

For all $g \colon n \in \Sigma'$, $b^{\tupl{g}}$ is a $T_{\U}$-homomorphism.

§.§.§ Tensor of Free Monads on Quantitative Theories

Let $\U, \U'$ be basic quantitative theories respectively of type $\Sigma, \Sigma'$.
We show that any model for $\U \otimes \U'$ is a $\tupl{\U \otimes \U'}$-bialgebra:
an extended metric space $A$ with both a $\Sigma$-algebra structure
$a \colon \Sigma A \to A$ satisfying $\U$ and a $\Sigma'$-algebra structure
$b \colon \Sigma' A \to A$ satisfying $\U'$ and respecting the diagrammatic condition below,
for all $f \colon n \in \Sigma$ and $g \colon m \in \Sigma'$

\begin{equation}
\begin{tikzcd}
A^{\underline{n}} \arrow[r, "a^f"] & A & A^{\underline{m}} \arrow[l, "b^g"'] \\
(A^{\underline{m}})^{\underline{n}} \arrow[rr, "\chi", "\iso"'] \arrow[u, "(b^g)^{\underline{n}}"]
& & (A^{\underline{n}})^{\underline{m}} \arrow[u, "(a^f)^{\underline{m}}"']
\end{tikzcd}
\label{eq:commDiagram}
\end{equation}

Formally, we denote by $\KK{(\Sigma, \U) \otimes (\Sigma', \U')}$ the
category of $\tupl{\U \otimes \U'}$-bialgebras, with morphisms the non-expansive
homomorphisms preserving both algebraic structures.  Then, the following isomorphism
of categories holds.

$\KK{\Sigma + \Sigma', \U \otimes \U'} \iso \KK{(\Sigma, \U) \otimes (\Sigma', \U')}$, for $\U, \U'$ basic theories.

The isomorphism is given by the pair of functors

\begin{equation*}
\begin{tikzcd}
\KK{\Sigma + \Sigma', \U \otimes \U'} \arrow[rr, bend left=5, "H"]
&  &
\KK{(\Sigma, \U) \otimes (\Sigma', \U')} \arrow[ll, bend left=5, "K"]
\end{tikzcd}
\end{equation*}

defined, for a $(\Sigma + \Sigma')$-algebra $(A,
a)$ satisfying $\U \otimes \U'$ and a
$\tupl{\U \otimes \U'}$-bialgebra $(B, b, b')$, respectively as

\begin{align*}
H(A, a) = (A, a \circ \inj_l, a \circ \inj_r) \,,
K(B, b, b') = (B, [b, b']) \,,
\end{align*}

where $[b, b'] \colon \Sigma B + \Sigma' B \to B$ is the unique map induced by $b$
and $b'$ by universality of the coproduct.
Both functors are identity on morphisms; it is easy to see that
a homomorphism in one sense is also a homomorphism in the other.

The pair of functors above is the restriction of the isomorphic pair of
functors used in the proof of <cit.>.
Thus, to show $H$ and $K$ are well defined we are just left to deal with checking
that the restriction conditions on the subcategories are preserved both ways.

As for $H$, we prove that whenever $\A = (A, a)$ satisfies the quantitative
equation in (<ref>), then $(A, a \circ \inj_l, a \circ \inj_r)$ satisfies
the commutativity of the diagram in (<ref>).
This follows as, for all $f \colon n \in \Sigma$ and $g \colon m \in \Sigma'$, by definition of algebraic
interpretation $(-)^\A$, we have

\begin{gather*}
f^\A = a \circ \inj_l \circ \inj_f = (a \circ \inj_l)^f \,, \\
g^\A = a \circ \inj_r \circ \inj_g = (a \circ \inj_r)^g \,.
\end{gather*}

Thus, the satisfiability (<ref>)

coincides with the commutativity of the diagram in (<ref>).

For $K$ we need to show that whenever
$(B, b, b')$ satisfies the commutativity of the diagram in (<ref>),
then $\A = (A, [b,b'])$ satisfies (<ref>). This follows as,
for all $f \colon n \in \Sigma$ and $g \colon m \in \Sigma'$, by definition of algebraic
interpretation $(-)^\A$, we have

\begin{gather*}
f^\A = [b,b'] \circ \inj_l \circ \inj_f = (b)^f \,, \\
g^\A = [b,b'] \circ \inj_r \circ \inj_g = (b')^g \,.
\end{gather*}

Thus, the commutativity of the diagram in (<ref>)
coincides with the satisfiability of (<ref>).

Moreover, by adapting the isomorphism of Theorem <ref> and
exploiting the density of symbolic pre-operations ( Corollary <ref>) the following is also true.

$ \KK{(\Sigma, \U) \otimes (\Sigma', \U')} \iso \comAlg{T_{\U}}{T_{\U'}}$, for $\U, \U'$ basic theories.

Recall the isomorphism of categories from Theorem <ref>

\begin{equation*}
\begin{tikzcd}
\Alg{T_{\U}} \arrow[rr, bend left=10, "H"]
&  &
\KK[\Sigma]{\U} \arrow[ll, bend left=10, "K"]
\end{tikzcd}
\end{equation*}

mapping morphisms to themselves and on objects acting as
follows: for $(A,a) \in \Alg{T_{\U}}$ and $(B, b) \in
\KK[\Sigma]{\U}$,

\begin{align*}
H(A, a) = (A, a \circ \psi^{\U}_A \circ \Sigma\eta^{\U}_A) \,,
K(B, b) = (B, b_\flat) \,,
\end{align*}

where $\beta_\flat \colon T_{\U}B \to B$ is the unique map that, by
Theorem <ref>,
satisfies the equations $b_\flat \circ \eta^{\U}_B = id_B$ and
$b_\flat \circ \psi^{\U}_B = b \circ \Sigma b_\flat$.
(for the details on the proof  <cit.>).

Next we show that the obvious point-wise extension of the above functors
on the categories of bialgebras $\KK{(\Sigma, \U) \otimes (\Sigma', \U')}$ and $\comAlg{T_{\U}}{T_{\U'}}$
is an isomorphism of categories.

Clearly, since $H$ and $K$ are inverse with each other, so are their point-wise
extensions. The only thing we are left to prove is that they are well defined; in
particular that the respective commutative conditions are preserved.

Let $(A,a,b) \in \comAlg{T_{\U}}{T_{\U'}}$. We need to show that
condition (<ref>) is satisfied by
$(A, a \circ \psi^{\U}_A \circ \Sigma\eta^{\U}_A, b \circ \psi^{\U}_A \circ \Sigma\eta^{\U}_A)$.
Let $(A,b)^{\underline{n}} = (A^{\underline{n}}, \bar{b})$.
By Corollary <ref> and Propositions <ref>,  <ref>, we have
that the bottom square diagram below commutes for all $f \colon n \in \Sigma$ and all $g \colon m \in \Sigma'$,
while the top commute by Proposition <ref>:

\begin{equation*}
\begin{tikzcd}
(A^{\underline{m}})^{\underline{n}} \arrow[d, "\chi"'] \arrow[dr, "(b^{\tupl{g}})^{\underline{n}}", bend left]\\
(A^{\underline{n}})^{\underline{m}} \arrow[r, "\bar{b}^{\tupl{g}}"] \arrow[d, "(a^{\tupl{f}})^{\underline{m}}"']
& A^{\underline{n}}  \arrow[d, "a^{\tupl{f}}"] \\
A^{\underline{m}} \arrow[r, "b^{\tupl{g}}"] & A
\end{tikzcd}
\end{equation*}

Since $a^{\tupl{f}} = (a \circ \psi^{\U}_A \circ \Sigma\eta^{\U}_A)^f$ and
$b^{\tupl{g}} = (b \circ \psi^{\U}_A \circ \Sigma\eta^{\U}_A)^g$, the above diagram proves
that condition (<ref>) holds.

Let $(A,a,b) \in \KK{(\Sigma, \U) \otimes (\Sigma', \U')}$. We need to show that $(A,a_\flat,b_\flat)$
is a $\tupl{T_{\U}, T_{\U'}}$-bialgebra.
By Corollary <ref>, it is sufficient
to prove that the following diagram commutes for all $g \colon m \in \Sigma'$,

\begin{equation}
\begin{tikzcd}
T_{\U} A^{\underline{m}} \arrow[r, "\overline{a_\flat}"] \arrow[d, "T_{\U}(b_\flat^{\tupl{g}})"']
& A^{\underline{m}}  \arrow[d, "b_\flat^{\tupl{g}}"] \\
T_{\U} A \arrow[r, "a_\flat"] & A
\end{tikzcd}
\label{eq:goal}
\end{equation}

where $(A,a_\flat)^{\underline{m}} = (A^{\underline{m}}, \overline{a_\flat})$.

Toward proving (<ref>), first notice that the diagram below commutes
for all $f \colon n \in \Sigma$ and $g \colon m \in \Sigma'$

\begin{equation}
\begin{tikzcd}
(A^{\underline{n}})^{\underline{m}} \arrow[rr, "\bar{a}^f"]
\arrow[rd, "\chi^{-1}", bend left=10] \arrow[dd, "(b^g)^{\underline{n}}"']
& & A^{\underline{m}} \arrow[dd, "b^g"] \\
& (A^{\underline{m}})^{\underline{n}} \arrow[lu, "\chi", bend left=10]
\arrow[ru, "(a^f)^{\underline{m}}"', near start] \\
A^{\underline{n}} \arrow[rr, "a^f"] \arrow[ur, phantom, "\eqref{eq:commDiagram}" gray] & & A
\end{tikzcd}
\label{eq:bg-homo}
\end{equation}

for $(A,a)^{\underline{m}} = (A^{\underline{m}}, \bar{a})$ and $(A,b)^{\underline{n}} = (A^{\underline{n}}, \bar{b})$. Indeed, the bottom commutes because $(A,a,b)$ satisfies (<ref>), and the
top triangle does by Proposition <ref>.

Going back to proving (<ref>), by Theorem <ref>, it suffices to show
that both $b_\flat^{\tupl{g}} \circ \overline{a_\flat}$ and $a_\flat \circ T_{\U}(b_\flat^{\tupl{g}})$ are the (unique)
homomorphic extension of $a$ along $b_\flat^g$.
This is shown by the following diagrams

\begin{equation*}
\begin{tikzcd}
A^{\underline{m}} \arrow[r, "\eta^{{\U}}"] \arrow[d, "b_\flat^{\tupl{g}}"']
& T_{\U} A^{\underline{m}}  \arrow[d, "T_{\U} b_\flat^{\tupl{g}}"] \\
A \arrow[r, "\eta^{\U}"] \arrow[dr, "id"'] & T_{\U} A \arrow[d, "a_\flat"] \\
& A
\end{tikzcd}
\quad
\begin{tikzcd}
A^{\underline{m}} \arrow[r, "\eta^{{\U}}"] \arrow[dr, "id"'] \arrow[ddr, "b_\flat^{\tupl{g}}"', bend right]
& T_{\U} A^{\underline{m}}  \arrow[d, "\overline{a_\flat}"] \\
& A^{\underline{m}} \arrow[d, "b_\flat^{\tupl{g}}"] \\
& A
\end{tikzcd}
\end{equation*}

\begin{equation*}
\begin{tikzcd}
T_{\U}A^{\underline{m}} \arrow[d, "T_{\U}b_\flat^{\tupl{g}}"']
& \Sigma T_{\U} A^{\underline{m}}  \arrow[l, "\psi^{\U}"'] \arrow[d, "\Sigma T_{\U}b_\flat^{\tupl{g}}"] \\
T_{\U}A \arrow[d, "a_\flat"'] & \Sigma T_{\U}A \arrow[l, "\psi^{\U}"'] \arrow[d, "\Sigma a_\flat"] \\
A & \Sigma A \arrow[l, "a"']
\end{tikzcd}
\end{equation*}

\begin{equation*}
\begin{tikzcd}
& T_{\U}A^{\underline{m}} \arrow[d, "\overline{a_\flat}"']
& \Sigma T_{\U} A^{\underline{m}}  \arrow[l, "\psi^{\U}"'] \arrow[d, "\Sigma \overline{a_\flat}"] \\
\Sigma'T_{\U'}A \arrow[d, "id"]
& A^{\underline{m}} \arrow[d, "\inj_g"]
& \Sigma A^{\underline{m}} \arrow[d, "\Sigma \inj_g"'] \arrow[l, "\overline{a}"'] &
\Sigma\Sigma'T_{\U'}A \arrow[d, "id"] \\
\Sigma'T_{\U'}A \arrow[d, "\psi^{\U'}"]
& \Sigma' A \arrow[d, "b"] \arrow[l, "\Sigma' b_\flat"] \arrow[ul, "\Sigma' \eta^{\U'}"', near end] &
\Sigma \Sigma' A \arrow[d, "\Sigma b"] \arrow[r, "\Sigma \Sigma' b_\flat"'] \arrow[ur, "\Sigma \Sigma' \eta^{\U'}", near end] &
\Sigma \Sigma'T_{\U'}A \arrow[d, "\psi^{\U'}"] \\
T_{\U'}A \arrow[r, "b_\flat"] & A & \Sigma A \arrow[l, "a"'] & \Sigma T_{\U'} \arrow[l, "\Sigma b_\flat"']
\end{tikzcd}
\end{equation*}

that commute by definitions of $a_\flat$, $b_\flat$, $b_\flat^{\tupl{g}}$, $b^g$; by naturality of
$\eta^{\U}$, $\psi^{\U}$; since $(A,a_\flat)^{\underline{m}}$ is a EM $T_{\U}$-algebra; because
by Theorem <ref> $(A,a_\flat)^{\underline{m}} = (A,a)^{\underline{m}}$; and
since from Propositions <ref>, <ref> and (<ref>) we have that $b^g$ is a $\Sigma$-homomorphism.

By combining the above two propositions we get the main theorem of this section.

Let $\U, \U'$ be basic quantitative theories.  Then, the monad $T_{\U \otimes \U'}$ in $\Met$
is the tensor of monads $T_{\U} \otimes T_{\U'}$.

By Propositions <ref> and <ref> the
forgetful functor from $\comAlg{T_{\U}}{T_{\U'}}$ to $\Met$ has a
left adjoint and the monad generated by this adjunction is isomorphic to
$T_{\U \otimes \U'}$.  Thus, by definition of tensor of monads,
$T_{\U \otimes \U'} \iso T_{\U} \otimes T_{\U'}$.

The above results do not require any specific property of
$\Met$, apart that its morphisms are non-expansive maps.
Thus, when the quantitative equational theories are continuous,
we can reformulate an alternative version of Theorem <ref>
which is valid in $\CMet$.

Let $\U, \U'$ be continuous quantitative theories.
Then, $\CC T_{\U \otimes \U'}$ in $\CMet$ is the tensor of monads $\CC T_{\U} \otimes \CC T_{\U'}$.

The tensor $\U \otimes \U'$ of continuous theories is also continuous, so that, by
Theorem <ref>, the free monad on it in $\CMet$ is $\CC T_{\U \otimes \U'}$.
Moreover, by exploiting the universal property of Theorem <ref>, we
can refactor the proofs of Propositions <ref> and <ref>
to obtain the isomorphism $\CC\KK{\Sigma + \Sigma', \U \otimes \U'} \iso \comAlg{\CC T_{\U}}{\CC T_{\U'}}$.
Thus, by definition of tensor of monads, $\CC T_{\U \otimes \U'} \iso \CC T_{\U} \otimes \CC T_{\U'}$.

§.§ Tensor with Reader/Writer Effects

As an example of commutative combination of effects we consider the operation of tensoring a generic
quantitative theory with the quantitative reader and writer theories, respectively.  Similarly to Hyland et al. [19], we show that these operations corresponds, at the level of monads, to the so called reader and writer monad transformers of Moggi and Cenciarelli [35, 11].

§.§.§ Reader Monad Transformer

Let $T$ be a strong monad with strength $t$ and $E$ a finite set.

The strength $t$ gives rise to a distributive law of the monad $T$ over the monad $(-)^{\underline{E}}$

\begin{equation*}
\lambda_X \colon TX^{\underline{E}} \nat (TX)^{\underline{E}}
\end{equation*}

obtained by currying $T\ev_X^{\underline{E}} \circ t_{{\underline{E}},X^{\underline{E}}}$.
As distributive laws induce a notion of monad composition [7], Moggi's reader monad

\begin{equation*}
T \mapsto (T-)^{\underline{E}}
\end{equation*}

is also available in $\Met$. The following says that we can recover this monad transformer
as the operation of tensoring with the reader monad.

Let $T$ be a strong monad.  Then, $T \otimes (-)^{\underline{E}}$ exists and is given
as the monad composition $(T-)^{\underline{E}}$.

Recall that the composite $(T-)^{\underline{E}}$ is the monad that arises
from the adjunction with the forgetful functor $\distAlg{\lambda} \to \Met$,
where $\distAlg{\lambda}$ denotes the full subcategory of
EM $\tupl{T, (-)^{\underline{E}}}$-bialgebras $(A,a,b)$ satisfying the
commutativity of the diagram

\begin{equation}
\begin{tikzcd}
TA \arrow[r, "a"] & A & A^{\underline{E}} \arrow[l, "b"'] \\
T(A^{\underline{E}}) \arrow[rr, "\lambda"] \arrow[u, "Tb"]
& & (TA)^{\underline{E}} \arrow[u, "(a)^{\underline{E}}"']
\end{tikzcd}
\label{eq:lambdaDiagram}
\end{equation}

The bialgebras satisfying (<ref>) are called, $\lambda$-bialgebras for the law $\lambda \colon T(-^{\underline{E}}) \nat (T-)^{\underline{E}}$ (see e.g., [7]).
We show that the category of $\lambda$-bialgebras is identical to
the category of commutative $\tupl{T \otimes (-)^{\underline{E}}}$-bialgebras,
that is, that the commutativity of the diagram above corresponds to either one of
the equivalent conditions from Proposition <ref>.

One direction is easy, as if we assume $(A,a,b)$ to be a commutative
$\tupl{T \otimes (-)^{\underline{E}}}$-bialgebra, then (<ref>)
is just the instantiation of (<ref>) from Proposition <ref>
for $h = id \in \Op[(-)^{\underline{E}}](\underline{E})$ as, by definition of $\underline{E}$-power algebra,
$(A, a)^{\underline{E}} = (A^{\underline{E}}, (a)^{\underline{E}} \circ \lambda_A)$.

For the converse direction, assume (<ref>) holds and let $g \in \Op[T](v)$,
for some $v \in \Met$.  Then, asking that $a^g$ is a $(-)^{\underline{E}}$-homomorphism (, condition (<ref>) from Proposition <ref>) corresponds to
the commutativity of the following diagram, as $(A, b)^v = (A^v, b^v \circ \sigma_A)$ and
$(A, a)^{\underline{E}} = (A^{\underline{E}}, (a)^{\underline{E}} \circ \lambda_A)$:

\begin{equation*}
\begin{tikzcd}
(A^v)^{\underline{E}} \arrow[r, "\sigma"] \arrow[d, "g^{\underline{E}}"']
& (A^{\underline{E}})^v \arrow[r, "b^v"] \arrow[d, "g"']
& A^v \arrow[d, "g"'] \\
(TA)^{\underline{E}} \arrow[dr, "a^{\underline{E}}"', near start, bend right]
& T(A^{\underline{E}}) \arrow[r, "Tb"] \arrow[d, "(a)^{\underline{E}} \circ \lambda"']
& TA \arrow[d, "a"] \\
& A^{\underline{E}} \arrow[r, "b"] & A
\end{tikzcd}
\end{equation*}

The bottom-left square is (<ref>), so commutes by hypothesis;
the top-right square commutes by naturality of $g$; and finally, the left square
commutes by Proposition <ref> as, by definitions of the strengths of $(-)^v$ and
$(-)^{\underline{E}}$, $\sigma \colon (A^v)^{\underline{E}} \nat (A^{\underline{E}})^v$
coincides with the canonical isomorphism (denoted as $\chi$ in Proposition <ref>).

Therefore, as the two categories of bialgebras coincide, by definition of tensor
of monads, $T \otimes (-)^{\underline{E}} = (T-)^{\underline{E}}$.

By using the above result in combination with Theorem <ref>, we obtain an
analogous transformer at the level of quantitative equational theories as follows.

Let $\U$ be a basic quantitative equational theory.
Then, $(T_{\U} -)^{\underline{E}}$ is the free monad on the theory $\U \otimes \R[]$ in $\Met$.

Moreover, as $\R[]$ is a continuous theory, by Theorems <ref>, <ref>, and <ref>, we obtain the following variant of the
quantitative reader theory transformer on continuous  theories.

Let $\U$ be a continuous quantitative theory.
Then, $(\CC T_{\U} - )^{\underline{E}}$ is the free monad on the theory $\U \otimes \R[]$ in $\CMet$.

§.§.§ Writer Monad Transformer

Let $T$ be a strong monad with strength $t$ and $(\Lambda, *, 0)$ a monoid
structure with $\Lambda \in \Met$, unit $0 \in \Lambda$, and non-expansive multiplication $* \colon \Lambda \times \Lambda \to \Lambda$.

The strength $t$ gives rise to a canonical distributive law of the monad
$(\Lambda \mprod -)$ over $T$ as

\begin{equation*}
t_{\Lambda, -} \colon (\Lambda \mprod T-) \nat T(\Lambda \mprod -) \,.
\end{equation*}

So the composite $T(\Lambda \mprod -)$ acquires a canonical monad structure via the above distributive law [7], and we
obtain the following version of Moggi's writer monad transformer in $\Met$:

\begin{equation*}
T \mapsto T(\Lambda \mprod -) \,.
\end{equation*}

Hyland et al. In [20] observed that Moggi's writer monad transformer
can be equivalently recovered as the operation of tensoring with the writer monad.

Let $T$ be a strong monad with countable rank.  Then, the monad composition $T(\Lambda \mprod -)$
is given as $T \otimes (\Lambda \mprod -)$.

As any quantitative theory $\U$ induces a
monad $T_{\U}$ with countable rank ( Ford et al. [14]), by combining the above with Theorems <ref> and <ref>,
we get an analogous transformer at the level of quantitative equational theories as follows:

Let $\U$ be a basic quantitative theory.
Then, $T_{\U}(\Lambda \mprod -)$ is the free monad on the theory $\U \otimes \Wr[]$ in $\Met$.

As $\Wr[]$ is also a continuous quantitative theory, by similar arguments as before,
we obtain the following variant of quantitative writer theory transformer on continuous theories.

Let $\U$ be a continuous quantitative theory.
Then, $\CC T_{\U}(\Lambda \mprod -)$ is the free monad on the theory $\U \otimes \Wr[]$ in $\CMet$.

§.§ The Algebras of Labeled Markov Processes

In this section we provide a quantitative equational axiomatization of labelled Markov processes with their discounted bisimilarity metric <cit.>.

§.§.§ Labelled Markov Processes over Metric Spaces

Let $A$ be a finite set of action labels.
As in <cit.>, we regard $A$-labelled Markov processes
over extended metric spaces as coalgebras on the category of metric spaces.
In detail, we consider two variants of labelled Markov processes:

\begin{align*}
X &\longrightarrow \Pi(c \cdot X + 1 )^{\underline{A}}  \quad \text{in $\Met$} \,, \\
X &\longrightarrow \Delta(c \cdot X + 1 )^{\underline{A}}  \quad \text{in $\CMet$} \,,
\end{align*}

where $\Pi$ and $\Delta$ are the functors from Section <ref>, mapping a
metric space $X$ to a space of probability measures with Kantorovich metric. We will collectively refer these coalgebras as labelled $c$-Markov processes.

Similarly to Section <ref>, the use of the rescaling functor $(c \cdot -)$ is
to encompass the case where the probabilistic bisimilarity distance is discounted
by a factor $0 < c < 1$. This will not change the essence of the results
from [46] that are used in this section to characterise
the probabilistic bisimilarity metric.

In [46], van Breugel et al. characterised the bisimilarity distance
on labelled Markov processes as the pseudometric induced by the unique homomorphism to the final coalgebra. Specifically, the $c$-discounted bisimilarity pseudometric on a labelled $c$-Markov process $(X, \tau)$ is obtained as the function $\dist \colon X \times X \to [0,1]$ given as

\begin{equation*}
\dist(x,x') = d_{Z}(h(x), h(x')) \,,
\end{equation*}

where $h \colon X \to {Z}$ is the unique homomorphism to the final labelled $c$-Markov
process $(Z,\omega)$.

This distance has a characterisation as the least fixed point of a
monotone function on a complete lattice of $1$-bounded pseudometrics.

The $c$-discounted bisimilarity pseudometric $\dist$ on $(X, \tau)$
is the unique fixed point
of the following operator on the complete lattice of extended pseudometrics $d$ on $X$
with point-wise order $\sqsubseteq$, such that $d \sqsubseteq d_X$,

\begin{equation*}
\Psi^c(d)(x,x') = \sup_{a \in A} \; \sup_{f} \left| \lebint{f}{\tau(x)(a)} - \lebint{f}{\tau(x')(a)} \right| \,,
\end{equation*}

with $f$ ranging over non-expansive positive $1$-bounded
real valued functions on $c \cdot X + 1$.

§.§.§ Quantitative Algebraic Presentation

We provide a quantitative equational theory that
axiomatizes (the monad of) $A$-labelled Markov processes with
$c$-discounted bisimilarity metric. We do this by extending the axiomatization of (unlabelled) Markov processes from Section <ref>  with a new “reading” operator used to describe
the reaction to the choice of a label from a finite set $A$ of action labels.
As expected, the reading operations will be axiomatised by the theory $\R[A]$ of reading computations ( Section <ref>).

Formally,  for $A = \ens{a_1, \dots, a_n}$ we define the quantitative theory of labelled Markov processes as the following combination of quantitative theories,

\begin{equation*}
\U_{\textbf{LMP}} = ((\B + \mathcal{E}_{1}) \otimes \R[A]) + \O{\Sigma_{\diamond}} \,.
\end{equation*}

with signature $\Sigma_{\textbf{MP}} = \Sigma_{\B} \cup \Sigma_{1} \cup \Sigma_{\R[A]}
\cup \Sigma_{\diamond}$ given
as the disjoint union of those from its component theories. Explicitly,

\begin{equation*}
\Sigma_{\textbf{LMP}}  = \set{ +_e \colon 2}{ e \in [0,1]} \cup
\{ \textsf{raise}_* \colon 0 \} \cup \{ \rd \colon |A| \} \cup \{ \diamond \colon \tupl{1, c} \}
\end{equation*}

theory $\U_{\textbf{LMP}}$ is given by the following set of axioms

\begin{align*}
& \vdash x +_1 y =_0 x \,, \\
& \vdash x +_e x =_0 x \,, \\
& \vdash x +_e y =_0 y +_{1-e} x \,, \\
& \vdash (x +_e y) +_{e'} z =_0 x +_{ee'} (y +_{\frac{e' - ee'}{1 - ee'}} z) \,, \text{ for $e,e' \in [0,1)$} \,,
\\
& \{ x \,{=_\e}\, y, x' \,{=_{\e'}}\, y' \} \,{\vdash}\, x +_e x' \,{=_{\delta}}\, y +_e y', \, \text{for $\delta \geq e \e + (1-e) \e'$,}
\\
& \vdash x =_0 \rd(x, \dots, x) \,, \\
& \vdash \rd(x_{1,1}, \dots, x_{n,n} ) =_0
\rd( \rd(x_{1,1}, \dots, x_{1,n}), \dots, \rd(x_{n,1}, \dots, x_{n,n}) )
\\
& \vdash \rd(x_1 +_e y_1, \dots, x_n +_e y_n) =_0 \rd(x_1, \dots, x_n) +_e \rd(y_1, \dots, y_n) \,,
\\
& \{x =_\e y \} \vdash \diamond(x) =_{\delta} \diamond(y) \,,
\text{ for $\delta \geq c \e$} \,.
\end{align*}

Note that, the constant $\textsf{raise}_*$ has no explicit associated axiom since $\mathcal{E}_{1}$ is the trivial theory and  () already implies the commutativity axiom required by tensoring with $\R[A]$.

Intuitively, $\Sigma_{\textbf{LMP}}$-terms (modulo $=_0$ provability) should be interpreted as equivalence classes of behaviours of labelled Markov processes up-to bisimilarity. The term $t +_e t'$ expresses convex combination of behaviours; $\textsf{raise}_*$ represents termination; $\rd(t_1, \dots, t_n)$ is used to express that $t_i$ is the selected behaviour after the choice of the action label $a_i \in A$; and $\diamond(t)$ expresses the ability of taking a transition
to the behaviour $t$.

*On Metric Spaces

We characterise the monad $T_{\U_{\textbf{LMP}}}$ on $\Met$  in steps, by explaining
the contribution of the different theories in

\begin{equation*}
\U_{\textbf{LMP}} = ((\B + \mathcal{E}_{1}) \otimes \R[A]) + \O{\Sigma_{\diamond}} \,.
\end{equation*}

(Step 1) As shown in Section <ref>, $T_{\B + \mathcal{E}_1}$
is the finitely supported sub-distribution monad

\begin{equation*}
T_{\B + \mathcal{E}_1} \iso \Pi(- + 1) \,.
\end{equation*}

Thus, $\B + \mathcal{E}_1$ axiomatizes finitely supported sub-distributions with Kantorovich metric.

(Step 2) By Theorem <ref> and Corollary <ref>,
we further get the monad isomorphism

\begin{equation*}
T_{(\B + \mathcal{E}_1) \otimes \R[A]} \iso
\Pi(1+ -) \otimes (-)^{\underline{A}} \iso
(\Pi(1+ -))^{\underline{A}} \,,
\end{equation*}

saying that tensoring with the theory $\R[A]$ of reading computations corresponds
to axiomatically adding the capability of reacting to the choice of
an action label.

(Step 3) The final step is to sum the above with the theory $\O{\Sigma_\diamond}$.
Then, by Corollary <ref>, the monad on
$\U_{\textbf{LMP}}$ is

\begin{equation*}
\iso \mu y.  T_{(\B + \mathcal{E}_1) \otimes \R[A]}(c \cdot y + - )
\iso \mu y.  \Pi(c \cdot y + 1 + -)^{\underline{A}} \,,
\end{equation*}

where we implicitly applied the isomorphisms $c \cdot (A + B) \iso c \cdot A + c \cdot B$ and $1 \iso c \cdot 1$.

Explicitly, this means that, the free monad on $\U_{\textbf{LMP}}$
assigns to an arbitrary metric space $X \in \Met$ the initial solution
of the following functorial equation in $\Met$

\begin{equation*}
\FMP[X] \iso (\Pi(c \cdot \FMP[X] + 1 + X))^{\underline{A}} \,.
\end{equation*}

In particular, when $X = 0$ is the empty metric space (, the initial object in $\Met$)
the above corresponds to the isomorphism on the initial $(\Pi(c \cdot - + 1))^{\underline{A}}\,$-algebra.

The isomorphism gives us also a $(\Pi(c \cdot - + 1))^{\underline{A}}\,$-coalgebra
structure $\tau_0 \colon \FMP[0] \to (\Pi(c \cdot \FMP[0] + 1))^{\underline{A}}$ on $\FMP[0]$.

The key observation is that the metric of $\FMP[0]$ is the bisimilarity metric.

$d_{\FMP[0]}$ is the $c$-discounted probabilistic bisimilarity metric on $(\FMP[0], \tau_0)$.

Similar to Lemma <ref>.

*On Complete Metric Spaces

Since all the quantitative theories considered are continuous, we can replicate
the same steps also while interpreting the theory $\U_{\textbf{LMP}}$ over complete metric spaces, obtaining
the monad

\begin{equation*}
\CC T_{\U_{\textbf{LMP}}} \iso \mu y. \Delta(c \cdot y + 1 + -)^{\underline{A}} \,.
\end{equation*}

By following similar arguments to Section <ref>, one can
prove that the the functorial equation $\FMP[X] \iso \Delta(c \cdot \FMP[X] + 1 + X)^{\underline{A}}$ has a unique solution.
By applying the monad above on $X = 0$ we recover the carrier of the final $(\Delta(c \cdot - + 1))^{\underline{A}}\,$-coalgebra, equipped with $c$-discounted probabilistic bisimilarity metric.

§.§ The Algebras of Mealy Machines

In a similar spirit to the axiomatization of labelled Markov processes, here we
provide a quantitative axiomatization of Mealy machines with their (coalgebraically defined) discounted bisimilarity metric.

§.§.§ Mealy machines over Metric Spaces

Informally, Mealy machines are deterministic automata with outputs.
Formally, they are tuples $(X, I, \Lambda, t, o)$ consisting of a set of states $X$, a
finite set $I = \ens{i_1, \dots, i_n}$ of inputs, a set $\Lambda$ of
outputs, a transition function $t \colon X \times I \to X$, and an output function $o \colon X \times I \to \Lambda$.

These structures are clearly $\Set$ coalgebras for the functor $(\Lambda \times -)^I$ [41, 42]. In order to give a coalgebraic definition of a
bisimilarity metric for Mealy machines, we will interpret them as coalgebras $(X,\tau)$ on categories of metric spaces. Specifically

\begin{align*}
\tau \colon X &\longrightarrow (c \cdot X \mprod \Lambda)^{\underline{I}}  \quad
\text{in $\Met$/$\CMet$} \,,
\end{align*}

where  $0 < c < 1$ and we assume $\Lambda$ to be a complete metric space
of outputs.
The rescaling functor $(c \cdot -)$ is used to obtain a discounted bisimilarity
distance. When we want to emphasize the rôle of the discount factor
we call these coalgebras $c$-Mealy machines.

Similarly to [46], we define the the $c$-discounted bisimilarity pseudometric on a $c$-Mealy machine $(X, \tau)$ as the pseudometric
induced by the unique homomorphism to the final coalgebra. That is,

\begin{equation*}
\dist(x,x') = d_{Z}(h(x), h(x')) \,,
\end{equation*}

where $h \colon X \to {Z}$ is the unique homomorphism to the
final $c$-Mealy machine $(Z,\omega)$.

A concrete characterisation of the final $c$-Mealy machine can be obtained as in [41]. We don't repeat the argument here as it is not necessary for our technical development, which requires only its existence.

This distance has a characterisation as the least fixed point of a
monotone function on a complete lattice of $[0,\infty]$-valued pseudometrics.

The $c$-discounted bisimilarity pseudometric $\dist$ on $(X, \tau)$
is the unique fixed point
of the following operator on the complete lattice of extended pseudometrics $d$ on $X$
with point-wise order $\sqsubseteq$, such that $d \sqsubseteq d_X$,

\begin{equation*}
\Psi^c(d)(x,x') = \sup_{i \in I} \left( c \cdot d(x_i, x'_i) + d_\Lambda(\lambda_i, \lambda'_i)  \right)  \,,
\end{equation*}

where $\tau(i)(x) = (x_i, \lambda_i)$ and $\tau(i)(x') = (x'_i, \lambda'_i)$.

The unicity of the fixed point follows by Banach fixed point theorem. Indeed, the set of extended real valued functions on $X \times X$
(which is a superset of the set of extended pseudometrics on $X$) can be turned into a complete Banach space
by means of the sup-norm $|| f || = \sup_{x,x'} |f(x,x')|$ and $\Psi^c$ is a $c$-contractive operator on it. Moreover, $\dist = \lim_{n\to \infty} (\Psi^c)^n(\mathbf{0})$,
where $\mathbf{0}$ is the constantly $0$ pseudometric. Since $\Psi^c$ is a monotone operator, $(\Psi^c)^n(\mathbf{0}) \sqsubseteq (\Psi^c)^{n+1}(\mathbf{0})$.
Moreover, $\Psi^c$ maps pseudometrics into pseudometrics. As pseudometrics are closed under point-wise suprema, $\dist$ is a pseudometric.

§.§.§ Quantitative Algebraic Presentation

Next we provide a quantitative equational theory that axiomatizes (the monad of)
Mealy machines with $c$-discounted bisimilarity metric.
As we did already in the previous sections we will do this by combining simpler theories via of sum and tensor. The basic theories we use are:

* The quantitative theory $\R[I]$ of reading computations
will be used to axiomatize the reaction to the choice of an input symbol $i \in I$
( Section <ref>);

* The quantitative theory $\Wr[\Lambda]$ of writing computations will be used
to describe the action of outputing a symbol $\alpha \in \Lambda$. ( Section <ref>). In our axiomatic interpretation, we assume
$\Lambda$ to have a monoid structure and outputs to be recorded in a “output tape” by means writing operations.

* The quantitative theory of contractive operators $\O{\Sigma_{\diamond}}$
with signature $\Sigma_{\diamond} = \ens{\diamond \colon \tupl{1,c} }$ will be used to axiomatise the transition to a next state with discounting factor $0 < c < 1$ ( Section <ref>).

Formally, for a finite set of inputs $I = \ens{i_1, \dots, i_n}$ and complete metric space $\Lambda$ of outputs with monoid structure $(\Lambda, 0, *)$, we define the quantitative theory of Mealy machines as the following combination of quantitative theories,

\begin{equation*}
\U_{\textbf{MM}} = (\R[I] \otimes \Wr[\Lambda]) + \O{\Sigma_{\diamond}} \,.
\end{equation*}

with signature $\Sigma_{\textbf{MM}} = \Sigma_{\R[I]} \cup \Sigma_{\Wr[\Lambda]}
\cup \Sigma_{\diamond}$ given
as the disjoint union of those from its component theories. Explicitly,

\begin{equation*}
\Sigma_{\textbf{MM}}  = \{ \rd \colon |I| \} \cup \{ \wrt{\alpha} \colon 1 \mid \alpha \in \Lambda  \} \cup \{ \diamond \colon \tupl{1, c} \}
\end{equation*}

and the theory $\U_{\textbf{MM}}$ is given by the following axioms

\begin{align*}
& \vdash x =_0 \rd(x, \dots, x) \,,
\\
& \vdash \rd(x_{1,1}, \dots, x_{n,n} ) =_0
\rd( \rd(x_{1,1}, \dots, x_{1,n}), \dots, \rd(x_{n,1}, \dots, x_{n,n}) )
\\
(\Zero) \,
& \vdash x =_0 \wrt{0}(x) \,,
\\
(\Mult) \,
& \vdash \wrt{\alpha}( \wrt{\alpha'}(x) ) =_0  \wrt{\alpha * \alpha'}(x) \,,
\\
(\Diff) \,
& \{x =_\e x'\} \vdash \wrt{\alpha}(x) =_\delta  \wrt{\alpha'}(x')\,,
\text{ for $\delta \geq d_\Lambda(\alpha, \alpha') + \e $} \,,
\\
& \vdash \rd(\wrt{\alpha}(x_1), \dots, \wrt{\alpha}(x_n)) =_0
\wrt{\alpha}( \rd(x_1, \dots, x_n) ) \,,
\\
& \{x =_\e y \} \vdash \diamond(x) =_{\delta} \diamond(y) \,,
\text{ for $\delta \geq c \e$} \,.
\end{align*}

Intuitively, $\Sigma_{\textbf{MM}}$-terms (modulo $=_0$ provability) should be interpreted as equivalence classes of behaviours of Mealy machines up-to bisimilarity. The term $\rd(t_1, \dots, t_n)$ is used to express that $t_k$ is the selected behaviour after reading input $i_k \in I$; $\wrt{\alpha}(t)$ is the term expressing behaviour of writing the output $\alpha \in \Lambda$ in the output tape; and $\diamond(t)$ expresses the ability of taking a transition to the behaviour $t$.

*On Metric Spaces

We characterise the monad $T_{\U_{\textbf{MM}}}$ on $\Met$  in steps, by explaining
the contribution of the different theories in $\U_{\textbf{MM}}$.

(Step 1) As shown in Section <ref>, $T_{\R[I]}$
is the reader monad

\begin{equation*}
T_{\R[I]} \iso (-)^{\underline{I}} \,.
\end{equation*}

Thus, $\R[I]$ axiomatizes the space of functions with domain the set $I$.

(Step 2) By Theorem <ref> and Corollary <ref> (equivalently, Corollary <ref>), we further get the monad isomorphisms

\begin{equation*}
T_{\R[I] \otimes \Wr[\Lambda]} \iso (-)^{\underline{I}} \otimes (- \mprod \Lambda) \iso
(- \mprod \Lambda)^{\underline{I}} \,,
\end{equation*}

saying that tensoring with the theory $\Wr[\Lambda]$ of writing computations corresponds to axiomatically adding the capability of writing an output symbol after
reading an input action.

(Step 3) By summing the above theories with the theory $\O{\Sigma_\diamond}$,
by Corollary <ref>, we get that the free monad on
$\U_{\textbf{MM}}$ is

\begin{equation*}
\iso \mu y.  T_{\R[I] \otimes \Wr[\Lambda]}(c \cdot y + - )
\iso \mu y.  ((c \cdot y  + -) \mprod \Lambda)^{\underline{I}} \,.
\end{equation*}

Explicitly, the free monad on $\U_{\textbf{MM}}$
assigns to an arbitrary metric space $X \in \Met$ the initial solution
of the following functorial equation in $\Met$

\begin{equation*}
\MM[X] \iso (c \cdot \MM[X] + X) \mprod \Lambda)^{\underline{I}} \,.
\end{equation*}

In particular, when $X = 0$ is the empty metric space
the above corresponds to the isomorphism of the initial $(c \cdot - \mprod \Lambda)^{\underline{I}}\,$-algebra.

From this we recover a $(c \cdot - \mprod \Lambda)^{\underline{I}}\,$-coalgebra
structure $\tau_0 \colon \MM[0] \to (c \cdot \MM[0] \mprod \Lambda)^{\underline{I}} $ on $\MM[0]$, whence a $c$-Mealy machine.

$d_{\MM[0]}$ is the $c$-discounted probabilistic bisimilarity metric on $(\MM[0], \tau_0)$.

Similar to Lemma <ref>.

*On Complete Metric Spaces

As the quantitative theories considered are continuous, we can replicate
the same steps also while interpreting the theory $\U_{\textbf{MM}}$ over complete metric spaces, obtaining
the monad

\begin{equation*}
\CC T_{\U_{\textbf{MM}}}
\iso \mu y.  ((c \cdot y  + -) \mprod \Lambda)^{\underline{I}} \,.
\end{equation*}

By following similar arguments to Section <ref>, one can
prove that the the functorial equation $\MM[X] \iso (c \cdot \MM[X] + X) \mprod \Lambda)^{\underline{I}}$ has a unique solution in $\CMet$.
Hence, by applying the monad above on $X = 0$ we recover the carrier of the final
$(c \cdot - \mprod \Lambda)^{\underline{I}}\,$-coalgebra, equipped with $c$-discounted probabilistic bisimilarity metric.

§.§ The Algebras of Markov Decision Processes with Rewards

In this section we provide a quantitative equational axiomatization of Markov decision processes with rewards and their (coalgebraically defined) discounted bisimilarity metric. The axiomatization is obtained by extending that of labelled Markov processes
from Section <ref> by adding the ability to record the rewards associated with a specific probabilistic decision.

§.§.§ Markov Decision Processes over Metric Spaces

Informally, Markov decision processes are labelled Markov processes where
each choice of action label (decision) is associated with a probabilistic reward.
Formally, as in [46], we regard them as coalgebras on the category of extended metric spaces. In detail, we consider two variants of Markov decision processes:

\begin{align*}
X &\longrightarrow \Pi(c \cdot X \mprod \reals )^{\underline{A}}  \quad \text{in $\Met$} \,, \\
X &\longrightarrow \Delta(c \cdot X \mprod \reals)^{\underline{A}}  \quad \text{in $\CMet$} \,,
\end{align*}

where $\Pi$ and $\Delta$ are the functors from Section <ref>.
For convenience, the rescaling functor $(c \cdot - )$ is used to account of a
discount factor on the bisimilarity metric and the functor $(- \mprod \reals)$
is to give a metric interpretation to the combination with the reward structure.

In [40] a Markov decision process is defined as a tuple $(S, p(\cdot | s,a), r(s, a))$ with a Markov kernel $p \colon S \times A \to \Delta(S)$ and randomised reward function $r \colon S \times A \to \Delta(\reals)$.
Our coalgebraic representation is the natural generalisation over metric spaces, where the
randomness of the Markov kernel and reward function is combined as a probability measure on $(c \cdot S \mprod \reals)$, by regarding $\reals$ and $S$ as extended metric spaces.

Similar to Section <ref>, one can show that the final coalgebra for
the functors $\Pi(c \cdot - \mprod \reals )^{\underline{A}}$ in $\Met$ and
$\Delta(c \cdot - \mprod \reals)^{\underline{A}}$ in $\CMet$ exists, thus we define
the $c$-discounted probabilistic bisimilarity distance on a Markov decision process
$(X, \tau)$ as the pseudometric

\begin{equation*}
\dist(x,x') = d_{Z}(h(x), h(x'))
\end{equation*}

induced by the unique homomorphism $h \colon X \to {Z}$ to the final coalgebra.

Also in this time, the probabilistic bisimilarity distance can be given a fixed point

The $c$-discounted bisimilarity pseudometric $\dist$ on $(X, \tau)$
is the unique fixed point
of the following operator on the complete lattice of extended pseudometrics $d$ on $X$
with point-wise order $\sqsubseteq$, such that $d \sqsubseteq d_X$,

\begin{equation*}
\Psi^c(d)(x,x') = \sup_{a \in A}
\sup_{f} \left| \lebint{f}{\tau(x)(a)} - \lebint{f}{\tau(x')(a)} \right| \,,
\end{equation*}

with $f$ ranging over non-expansive positive $1$-bounded
real valued functions on $c \cdot X \mprod \reals$.

§.§.§ Quantitative Algebraic Presentation

We provide a quantitative axiomatization
of Markov decision processes with rewards equipped with discounted bisimilarity metric.
As the construction is similar to Section <ref>, we avoid repeating the details of
each step of the monad characterization.

Let $A = \ens{a_1, \dots, a_n}$ be a finite set of actions and $(\reals, +, 0)$ be the standard monoid structure on the reals. We define the quantitative theory $\U_{\textbf{MDP}}$ of Markov decision processes with real-valued rewards as the following combination of quantitative theories,

\begin{equation*}
\U_{\textbf{MDP}} = ((\B \otimes \Wr[\reals]) \otimes \R[A]) + \O{\Sigma_{\diamond}} \,.
\end{equation*}

with signature $\Sigma_{\textbf{MDP}} = \Sigma_{\B} \cup \Sigma_{\Wr[\reals]} \cup \Sigma_{\R[A]} \cup \Sigma_{\diamond}$ given
as the disjoint union of those from its component theories.

*On Metric Spaces and Complete Metric Spaces

Similarly to what we have done in for labelled Markov processes,
we relate Markov decision processes and their $c$-discounted
probabilistic bisimilarity pseudometric with the free monads on the
theory $\U_{\textbf{MDP}}$ in $\Met$ and $\CMet$.

The only step that changes in the characterisation of the monad $T_{\U_{\textbf{MDP}}}$ in $\Met$,
regards the combination of theories $\B \otimes \Wr[\reals]$, which is dealt using Corollary <ref>. Thus, similarly to Section <ref> we get

\begin{equation*}
T_{\U_{\textbf{MDP}}} =
T_{((\B \otimes \Wr[\reals]) \otimes \R[A]) + \O{\Sigma_{\diamond}}} \iso
\mu y.  \Pi((c \cdot y + - ) \mprod \reals)^{\underline{A}} \,.
\end{equation*}

The metric on the initial solution for the functorial fixed point definition
corresponds to the $c$-discounted probabilistic bisimilarity (pseudo)metric on
its coalgebra structure.

Similar considerations apply also when interpreting the theories in the category $\CMet$
of complete metric spaces, as the argument follows without issues because $\reals$
a complete metric space.  Thus we obtain the following
characterisation for the monad:

\begin{equation*}
\CC T_{\U_{\textbf{LMP}}} \iso
\mu y.  \Delta((c \cdot y + - ) \mprod \reals)^{\underline{A}} \,.
\end{equation*}

As the fixed point solution in $\CMet$ is unique, $\CC T_{\U_{\textbf{LMP}}}0$ is an algebraic characterization of the final $\Delta((c \cdot - ) \mprod \reals)^{\underline{A}}\,$-coalgebra with probabilistic bisimilarity metric.

§ CONCLUSIONS

We studied the disjoint and commutative combinations of quantitative effects, respectively
as the sum and tensor of their quantitative equational theories.  The key results are
Theorems <ref> and <ref>, asserting that
the sum and tensor of two quantitative theories corresponds to the categorical sum and
tensor, respectively, of their free monads.  In addition to these general results, we
provide quantitative analogues Moggi's monad transformers for exceptions, resumption,
reader, and writer.

We illustrate the applicability of our theoretical development with the axiomatisations
four coalgebraic bisimilarity metrics: for Markov processes, labeled Markov processes,
Mealy machines, and Markov decision processes. Apart from the intrinsic interest in their
quantitative equational presentation as effects, what is particularly pleasant is the
systematic compositional way with which one can obtain quantitative axiomatisations of
different variants of coalgebraic structures by just combining theories as new basic

An example that escapes our compositional treatment via sum and tensor is the
combination of probabilities and non-determinism as illustrated
in [33].  A possible future work in this direction is to extend the
combination of theories with another operator: the distributive tensor (see <cit.>).
Following an intuition similar to Cheng [12], we claim that these correspond in a suitable way to Garner's weak distributive law [16].
Our claim seems promising in the light of the work [17, 9]
which consider equational axiomatisations combining probabilities and non-determinism.

§ ACKNOWLEDGMENT

The first author wish to acknowledge fruitful discussions with Dexter Kozen
and Ugo Dal Lago during a workshop at the Bellairs Research Institute in Barbados.

[1]
Jirí Adámek, Stefan Milius, Nathan Bowler, and Paul Blain Levy.
Coproducts of monads on set.
In LICS 2012, pages 45–54. IEEE Computer Society, 2012.

[2]
Jirí Adámek, Stefan Milius, and Lawrence S. Moss.
On finitary functors and their presentations.
In CMCS 2012, volume 7399 of Lecture Notes in Computer
Science, pages 51–70. Springer, 2012.

[3]
Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin.
An algebraic theory of markov processes.
In LICS, pages 679–688. ACM, 2018.

[4]
Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin.
Tensor of quantitative equational theories.
In CALCO, volume 211 of LIPIcs, pages 7:1–7:17.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.

[5]
Michael Barr.
Coequalizers and free triples.
Mathematische Zeitschrift, 116(4):307–322, 1970.

[6]
Robert G. Bartle.
The Elements of Integration and Lebesgue Measure.
John Wiley & Sons, 1995.

[7]
Jon Beck.
Distributive laws.
In Seminar on Triples and Categorical Homology Theory, volume
80 of Lect. Notes Math., pages 119–140. Springer, 1966.

[8]
Patrick Billingsley.
Convergence of Probability Measures.
Wiley Series in Probability and Statistics: Probability and
Statistics. John Wiley & Sons Inc., second edition, 1999.
A Wiley-Interscience Publication.

[9]
Filippo Bonchi and Alessio Santamaria.
Combining semilattices and semimodules.
CoRR, abs/2012.14778, 2020.

[10]
Nathan J. Bowler, Sergey Goncharov, Paul Blain Levy, and Lutz Schr   "o der.
Exploring the boundaries of monad tensorability on set.
Log. Methods Comput. Sci., 9(3), 2013.

[11]
Pietro Cenciarelli and Eugenio Moggi.
A syntactic approach to modularity in denotational semantics.
Technical report, CWI, 1993.
Proc. 5th. Biennial Meeting on Category Theory and Computer Science.

[12]
Eugenia Cheng.
Distributive laws for lawvere theories.
Compositionality, 2:1, May 2020.

[13]
Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.
Metrics for labelled Markov processes.
Theoretical Computer Science, 318(3):323–354, 2004.

[14]
Chase Ford, Stefan Milius, and Lutz Schröder.
Monads on categories of relational structures.
In CALCO, volume 211 of LIPIcs, pages 14:1–14:17.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.

[15]
Peter J. Freyd.
Algebra valued functors in general and tensor products in particular.
Colloq. Math., 14:89–106, 1966.

[16]
Richard Garner.
The vietoris monad and weak distributive laws.
Appl. Categorical Struct., 28(2):339–354, 2020.

[17]
Alexandre Goy and Daniela Petrisan.
Combining probabilistic and non-deterministic choice via weak
distributive laws.
In LICS, pages 454–464. ACM, 2020.

[18]
Jeff Henrikson.
Completeness and total boundedness of the Hausdorff metric.
MIT Undergraduate Journal of Mathematics, 1(69-80):10, 1999.

[19]
Martin Hyland, Paul Blain Levy, Gordon D. Plotkin, and John Power.
Combining algebraic effects with continuations.
Theor. Comput. Sci., 375(1-3):20–40, 2007.

[20]
Martin Hyland, Gordon D. Plotkin, and John Power.
Combining effects: Sum and tensor.
Theor. Comput. Sci., 357(1-3):70–99, 2006.

[21]
Martin Hyland and John Power.
Discrete lawvere theories and computational effects.
Theor. Comput. Sci., 366(1-2):144–162, 2006.

[22]
Martin Hyland and John Power.
The category theoretic understanding of universal algebra: Lawvere
theories and monads.
Electronic Notes in Theor. Comp. Sci., 172:437–458, 2007.

[23]
Leonid Vitalevich Kantorovich.
On the transfer of masses (in Russian).
Doklady Akademii Nauk, 5(5-6):1–4, 1942.
Translated in Management Science, 1958.

[24]
G.M. Kelly.
A unified treatment of transfinite constructions for free algebras,
free monoids, colimits, associated sheaves, and so on.
Bulletin of the Australian Mathematical Society, 22(1):1–83,

[25]
Gregory M. Kelly.
Basic concepts of enriched category theory.
Theory and Applications of Categories, 1982.
Reprinted in 2005.

[26]
Anders Kock.
Strong functors and monoidal monads.
Arch. Math. (Basel), 23:113–120, 1972.

[27]
Saunders Mac Lane.
Categories for the Working Mathematician.
Graduate Texts in Mathematics. Springer New York, 2nd edition, 1998.

[28]
William F. Lawvere.
Metric spaces, generalized logic, and closed categories.
In Seminario Mat. e. Fis. di Milano, volume 43, pages 135–166.
Springer, 1973.

[29]
Ernest Manes.
A Triple Theoretic Construction of Compact Algebras.
In Seminar on Triples and Categorical Homology Theory, volume
80 of Lect. Notes Math., pages 91–118. Springer, 1966.

[30]
Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin.
Quantitative Algebraic Reasoning.
In LICS, pages 700–709. ACM, 2016.

[31]
Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin.
On the axiomatizability of quantitative algebras.
In LICS 2017, pages 1–12. IEEE Computer Society, 2017.

[32]
Matteo Mio, Ralph Sarkis, and Valeria Vignudelli.
Combining nondeterminism, probability, and termination: Equational
and metric reasoning.
In LICS, pages 1–14. IEEE, 2021.

[33]
Matteo Mio and Valeria Vignudelli.
Monads and quantitative equational theories for nondeterminism and
In CONCUR, volume 171 of LIPIcs, pages 28:1–28:18.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.

[34]
Eugenio Moggi.
The partial lambda calculus.
PhD thesis, University of Edinburgh. College of Science and
Engineering. School of Informatics., 1988.

[35]
Eugenio Moggi.
Notions of computation and monads.
Information and computation, 93(1):55–92, 1991.

[36]
Gordon Plotkin and John Power.
Semantics for algebraic operations.
Electronic Notes in Theoretical Computer Science, 45:332–345,

[37]
Gordon Plotkin and John Power.
Notions of computation determine monads.
In Foundations of Software Science and Computation Structures,
pages 342–356. Springer, 2002.

[38]
Gordon D. Plotkin and John Power.
Semantics for algebraic operations.
In MFPS, volume 45 of Electronic Notes in Theoretical
Computer Science, pages 332–345. Elsevier, 2001.

[39]
Gordon D. Plotkin and John Power.
Algebraic operations and generic effects.
Appl. Categorical Struct., 11(1):69–94, 2003.

[40]
M. L. Puterman.
Markov Decision Processes.
Wiley, 2005.

[41]
Jan J. M. M. Rutten.
Algebraic specification and coalgebraic synthesis of mealy automata.
Electron. Notes Theor. Comput. Sci., 160:305–319, 2006.

[42]
Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M.
Generalizing determinization from automata to coalgebras.
Log. Methods Comput. Sci., 9(1), 2013.

[43]
Marshall H. Stone.
Postulates for the barycentric calculus.
Annali di Matematica Pura ed Applicata, 29(1):25–30, 1949.

[44]
Regina Tix, Klaus Keimel, and Gordon D. Plotkin.
Semantic domains for combining probability and non-determinism.
Electron. Notes Theor. Comput. Sci., 222:3–99, 2009.

[45]
Daniele Turi and Jan J. M. M. Rutten.
On the foundations of final coalgebra semantics.
Mathematical Structures in Computer Science, 8(5):481–540,

[46]
Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell.
Recursively defined metric spaces without contraction.
Theor. Comput. Sci., 380(1-2):143–163, 2007.

[47]
Cédric Villani.
Optimal transport: old and new.
Springer-Verlag, 2008.

§ LIMITS AND COLIMITS OF EXTENDED METRIC SPACES

Limits and colimits in the category $\Met$ of extended metric spaces and non-expansive maps are defined
similarly to those in $\Set$, at least for the part of their underlying set. Some care, though, should to taken
in the definition of the distance function.

From an abstract point of view, the reason is that the forgetful functor $U \colon \Met \to \Set$, sending
an extended metric space $(X,d_X)$ to its underlying set $X$, is faithful (, homsets are mapped injectively), and has as left adjoint the functor $\mathit{Disc} \colon \Set \to \Met$ that assigns to
each set $X$ the discrete extended metric space $\underline{X}$ giving distance $\infty$ to every distinct pair of
elements. Therefore $U$ preserves all limits which may exist in $\Met$ (this is why the underlying
set of product spaces is the cartesian product of their underlying sets).

Moreover, $\Met$ is a full reflective subcategory of $\PMet$, the category of extended pseudometric spaces (, a relaxation of extended metric spaces where different elements $x \neq y$ can be assigned distance $d(x,y) = 0$),
with reflection mapping a pseudometric space $(X,d_X)$ into its quotient modulo the equivalence
$x \cong y$ iff $d_X(x,y) = 0$. Since $\PMet$ is cocomplete with colimits constructed similarly to $\Set$ also $\Met$ is cocomplete and its colimits are just simple quotiented versions of those in $\Set$.

Although the abstract argument above is enough to prove completeness and cocompleteness of $\Met$, in the proof below we give a direct concrete construction of its limits and colimits.

$\Met$ is a complete and cocomplete category.

Let $D \colon \mathcal{I} \to \Met$ be a small diagram, and let $D(i) = (X_i, d_i)$, for each object $i \in \mathcal{I}$.
Let $U \colon \Met \to \Set$ be the standard forgetful functor, sending $(X,d_X)$ to $X$. Clearly,
also $UD \colon \mathcal{I} \to \Set$ is a small diagram.
We show completeness and cocompleteness separately:

Completeness Let $(f_i \colon L \to X_i)_{i \in \mathcal{I}}$ be the limit cone to $UD$. We define
$d_L \colon L \times L \to [0, \infty]$ as follows, for arbitrary $x,y \in L$

\begin{equation*}
d_L(x, y) = \sup_{i \in \mathcal{I}} d_i(f_i(x), f_i(y)) \,,
\end{equation*}

and claim that this is an extended metric
[Note that the definition of $d_L$ makes sense since the supremum exists in $[0, \infty]$;
this would not be true for standard (finite) metrics taking values in $[0, \infty)$.].

Let $x,y,z \in L$.
Identity of indiscernible follows by

\begin{align*}
d_L(x,y) = 0
&\iff \sup_{i \in \mathcal{I}} d_i(f_i(x), f_i(y)) = 0 \tag{def.\ $d_L$} \\
&\iff \forall i \in \mathcal{I}, \,  d_i(f_i(x), f_i(y)) =  0  \tag{$d_i$ positive} \\
&\iff \forall i \in \mathcal{I}, \, f_i(x) = f_i(y)  \tag{$d_i$ metric} \\
&\iff  x = y \,,  \tag{$(f_i)_{i \in \mathcal{I}}$ limit cone }
\end{align*}

symmetry by

\begin{align*}
&= \sup_{i \in \mathcal{I}} d_i(f_i(x), f_i(y)) \tag{def.\ $d_L$} \\
&= \sup_{i \in \mathcal{I}} d_i(f_i(y), f_i(x)) \tag{$d_i$ metric} \\
&= d_L(y,x) \,,  \tag{def.\ $d_L$}
\end{align*}

and triangular inequality by

\begin{align*}
d_L(x,z) +  d_L(z,y)
&= \sup_{i \in \mathcal{I}} d_i(f_i(x), f_i(z)) + \sup_{i \in \mathcal{I}} d_i(f_i(z), f_i(y)) \tag{def.\ $d_L$} \\
&\geq \sup_{i \in \mathcal{I}} \big( d_i(f_i(x), f_i(z)) + d_i(f_i(z), f_i(y)) \big) \tag{$\sup$} \\
&\geq \sup_{i \in \mathcal{I}} d_i(f_i(x), f_i(y)) \tag{$d_i$ metric} \\
&= d_L(x,y) \,.  \tag{def.\ $d_L$}
\end{align*}

With this metric all $f_i$ are non-expansive functions. Indeed we have, for all $i \in \mathcal{I}$ and $x, y \in L$

\begin{equation*}
d_i(f_i(x), f_i(y)) \leq \sup_{i \in \mathcal{I}} d_i(f_i(x), f_i(y)) = d_L(x,y) \,.
\end{equation*}

Since the forgetful functor $U \colon \Met \to \Set$ is faithful, the non-expansiveness of
the maps $f_i$ implies that $(f_i \colon (L,d_L) \to (X_i, d_i))_{i \in \mathcal{I}}$ is a cone to $D$.
Next we show that this is actually the limiting cone.

Let $(h_i \colon (H,d_H) \to (X_i,d_i))_{i \in \mathcal{I}}$ be a cone to $D$. Then $(h_i \colon H \to X_i)_{i \in \mathcal{I}}$ is
a cone to $UD$. Since $(f_i \colon L \to X_i)_{i \in \mathcal{I}}$ is the limit cone
to $UD$, there exists a unique function $g \colon H \to L$ in $\Set$ satisfying
$f_i \circ g = h_i$, for all $i \in \mathcal{I}$. We finish our proof by showing that $g$ is a non-expansive function.
By non-expansiveness of the $h_i$'s we have that, for all $i \in \mathcal{I}$ and $a,b \in H$,
$d_i(h_i(a), h_i(b)) \leq d_H(a,b)$, and thus also

\begin{align*}
d_L(g(a), g(b))
&= \sup_{i \in \mathcal{I}} d_i(f_i(g(a)), f_i(g(b))) \tag{def.\ $d_L$} \\
&= \sup_{i \in \mathcal{I}} d_i(h_i(a), h_i(b)) \tag{$f_i \circ g = h_i$} \\
&\leq d_H(a,b) \,. \tag{$h_i$ non-expansive}
\end{align*}

Thus we conclude that
$(f_i \colon (L,d_L) \to (X_i, d_i))_{i \in \mathcal{I}}$ is a limit cone to $D$.

Cocompleteness Let $(f_i \colon X_i \to L)_{i \in \mathcal{I}}$ be the colimit cocone to $UD$. We define
$d_L \colon L \times L \to [0, \infty]$, for arbitrary $x,y \in L$, as follows:

\begin{equation*}
d_L(x,y) = \sup_{d \in M_L} d(x,y) \,,
\end{equation*}

where $M_L$ is the set of all extended pseudometrics $d$ on $L$ making
all $f_i$'s non-expansive functions $f_i \colon (X_i,d_i) \to (L,d)$.
We claim that this is an extended pseudometric.
Since all $d \in M_L$ are pseudometrics, we can derive immediately that $d_L(x,x) = 0$ and
$d_L(x,y) = d_L(y,x)$, for all $x,y \in L$. Moreover, for all $x,y,z \in L$, we have

\begin{align*}
d_L(x,z) +  d_L(z,y)
&= \sup_{d \in M_L} d(x,z) + \sup_{d \in M_L} d(z,y) \tag{def.\ $d_L$} \\
&\geq \sup_{d \in M_L} d(x,z) + d(z,y) \tag{$\sup$} \\
&\geq \sup_{d \in M_L} d(x,y) \tag{$d$ metric} \\
&= d_L(x,y) \,.  \tag{def.\ $d_L$}
\end{align*}

Moreover, for all $i \in \mathcal{I}$ and $x, y \in X_i$

\begin{align*}
d_i(f_i(x), f_i(y))
&\leq \sup_{d \in M_L} d(x, y) \tag{def.\ $M_L$} \\
&=  d_L(x, y) \,. \tag{def.\ $d_L$}
\end{align*}

Thus, all the functions $f_i$ are non-expansive w.r.t. the pseudometric $d_L$.

Now we turn the extended pseudometric space $(L, d_L)$ into an extended metric space
$(C, d_C)$ by taking the quotient modulo the equivalence $x \cong y$ iff $d_L(x,y) = 0$.
The extended metric $d_C \colon C \times C \to [0, \infty]$ is given by

\begin{equation*}
d_C([x], [y]) = d_L(x,y)
\end{equation*}

for all $x,y \in L$, where $[\cdot] \colon L \to C$ denote the quotient map w.r.t. $\cong$.
Note that $d_C$ is well-defined because by triangular inequality of $d_L$ the definition
above is independent from the choice of the representative $x$ of the $\cong$-equivalence
class $[x]$ in $C$.

From the non-expansiveness of the maps $f_i$ we have that also $[\cdot] \circ f_i$ are non expansive.
Thus, since the forgetful functor $U \colon \Met \to \Set$ is faithful, $([\cdot] \circ f_i \colon (X_i, d_i) \to (C,d_C))_{i \in \mathcal{I}}$ is a cocone to $D$ in $\Met$.
Next we show that this is actually the colimiting cocone.

Let $(h_i \colon (X_i,d_i) \to (H,d_H))_{i \in \mathcal{I}}$ be a cocone to $D$. Then $(h_i \colon X_i \to H)_{i \in \mathcal{I}}$ is
a cocone to $UD$. Since $(f_i \colon X_i \to L)_{i \in \mathcal{I}}$ is the colimit cocone
to $UD$, there exists a unique function $g \colon L \to H$ in $\Set$ satisfying
$g \circ f_i = h_i$, for all $i \in \mathcal{I}$. We prove that $g$ is non-expansive w.r.t. the pseudometric $d_L$.
Let $d_g \colon L \times L \to [0,\infty]$ be defined as $d_g(x,y) = d_H(g(x), g(y))$.
It is easy to see that this is an extended pseudometric on $L$. Moreover, for all $i \in \mathcal{I}$ and $x',y' \in X_i$
we have

\begin{align*}
d_g(f_i(x'), f_i(y'))
&= d_H(g(f_i(x')), g(f_i(y'))) \tag{def.\ $d_g$} \\
&= d_H(h_i(x'), h_i(y')) \tag{$g \circ f_i = h_i$} \\
&\leq d_i(x', y') \,. \tag{$h_i$ non-expansive}
\end{align*}

Thus $d_g \in M_L$. Using this we observe that, for all $x, y \in L$

\begin{equation}
d_L(x,y) = \sup_{d \in M_L} d(x,y) \geq d_g(x,y) = d_H(g(x), g(y)) \,.
\label{eq:gnexp}
\end{equation}

Let $g'([x]) = g(x)$, for all $x \in L$. By (<ref>) and
the fact that $d_H$ is a metric, $g(x) = g(y)$ whenever $x \cong y$, hence the $g' \colon C \to H$
is a well-defined function on $C$. Moreover, by definition of $d_C$ and (<ref>), $g'$ is also
non-expansive as a map $g' \colon (C,d_C) \to (H,d_H)$ in $\Met$.

Clearly, $g' \circ [\cdot] \circ f_i = h_i$, for all $i \in \mathcal{I}$. Assume that there exists
another map $g'' \colon C \to H$ such that $g'' \circ [\cdot] \circ f_i = h_i$, for all $i \in \mathcal{I}$.
By the universal property of $g$, $g' \circ [\cdot] = g = g'' \circ [\cdot]$, thus $g'([x]) = g''([x])$, for all $x \in L$.

Thus $([\cdot] \circ f_i \colon (X_i, d_i) \to (C,d_C))_{i \in \mathcal{I}}$ is the colimit cocone to $D$.

The situation is very similar when we consider the full subcategory $\CMet$ of complete extended metric spaces.
Indeed, $\CMet$ is closed under limits, which are defined as in $\Met$. Moreover, as $\CMet$ is a reflective subcategory of $\Met$, with reflection the Cauchy completion functor, we have that also $\CMet$ is cocomplete, with colimits constructed as in $\Met$ and completed via Cauchy completion.

$\CMet$ is a complete and cocomplete category.

§ EXTENDED METRIC SPACES ARE LOCALLY COUNTABLY PRESENTABLE

Let $\lambda$ be a regular infinite cardinal (i.e., one that is not cofinal to any smaller cardinal).
A small category is called $\lambda$-filtered if any subcategory of
less than $\lambda$ morphisms has a cocone in it.
When $\lambda = \aleph_0$, the term finitely filtered (or simply, filtered) is most commonly
used, and countably filtered in the case $\lambda = \aleph_1$.

Let $\aleph_0$ denote the skeleton of the category of finite sets and all functions between them.
Then $\aleph_0$ is finitely filtered, but not countably filtered. While the skeleton category $\aleph_1$
of all countable sets is countably filtered.

A diagram is $\lambda$-filtered if its domain is $\lambda$-filtered, and
a colimit is $\lambda$-filtered when it is the colimit of a $\lambda$-filtered diagram.
A functor $F \colon \mathcal{C} \to \mathcal{D}$ is called $\lambda$-accessible if its domain
$\mathcal{C}$ has $\lambda$-filtered colimits and $F$ preserves them
[In some literature $\aleph_0$-accessible functors are said of finite rank and
and $\aleph_1$-accessible functors of countable rank. This is the terminology preferred
by John Power in his seminal work about enriched Lavwere theories.].

An object $X$ of a small category $\mathcal{C}$ is $\lambda$-presentable if its hom-functor

\begin{equation*}
\mathcal{C}(X, -) \colon \mathcal{C} \to \Set
\end{equation*}

is $\lambda$-accessible.
Explicitly, $X$ is $\lambda$-presentable iff for each $\lambda$-filtered colimit cocone
$(c_i \colon D(i) \to C)_{i \in \mathcal{I}}$ of a $\lambda$-filtered diagram $D \colon \mathcal{I} \to \mathcal{C}$, and each morphism $f \colon X \to C$, there exists $i \in \mathcal{I}$ such that

* $f$ factorizes through $c_i$, , $f = c_i \circ g$ for some $g \colon X \to D(i)$, and

* the factorization is essentially unique in the sense that if $f = c_i \circ g = c_i \circ g'$,
then $D(i \to j) \circ g = D(i \to j) \circ g'$, for some $j \in \mathcal{I}$.

[Accessibility and Local Presentability]
A category $\mathcal{C}$ is $\lambda$-accessible if

* it has all $\lambda$-filtered colimits;

* there is a set $\mathcal{C}_\lambda$ of $\lambda$-presentable objects such that every object is a
$\lambda$-filtered colimit of objects of $\mathcal{C}_\lambda$.

It is locally $\lambda$-presentable if, moreover, it has all small colimits (, it is cocomplete).

A category is said accessible (resp. locally presentable) if it is $\lambda$-accessible
(resp. $\lambda$-locally presentable) for some regular infinite cardinal $\lambda$.
In the case $\lambda = \aleph_0$, we speak about locally finitely presentable category,
and for $\lambda = \aleph_1$ about locally countably presentable category.

The category $\Set$ is locally finitely presentable with finitely presentable objects precisely the finite
sets (for $\Set_{\aleph_0}$ we can choose the set of all natural numbers).
The category $\omega\mathbf{CPO}$ of cpo's (, posets with joints of all increasing
$\omega$-chains) and $\omega$-continuous functions is not locally finitely presentable, however,
it is locally countably presentable with countably presentable objects precisely the countable cpo's
(for $\omega\mathbf{CPO}_{\aleph_1}$ we can choose the set of all countable ordinals with
standard partial order).

Next we focus our attention to the category $\Met$. In turn we prove that

* the only finitely presentable objects in $\Met$ are the finite discrete spaces,
with distances either $0$ or $\infty$ (Proposition <ref>);

* $\Met$ is locally countably presentable, with countably presentable objects precisely
the countable spaces (Lemma <ref> and Theorem <ref>)

Note that a direct consequence of (1) is that $\Met$ is not locally finitely presentable, since
filtered colimits of discrete spaces are discrete.

The proofs of these results are immediate adaptations of [2] which shows
that the category of 1-bounded pseudometric spaces with non-expansive maps is locally countably

Finitely presentable objects in $\Met$ are finite and discrete.

Note that every extended metric space is a colimit of the filtered diagram obtained by taking all its
finite subspaces and their inclusion maps.
Let $(X,d_X)$ be a finitely presentable object in $\Met$. Then the identity must
factorize through the inclusion of one of the finite subspaces. Thus, $X$ must be finite.

For each positive integer $n > 0$, define the function $d_n \colon X \times X \to [0,\infty]$ as

\begin{equation*}
d_n(x,y) = \left( 1+ \frac{1}{n} \right) \cdot d_X(x,y) \,,
\end{equation*}

where $\infty \cdot r = \infty$ for any $r \in [0, \infty)$. Clearly, all $d_n$'s are extended metrics.
Consider the $\omega$-chain of spaces $(X, d_n)$ with identities as connecting maps.
This is a countably filtered diagram with colimit cocone $(id_X \colon (X, d_n) \to (X,d_X))_{n > 0}$.
Since $(X,d_X)$ is finitely presentable, the identity $id_X \colon (X,d_X) \to (X,d_X)$
must factorize through the a colimit map $id_X \colon (X, d_n) \to (X,d_X)$ for some positive
integer $n > 0$.
But the distances in $(X,d_X)$ which are strictly between $0$ and $\infty$ are increased by $d_n$.
So $(X,d_X)$ must discrete.

Let $(f_i \colon D(i) \to (C, d_C))_{i \in \mathcal{I}}$ be the colimit cocone to a small diagram
$D \colon \mathcal{I} \to \Met$ and $D(i) = (X_i, d_i)$, for each $i \in \mathcal{I}$.
If $D$ is filtered,  $C$ is the quotient set of
$\coprod_{i \in \mathcal{I}} X_i$ under the equivalence

\begin{equation*}
in_i(x) \sim in_{i'}(x')
\quad \text{iff there exists $j \in \mathcal{I}$ with $D(i \to j)(x) = D(i' \to j)(x')$} \,,
\end{equation*}

where $in_i \colon X_i \to \coprod_{i \in I} X_i$ are the canonical injections into the coproduct
and $f_i$ assigns to each $x \in X_i$ the equivalence class of $in_i(x)$, for all $i \in \mathcal{I}$.

We prove that $\sim$ is an equivalence relation. Reflexivity and symmetry are trivially satisfied.
Transitivity follows by the fact that $\mathcal{I}$ is filtered. Indeed, let $in_i(x) \sim in_{i'}(x')$ and
$in_{i'}(x') \sim in_{i''}(x'')$. Then there exist $j, j' \in \mathcal{I}$ such that
$D(i \to j)(x) = D(i' \to j)(x')$ and $D(i' \to j')(x') = D(i'' \to j')(x'')$. Since $\mathcal{I}$ is filtered, there
exists $j'' \in \mathcal{I}$ above $i, i', i'', j$, and $j'$ such that

\begin{gather*}
D(i \to j'') = D(j \to j'') \circ D(i \to j) \,, \\
D(i' \to j'') = D(j \to j'') \circ D(i' \to j) = D(j' \to j'') \circ D(i' \to j') \,, \text{ and} \\
D(i'' \to j'') = D(j' \to j'') \circ D(i'' \to j') \,.
\end{gather*}

From this we derive $D(i \to j'')(x) = D(i'' \to j'')(x'')$, i.e., $in_{i}(x) \sim in_{i''}(x'')$.

Let $U \colon \Met \to \Set$ denote the forgetful functor into $\Set$.
By the construction of colimits in $\Met$ (see Proposition <ref>) it suffices
to prove that $(f_i \colon X_i \to (\coprod_{i \in I} X_i)/_{\sim})_{i \in \mathcal{I}}$ is a colimit cocone
to $UD$ in $\Set$.

For convenience, let $X = (\coprod_{i \in I} X_i)/_{\sim}$ and, for each $i \in \mathcal{I}$, let $[in_i(x)]$ denote the equivalence class of $in_i(x)$.
We first prove that $(f_i \colon X_i \to X)_{i \in \mathcal{I}}$ is a cocone to $UD$.
Let $i \to j \in \mathcal{I}$. Then from $D(i \to j)(x) = D(id_j)(D(i \to j)(x))$ for all $x \in X_i$,
we have $in_i(x) \sim in_j(D(i \to j)(x))$. Therefore, for all $x \in X_i$

\begin{equation*}
= [in_i(x)]
= [in_j(x)(D(i \to j)(x))]
= f_j (D(i \to j)(x)) \,.
\end{equation*}

Hence $f_i = f_j \circ D(i \to j)$ for all $i, j \in \mathcal{I}$.
Now we prove that $(f_i \colon X_i \to X)_{i \in \mathcal{I}}$ is a colimit.
Let $(h_i \colon X_i \to H)_{i \in \mathcal{I}}$ be a cocone to $UD$. Define
$g \colon X \to H$ for arbitrary $x \in X_i$ as follows:

\begin{equation*}
g([in_i(x)]) = \gamma (in_i(x)) \,,
\end{equation*}

where $\gamma \colon \coprod_{i \in I} X_i \to H$ is the unique map such
that $\gamma \circ in_i = h_i$, for all $i \in \mathcal{I}$.
Note that $g$ is well defined. Indeed, if $D(i \to j)(x) = D(i' \to j)(x')$ for some $j \in \mathcal{I}$, we have that

\begin{align*}
&= \gamma (in_i(x)) \tag{def.\ $g$} \\
&= h_i(x) \tag{$\gamma \circ in_i = h_i$} \\
&= h_j (D(i \to j)(x)) \tag{$(h_i \colon X_i \to H)_{i}$ cocone to $UD$} \\
&= h_j (D(i' \to j)(x')) \\
&= h_{i'}(x') \tag{$(h_i \colon X_i \to H)_{i}$ cocone to $UD$} \\
&= \gamma (in_{i'}(x')) \tag{$\gamma \circ in_{i'} = h_{i'}$} \\
&= g([in_{i'}(x')]) \,.  \tag{def.\ $g$}
\end{align*}

Let $i \in \mathcal{I}$. Then, for all $x \in X_i$

\begin{align*}
g \circ f_i (x)
&= g ([in_i(x)]) \tag{def.\ $f_i$} \\
&= \gamma (in_i(x)) \tag{def.\ $g$} \\
&= h_i(x) \,. \tag{$\gamma \circ in_i = h_i$}
\end{align*}

Thus $g \circ f_i  = h_i$ for all $i \in \mathcal{I}$. Assume now that there exists $g' \colon X \to H$ such that
$g' \circ f_i  = h_i$ for all $i \in \mathcal{I}$. Then, for all $x \in X_i$

\begin{align*}
&= g'(f_i (x))  \tag{def.\ $f_i$} \\
&= h_i(x) \tag{$g' \circ f_i  = h_i$} \\
&= g(f_i(x)) \tag{$g \circ f_i  = h_i$} \\
&= g([in_i(x)]) \,.   \tag{def.\ $f_i$}
\end{align*}

Thus $g' = g$.

Let $(f_i \colon D(i) \to (C, d_C))_{i \in \mathcal{I}}$ be the colimit cocone to a small diagram
$D \colon \mathcal{I} \to \Met$ and $D(i) = (X_i, d_i)$, for each $i \in \mathcal{I}$. If $D$ is filtered, then, for all $x,y \in C$

\begin{equation*}
d_C(x,y) = \inf \{ d_i(x', y') \mid i \in \mathcal{I}\,, f_i(x') = x \,, \text{and } f_i(y') = y \} \,.
\end{equation*}

Assume $D$ is filtered.
As shown in Proposition <ref>,

\begin{equation}
d_C(x,y) = \sup_{d \in M_C} d(x,y) \,,
\label{eq:colimitsupmetric}
\end{equation}

where $M_C$ is the set of all extended pseudometrics $d'$ on $C$ making
all the functions $f_i \colon (X_i, d_i) \to (C,d')$ non-expansive.
Let $d \colon C \times C \to [0,\infty]$ be

\begin{equation}
d(x,y) = \inf \{ d_i(x', y') \mid i \in \mathcal{I}\,, f_i(x') = x \,, \text{and } f_i(y') = y \} \,.
\label{eq:infdistance}
\end{equation}

Since $D$ is filtered, then also $UD$ is so, where $U \colon \Met \to \Set$ is the obvious forgetful functor
to $\Set$. Since $\Set$ is locally finitely representable, then for any finite subset $\{x_1, \dots, x_n\} \subseteq C$, there exist $i \in \mathcal{I}$ and $\{x'_1, \dots, x'_n\} \subseteq X_i$ such that $f_i(x'_j) = x_j$, for all $0 \leq j \leq n$.
In particular, this implies that for any $x,y \in C$, the infimum in (<ref>) never ranges over an empty set.

Let $x,y \in C$. We prove $d_C(x,y) \leq d(x,y)$ and $d_C(x,y) \geq d(x,y)$ separately.

* By non-expansivity of the maps $f_i \colon (X_i, d_i) \to (C, d_C)$, for any $i \in \mathcal{I}$
such that $f_i(x') = x$ and $f_i(y') = y$ for some $x', y' \in X_i$, we have

\begin{equation*}
d_i(x',y') \geq d_C(f_i(x'),f_i(y')) = d_C(x,y) \,.
\end{equation*}

Thus $d_C(x,y) \leq \inf \{ d_i(x', y') \mid i \in \mathcal{I}\,, f_i(x') = x \,, \text{and } f_i(y') = y \}$.
By (<ref>), $d_C(x,y) \leq d(x,y)$.

* We prove $d \in M_L$. We start by showing that $d$ is a pseudometric on $C$.
Since all $d_i$ are extended metrics, we immediately derive that $d(x,x) = 0$ and $d(x,y) = d(y,x)$
for all $x,y \in C$. Moreover, for all $x,y,z \in C$:

\begin{align*}
&= \inf \{ d_i(x', y') \mid i \in \mathcal{I}\,, f_i(x') = x \,, \text{and } f_i(y') = y \}  \\
&\leq \inf \{ d_i(x', z') + d_i(z',y') \mid i \in \mathcal{I}\,, f_i(x') = x \,, f_i(y') = y \,, f_i(z') = z \}  \\
&\leq d(x,z) + d(z,y) \,,
\end{align*}

where the last inequality follows by the fact that $D$ is filtered, hence
for all $j,k \in \mathcal{I}$ there exists $i \in \mathcal{I}$ and non-expansive maps $D(j \to i)$, $D(k \to i)$ such that $f_j = f_i \circ D(j \to i)$ and $f_k = f_i \circ D(k \to i)$.
Therefore, $d$ is a pseudometric.
The non-expansiveness of the maps $f_j \colon (X_j, d_j) \to (C,d)$, for all $j \in \mathcal{I}$
follows immediately by (<ref>):

\begin{equation*}
d(f_j(x'), f_j(y')) = \inf \{ d_i(x', y') \mid i \in \mathcal{I} \text{ and } x',y' \in X_j \} \leq d_j(x', y') \,.
\end{equation*}

Thus, $d \in M_L$. Therefore, by (<ref>) we have $d_C(x,y) \geq d(x,y)$.

$(X,d_X) \in \Met$ is countably presentable iff it is countable.

Every extended metric space $(X,d_X)$ is a countably filtered colimit of its countable subspaces.
If $(X,d_X)$ is countably presentable, then the identity $id_X$ must factorize through the inclusion of
one of the countable subspaces of $(X,d_X)$. Thus, $(X,d_X)$ is countable.

Conversely, let $(X,d_X)$ be a countable space,
and let $(f_i \colon D(i) \to (C, d_C))_{i \in \mathcal{I}}$ be the colimit cocone to a countably
filtered diagram $D \colon \mathcal{I} \to \Met$.
Any morphism $h \colon (X,d_X) \to (C,d_C)$ factorizes through the image $h(X) \subseteq (C,d_C)$.
Note that $h(X)$ is countable space because $X$ is so.

For each $i \in \mathcal{I}$, let $D(i) = (X_i, d_i)$. Since $D$ is filtered, by Proposition <ref>,
for any $x,y \in h(X)$,

\begin{equation}
d_C(x,y) = \inf \{ d_i(x', y') \mid i \in \mathcal{I}\,, f_i(x') = x \,, \text{and } f_i(y') = y \} \,.
\label{eq:infmetric}
\end{equation}

Thus, for any $n \in \mathbb{N}$ there exist
$j_{n} \in \mathcal{I}$ and $x_{n}, y_{n} \in X_{j_{n}}$ such that

\begin{gather}
f_{j_{n}}(x_{n}) = x \,, \;  f_{j_{n}}(y_{n}) = y \,,  \text{ and } \,
%\label{eq:approximantsmapsto} \\
d_{j_{n}}(x_{n}, y_{n}) \leq d_C(x,y) + \frac{1}{n+1} \,.
\label{eq:approximants}
\end{gather}

Since $D$ is countably filtered, by (<ref>) and Proposition <ref>,
there exist $j_{x,y} \in \mathcal{I}$ and connecting morphisms $D(j_n \to j_{x,y}) \colon X_{j_{n}} \to X_{j_{x,y}}$,
mapping all $x_{n}$ to a single element in $\bar{x}_y \in X_{j_{x,y}}$,
i.e., for all $n \in \mathbb{N}$

\begin{equation}
D(j_n \to j_{x,y})(x_n) = \bar{x}_y
\quad \text{and} \quad f_{j_{x,y}}(\bar{x}_y) = x
%\quad \text{and} \quad D(j_n \to j_{x,y})(y_n) = y'
\,.
\label{eq:commonpair}
\end{equation}

From (<ref>) and the fact that $h(X)$ is countable, by Proposition <ref>,
there exists $j \in \mathcal{I}$ and connecting morphisms such that, for all $x,y \in h(X)$.

\begin{equation}
D(j_{x,y} \to j)(\bar{x}_y) = \bar{x}
\quad \text{and} \quad f_{j}(\bar{x}) = x \,.
\label{eq:finalelement}
\end{equation}

From the construction above, we can define the map $g \colon X \to X_j$ as follows:

\begin{equation*}
g(x) = \overline{h(x)} \,,
\end{equation*}

where $\overline{h(x)}$ is the element in $X_j$ satisfying (<ref>).
Next we prove that $g$ is non-expansive. Assume by contradiction that, $d_X(x,y) < d_j(g(x),g(y))$ for some
$x,y \in X$.
Then there exists $n \in \mathbb{N}$ such that $d_X(x,y) + \frac{1}{n+1} \leq d_j(g(x),g(y))$,
and by non-expansivity of $h$

\begin{equation}
d_C(h(x),h(y)) + \frac{1}{n+1} \leq d_j(g(x),g(y)) = d_j( \overline{h(x)} , \overline{h(y)}) \,.
\label{eq:contraddiction}
\end{equation}

But, by (<ref>) $f_j(\overline{h(x)}) = h(x)$ and $f_j(\overline{h(y)}) = h(y)$. Thus  (<ref>) contradicts (<ref>). Consequently, for all $x,y \in X$, $d_X(x,y) \leq d_j(g(x),g(y))$, i.e., $g$ is non-expansive.

By definition of $g$ and (<ref>) we immediately obtain that $h = f_j \circ g$.
Hence $h$ factorizes through $f_j$. By Proposition <ref> the factorization is essentially unique.
Indeed, whenever $y,y' \in X_i$ fulfil $f_i(y) = f_i(y')$, then there exists $j \in \mathcal{I}$ such that
$D(i \to j)(y) = D(i' \to j)(y')$.

$\Met$ is a locally countably presentable category.

By Proposition <ref>, $\Met$ is cocomplete.
Every extended metric space is the countably filtered colimit of its countable subspaces.
By Lemma <ref> the countable spaces are countably presentable.
Hence for $\Met_{\aleph_1}$ one can take the set of objects of the skeleton category of the full
subcategory of all countable extended metric spaces, or equivalently, the set of all countable ordinals
endowed with an extended metric space.