The proof proceeds by showing that the colimits exhibited in (20) and
subsequently in Proposition 9 constitute a density presentation of $D$ [40,
Section 5.4].

The functors ${\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ that arise as left
Kan extensions in diagram (30) are precisely those that have a presentation by
finitary operations and equations. Note that the elements $n\in{\mathsf{Fin}}$
appear as the arities $X^{n}\longrightarrow X$ of the operations of the
presentation. Similarly, we may speak of the functors that arise as left Kan
extensions in diagram (31) as functors that have a _presentation in discrete
arities_ , with the presentation given by the usual formula
$({\mathrm{Lan}}_{D}H){\mathscr{X}}=\int^{S}{\mathscr{X}}^{DS}\otimes
HS$,161616Note that although ${\mathsf{Set}}$ is not small, the coend does
exist, by [40, Section 4.2]. but which is more easily computed by applying $H$
to the ${\mathscr{V}}$-nerve as in Equation (22).

A complication, studied in Proposition 4, is that
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ is not fully faithful if ${\mathscr{V}}$ is not integral,
that is, if $e<\top$.

Nevertheless we know from Corollary 12, even without restricting to integral
${\mathscr{V}}$, that the discrete functor
${\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$
is dense. Here we show that this result also follows for general reasons that
do not depend on the particular presentation of ${\mathscr{V}}$-categories as
colimits of ${\mathscr{V}}$-nerves.

######  Proposition 21.

The ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ is dense.

######  Proof 3.8.

Let $\mathbb{I}$ denote the unit ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-category (which has only one object $*$ and
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-hom
$\mathbb{I}(*,*)=\mathbb{1}$). Consider the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functors $F:\mathbb{I}\longrightarrow{\mathsf{Set}},\quad
F(*)=\underline{1}$, where $\underline{1}$ denotes a one-element set, and
$G:\mathbb{I}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}},\quad G(*)=\mathbb{1}$. Then the usual coend formula gives
$\mathsf{Lan}_{F}G=D$, using that $\mathbb{I}$ is small and
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ is cocomplete. Now by [40,
(5.17)], $G$ is dense, and by [40, Proposition 5.10], $D$ is also dense, given
that $F$ is fully faithful.

The result on density presentations in [40, Chapter 5] requires Kan extensions
along fully faithful functors. We will henceforth demand in the remaining of
this Section that the quantale ${\mathscr{V}}$ is integral, that is, $e=\top$,
see Proposition 4.

Recall from Proposition 9 that every ${\mathscr{V}}$-category ${\mathscr{X}}$
is the colimit $N\ast DF_{\mathscr{X}}$ of the diagram $(N,DF_{\mathscr{X}})$
of discrete ${\mathscr{V}}$-categories.

######  Theorem 22.

The ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ is dense and the diagrams $(N,DF_{\mathscr{X}})$ form a
density presentation of
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$.

######  Proof 3.9.

We know that $D$ is dense from Proposition 21. Using Proposition 9, we see
that all ${\mathscr{V}}$-coinserters $N\ast DF_{\mathscr{X}}$ exist in
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ and the category
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ is the closure of
${\mathsf{Set}}$ under these colimits. By [40, Theorem 5.19], in order to
establish the density presentation of $D$, it remains to show that the
colimits $N\ast DF_{\mathscr{X}}$ are preserved by the functors
${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(DS,-):{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ for all sets $S$. Abbreviate as earlier
${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(DS,{\mathscr{X}})={\mathscr{X}}^{DS}$. Going back to the
notation of the proof of Proposition 9, we notice that
$(DX_{r})^{DS}=({\mathscr{X}}^{DS})_{r}$ and $(DX_{{\sf
o}})^{DS}=({\mathscr{X}}^{DS})_{{\sf o}}$, so that the diagram
$(DF_{\mathscr{X}})^{DS}$

$\textstyle{(DX_{r})^{DS}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Dd_{1}^{r})^{DS}}$$\scriptstyle{(Dd_{0}^{r})^{DS}}$$\textstyle{(DX_{{\sf
o}})^{DS}}$

is equally the diagram $DF_{{\mathscr{X}}^{DS}}$

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
17.30786pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{({\mathscr{X}}^{DS})r\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces{\hbox{\kern
40.81052pt\raise 2.15277pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{$\scriptstyle{}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern
71.30786pt\raise 2.15277pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces{\hbox{\kern
40.81052pt\raise-2.15277pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{$\scriptstyle{}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern
71.30786pt\raise-2.15277pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
41.30786pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 71.30786pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{({\mathscr{X}}^{DS})_{{\sf
o}}}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

This gives us, using Proposition 9, that

$\displaystyle{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}(DS,N\ast
DF_{\mathscr{X}})$ $\displaystyle\cong{\mathscr{X}}^{DS}$ $\displaystyle\cong
N\ast DF_{{\mathscr{X}}^{DS}}$ $\displaystyle\cong
N\ast(DF_{\mathscr{X}})^{DS}$ $\displaystyle\cong
N\ast{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}(DS,DF_{\mathscr{X}})$

showing that ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}(DS,-)$ preserves
$N\ast DF_{\mathscr{X}}$.

We next characterise the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functors with presentations in discrete arities, that is,
the functors that are left Kan extensions of their restrictions along
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$, as those functors that preserve colimits of
${\mathscr{V}}$-nerves.

######  Theorem 23 (Characterisation of ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functors with presentations in discrete arities).

For $G:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ the following are equivalent:

  1. (1)

There exists a functor
$H:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ such that $G\cong{\mathrm{Lan}}_{D}H$.

  2. (2)

$G$ preserves the colimits of all diagrams $(N,DF_{\mathscr{X}})$.

######  Proof 3.10.

Since the $(N,DF_{\mathscr{X}})$ form a density presentation (Theorem 22),
this is the equivalence of items (i) and (iii) of [40, Theorem 5.29].

${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ifications are similarly
characterised but additionally preserve discreteness.

######  Theorem 24 (Characterisation of ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ifications).

For $G:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ the following are equivalent.

  1. (1)

There exists a functor $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ such
that $G\cong{\mathrm{Lan}}_{D}(DT)$, that is, $G$ is $T_{\mathscr{V}}$, the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of $T$.

  2. (2)

$G$ preserves the colimits of all diagrams $(N,DF_{\mathscr{X}})$, and $G$
preserves discrete ${\mathscr{V}}$-categories.

######  Proof 3.11.

We use Theorem 23 and observe that $G$ mapping discrete
${\mathscr{V}}$-categories to discrete ${\mathscr{V}}$-categories is
equivalent to $GD$ factoring as $DT$ for some $T$.

We will now give an example of a ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functor $G:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ which is not a ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification, even though it preserves discreteness of
${\mathscr{V}}$-categories. $G$ is presented in non-discrete arities as
follows: For a ${\mathscr{V}}$-category ${\mathscr{X}}$, put
$G{\mathscr{X}}={\mathscr{X}}^{{\mathbb{2}}_{r}}$, where the
${\mathscr{V}}$-category ${\mathbb{2}}_{r}$ was introduced in (11), for $r$ an
element of the quantale. Notice that $G$ is the identity on discrete
${\mathscr{V}}$-categories, for every $\bot<r\leq e$. Hence, if $G$ was
${\mathrm{Lan}}_{D}(DT)$ for some
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, we could choose $T$ to be the
identity and then $G$ would also have to be the identity, by Theorem 22 and
[40, Theorem 5.1].

###  3.5. Extending polynomial and finitary functors

Let now ${\mathscr{V}}$ be an arbitrary commutative quantale. We show that
functors defined by finite powers and colimits extend from ${\mathsf{Set}}$ to
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ via their universal
properties. In particular, the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of a finitary functor is presented by the same
operations and equations as its underlying ${\mathsf{Set}}$-functor.

[The ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of polynomial
functors]

  1. (1)

Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, be a constant functor at
a set $S$. Then $T_{\mathscr{V}}$ acts as follows: For any
${\mathscr{V}}$-category ${\mathscr{X}}$, $T_{\mathscr{V}}{\mathscr{X}}$ is
the constant ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor to the
${\mathscr{V}}$-category with $S$ as set of objects, with
${\mathscr{V}}$-distances

$T_{\mathscr{V}}{\mathscr{X}}(x^{\prime},x)=\begin{cases}\,\top\ \ ,\ \
x^{\prime}=x\\\ \bot\ \ ,\ \ \mbox{otherwise}\end{cases}$

That is, $T_{\mathscr{V}}{\mathscr{X}}=S\cdot{\mathbb{1}}_{\top}$ is the
coproduct in ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ of $S$ copies
of the terminal ${\mathscr{V}}$-category ${\mathbb{1}}_{\top}$. Observe that
in case ${\mathscr{V}}$ is integral, we obtain
$T_{\mathscr{V}}{\mathscr{X}}=DS$ for any ${\mathscr{V}}$-category
${\mathscr{X}}$.

  2. (2)

Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be the functor $TX=X^{n}$,
for $n$ a natural number. Then $T_{\mathscr{V}}$ maps a
${\mathscr{V}}$-category ${\mathscr{X}}$ to its $n$-th power
${\mathscr{X}}^{n}$, where an easy computation shows that

${\mathscr{X}}^{n}((x^{\prime}_{0},\dots,x^{\prime}_{n-1}),(x_{0},\dots,x_{n-1}))={\mathscr{X}}(x^{\prime}_{0},x_{0})\wedge\dots\wedge{\mathscr{X}}(x^{\prime}_{n-1},x_{n-1}).$
(32)

  3. (3)

If $n$ is an arbitrary cardinal number, the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification $T_{\mathscr{V}}$ of
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, $TX=X^{n}$ also exists and
$T_{\mathscr{V}}{\mathscr{X}}((x^{\prime}_{i}),(x_{i}))=\bigwedge_{i}{\mathscr{X}}(x^{\prime}_{i},x_{i})$.
That is, $T_{\mathscr{V}}{\mathscr{X}}={\mathscr{X}}^{n}$.

  4. (4)

The ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of a finitary
polynomial functor $X\mapsto\coprod_{n}X^{n}\bullet\Sigma n$ is the “strongly
polynomial” ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
${\mathscr{X}}\mapsto\coprod_{n}{\mathscr{X}}^{n}\otimes D\Sigma n$, where $n$
ranges through finite sets. In particular, the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of the list functor $LX=X^{*}=\coprod_{n}X^{n}$
maps a ${\mathscr{V}}$-category ${\mathscr{X}}$ to the
${\mathscr{V}}$-category having as objects tuples of objects of
${\mathscr{X}}$, with non-trivial ${\mathscr{V}}$-distances only between
tuples of same order, given by (32).

Our next aim is to show that quotients of polynomial functors can be
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ified by taking the “same”
quotients in ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$.

######  Remark 25.

The ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ preserves conical colimits. This follows from the $D_{o}$
being an _ordinary_ left adjoint. However, the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functor
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ is not a left _${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ -adjoint_, as its ordinary right adjoint functor $V$
cannot be extended to a ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functor.

######  Proposition 26.

The assignment
$({-})_{\mathscr{V}}:[{\mathsf{Set}},{\mathsf{Set}}]\longrightarrow[{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}},{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}]$,
$T\mapsto T_{\mathscr{V}}$ of the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification preserves all colimits preserved by
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$. In particular, $T\mapsto T_{\mathscr{V}}$ preserves
conical colimits.

######  Proof 3.12.

Any natural transformation $\tau:T\longrightarrow S$ induces a
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-natural transformation

$(\tau_{\mathscr{V}})_{\mathscr{X}}={N}\mathop{*}{(D\tau
F\\!_{\mathscr{X}})}:{N}\mathop{*}{(DTF\\!_{\mathscr{X}})}\longrightarrow{N}\mathop{*}{(DSF\\!_{\mathscr{X}})}$

Since any colimit is cocontinuous in its weight and since

${N}\mathop{*}{(DTF\\!_{\mathscr{X}})}\cong{(DTF\\!_{\mathscr{X}})}\mathop{*}{N}$

holds [40, Section 3.1], the assignment $T\mapsto T_{\mathscr{V}}$ preserves
all colimits that are preserved by
$D:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$. The last statement follows from Remark 25.

######  Corollary 27.

Suppose that the coequalizer

$\textstyle{T_{\Gamma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\lambda}$$\scriptstyle{\rho}$$\textstyle{T_{\Sigma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\gamma}$$\textstyle{T}$

is the equational presentation of an accessible functor
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$. Then the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification $T_{\mathscr{V}}$
can be obtained as the coequalizer

$\textstyle{(T_{\Gamma})_{\mathscr{V}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\lambda_{\mathscr{V}}}$$\scriptstyle{\rho_{\mathscr{V}}}$$\textstyle{(T_{\Sigma})_{\mathscr{V}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\gamma_{\mathscr{V}}}$$\textstyle{T_{\mathscr{V}}}$

in $[{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}},{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}]$.

######  Remark 28 (The ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of finitary functors).

Corollary 27 allows us to say that the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification $T_{\mathscr{V}}$ of a finitary functor $T$
presented by operations and equations is given by imposing the “same”
operations and equations in ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$.171717 This explains [4, Remark 6.5(1)].  This gives us
an alternative way of computing the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of a finitary (or accessible) functor $T$:
First, one presents $T$ as the quotient of a polynomial functor. Then one
extends the polynomial functor to ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ as in Example 3.5. Finally, one computes the relevant
coequalizers to take a quotient in ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ (see [69, Proposition 2.11] on coequalizers in
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$).

The finite powerset functor is a quotient of the list functor by the familiar
equations stating that sets are invariant under the order and multiplicity of
elements. It is shown in [65] that adding to these equations the requirement
that lists are monotone, one obtains the finite convex powerset functor, which
is indeed the posetification of the finite powerset functor [8].

###  3.6. Extending functors via relation lifting

Extending set-functors to various (ordered) categories using the so-called
relation lifting is an established topic of research going back to [12] and
[63]. Using the representation of quantale-enriched categories as relational
presheaves of Section 2.2, we will see here that this idea can also be applied
to the extension of ${\mathsf{Set}}$-functors to ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ and, moreover, that ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ifications of weak-pullback preserving functors are more
easily computed in this way. In particular, (34) simplifies (28)
significantly. As an application, we will compute the extension of the
multiset functor and show that the well-known Pompeiu-Hausdorff metric arises
as a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of the
powerset functor.

As in [68], “what we do in effect is to reason about metric spaces (or other
structures) in a universe where they are pre-orders, viz. in sheaves over
$[0,\infty]$ (or other ${\mathscr{V}}$).” This point of view is summarised by
Theorem 34 stating mild conditions under which the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification is obtained by
applying the relation lifting to these preorders.

######  Remark 29 (Relation lifting, see for example [12, 63, 28, 35, 44]).

Let $\mathsf{Rel}$ be the 2-category of sets with relations ordered by
inclusion as arrows and
$(-)_{\diamond}:{\mathsf{Set}}\longrightarrow\mathsf{Rel}$ the functor mapping
a function to its graph. Given a functor
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ the relation lifting
$\mathsf{Rel}_{T}:\mathsf{Rel}\longrightarrow\mathsf{Rel}$ extends $T$ to a
colax functor

$\textstyle{\mathsf{Rel}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{Rel}_{T}}$$\textstyle{\mathsf{Rel}}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T}$$\scriptstyle{(-)_{\diamond}}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(-)_{\diamond}}$

and is defined as follows. Let $p:Z\longrightarrow X$ and $q:Z\longrightarrow
Y$ two arrows (called a span from $X$ to $Y$). A _span $(p,q)$ represents the
relation_

$q_{\diamond}\cdot(p_{\diamond})^{-1}=\\{(x,y)\mid\mbox{ there is $z\in Z$
s.t. $x=p(z)$ and $q(z)=y$}\\}$ (33)

where $\cdot$ is composition and -1 is relational inverse. Composition of two
relations is represented by the pullback of their spans. Let $R$ be a relation
represented by the span $(p,q)$. Then _$\mathsf{Rel}_{T}(R)$ is the relation
represented by $(Tp,Tq)$_. This definition is independent of the choice of
span. In the following we only need to know that $\mathsf{Rel}_{T}$ is
monotone, preserves identities, and that it preserves function composition iff
$T$ preserves weak pullbacks. ∎

The following lemma considerably simplifies the formula in Corollary 13 for
computing the left-Kan extension ${\mathrm{Lan}}_{D}H$ in case $H=DT$ with $T$
preserving weak pullbacks.

######  Lemma 30.

Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be a weak pullback
preserving functor. Then the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of $T$ is given by

$T_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)=\bigvee_{s}\\{s\mid(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{s})\\}$
(34)

######  Proof 3.13.

To show “$\geq$” assume $(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{s})$. Then there
is some $C\in T(X_{s})$ such that $Td_{0}^{s}(C)=A^{\prime}$ and
$Td_{1}^{s}(C)=A$. Since this is a (very special) zig-zag of the form of
Corollary 13 it follows that $T_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)\geq
s$.

Conversely, for “$\leq$”, consider a zig-zag

$(A^{\prime},A_{0},C_{1}\in DTX_{r_{1}},A^{\prime}_{1},A_{2},C_{1}\in
DTX_{r_{2}},\ldots,A_{n}^{\prime})$

as in Corollary 13, contributing with

$r=r_{1}\otimes\ldots r_{n}$

to the distance $T_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)$. We want to see
that

$(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{r}).$

Note that $A^{\prime}=A_{0}$ and $A^{\prime}_{i}=A_{i+1}$, $0<i<n$, and
$A^{\prime}_{n}=A$, so that we are looking at the zig-zag

---
$\textstyle{DTX_{r_{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{DTd^{r_{1}}_{0}}$$\textstyle{DTX_{r_{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\quad\cdots\quad\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cdots}$$\scriptstyle{\cdots}$$\textstyle{DTX_{r_{n}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{DTd^{r_{n}}_{1}}$$\textstyle{DTX}$$\textstyle{DTX}$$\textstyle{DTX}$$\textstyle{DTX}$$\textstyle{DTX}$
(35)

Consequently, $(A^{\prime},A)$ is in the relation represented by the zig-zag
(35), that is, in

$\mathsf{Rel}_{T}(X_{r_{1}})\cdot\mathsf{Rel}_{T}(X_{r_{2}})\cdot\ldots\cdot\mathsf{Rel}_{T}(X_{r_{n}})$

We calculate

$\displaystyle\mathsf{Rel}_{T}(X_{r_{1}})\cdot\mathsf{Rel}_{T}(X_{r_{2}})\cdot\ldots\cdot\mathsf{Rel}_{T}(X_{r_{n}})$
$\displaystyle=\mathsf{Rel}_{T}(X_{r_{1}}\cdot X_{r_{2}}\cdot\ldots\cdot
X_{r_{n}})$ $\displaystyle\subseteq\mathsf{Rel}_{T}(X_{r_{1}\otimes
r_{2}\otimes\ldots\otimes r_{n}})$ $\displaystyle=\mathsf{Rel}_{T}(X_{r})$

where the first step is due to $T$ preserving weak pullbacks and the second
step is due to $X_{\\_}$ being lax monoidal, see (7).

[The ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of the
multiset functor] The (finitary) multiset functor
$M:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ can be presented as
$MX=\coprod_{n}X^{n}/S_{n}$, where $S_{n}$ denotes the full $n$-permutation
group [33]. Denote by $\widehat{[x_{1},\ldots,x_{n}]}$ the equivalence class
(multiset) of the tuple $(x_{1},...,x_{n})$ under the action of $S_{n}$.

By Lemma 30 and Equation (33), the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification $M_{\mathscr{V}}$ admits the following
description: it maps a ${\mathscr{V}}$-category ${\mathscr{X}}$ to the
${\mathscr{V}}$-category having as objects multisets of objects of
${\mathscr{X}}$ – formally, $(M_{\mathscr{V}}{\mathscr{X}})_{{\sf o}}=MX_{{\sf
o}}$, and the only possible non-trivial ${\mathscr{V}}$-distances are between
multisets of same cardinal, namely

$\displaystyle
M_{\mathscr{V}}{\mathscr{X}}(\widehat{[x^{\prime}_{1},\ldots,x^{\prime}_{n}]},\widehat{[x_{1},\ldots,x_{n}]})$
$\displaystyle=$ $\displaystyle\bigvee_{s}\\{s\mid\mbox{ there is }C\in
MX_{s}\mbox{ s.t.
}Md_{0}^{s}(C)=\widehat{[x^{\prime}_{1},\ldots,x^{\prime}_{n}]}$
$\displaystyle\mbox{ and }Md_{1}^{s}(C)=\widehat{[x_{1},\ldots,x_{n}]}\,\\}$
$\displaystyle=$ $\displaystyle\bigvee_{s}\\{s\mid\mbox{ there is }\sigma\in
S_{n}\mbox{ s.t. }s\leq{\mathscr{X}}(x^{\prime}_{i},x_{\sigma(i)})$
$\displaystyle\mbox{ for all }i=1,n\,\\}$ $\displaystyle=$
$\displaystyle\bigvee_{\sigma\in S_{n}}\bigvee_{s}\\{s\mid
s\leq{\mathscr{X}}(x^{\prime}_{i},x_{\sigma(i)})\mbox{ for all }i=1,n\,\\}$
$\displaystyle=$ $\displaystyle\bigvee_{\sigma\in
S_{n}}\bigwedge_{i}{\mathscr{X}}(x^{\prime}_{i},x_{\sigma(i)})$

The reader might notice that for
${\mathscr{V}}=([0,\infty],\geq_{\mathbb{R}}+,0)$, we regain by the above
formula the matching metric on multisets [22] employed in image recognition
techniques. Also, it generalises [20], where the case
${\mathscr{V}}={\mathbb{2}}$ (that is, ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}={\mathsf{Preord}}$) was considered, in the sense that
given a (pre)ordered set $(X,\leq)$, multisets on $X$ are ordered by

$\widehat{[x^{\prime}_{1},\ldots,x^{\prime}_{n}]}\leq\widehat{[x_{1},\ldots,x_{n}]}\Longleftrightarrow\mbox{
there is }\sigma\in S_{n}\mbox{ s.t. }x^{\prime}_{i}\leq x_{\sigma(i)}\mbox{
for all }i=1,n$

In fact, [20] corroborated with Lemma 30 and (33) gives us the recipe to
compute the ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of any
analytic ${\mathsf{Set}}$-functor,181818 Analytic functors
${\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ preserve weak pullbacks [33,
Lemma 1.8].  not just of the multiset functor.

[The ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of the
powerset] Let $\mathcal{P}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be the
powerset functor. Using Lemma 30 and Equation (33), the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification
$\mathcal{P}_{\mathscr{V}}$ is described as follows. Let ${\mathscr{X}}$ be
any small ${\mathscr{V}}$-category. Then the objects of
$\mathcal{P}_{\mathscr{V}}{\mathscr{X}}$ are subsets of the set of objects of
${\mathscr{X}}$, while the ${\mathscr{V}}$-“distances” in
$\mathcal{P}_{\mathscr{V}}{\mathscr{X}}$ are computed as follows:

$\displaystyle\mathcal{P}_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)$
$\displaystyle=$ $\displaystyle\bigvee_{s}\\{s\mid\mbox{ there is $C$ in
$\mathcal{P}X_{s}$ s.t. $\mathcal{P}d_{0}^{s}(C)=A^{\prime}$ and
$\mathcal{P}d_{1}^{s}(C)=A$}\\}$ $\displaystyle=$
$\displaystyle\bigvee_{s}\\{s\mid\forall\,x^{\prime}\in
A^{\prime}\,\exists\,x\in A.\,s\leq{\mathscr{X}}(x^{\prime},x)\mbox{ and
}\forall\,x\in A\,\exists\,x^{\prime}\in
A^{\prime}.\,s\leq{\mathscr{X}}(x^{\prime},x)\\}$

Remembering that the join in ${\mathscr{V}}$ denotes the infimum over all
distances, we recognise the familiar Pompeiu-Hausdorff metric as seen in [11,
Definition 2.2], now generalised to categories enriched over an arbitrary
commutative quantales ${\mathscr{V}}$. We will discuss the relationship to the
more customary formulation in the following. ∎

Recall from [25, 51] that a quantale (more generally, a poset) ${\mathscr{V}}$
is called completely distributive if the function from the poset of downsets
of ${\mathscr{V}}$ to ${\mathscr{V}}$,
$\mathfrak{D}\mapsto\bigvee\mathfrak{D}$, has a left adjoint. This left
adjoint maps each $r\in{\mathscr{V}}$ to the downset $\\{s\mid s\ll r\\}$ of
all elements totally-below it, where the “totally-below” relation is

$s\ll
r\quad\Longleftrightarrow\quad(\,\forall\,\mathfrak{D}\subseteq{\mathscr{V}}\mbox{
downset such
that}\,\,r\leq\bigvee\mathfrak{D}\Rightarrow\,s\in\mathfrak{D}\,)$

Examples of completely distributive quantales are ${\mathscr{V}}=[0,1]$ and
${\mathscr{V}}=[0,\infty]$. For such a quantale, we provide below another
characterisation of the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of the powerset functor:

######  Proposition 31 (The ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of the powerset, continued).

If the quantale ${\mathscr{V}}$ is completely distributive, then the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of the powerset
functor can be described as follows: for a ${\mathscr{V}}$-category
${\mathscr{X}}$, $\mathcal{P}_{\mathscr{V}}{\mathscr{X}}$ is the
${\mathscr{V}}$-category with objects $\mathcal{P}X_{{\sf o}}$, and
${\mathscr{V}}$-homs

$\mathcal{P}_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)=\big{(}\bigwedge_{x^{\prime}\in
A^{\prime}}\bigvee_{x\in
A}{\mathscr{X}}(x^{\prime},x)\big{)}\bigwedge\big{(}\bigwedge_{x\in
A}\bigvee_{x^{\prime}\in A^{\prime}}{\mathscr{X}}(x^{\prime},x)\big{)}$ (36)

We will first need a lemma:

######  Lemma 32.

Let $r\in{\mathscr{V}}$ and $S\subseteq{\mathscr{V}}$. Then $r\ll\bigvee S$ if
and only if there is some $s\in S$ with $r\ll s$.

######  Proof 3.14 (Proof of Lemma 32).

The “if” implication is immediate. To see the other implication, assume that
for all $s\in S$, $r\not\ll s$. That is, for each $s\in S$ there is a downset
$\mathfrak{D}_{s}$ with $s\leq\bigvee\mathfrak{D}_{s}$ and
$r\not\in\mathfrak{D}_{s}$. But then $\bigcup_{s\in S}\mathfrak{D}_{s}$ is
again a downset and

$\bigvee S\leq\bigvee\bigcup_{s\in S}\mathfrak{D}_{s}\quad\mbox{ but
}r\not\in\bigcup_{s\in S}\mathfrak{D}_{s}$

which contradicts $r\ll\bigvee S$.

We are now ready to prove Proposition 31.

######  Proof 3.15 (Proof of Proposition 31).

Remember that in Example 3.13, we have obtained that

$\displaystyle\mathcal{P}_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)$
$\displaystyle=$
$\displaystyle\bigvee_{s}\\{s\mid\mbox{$\forall\,x^{\prime}\in A^{\prime}\
\exists\,x\in A.\,s\leq{\mathscr{X}}(x^{\prime},x)$ and $\forall\,x\in A\
\exists\,x^{\prime}\in A^{\prime}.\,s\leq{\mathscr{X}}(x^{\prime},x)$}\\}$

Denote for simplicity

$S=\\{s\mid\mbox{ $\forall\,x^{\prime}\in A^{\prime}\ \exists\,x\in
A.\,s\leq{\mathscr{X}}(x^{\prime},x)$ and $\forall\,x\in A\
\exists\,x^{\prime}\in A^{\prime}.\,s\leq{\mathscr{X}}(x^{\prime},x)$ }\\}$

and notice that $S$ is a downset; also put

$r=\big{(}\bigwedge_{x^{\prime}\in A^{\prime}}\bigvee_{x\in
A}{\mathscr{X}}(x^{\prime},x)\big{)}\bigwedge\big{(}\bigwedge_{x\in
A}\bigvee_{x^{\prime}\in A^{\prime}}{\mathscr{X}}(x^{\prime},x)\big{)}$

Thus we want to see that $r=\displaystyle{\bigvee}S$. The inequality “$\geq$”
follows easily with no assumption on the quantale ${\mathscr{V}}$. For the
other inequality, use complete distributivity to see that

$r\leq\bigvee S$

is equivalent with

$\\{s\mid s\ll r\\}\subseteq S$

Let now $s\ll r$. Then for each $x^{\prime}\in A^{\prime}$, it follows that
$s\ll\bigvee_{x\in A}{\mathscr{X}}(x^{\prime},x)$, thus by the above lemma we
find some $x\in A$ with $s\ll{\mathscr{X}}(x^{\prime},x)$, which implies
$s\leq{\mathscr{X}}(x^{\prime},x)$. Similarly, for all $x\in A$ there is
$x^{\prime}\in A^{\prime}$ with $s\leq{\mathscr{X}}(x^{\prime},x)$.
Consequently, $s\in S$ and the proof is finished.

######  Remark 33.

  1. (1)

Let us switch notation to the dual order (that is, the natural “less-or-equal”
order in case of the reals). So we write $\inf$ for $\bigvee$ and $\sup$ for
$\bigwedge$, in order to emphasise the interpretation of
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$’s as metric spaces. Then
formula (36) becomes

$\sup\\{\ \sup_{x^{\prime}\in A^{\prime}}\ \underset{x\in
A}{\vphantom{p}\inf\vphantom{p}}\ {\mathscr{X}}(x^{\prime},x)\ ,\ \sup_{x\in
A}\ \underset{x^{\prime}\in A^{\prime}}{\vphantom{p}\inf\vphantom{p}}\
{\mathscr{X}}(x^{\prime},x)\\}$ (37)

As mentioned earlier, this metric given by Equation (37) above, is known as
the Pompeiu-Hausdorff metric ([34, § 28], [50, § 21], [46, § 21.VII]). We
should mention also the connection with the work of [3]. Finally, observe that
in case ${\mathscr{V}}={\mathbb{2}}$ (so ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}={\mathsf{Preord}}$), the above specialises to the locally
monotone functor
$\mathcal{P}_{\mathbb{2}}:{\mathsf{Preord}}\longrightarrow{\mathsf{Preord}}$
which sends a preorder $(X,\leq)$ to the Egli-Milner preorder

$A^{\prime}\sqsubseteq A\quad\mbox{iff}\quad\forall\,x^{\prime}\in A^{\prime}\
\exists\,x\in A.\,x^{\prime}\leq x\mbox{ and }\forall\,x^{\prime}\in A\
\exists\,x\in A^{\prime}.\,x^{\prime}\leq x$

on the powerset $\mathcal{P}X$.

  2. (2)

Notice that the ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of
the powerset functor obtained in Proposition 31 for completely distributive
quantale is the (symmetrised version of the) free cocompletion monad with
respect to (the saturated class of) conical colimits in
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ [61].

Example 3.13 raises the question whether the relations
$(T_{\mathscr{V}}{\mathscr{X}})_{r}$ can be computed simply by applying the
relation lifting $\mathsf{Rel}_{T}$ to the $X_{r}$. The next example shows
that we need to be careful with this.

Let ${\mathscr{X}}$ be the metric space of real numbers considered as a
generalised metric space over ${\mathscr{V}}=[0,\infty]$. Let $A^{\prime}$ be
the subset of irrational reals and $A$ the subset of rational reals. Then
$\mathcal{P}_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)=0$ but
$(A^{\prime},A)\notin\mathsf{Rel}_{\mathcal{P}}(X_{0})$. Indeed,
$\mathsf{Rel}_{\mathcal{P}}(X_{0})$ is the diagonal, since $X_{0}$ is the
diagonal.

In terms of Section 2.2, the example above shows that the relational presheaf

$\displaystyle(\Sigma{\mathscr{V}})^{\mathsf{coop}}$
$\displaystyle\longrightarrow\ \mathsf{Rel}$ $\displaystyle r\ \ \ $
$\displaystyle\ \mapsto\ \mathsf{Rel}_{\mathcal{P}}(X_{r})$

is not continuous as we have
$(A^{\prime},A)\in\mathsf{Rel}_{\mathcal{P}}(X_{\varepsilon}),\varepsilon>_{\mathbb{R}}0$,
but $(A^{\prime},A)\notin\mathsf{Rel}_{\mathcal{P}}(X_{0})$. We can repair
this defect by closing the presheaf as follows. Given a relational presheaf
$F:(\Sigma{\mathscr{V}})^{\mathsf{coop}}\longrightarrow\mathsf{Rel}$, and
assuming that ${\mathscr{V}}$ is completely distributive, define its closure
as

$\displaystyle\mathcal{C}F:(\Sigma{\mathscr{V}})^{\mathsf{coop}}$
$\displaystyle\longrightarrow\ \mathsf{Rel}$ $\displaystyle*\ \ \ $
$\displaystyle\ \mapsto F(*)$ $\displaystyle r\ \ \ $ $\displaystyle\ \mapsto\
\bigcap\\{F(s)\mid s\ll r\\}$

It is immediate from the respective definitions that $\mathcal{C}F$ is a
continuous relational presheaf, assuming the tensor laxly preserves the
totally-below relation, in the sense that $r\ll s$ and $r^{\prime}\ll
s^{\prime}$ imply $s\otimes s^{\prime}\ll r\otimes r^{\prime}$. Also, that
$\mathcal{C}(\mathcal{C}F)=\mathcal{C}F$. That is, $\mathcal{C}$ acts like a
closure operator on relational presheaves. This construct extends to a functor
$\mathcal{C}:\mathsf{RelPresh}\longrightarrow\mathsf{RelPresh}_{c}$.

The idea that the ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification
of a weak pullback preserving ${\mathsf{Set}}$-functor $T$ can be computed on
a ${\mathscr{V}}$-category ${\mathscr{X}}$ by applying the relation lifting of
$T$ to the “uniformity” $(X_{r})_{r\in{\mathscr{V}}}$ of ${\mathscr{X}}$ can
now be formalised as in next result. It is a consequence of Proposition 2 and
of Lemma 30.

######  Theorem 34.

Suppose ${\mathscr{V}}$ is a completely distributive quantale, such that the
tensor laxly preserves the totally-below relation. Let
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be a functor which preserves
weak pullbacks. Then post-composition with
$\mathsf{Rel}_{T}:\mathsf{Rel}\longrightarrow\mathsf{Rel}$ yields a functor

$\mathsf{Rel}_{T}\circ(-):\mathsf{RelPresh}_{c}\longrightarrow\mathsf{RelPresh}$

such that the diagram

$\textstyle{\mathsf{RelPresh}_{c}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{Rel}_{T}\circ(-)}$$\textstyle{\mathsf{RelPresh}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathcal{C}}$$\textstyle{\mathsf{RelPresh}_{c}}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T}$$\scriptstyle{D}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$$\scriptstyle{{\mathsf{Id}}}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$

commutes. Moreover, the composite in the upper row is the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of $T$.

######  Proof 3.16.

Let ${\mathscr{X}}$ be a ${\mathscr{V}}$-category and let
$\Phi({\mathscr{X}})$ be its continuous relational presheaf. We compute

$\displaystyle(A^{\prime},A)\in(T_{\mathscr{V}}{\mathscr{X}})_{r}$
$\displaystyle\ \Longleftrightarrow\
r\leq\bigvee_{s}\\{s\mid(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{s})\\}$
$\displaystyle\ \Longleftrightarrow\ \forall s\,.\,s\ll
r\,\Longrightarrow\,(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{s})$ $\displaystyle\
\Longleftrightarrow\ (A^{\prime},A)\in\bigcap\\{\mathsf{Rel}_{T}(X_{s})\mid
s\ll r\\}$ $\displaystyle\ \Longleftrightarrow\
(A^{\prime},A)\in\mathcal{C}(\mathsf{Rel}_{T}\circ\Phi({\mathscr{X}}))(r)$

where the respective steps are due to the following. (i) Lemma 30. (ii) For
all downsets $\mathfrak{D}$ in a completely distributive ${\mathscr{V}}$ one
has $r\leq\bigvee\mathfrak{D}\Longleftrightarrow\forall s(s\ll
r\Longrightarrow s\in\mathfrak{D})$. (iii) Definition of $\bigcap$. (iv)
Definition of $\mathcal{C}$.

###  3.7. Extending ${\mathsf{Set}}$-functors equipped with a
${\mathscr{V}}$-metric

In Section 4.2, we will see that the behaviour of coalgebras for a
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification is metrically
trivial. But often ${\mathsf{Set}}$-functors carry a natural metric and thus
can be considered to be functors
${\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$, which in turn produce ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-endofunctors with non-trivial metric coalgebraic
behaviour.

  1. (1)

Consider ${\mathscr{V}}={\mathbb{2}}$ and let
$H:{\mathsf{Set}}\longrightarrow{\mathsf{Preord}}$ be the powerset functor
with the usual inclusion relation on subsets $HX=(\mathcal{P}(X),\subseteq)$.
Then by [7], the extension $H^{\sharp}$ to ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}={\mathsf{Preord}}$ maps a (pre)ordered set $(X,\leq)$ to
$\mathcal{P}(X)$, ordered with the lower half of the Egli-Milner order on
subsets, namely

$A^{\prime}\leq A\iff\forall\,x^{\prime}\in A^{\prime}\,.\,\exists\,x\in
A\,.\,x^{\prime}\leq x$

for all $A^{\prime},A\in\mathcal{P}(X)$.

  2. (2)

Consider the functor $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$,
$TX=X^{A}\times B$. Recall that $T$-coalgebras are known as deterministic
automata with input set $A$ and outputs in $B$: the transition map of a
coalgebra $X\longrightarrow X^{A}\times B$ sends a state $x\in X$ to a pair:
the associated next-state function $next(x):A\longrightarrow X$ that works
when receiving an input from $A$, and an output $out(x)$ in $B$.

Assume that the output set $B$ carries the additional structure of a
${\mathscr{V}}$-category – that, is, there is a ${\mathscr{V}}$-category
${\mathscr{B}}$ with underlying set of objects $B$. This is the case for
example whenever there is a natural order on $B$, or a metric, which measures
how far apart two outputs might be.

Then the ordinary functor $T_{o}$ can be written as the composite $VH_{o}$,
where $H:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ is the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functor $HX=DX^{A}\otimes{\mathscr{B}}$. Now it is
immediate to see that the latter extends to the functor $H^{\sharp}$ on
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ over the “generalised metric
space” ${\mathscr{B}}$, mapping a ${\mathscr{V}}$-category ${\mathscr{X}}$ to
the tensor product of ${\mathscr{V}}$-categories
$H^{\sharp}{\mathscr{X}}={\mathscr{X}}^{A}\otimes{\mathscr{B}}$, where
${\mathscr{X}}^{A}={\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(DA,{\mathscr{X}})$.

There are two particular cases of this functor that are worth mentioning from
a coalgebraic point of view:

    1. (a)

We start with the easiest case, when $A$ is a singleton. The coalgebras for
the functor $TX=X\times B$ are usually called stream automata; under the
assumption that $B$ carries the structure of a ${\mathscr{V}}$-category
${\mathscr{B}}$, we obtain as above
$H^{\sharp}{\mathscr{X}}={\mathscr{X}}\otimes{\mathscr{B}}$ the stream functor
on ${\mathscr{V}}$-metric spaces.

    2. (b)

If we take an arbitrary set of inputs $A$, but particularise $B$ to
$\\{0,1\\}$, then the transition function of a coalgebra provides binary
outputs, deciding if a state is accepting (response $1$) or not – that is,
$T$-coalgebras are deterministic automata. Enhance now the set of outputs with
a ${\mathscr{V}}$-category structure ${\mathbb{2}}_{r,s}$ generalising (11)

${\mathbb{2}}_{r,s}(0,0)={\mathbb{2}}_{r,s}(1,1)=e\,,\,{\mathbb{2}}_{r,s}(0,1)=r\,,\,{\mathbb{2}}_{r,s}(1,0)=s$

where the elements $r,s$ of the quantale satisfy $r\otimes s\leq e$, in order
to produce the ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-endofunctor
$H^{\sharp}{\mathscr{X}}={\mathscr{X}}^{A}\otimes{\mathbb{2}}_{r,s}$.

The above examples are typical. It happens quite often for endofunctors $T$ on
${\mathsf{Set}}$ to carry an interesting ${\mathscr{V}}$-metric. Then $TX$ is
a ${\mathscr{V}}$-category rather than a mere set. The following generalises
the notion of an order on a functor [38] from ${\mathbb{2}}$ to an arbitrary
quantale ${\mathscr{V}}$.

Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be a functor. We say that
$T$ carries a ${\mathscr{V}}$-metric if there is a
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$H:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ such that $T_{o}$ coincides with the composite

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
11.30168pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{\mathsf{Set}}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
16.1385pt\raise 5.82222pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.9611pt\hbox{$\scriptstyle{H_{o}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 35.30168pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
35.30168pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
75.26337pt\raise 5.39166pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\scriptstyle{V}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 93.08281pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
93.08281pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{{\mathsf{Set}}_{o}}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

Let $T$ and $H$ be as in the above definition. How are $T$ and $H^{\sharp}$,
the left Kan extension of $H$ along $D$ as provided by Theorem 11, related?

Recall from Theorem 11 and Corollary 13 that the unit $\alpha:H\longrightarrow
H^{\sharp}D$ of the left Kan extension is the identity on objects, in
particular that $\alpha$ is a ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-natural isomorphism in case $D$ is fully faithful, that
is, if the quantale is integral. Hence $T_{o}=VH_{o}\cong
VH_{o}^{\sharp}D_{o}$ always holds; using now that the counit of the ordinary
adjunction $D_{o}\dashv V$ is again the identity on objects, we obtain an
ordinary natural transformation

$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H^{\sharp}_{o}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}_{o}}$$\textstyle{{\mathsf{Set}}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T_{o}}$$\scriptstyle{V}$$\scriptstyle{\nearrow\beta}$$\textstyle{{\mathsf{Set}}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{V}$

######  Proposition 35.

The natural transformation $\beta$ is component-wise bijective.

Consequently, $H^{\sharp}$ is a lifting of $T$ to ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ as in Definition 3.1(2).

We will exhibit below another possible way of lifting $T$ to
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$.

[The Kantorovich lifting]

Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be a functor and let
$\heartsuit:T{\mathscr{V}}_{o}\longrightarrow{\mathscr{V}}_{o}$ be an
arbitrary map (a ${\mathscr{V}}$-valued predicate lifting), where by slight
abuse we identify the quantale with its underlying set of elements.

Using the ${\mathscr{V}}$-valued predicate lifting $\heartsuit$, we can endow
$T$ with a ${\mathscr{V}}$-metric
$H:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ as follows: for each set $X$, put $HX$ to be the
${\mathscr{V}}$-category with set of objects $TX$, and
${\mathscr{V}}$-distances

$(HX)(A^{\prime},A)=\bigwedge_{h:X\longrightarrow{\mathscr{V}}_{o}}[(\heartsuit\circ
Th)(A^{\prime}),(\heartsuit\circ Th)(A)]$ (38)

Remark that the ${\mathscr{V}}$-category $HX$ is precisely the initial lift of
$TX$ with respect to the family of maps $\heartsuit\circ
Th:TX\longrightarrow{\mathscr{V}}_{o}$ indexed by all
$h:X\longrightarrow{\mathscr{V}}_{o}$. In particular, the
${\mathscr{V}}$-distances $(HX)(A^{\prime},A)$ are the greatest such that all
maps $\heartsuit\circ Th$ are actually ${\mathscr{V}}$-functors
$HX\longrightarrow{\mathscr{V}}$.

For a map $f:X\longrightarrow Y$, we let $Hf$ act as $Tf$ on objects. It is
easy to see that $Hf:HX\longrightarrow HY$ is a ${\mathscr{V}}$-functor.

The above defines a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$H:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ (the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-enrichment being a consequence of ${\mathsf{Set}}$ being
free as a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-category) with
$VH_{o}=T_{o}$, for every map
$\heartsuit:T{\mathscr{V}}_{o}\longrightarrow{\mathscr{V}}_{o}$.

That is, $H$ is a ${\mathscr{V}}$-metric for $T$ and we may consider the
lifting of $T$ given by the left Kan extension $H^{\sharp}$, as discussed
above. In order to obtain (possibly) another lifting of $T$ to
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$, we make an additional
assumption: $\heartsuit$ is ${\mathscr{V}}$-monotone,191919 This generalises
the notion of monotone predicate lifting from the two-element quantale to
arbitrary ${\mathscr{V}}$, see [8, Section 7]. in the following sense: for
every set $X$ and maps $h,k:X\longrightarrow{\mathscr{V}}_{o}$, the inequality

$\bigwedge_{x\in X}[h(x),k(x)]\leq\bigwedge_{A\in TX}[(\heartsuit\circ
Th)(A),(\heartsuit\circ Tk)(A)]$ (39)

holds.202020 In categorical terms, it says that the correspondence
${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(DX,{\mathscr{V}}){\rightarrow}{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(DTX,{\mathscr{V}})$, $h\mapsto\heartsuit\circ Th$ is a
${\mathscr{V}}$-functor. In particular, taking $X=\emptyset$ and $h=k$ the
unique map from the empty set, we see that ${\mathscr{V}}$-monotonicity of
$\heartsuit$ entails that self-distances on objects of $H\emptyset$ are
$\top$, hence $H^{\sharp}D=H$ by Theorem 20.

Consider the ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$\bar{H}:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ which maps a ${\mathscr{V}}$-category ${\mathscr{X}}$ to
the ${\mathscr{V}}$-category $\bar{H}{\mathscr{X}}$ with set of objects
$TX_{{\sf o}}$, and ${\mathscr{V}}$-homs

$\bar{H}{\mathscr{X}}(A^{\prime},A)=\bigwedge_{h:{\mathscr{X}}\longrightarrow{\mathscr{V}}}[(\heartsuit\circ
Th_{{\sf o}})(A^{\prime}),(\heartsuit\circ Th_{{\sf o}})(A)]$ (40)

for every $A^{\prime},A$ in $TX_{{\sf o}}$, where this time $h$ ranges over
${\mathscr{V}}$-functors and the notation $h_{{\sf o}}$ refers to the object
assignment of a ${\mathscr{V}}$-functor $h$, as in item (1) of the proof of
Theorem 11.

As above for $H$, the ${\mathscr{V}}$-category $\bar{H}{\mathscr{X}}$ is
precisely the initial lift of $TX_{{\sf o}}$ with respect to the family of
maps $\heartsuit\circ Th_{{\sf o}}:TX_{{\sf
o}}\longrightarrow{\mathscr{V}}_{o}$ (indexed by all ${\mathscr{V}}$-functors
$h:{\mathscr{X}}\longrightarrow{\mathscr{V}}$), in particular (40) provides
the greatest ${\mathscr{V}}$-distances such that for all
${\mathscr{V}}$-functors $h:{\mathscr{X}}\longrightarrow{\mathscr{V}}$, the
composite maps $\heartsuit\circ Th_{{\sf o}}$ are also
${\mathscr{V}}$-functors.

For $f:{\mathscr{X}}\longrightarrow{\mathscr{Y}}$ a ${\mathscr{V}}$-functor,
let $\bar{H}f$ act as $Tf_{{\sf o}}$ on objects. Observe that it is the
${\mathscr{V}}$-monotonicity of $\heartsuit$ which ensures that $\bar{H}$ is
indeed a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor. It is
clear that this ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$\bar{H}$ is a lifting for $T$. The particular case ${\mathscr{V}}=[0,\infty]$
provides a generalised Kantorovich lifting as in [10].

Relations (38) and (40) ensure that for each ${\mathscr{V}}$-category
${\mathscr{X}}$, the identity on objects is a ${\mathscr{V}}$-functor
$\bar{c}_{\mathscr{X}}:HX_{{\sf o}}\longrightarrow\bar{H}{\mathscr{X}}$. We
will now prove that $\bar{c}_{\mathscr{X}}$ satisfies (23), thus it induces a
${\mathscr{V}}$-functor
$\gamma_{\mathscr{X}}:H^{\sharp}{\mathscr{X}}\longrightarrow\bar{H}{\mathscr{X}}$
such that $\gamma_{\mathscr{X}}\circ c_{\mathscr{X}}=\bar{c}_{\mathscr{X}}$.

Let thus $r$ an arbitrary element of the quantale. Then we have

$\displaystyle\bigwedge_{C\in
HX_{r}}\bar{H}{\mathscr{X}}(\bar{c}_{\mathscr{X}}Hd^{r}_{0}(C),\bar{c}_{\mathscr{X}}Hd^{r}_{1}(C))$
$\displaystyle=$
$\displaystyle\bigwedge_{(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{r})}\bar{H}{\mathscr{X}}(\bar{c}_{\mathscr{X}}(A^{\prime}),\bar{c}_{\mathscr{X}}(A))$
(41) $\displaystyle=$
$\displaystyle\bigwedge_{(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{r})}\bigwedge_{h:{\mathscr{X}}\longrightarrow{\mathscr{V}}}[\heartsuit\circ
Th_{{\sf o}}(A^{\prime}),\heartsuit\circ Th_{{\sf o}}(A)]$ $\displaystyle\geq$
$\displaystyle\quad\bigwedge_{w\in T{\mathscr{V}}_{r}}[\heartsuit\circ
Td^{r}_{0}(w),\heartsuit\circ Td^{r}_{1}(w)]$

because

$(Th_{{\sf o}}\times Th_{{\sf
o}})(\mathsf{Rel}_{T}(X_{r}))\subseteq\mathsf{Rel}_{T}((h_{{\sf o}}\times
h_{{\sf o}})(X_{r}))\subseteq\mathsf{Rel}_{T}({\mathscr{V}}_{r})$

In the above, we have used that $h:{\mathscr{X}}\longrightarrow{\mathscr{V}}$
is a ${\mathscr{V}}$-functor and that relation lifting preserves inclusions,
and denoted ${\mathscr{V}}_{r}=\\{(s^{\prime},s)\mid r\leq[s^{\prime},s]\\}$
and $d^{r}_{0},d^{r}_{1}:{\mathscr{V}}_{r}\longrightarrow{\mathscr{V}}_{{\sf
o}}$ as for any ${\mathscr{V}}$-category.

Using now (39) for the set ${\mathscr{V}}_{r}$ and for the maps
$d^{r}_{0},d^{r}_{1}$, we see that

$r\leq\bigwedge_{(s^{\prime},s)\in{\mathscr{V}}_{r}}[d^{r}_{0}(s^{\prime},s),d^{r}_{1}(s^{\prime},s)]\leq\bigwedge_{w\in
T{\mathscr{V}}_{r}}[\heartsuit\circ Td^{r}_{0}(w),\heartsuit\circ
Td^{r}_{1}(w)]$ (42)

Putting together (41) and (42) shows that $\bar{c}_{\mathscr{X}}$ satisfies
(23).

In conclusion, there is a ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-natural transformation $H^{\sharp}\longrightarrow\bar{H}$
whose components act as identity on objects, that is, the
${\mathscr{V}}$-distances in $H^{\sharp}{\mathscr{X}}$ are always smaller than
in $\bar{H}{\mathscr{X}}$.

Corroborating the above with the particular example of the Hausdorff metric
$\bar{H}$ on the (finite) powerset functor $T=\mathcal{P}$ exhibited in [10],
it raises the question under which conditions $\bar{H}\cong H^{\sharp}$ holds,
very much in the spirit of the Kantorovich duality [67]. Currently this aspect
is still under research and will not be treated in this paper. ∎

###  3.8. Closure properties of ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ifications

We have seen in Proposition 26 that ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ifications are closed under conical colimits. In this
section, we give sufficient conditions for the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ifications to be closed under composition and finite
products.

We will first discuss when ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ifications are closed under composition: Generalising a
result from [8, Remark 4.8(4)] for the case ${\mathscr{V}}={\mathbb{2}}$,
given weak pullback preserving functors
$T,T^{\prime}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, we will see that
the ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of
$TT^{\prime}$ is the composite of the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ifications $T_{\mathscr{V}}$ and
$T^{\prime}_{\mathscr{V}}$ if the quantale ${\mathscr{V}}$ satisfies the
additional assumption of being completely distributive.

Observe that by the universal property of left Kan extensions, there is a
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-natural transformation
$(TT^{\prime})_{\mathscr{V}}\longrightarrow
T_{\mathscr{V}}T^{\prime}_{\mathscr{V}}$, for any functors
$T,T^{\prime}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$. The component of
this natural transformation at a ${\mathscr{V}}$-category ${\mathscr{X}}$,
namely the ${\mathscr{V}}$-functor
$(TT^{\prime})_{\mathscr{V}}{\mathscr{X}}\longrightarrow
T_{\mathscr{V}}T^{\prime}_{\mathscr{V}}{\mathscr{X}}$, is easily seen to act
as identity on objects,212121 Notice that both ${\mathscr{V}}$-categories
$(TT^{\prime})_{\mathscr{V}}{\mathscr{X}}$ and
$T_{\mathscr{V}}T^{\prime}_{\mathscr{V}}{\mathscr{X}}$ share the same set of
objects, namely $TT^{\prime}X_{{\sf o}}$. and on ${\mathscr{V}}$-homs it
provides the inequality

$(TT^{\prime})_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)\leq
T_{\mathscr{V}}T^{\prime}_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)$

for all objects $A^{\prime},A\in TT^{\prime}X_{{\sf o}}$.

######  Proposition 36.

Assume that the quantale ${\mathscr{V}}$ is completely distributive. Let
$T,T^{\prime}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be functors which
preserve weak pullbacks. Then the inequality

$T_{\mathscr{V}}T^{\prime}_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)\leq(TT^{\prime})_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)$

holds for all $A^{\prime},A\in TT^{\prime}X_{{\sf o}}$.

######  Proof 3.17.

Because $T$ preserves weak pullbacks,
$T_{\mathscr{V}}T^{\prime}_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)=\bigvee\\{r\mid(A^{\prime},A)\in\mathsf{Rel}_{T}((T^{\prime}_{\mathscr{V}}{\mathscr{X}})_{r})\\}$
by Lemma 30. Let $r\in{\mathscr{V}}_{o}$ such that
$(A^{\prime},A)\in\mathsf{Rel}_{T}((T^{\prime}_{\mathscr{V}}{\mathscr{X}})_{r})$.
Given that ${\mathscr{V}}$ is completely distributive, to show that

$r\leq(TT^{\prime})_{\mathscr{V}}{\mathscr{X}}(A^{\prime},A)=\bigvee\\{s\mid(A^{\prime},A)\in\mathsf{Rel}_{TT^{\prime}}(X_{s})\\}$

is the same as

$\forall\,s\in{\mathscr{V}}_{o}\,.\,s\ll
r\,\Longrightarrow(A^{\prime},A)\in\mathsf{Rel}_{TT^{\prime}}(X_{s})$

because $\\{s\mid(A^{\prime},A)\in\mathsf{Rel}_{TT^{\prime}}(X_{s})\\}$ is a
downset and ${\mathscr{V}}$ is completely distributive. Also notice that

$(T^{\prime}_{\mathscr{V}}{\mathscr{X}})_{r}\subseteq\mathsf{Rel}_{T}^{\prime}(X_{s})\
\ \ $ (43)

holds for all $s\ll r$. Indeed, for
$(B^{\prime},B)\in(T^{\prime}_{\mathscr{V}}{\mathscr{X}})_{r}$, we have that

$r\leq
T^{\prime}_{\mathscr{V}}{\mathscr{X}}(B^{\prime},B)=\bigvee\\{s\mid(B^{\prime},B)\in\mathsf{Rel}_{T}^{\prime}(X_{s})\\}$

using that $T^{\prime}$ preserves weak pullbacks and Lemma 30. But the
relation above is equivalent to

$\forall\,s\in{\mathscr{V}}_{o}\,.\,s\ll
r\,\Longrightarrow(B^{\prime},B)\in\mathsf{Rel}_{T}^{\prime}(X_{s})$

Hence
$(T^{\prime}_{\mathscr{V}}{\mathscr{X}})_{r}\subseteq\mathsf{Rel}_{T}^{\prime}(X_{s})$
holds for all $s\ll r$. Therefore we have

$(A^{\prime},A)\in\mathsf{Rel}_{T}((T^{\prime}_{\mathscr{V}}{\mathscr{X}})_{r})\subseteq\mathsf{Rel}_{T}(\mathsf{Rel}_{T^{\prime}}(X_{s}))=\mathsf{Rel}_{TT^{\prime}}(X_{s})$

for all $s\ll r$, where the last equality follows from [16, Section 4.4].

######  Corollary 37.

Let ${\mathscr{V}}$ be a completely distributive commutative quantale and
$T,T^{\prime}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ functors which
preserve weak pullbacks. Then

$(TT^{\prime})_{\mathscr{V}}=T_{\mathscr{V}}T^{\prime}_{\mathscr{V}}$

holds.

Next we show that the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification process is also closed under finite products,
if some additional conditions are imposed to ${\mathscr{V}}$.

######  Proposition 38.

Let ${\mathscr{V}}$ be an integral commutative quantale such that finite meets
distribute over arbitrary joins in ${\mathscr{V}}$ (the underlying lattice of
${\mathscr{V}}$ is a frame). Then the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification assignment
$({-})_{\mathscr{V}}:[{\mathsf{Set}},{\mathsf{Set}}]\longrightarrow[{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}},{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}]$,
$T\mapsto T_{\mathscr{V}}$, preserves finite products of weak pullback
preserving functors.

######  Proof 3.18.

The empty product, that is, the constant functor
${\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ at the one-element set has as
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification the constant
functor at ${\mathbb{1}}$. Because $e=\top$ holds in ${\mathscr{V}}$ by
hypothesis, the latter is the terminal object in $[{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}},{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}]$ [15].

Let us look now at binary products of weak-pullback preserving functors
$T,T^{\prime}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$. We will denote by
$T\times{T^{\prime}}$ the product in $[{\mathsf{Set}},{\mathsf{Set}}]$,
sending $X$ to $TX\times{T^{\prime}}X$ and shall extend this notation to
$[{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}]$.

Now observe that for a ${\mathscr{V}}$-category ${\mathscr{X}}$, the
${\mathscr{V}}$-categories $T_{\mathscr{V}}{\mathscr{X}}\times
T^{\prime}_{\mathscr{V}}{\mathscr{X}}$ and
$(T\times{T^{\prime}})_{\mathscr{V}}{\mathscr{X}}$ share the same objects. The
universal property of products induces a ${\mathscr{V}}$-functor $(T\times
T^{\prime})_{\mathscr{V}}{\mathscr{X}}\longrightarrow
T_{\mathscr{V}}{\mathscr{X}}\times T^{\prime}_{\mathscr{V}}{\mathscr{X}}$,
which on the corresponding ${\mathscr{V}}$-homs says that the inequality

$(T\times{T^{\prime}})_{\mathscr{V}}({\mathscr{X}})((A^{\prime},B^{\prime}),(A,B))\leq(T_{\mathscr{V}}\times
T^{\prime}_{\mathscr{V}})({\mathscr{X}})((A^{\prime},B^{\prime}),(A,B))$

holds for each objects $A^{\prime},A$ of $T_{\mathscr{V}}{\mathscr{X}}$ and
$B^{\prime},B$ of $T^{\prime}_{\mathscr{V}}{\mathscr{X}}$. The converse
inequality is shown below, using Lemma 30 and the frame law:

$\displaystyle(T_{\mathscr{V}}\times
T^{\prime}_{\mathscr{V}})({\mathscr{X}})((A^{\prime},B^{\prime}),(A,B))=$
$\displaystyle T_{\mathscr{V}}({\mathscr{X}})(A^{\prime},A)\wedge
T^{\prime}_{\mathscr{V}}({\mathscr{X}})(B^{\prime},B)=$
$\displaystyle\bigvee\\{t\mid(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{t}))\\}\wedge\bigvee\\{s\mid(B^{\prime},B)\in\mathsf{Rel}_{T^{\prime}}(X_{s}))\\}=$
$\displaystyle\bigvee\\{t\wedge
s\mid(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{t}),(B^{\prime},B)\in\mathsf{Rel}_{T^{\prime}}(X_{s})\\}\leq$
$\displaystyle\bigvee\\{t\wedge
s\mid(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{t\wedge
s}),(B^{\prime},B)\in\mathsf{Rel}_{T^{\prime}}(X_{t\wedge s})\\}\leq$
$\displaystyle\bigvee\\{r\mid(A^{\prime},A)\in\mathsf{Rel}_{T}(X_{r}),(B^{\prime},B)\in\mathsf{Rel}_{T^{\prime}}(X_{r})\\}=$
$\displaystyle\bigvee\\{r\mid((A^{\prime},B^{\prime}),(A,B))\in\mathsf{Rel}_{T\times
T^{\prime}}(X_{r})\\}=$ $\displaystyle(T\times
T^{\prime})_{\mathscr{V}}({\mathscr{X}})((A^{\prime},B^{\prime}),(A,B))$

That is, $(T\times T^{\prime})_{\mathscr{V}}=T_{\mathscr{V}}\times
T^{\prime}_{\mathscr{V}}$ holds for all functors $T,T^{\prime}$ which preserve
weak pullbacks.

##  4\. Solving domain equations across different base categories

In the previous section, we studied those functors on
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ that arise as left Kan
extensions of functors on ${\mathsf{Set}}$, with Theorems 24 and 23 accounting
for the situations depicted on the left and right below.

$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T}$$\scriptstyle{D}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$
$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$$\scriptstyle{H}$

In this section, we study the relationship between solving recursive equations
in ${\mathsf{Set}}$ and in ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$.
In both cases, accounted for by Theorems 52 and 53, if we have a coalgebra
$X\longrightarrow TX$ or $X\longrightarrow VHX$, then two states in $X$ are
behaviourally equivalent (bisimilar) iff they are behaviourally equivalent in
$DX\longrightarrow\overline{T}DX$. Moreover, while in the first case the
behavioural distance of two states is either $0$ or $\infty$ (the states are
behaviourally equivalent or not), in the second case the enrichment typically
gives rise to non-trivial behavioural distances.

We first review in Section 4.1 what in relation to [60] could be called the
“formal theory of endofunctors”. Relevant references for this section include
[23, 60] in case of algebras for ${\mathscr{V}}$-enriched monads and [35, 48]
in case of (co)algebras for (${\mathscr{V}}$-enriched) endofunctors.

Section 4.2 carries out an analysis of categories of coalgebras for both
liftings and extensions, in case of “change-of-base” for the quantale
${\mathscr{V}}$, extending results of [7, 8]. As corollaries we get
information about final coalgebras of ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-endofunctors $\overline{T}$ as in the diagrams above.

###  4.1. A 2-categorical approach to coalgebras

In order to relate coalgebras for different type functors on different
categories, it will be convenient to work in a (2-)category where the objects
are types (endofunctors) and the arrows are certain natural transformations
that allow to connect types on different base categories. For the basic
notions of $2$-categories that we need in this section we refer to [42].

Let ${\mathscr{C}}$ be a 2-category. The category
$\mathsf{Endo}({\mathscr{C}})$ has objects $(X,T)$ given by 1-cells
$T:X\longrightarrow X$ in ${\mathscr{C}}$. An arrow
$(F,\varphi):(X,T)\longrightarrow(X^{\prime},T^{\prime})$ is given by a 1-cell
$F:X\longrightarrow X^{\prime}$ and a 2-cell $\varphi:FT\longrightarrow
T^{\prime}F$. A 2-cell
$\sigma:(F,\varphi)\longrightarrow(F^{\prime},\varphi^{\prime})$ is a 2-cell
$\sigma:F\longrightarrow F^{\prime}$ such that
$T^{\prime}\sigma\circ\varphi=\varphi^{\prime}\circ\sigma T$.

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T}$$\scriptstyle{F}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F}$$\scriptstyle{\swarrow\varphi}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F^{\prime}}$$\scriptstyle{T}$$\scriptstyle{F}$$\scriptstyle{\sigma\swarrow}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F}$$\scriptstyle{\swarrow\varphi}$$\scriptstyle{=}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T}$$\scriptstyle{F^{\prime}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F}$$\scriptstyle{F^{\prime}}$$\scriptstyle{\swarrow\sigma}$$\scriptstyle{\swarrow\varphi}$$\textstyle{X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T^{\prime}}$$\textstyle{X^{\prime}}$$\textstyle{X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T^{\prime}}$$\textstyle{X^{\prime}}$$\textstyle{X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T^{\prime}}$$\textstyle{X^{\prime}}$

Notice that there is a canonical inclusion 2-functor
$\mathsf{Incl}:{\mathscr{C}}\longrightarrow\mathsf{Endo}({\mathscr{C}})$
mapping each object $X$ to the pair $(X,{\mathsf{Id}})$.

The above definition is set-up precisely for the next proposition, which
allows us to say, in analogy to the formal theory of monads [60], that a
general 2-category ${\mathscr{C}}$ admits coalgebras (for endo-1-cells) if the
inclusion
$\mathsf{Incl}:{\mathscr{C}}\longrightarrow\mathsf{Endo}({\mathscr{C}})$ has a
right 2-adjoint.222222 Notice that changing the orientation of the 2-cells in
Definition 4.1 would lead to a different 2-category of endo-1-cells, such that
the right 2-adjoint to the inclusion (if exists) produces instead the
“category of algebras” for the endofunctor $T$. This result has been
independently mentioned by several authors at different moments of time (see
for example [48] for the 2-categorical story, but also the early [19] which
deals with algebras instead of coalgebras):

######  Proposition 39.

Let ${\mathscr{C}}$ be a 2-category with inserters.232323 Inserters are dual
to coinserters, see Example 2.5. Then the inclusion 2-functor $\mathsf{Incl}$
has a right 2-adjoint
$\mathsf{Coalg}:\mathsf{Endo}({\mathscr{C}})\longrightarrow{\mathscr{C}}$,
mapping an object $(X,T)$ to the inserter of ${\mathsf{Id}}:X\longrightarrow
X$ and $T$.

######  Proof 4.1.

This follows from the correspondences

(1-cell in ${\mathscr{C}}$) $\overline{F}:Z\longrightarrow\mathsf{Coalg}(X,T)$
---
(2-cell in ${\mathscr{C}}$) $\varphi:F\longrightarrow TF$ (where
$F:Z\longrightarrow X$ is a 1-cell in ${\mathscr{C}}$)
(1-cell in $\mathsf{Endo}({\mathscr{C}})$)
$(F,\varphi):(Z,{\mathsf{Id}})\longrightarrow(X,T)$

In the above, the second bijection is the definition of 1-cells in
$\mathsf{Endo}({\mathscr{C}})$, while the first bijection is due to the fact
that $\mathsf{Coalg}(X,T)$ is an inserter of ${\mathsf{Id}}$ and $T$ (in that
order). More precisely,

$\varphi:F\longrightarrow TF$

is an “inserter cone”, and therefore $\varphi$ gives rise to $\overline{F}$
(that is, to the factorisation through the “inserter cone”).

######  Remark 40.

In case ${\mathscr{C}}$ is the 2-category of ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-categories, ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functors, and ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-natural transformations, recall from [15, Sect. 6.1] how
to compute the inserter between two ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functors $F,G:{\mathbb{X}}\longrightarrow{\mathbb{Y}}$:

  * •

$\mathsf{Ins}(F,G)$ is the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-category having as objects pairs $(X,\tau)$, where $X$ is
an object of ${\mathbb{X}}$ and
$\tau:{\mathbb{1}}\longrightarrow{\mathbb{Y}}(FX,GX)$ is a
${\mathscr{V}}$-functor (which only picks an object, still denoted
$\tau:FX\longrightarrow GX$). The ${\mathscr{V}}$-category-hom
$\mathsf{Ins}(F,G)((X,\tau),(X^{\prime},\sigma))$ is the equaliser in
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ of the parallel pair

$\textstyle{{\mathbb{1}}\otimes{\mathbb{X}}(X,X^{\prime})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma\otimes
F_{X,X^{\prime}}}$$\textstyle{{\mathbb{Y}}(FX^{\prime},GX^{\prime})\otimes{\mathbb{Y}}(FX,FX^{\prime})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\phantom{MM}c_{FX,FX^{\prime},GX^{\prime}}}$$\textstyle{{\mathbb{X}}(X,X^{\prime})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\scriptstyle{\cong}$$\textstyle{{\mathbb{Y}}(FX,GX^{\prime})}$$\textstyle{{\mathbb{X}}(X,X^{\prime})\otimes{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{G_{X,X^{\prime}}\otimes\tau}$$\textstyle{{\mathbb{Y}}(FX,GX^{\prime})\otimes{\mathbb{Y}}(FX,GX)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\phantom{MM}c_{FX,GX,GX^{\prime}}}$

Explicitly, the objects of $\mathsf{Ins}(F,G)((X,\tau),(X^{\prime},\sigma))$
are objects $h:X\longrightarrow X^{\prime}$ of the ${\mathscr{V}}$-category
${\mathbb{X}}(X,X^{\prime})$ such that $\sigma\,\cdot\,Fh=Gh\,\cdot\,\tau$,
with ${\mathscr{V}}$-distances

$\mathsf{Ins}(F,G)((X,\tau),(X^{\prime},\sigma))(h,k)={\mathbb{X}}(X,X^{\prime})(h,k)$

for $h,k:X\longrightarrow X^{\prime}$ as above. Composition and identity in
$\mathsf{Ins}(F,G)((X,\tau),(X^{\prime},\sigma))$ are induced from the
composition in ${\mathbb{X}}(X,X^{\prime})$.

  * •

There is an obvious ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$J:\mathsf{Ins}(F,G)\longrightarrow{\mathbb{X}}$ mapping $(X,\tau)$ to $X$,
and a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-natural transformation
$\iota:FJ\Rightarrow GJ$ with components
$\iota_{(X,\tau)}:{\mathbb{1}}\longrightarrow{\mathbb{Y}}(FJ(X,\tau),GJ(X,\tau))$
mapping the unique object $0$ to $\tau$.

In particular, the above yields the description of the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-category $\mathsf{Coalg}(T)$
as $\mathsf{Ins}({\mathsf{Id}},T)$, for any ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functor $T:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$. More in detail:

  * •

Objects are $T$-coalgebras, that is, pairs $({\mathscr{X}},c)$ where
${\mathscr{X}}$ is a ${\mathscr{V}}$-category and
$c:{\mathscr{X}}\longrightarrow T{\mathscr{X}}$ is a ${\mathscr{V}}$-functor.

  * •

The ${\mathscr{V}}$-category
$\mathsf{Coalg}(T)(({\mathscr{X}},c),({\mathscr{Y}},d))$ is the equaliser of

$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}({\mathscr{X}},{\mathscr{Y}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}({\mathscr{X}},d)}$$\scriptstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(c,T{\mathscr{Y}})\circ
T_{{\mathscr{X}},{\mathscr{Y}}}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}({\mathscr{X}},T{\mathscr{Y}})}$

that is, it has as objects ${\mathscr{V}}$-functors
$f:{\mathscr{X}}\longrightarrow{\mathscr{Y}}$ such that $d\circ f=T(f)\circ
c$, with ${\mathscr{V}}$-distances between two such ${\mathscr{V}}$-functors
$f,g:{\mathscr{X}}\longrightarrow{\mathscr{Y}}$ being given by
$[{\mathscr{X}},{\mathscr{Y}}](f,g)=\bigwedge_{x}{\mathscr{Y}}(f(x),g(x))$.

  * •

There is a forgetful ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$\mathsf{Coalg}(T)\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ sending a $T$-coalgebra $({\mathscr{X}},c)$ to the
underlying ${\mathscr{V}}$-category ${\mathscr{X}}$.

One of the reasons to introduce the formal category
$\mathsf{Endo}({\mathscr{C}})$ is that it allows the following
characterisation of when adjunctions in ${\mathscr{C}}$ can be lifted.

######  Proposition 41.

$(L,\varphi)\dashv(R,\psi)$ in the 2-category $\mathsf{Endo}({\mathscr{C}})$
if and only if $L\dashv R$ holds in ${\mathscr{C}}$, $\psi$ is iso, and
$\varphi$ is the mate of $\psi^{-1}$ under the adjunction $L\dashv R$.

######  Proof 4.2.

By standard doctrinal adjunction [39].

Since $\mathsf{Coalg}$ is a 2-functor, it preserves adjunction of 1-cells,
thus we obtain a well-known corollary allowing us to lift an adjunction
$L\dashv R$ between base objects to an adjunction between “categories of
coalgebras”:

######  Corollary 42.

Let ${\mathscr{C}}$ be a 2-category with inserters, and let $L\dashv
R:X^{\prime}\longrightarrow X$ an adjunction in ${\mathscr{C}}$. For any
$T:X\longrightarrow X$, $T^{\prime}:X^{\prime}\longrightarrow X^{\prime}$,
such that there is an iso-2-cell $\psi:RT^{\prime}\longrightarrow TR$, it
follows that:

  1. (1)

$R$ lifts to
$\tilde{R}=\mathsf{Coalg}(R,\psi):\mathsf{Coalg}(X^{\prime},T^{\prime})\longrightarrow\mathsf{Coalg}(X,T)$

  2. (2)

There is an adjunction
$\tilde{L}\dashv\tilde{R}:\mathsf{Coalg}(X^{\prime},T^{\prime})\longrightarrow\mathsf{Coalg}(X,T)$,
where $\tilde{L}$ is the image under $\mathsf{Coalg}$ of the 1-cell in
$\mathsf{Endo}({\mathscr{C}})$ given by $L$ and the mate of the inverse of
$\psi:RT^{\prime}\longrightarrow TR$.

We end this section with observations on the existence and the computation of
limits and colimits in ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-categories of coalgebras. Again, these results seem to be
folklore, but being unable to find them explicitly in the literature, we
provide them below.

######  Proposition 43.

The ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-category
$\mathsf{Coalg}(T)$, for a ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functor $T:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$, is cocomplete, and has all (weighted) limits that $T$
preserves.

######  Proof 4.3.

Let $W:\mathcal{K}^{\mathsf{op}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ and
$\overline{F}:\mathcal{K}\longrightarrow\mathsf{Coalg}(T)$ be
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functors, denoting the
weight and the diagram of shape $\mathcal{K}$, a small
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-category. By the inserter’s
universal property, to give
$\overline{F}:\mathcal{K}\longrightarrow\mathsf{Coalg}(T)$ is the same as to
give a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor
$F:\mathcal{K}\longrightarrow{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$,
together with a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-natural
transformation $\xi:F\longrightarrow TF$. Then the colimit $W*F$ becomes a
$T$-coalgebra with structure $\alpha:W*F\longrightarrow T(W*F)$ being the
${\mathscr{V}}$-functor which corresponds to the identity on $W*F$ under the
composite

$\displaystyle{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}(W*F,W*F)$
$\displaystyle\cong$
$\displaystyle[\mathcal{K}^{\mathsf{op}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}](W,{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(F-,W*F))$ $\displaystyle\overset{T}{\longrightarrow}$
$\displaystyle[\mathcal{K}^{\mathsf{op}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}](W,{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(TF-,T(W*F)))$
$\displaystyle\overset{\xi}{\longrightarrow}$
$\displaystyle[\mathcal{K}^{\mathsf{op}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}](W,{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(F-,T(W*F)))$ $\displaystyle\cong$
$\displaystyle{\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}(W*F,T(W*F))$

Now, let $({\mathscr{X}},c:{\mathscr{X}}\longrightarrow T{\mathscr{X}})$ be an
arbitrary $T$-coalgebra and consider the diagram below:

$\textstyle{\mathsf{Coalg}(T)((W*F,\alpha),({\mathscr{X}},c))\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{[\mathcal{K}^{\mathsf{op}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}](W,\mathsf{Coalg}(T)(\overline{F}-,({\mathscr{X}},c)))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(W*F,{\mathscr{X}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\textstyle{[\mathcal{K}^{\mathsf{op}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}](W,{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(F-,{\mathscr{X}}))\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(W*F,T{\mathscr{X}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\textstyle{[\mathcal{K}^{\mathsf{op}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}](W,{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}(F-,T{\mathscr{X}}))}$

where the bottom square commutes serially and both columns are equalizers –
the left one by construction of ${\mathscr{V}}$-category-homs in the inserter
$\mathsf{Coalg}(T)$, and the right one because the representable
$[\mathcal{K}^{\mathsf{op}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}](W,-)$ preserves limits, in particular equalizers.
Consequently, there is a unique arrow (isomorphism)

$\textstyle{\mathsf{Coalg}(T)((W*F,\alpha),({\mathscr{X}},c))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\textstyle{[\mathcal{K}^{\mathsf{op}},{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}](W,\mathsf{Coalg}(T)(\overline{F}-,({\mathscr{X}},c)))}$

exhibiting $(W*F,\alpha)$ as the $W$-weighted colimit of $\overline{F}$.

A similar computation that we leave to the reader shows that
$\mathsf{Coalg}(T)$ has all weighted limits that $T$ preserves.

###  4.2. Relating behaviours across different base categories

We consider “change of base” across different ${\mathscr{V}}$. We therefore
now write
$D^{\mathscr{V}}:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ and $V^{\mathscr{V}}:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}_{o}\longrightarrow{\mathsf{Set}}_{o}$ to distinguish the
discrete and forgetful functors for different ${\mathscr{V}}$. We drop the
superscript $(-)^{\mathscr{V}}$ in case ${\mathscr{V}}={\mathbb{2}}$.

In the previous section, we have shown that every ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functor
$H:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ has a left Kan extension along $D^{\mathscr{V}}$, denoted
$H^{\sharp}$. Now, each such functor induces an ordinary set-endofunctor
simply by forgetting the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-structure

$\textstyle{{\mathsf{Set}}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H_{o}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{V^{\mathscr{V}}}$$\textstyle{{\mathsf{Set}}_{o}}$

Moreover, $H^{\sharp}$ is a lifting of $V^{\mathscr{V}}H_{o}$ according to
Proposition 35.

In the special case when $H$ is $D^{\mathscr{V}}T$, the above composite gives
back $T$ (formally, it is $T_{o}$), and $H^{\sharp}$ is $T_{\mathscr{V}}$, the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification of $T$.

We will see how the corresponding behaviours are related. In particular, we
will show at the end of the section that $H^{\sharp}$ and
$V^{\mathscr{V}}H_{o}$, hence $T_{\mathscr{V}}$ and $T$, induce the same
behavioural equivalence (bisimilarity), while $H^{\sharp}$ may additionally
induce a behavioural pseudometric.

######  Remark 44.

For each commutative quantale ${\mathscr{V}}$, the inclusion (quantale
morphism) $\mathsf{d}:{\mathbb{2}}\longrightarrow{\mathscr{V}}$ given by
$0\mapsto\bot,\ 1\mapsto e$, has a right adjoint (as it preserves suprema),
denoted $\mathsf{v}:{\mathscr{V}}\longrightarrow{\mathbb{2}}$ , which maps an
element $r$ of ${\mathscr{V}}$ to $1$ if $e\leq r$, and to $0$
otherwise.242424 Notice that $\mathsf{v}$ is only a _lax_ morphism of
quantales, being right adjoint. This induces as usual the _change-of-base_
adjunction (even a 2-adjunction, see [24])

$\textstyle{{\mathbb{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}}$$\scriptstyle{\perp}$$\textstyle{{\mathscr{V}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{v}}$$\textstyle{\mapsto}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}_{*}}$$\scriptstyle{\perp}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{v}_{*}}$

Explicitly, the functor $\mathsf{d}_{*}$ maps a preordered set $X$ to the
${\mathscr{V}}$-category $\mathsf{d}_{*}X$ with same set of objects, and
${\mathscr{V}}$-homs given by $\mathsf{d}_{*}X(x^{\prime},x)=e$ if
$x^{\prime}\leq x$, and $\bot$ otherwise. Its right adjoint transforms a
${\mathscr{V}}$-category ${\mathscr{X}}$ into the preorder
$\mathsf{v}_{*}{\mathscr{X}}$ with same objects again, and order
$x^{\prime}\leq x$ iff $e\leq{\mathscr{X}}(x^{\prime},x)$ holds. Hence
$\mathsf{d}_{*}X$ is the free ${\mathscr{V}}$-category on the preorder $X$,
while $\mathsf{v}_{*}{\mathscr{X}}$ is the underlying ordinary category (which
happens to be a preorder, due to the simple nature of quantales) of the
${\mathscr{V}}$-category ${\mathscr{X}}$. ∎

Note that $\mathsf{d}_{*}$ is both a ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-functor and a ${\mathsf{Preord}}$-functor, while its
right adjoint $\mathsf{v}_{*}$ (in fact, the whole adjunction
$\mathsf{d}_{*}\dashv\mathsf{v}_{*}$) is only ${\mathsf{Preord}}$-enriched.

######  Remark 45.

If ${\mathscr{V}}$ is nontrivial and integral, the embedding
$\mathsf{d}:{\mathbb{2}}\longrightarrow{\mathscr{V}}$ has also a left adjoint
$\mathsf{c}:{\mathscr{V}}\longrightarrow{\mathbb{2}}$, given by
$\mathsf{c}(r)=0$ iff $r=\bot$, otherwise $\mathsf{c}(r)=1$. Notice that
$\mathsf{c}$ is only a colax morphism of quantales, in the sense that
$\mathsf{c}(e)\leq 1$ (in fact, here we have equality) and
$\mathsf{c}(r\otimes s)\leq\mathsf{c}(r)\land\mathsf{c}(s)$, for all $r,s$ in
${\mathscr{V}}$.

We will in the sequel assume that $\mathsf{c}$ is actually a morphism of
quantales. The reader can check that this boils down to the requirement that
$r\otimes s=\bot$ in ${\mathscr{V}}$ implies $r=\bot$ or $s=\bot$. That is,
the quantale has no zero-divisors. All our examples satisfy this assumption.

If the quantale has no zero-divisors, $\mathsf{d}_{*}$ also has a left adjoint
$\mathsf{c}_{*}$ mapping a ${\mathscr{V}}$-category ${\mathscr{X}}$ to the
preorder $\mathsf{c}_{*}{\mathscr{X}}$ with same objects and $x^{\prime}\leq
x$ in ${\mathsf{c}_{*}{\mathscr{X}}}$ iff
${\mathscr{X}}(x^{\prime},x)\neq\bot$. Moreover, the adjunction
$\mathsf{c}_{*}\dashv\mathsf{d}_{*}$ is ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-enriched:

$\textstyle{{\mathbb{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}}$$\scriptstyle{\perp}$$\textstyle{{\mathscr{V}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{c}}$$\textstyle{\mapsto}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}_{*}}$$\scriptstyle{\perp}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{c}_{*}}$

From the above remark we obtain the following propositions.

######  Proposition 46.

Let ${\mathscr{V}}$ be an arbitrary commutative quantale and let
$\widehat{T}:{\mathsf{Preord}}\longrightarrow{\mathsf{Preord}}$ be a locally
monotone functor (that is, ${\mathsf{Preord}}$-enriched) and
$\overline{T}:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ be a lifting of $\widehat{T}$ to
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ (meaning that $\overline{T}$
is a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor such that
$\mathsf{v}_{*}\overline{T}\cong\widehat{T}\mathsf{v}_{*}$ holds). Then the
locally monotone adjunction $\mathsf{d}_{*}\dashv\mathsf{v}_{*}$ lifts to a
locally monotone adjunction
$\widetilde{\mathsf{d}}_{*}\dashv\widetilde{\mathsf{v}}_{*}$ between the
associated ${\mathsf{Preord}}$-categories of coalgebras.

$\textstyle{\mathsf{Coalg}(\widehat{T})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{\mathsf{d}}_{*}}$$\scriptstyle{\bot}$$\scriptstyle{\widetilde{\mathsf{v}}_{*}}$$\textstyle{\mathsf{Coalg}(\overline{T})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}_{*}}$$\scriptstyle{\bot}$$\scriptstyle{\mathsf{v}_{*}}$$\scriptstyle{\widehat{T}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}}$

######  Proposition 47.

Assume that ${\mathscr{V}}$ is a non-trivial integral commutative quantale
without zero divisors. Let again
$\widehat{T}:{\mathsf{Preord}}\longrightarrow{\mathsf{Preord}}$ be a locally
monotone functor, but this time consider
$\overline{T}:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ be an extension of $\widehat{T}$ to
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ (meaning that $\overline{T}$
is a ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-functor, such that
$\overline{T}\mathsf{d}_{*}\cong\widehat{T}\mathsf{d}_{*}$ holds). Then the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-adjunction
$\mathsf{c}_{*}\dashv\mathsf{d}_{*}$ lifts to a ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-adjunction
$\widetilde{\mathsf{c}}_{*}\dashv\widetilde{\mathsf{d}}_{*}$ between the
associated ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-categories of
coalgebras.

$\textstyle{\mathsf{Coalg}(\widehat{T})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{\mathsf{d}}_{*}}$$\scriptstyle{\bot}$$\scriptstyle{\widetilde{\mathsf{c}}_{*}}$$\textstyle{\mathsf{Coalg}(\overline{T})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}_{*}}$$\scriptstyle{\bot}$$\scriptstyle{\mathsf{c}_{*}}$$\scriptstyle{\widehat{T}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}}$

We return now to the discrete functor
$D^{\mathscr{V}}:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$. It is easy to see that it decomposes as
$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}_{*}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}}$. Additionally, recall the following (see also Example
3.1(2)):

  1. (1)

There are locally monotone functors
$D:{\mathsf{Set}}\longrightarrow{\mathsf{Preord}}$,
$C:{\mathsf{Preord}}\longrightarrow{\mathsf{Set}}$, where $D$ maps a set to
its discrete preorder and $C$ maps a preorder to its set of connected
components.

  2. (2)

There is a chain $C_{o}\dashv D_{o}\dashv
V:{\mathsf{Preord}}\longrightarrow{\mathsf{Set}}$ of ordinary adjunctions
where $V$ is the underlying-set forgetful functor.

  3. (3)

The locally monotone adjunction $C\dashv D$ is ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-enriched.

The next two propositions from [7] are similar to the two above, but connect
${\mathsf{Set}}$ with ${\mathsf{Preord}}$ instead of ${\mathsf{Preord}}$ with
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$.

######  Proposition 48.

Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ and
$\widehat{T}:{\mathsf{Preord}}\longrightarrow{\mathsf{Preord}}$ an extension
of $T$ (a locally monotone functor such that $DT\cong\widehat{T}D$). Then the
locally monotone adjunction $C\dashv D$ lifts to a locally monotone adjunction
$\widetilde{C}\dashv\widetilde{D}$ between the associated categories of
coalgebras:

$\textstyle{\mathsf{Coalg}(T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{D}}$$\scriptstyle{\bot}$$\scriptstyle{\widetilde{C}}$$\textstyle{\mathsf{Coalg}(\widehat{T})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$$\scriptstyle{\bot}$$\scriptstyle{C}$$\scriptstyle{T}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widehat{T}}$

Consequently, $\widetilde{D}$ will preserve limits, in particular, the final
coalgebra (if it exists).

######  Proposition 49.

Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ and
$\widehat{T}:{\mathsf{Preord}}\longrightarrow{\mathsf{Preord}}$ a lifting of
$T$ (an ordinary functor such that $TV\cong V\widehat{T}$). Then the ordinary
adjunction $D_{o}\dashv V$ lifts to an ordinary adjunction
$\widetilde{D}_{o}\dashv\widetilde{V}$ between the associated categories of
coalgebras.

$\textstyle{\mathsf{Coalg}(T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{D}_{o}}$$\scriptstyle{\bot}$$\scriptstyle{\widetilde{V}}$$\textstyle{\mathsf{Coalg}(\widehat{T})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D_{o}}$$\scriptstyle{\bot}$$\scriptstyle{V}$$\scriptstyle{T}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widehat{T}}$

Consequently, $\widetilde{V}$ will preserve ordinary limits; in particular,
the underlying set of a final $\widehat{T}$-coalgebra will be a final
$T$-coalgebra.

Let now $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ and denote by
$T_{\mathbb{2}}$ is ${\mathbb{2}}\mbox{-}\mathsf{cat}$-ification, that is, its
${\mathsf{Preord}}$-ification [8]. We plan to see how $T_{\mathbb{2}}$ and
$T_{\mathscr{V}}$, the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of $T$, are related. We start by the following
observation:

######  Proposition 50.

The embedding
$\mathsf{d}_{\ast}:{\mathsf{Preord}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ is dense.

######  Proof 4.4.

We have shown in Theorem 22 that $D^{\mathscr{V}}=\mathsf{d}_{*}D$ is
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-dense. Using that
$\mathsf{d}_{\ast}$ is fully faithful, it follows from [40, Theorem 5.13] that
both $D$ and $\mathsf{d}_{*}$ are ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-dense and that
$\mathsf{d}_{*}=\mathsf{Lan}_{D}(D^{\mathscr{V}})$ holds.

######  Remark 51.

Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be a set-functor and
$T_{\mathbb{2}}$ its ${\mathsf{Preord}}$-ification as above. Then the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification $T_{\mathscr{V}}$
of $T$ can be computed in two stages, as follows:

$\displaystyle T_{\mathscr{V}}\ $ $\displaystyle=$
$\displaystyle\mathsf{Lan}_{D^{\mathscr{V}}}(D^{\mathscr{V}}T)$
$\displaystyle=$
$\displaystyle\mathsf{Lan}_{(\mathsf{d}_{*}D)}(\mathsf{d}_{*}DT)=\mathsf{Lan}_{\mathsf{d}_{*}}(\mathsf{Lan}_{D}(\mathsf{d}_{*}DT))$
(by [40, Theorem 4.47], because $\mathsf{d}_{\ast}$ is fully faithful)
$\displaystyle\cong$
$\displaystyle\mathsf{Lan}_{\mathsf{d}_{*}}(\mathsf{Lan}_{D}(\mathsf{d}_{*}T_{\mathbb{2}}D))$
(because $DT\cong T_{\mathbb{2}}D$) $\displaystyle\cong$
$\displaystyle\mathsf{Lan}_{\mathsf{d}_{*}}(\mathsf{d}_{*}T_{\mathbb{2}})$

where the last isomorphism holds because
$\mathsf{Lan}_{D}(\mathsf{d}_{*}T_{\mathbb{2}}D)\cong\mathsf{d}_{*}T_{\mathbb{2}}$.
To verify the latter isomorphism, notice first that the
${\mathsf{Preord}}$-enriched left Kan extension
$\mathsf{Lan}_{D}(\mathsf{d}_{*}T_{\mathbb{2}}D)$ is also the
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-enriched left Kan extension
of $\mathsf{d}_{*}T_{\mathbb{2}}D$ along $D$, by a change-of-base argument as
in [66, Theorem 1.7.1]. Next, apply [40, Theorem 5.29] to the composite
${\mathsf{Preord}}$-functor $\mathsf{d}_{*}T_{\mathbb{2}}$, using the density
presentation of $D$ exhibited in [8] and the fact that $\mathsf{d}_{*}$ is
${\mathsf{Preord}}$-left adjoint.

The remark above says that the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification of an endofunctor $T$ of ${\mathsf{Set}}$ can
be obtained by taking first the ${\mathsf{Preord}}$-ification
$T_{\mathbb{2}}:{\mathsf{Preord}}\longrightarrow{\mathsf{Preord}}$ and then
the left Kan extension of $\mathsf{d}_{\ast}T_{\mathbb{2}}$ along
$\mathsf{d}_{*}$, as in

$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T_{\mathscr{V}}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T_{\mathbb{2}}}$$\scriptstyle{\mathsf{d}_{\ast}}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}_{\ast}}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T}$$\scriptstyle{D}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$

Putting things together we now obtain

######  Theorem 52.

Let ${\mathscr{V}}$ be a non-trivial integral commutative quantale without
zero divisors, and $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ an
arbitrary endofunctor, with ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-ification $T_{\mathscr{V}}:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$. Then the ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-adjunctions $C\dashv
D:{\mathsf{Set}}\longrightarrow{\mathsf{Preord}}$,
$\mathsf{c}_{*}\dashv\mathsf{d}_{*}:{\mathsf{Preord}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ lift to ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-adjunctions between the associated
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-categories of coalgebras:

$\textstyle{\mathsf{Coalg}(T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{D}}$$\scriptstyle{\bot}$$\scriptstyle{\widetilde{C}}$$\textstyle{\mathsf{Coalg}(T_{\mathbb{2}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{\mathsf{d}}_{*}}$$\scriptstyle{\bot}$$\scriptstyle{\widetilde{\mathsf{c}}_{*}}$$\textstyle{\mathsf{Coalg}(T_{\mathscr{V}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$$\scriptstyle{\bot}$$\scriptstyle{C}$$\scriptstyle{T}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{d}_{*}}$$\scriptstyle{\bot}$$\scriptstyle{\mathsf{c}_{*}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T_{\mathscr{V}}}$

Since the ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-ification
$T_{\mathscr{V}}$ of an endofunctor $T$ on ${\mathsf{Set}}$ is supposed to be
“$T$ in the world of ${\mathscr{V}}$-categories”, the theorem above confirms
the expectation that final $T_{\mathscr{V}}$-coalgebras have a discrete
metric. In fact, we can say that the final $T$-coalgebra is the final
$T_{\mathscr{V}}$-coalgebra, if we consider $\mathsf{Coalg}(T)$ as a full
(enriched-reflective) subcategory of $\mathsf{Coalg}(T_{\mathscr{V}})$.

The next theorem deals with a more general situation where the final metric-
coalgebra is the final set-coalgebra with an additional metric. This includes
in particular the case where $\overline{T}$ is $H^{\sharp}$ for some
$H:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ with $V^{\mathscr{V}}H_{o}=T_{o}$.

######  Theorem 53.

Let ${\mathscr{V}}$ be a commutative quantale,
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be an arbitrary endofunctor,
$\widehat{T}:{\mathsf{Preord}}\longrightarrow{\mathsf{Preord}}$ a lifting of
$T$ to ${\mathsf{Preord}}$, and $\overline{T}:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ be a lifting of $\widehat{T}$ to
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$. Then the ordinary
adjunction $D_{o}\dashv V:{\mathsf{Preord}}\longrightarrow{\mathsf{Set}}$ and
the ${\mathsf{Preord}}$-adjunction
$\mathsf{d}_{*}\dashv\mathsf{v}_{*}:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathsf{Preord}}$ lift to adjunctions
between the associated ${\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$-categories of coalgebras

$\textstyle{\mathsf{Coalg}(T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{V}}$$\scriptstyle{\bot}$$\scriptstyle{\widetilde{D}_{o}}$$\textstyle{\mathsf{Coalg}(\widehat{T})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{\mathsf{v}}_{*}}$$\scriptstyle{\bot}$$\scriptstyle{\widetilde{\mathsf{d}}_{*}}$$\textstyle{\mathsf{Coalg}(\overline{T})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{V}$$\scriptstyle{\bot}$$\scriptstyle{D_{o}}$$\scriptstyle{T}$$\textstyle{{\mathsf{Preord}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{v}_{*}}$$\scriptstyle{\bot}$$\scriptstyle{\mathsf{d}_{*}}$$\textstyle{{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}}$

It follows that $\overline{T}$ and $T$ induce the same notion of behavioural
equivalence (bisimilarity). Nevertheless, the final $\overline{T}$-coalgebra
can provide additional information about order and metric of non-bisimilar
elements.

Recall from Example 3.7(2) the functor $TX=X^{A}\times B$ and its lifting
$H^{\sharp}{\mathscr{X}}={\mathscr{X}}^{A}\otimes{\mathscr{B}}$. Assume that
the quantale is integral. Then the final $H^{\sharp}$-coalgebra is the power
${\mathscr{V}}$-category ${\mathscr{B}}^{A^{*}}$ having as objects all
functions mapping each finite sequence of inputs to the last observable output
in ${\mathscr{B}}$, with ${\mathscr{V}}$-distances

${\mathscr{B}}^{A^{*}}(h,k)=\bigwedge_{\mathsf{l}\in
A^{*}}{\mathscr{B}}(h(\mathsf{l}),k(\mathsf{l}))$

for each pair of behaviour functions $h,k:A^{*}\longrightarrow B$.

In particular, for the lifting $H^{\sharp}$ of the stream functor from Example
3.7(2a) we obtain the final $H^{\sharp}$-coalgebra as the
${\mathscr{V}}$-category ${\mathscr{B}}^{\mathbb{N}}$ of streams over $B$. The
lifting $H^{\sharp}$ of the deterministic automata functor from Example
3.7(2b) given by
$H^{\sharp}{\mathscr{X}}={\mathscr{X}}^{A}\otimes{\mathbb{2}}_{r,s}$ has now
as final coalgebra the “generalised metric space” ${\mathbb{2}}_{r,s}^{A^{*}}$
of languages over the alphabet $A$.

##  5\. Conclusion

This paper is part of a larger endeavour extending set-based coalgebra to
${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$-based coalgebra, see for
example [65, 43, 14, 8, 45, 6, 20]. Here, we showed that every functor
$H:{\mathsf{Set}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$ has a left-Kan extension
$H^{\sharp}:{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}\longrightarrow{\mathscr{V}}\mbox{-}\hskip
0.9pt{\mathsf{cat}}$, and that the final $H^{\sharp}$-coalgebra is the
corresponding final coalgebra over ${\mathsf{Set}}$ equipped with a
${\mathscr{V}}$-metric.

There are several directions in which to expand our results. For example, it
would be interesting to move from commutative to general quantales and to
quantaloids [53, 62]. There is also the question whether one can extend not
only functors but also monads in a uniform way, which could be related to
(metric) trace (bi)simulation as in [10].

Coalgebraically, it would be interesting to further develop the topic, barely
touched upon in the last section, of behavioural pseudo-metrics [31, 21, 55,
70], while on the logical side, we aim to combine this paper with [45, 6] in
the pursuit of an equational approach to quantitative reasoning about
coalgebras/transition systems, an objective related to recent work on
quantitative algebraic reasoning [49].

## Acknowledgements

We thank the anonymous referees of CALCO and LMCS for their valuable comments
and patience that allowed us to improve the presentation of our results.

## References

  * [1] S. Abramsky and A. Jung.  Domain theory.  In: S. Abramsky et al (eds.), Handbook of Logic in Computer Science. Vol. 3. Semantic Structures. pp. 1–168, Oxford University Press (1994)
  * [2] P. Aczel.  Non-well-founded sets.  CSLI Lecture Notes 14. Stanford University, Center for the Study of Language and Information, Stanford, CA (1988)
  * [3] A. Akhvlediani, M. M. Clementino and W. Tholen.  On the categorical meaning of the Hausdorff and Gromov distances I.  Topology and its Applic. 157(8):1275–1295 (2010)
  * [4] J. Adámek, S. Milius, L. S. Moss and H. Urbat.  On finitary functors and their presentations.  J. Comput. Syst. Sci. 81(5):813–833 (2015)
  * [5] P. America and J. Rutten.  Solving reflexive domain equations in a category of complete metric spaces.  J. Comput. Syst. Sci. 39(3):343–375 (1989)
  * [6] O. Băbuş and A. Kurz.  On the Logic of Generalised Metric Spaces.  In: I. Hasuo (ed.) CMCS 2016.  Lect. Notes Comput. Sci. 9608, pp. 136–155,  Springer (2016)
  * [7] A. Balan and A. Kurz.  Finitary functors: from ${\mathsf{Set}}$ to ${\mathsf{Preord}}$ and $\mathsf{Poset}$.  In: A. Corradini et al (eds.), CALCO 2011.  Lect. Notes Comput. Sci. 6859, pp. 85–99,  Springer (2011)
  * [8] A. Balan, A. Kurz and J. Velebil.  Positive fragments of coalgebraic logics,  Log. Methods Comput. Sci. 11(3:18):1–51 (2015)
  * [9] A. Balan, A. Kurz and J. Velebil.  Extensions of functors from ${\mathsf{Set}}$ to ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$.  In: L. S. Moss and P. Sobocinski (eds.), CALCO 2015.  LIPIcs 35:17–34 (2015)
  * [10] P. Baldan, F. Bonchi, H. Kerstan and B. König.  Coalgebraic behavioral metrics.  Log. Methods Comput. Sci. 14(3:20):1–61 (2018)
  * [11] J. de Bakker and E. de Vink.  _Control Flow Semantics._ MIT Press (1996)
  * [12] M. Barr.  Relational algebras.  In: H. Applegate et al (eds.), Reports of the Midwest Category Seminar IV,  Lect. Notes Math. 137, pp. 39–55, Springer (1970)
  * [13] R. Betti.  Automi e categorie chiuse.  Boll. Un. Mat. Ital. Ser. V B 17(1):44–58 (1980)
  * [14] M. Bílková, A. Kurz, D. Petrişan and J. Velebil.  Relation lifting, with an application to the many-valued cover modality.  Log. Methods Comput. Sci. 9(4:8):1–48 (2013)
  * [15] G. J. Bird.  Limits in 2-categories of locally presentable categories.  PhD thesis, University of Sydney (1984)
  * [16] A. Carboni, G. M. Kelly and R. J. Wood,  A 2-categorical approach to change of base and geometric morphisms I,  Cah. Topol. Géom. Différ. Catég. XXXII(1):47–95 (1991)
  * [17] R. Casley.  On the specification of concurrent systems.  PhD thesis, Stanford University (1991)
  * [18] R. Casley, R. F. Crew, J. Meseguer and V. R. Pratt.  Temporal Structures.  Math. Struct. Comput. Sci. 1(2):179–213 (1991)
  * [19] J. R. B. Cockett and D. Spencer.  Strong categorical datatypes I.  In: R. A. G. Seely (ed.), Category theory 1991,  Canad. Math. Soc. Proc., pp. 141–169, Amer. Math. Soc. (1992)
  * [20] F. Dahlqvist and A. Kurz.  The Positivication of Coalgebraic Logics.  In: F. Bonchi and B. König (eds.). CALCO 2017.  LIPIcs 72(9):1–15 (2017)
  * [21] J. Desharnais, V. Gupta, R. Jagadeesan and P. Panangaden.  Metrics for labeled Markov systems.  In: J. C. M. Baeten and S. Mauw (eds.) CONCUR 1999 Lect. Notes Comput. Sci. 1664, pp.258–273, Springer (1999)
  * [22] M. M. Deza and E. Deza.  Encyclopedia of Distances (4th ed.),  Springer (2016)
  * [23] E. Dubuc.  Kan extensions in enriched category theory. Lect. Notes Mathem. 145, Springer (1970)
  * [24] S. Eilenberg and G. M. Kelly.  Closed categories.  In: S. Eilenberg et al (eds.), Proceedings of the Conference on Categorical Algebra, pp. 421–562,  Springer (1966)
  * [25] B. Fawcett and R. J. Wood.  Constructive complete distributivity I.  Math. Proc. Camb. Phil. Soc. 107:81–89 (1990)
  * [26] B. Flagg and R. Kopperman.  Continuity spaces: reconciling domains and metric spaces.  Theoret. Comput. Sci. 177(1):111-138 (1997)
  * [27] P. Fletcher and W. Lindgren.  Quasi-uniform spaces.  Lect. Notes Pure Appl. Math.,  Marcel Dekker (1982)
  * [28] P. Freyd and A. Scedrov.  Categories, Allegories.  North Holland (1990)
  * [29] H. Gaifman and V. Pratt. Partial order models of concurrency and the computation of functions. In: LICS 1987, pp. 72–85 IEEE Computer Society Press, Ithaca, NY (1987)
  * [30] H. Gaifman.  Modeling concurrency by partial orders and nonlinear transition systems.  In: REX Workshop,  pp. 467–488 (1988)
  * [31] A. Giacalone, C. Jou and S. Smolka.  Algebraic reasoning for probabilistic concurrent systems.  In: Proc. IFIP TC2 Working Conference on Programming Concepts and Methods.  pp.443–458, North-Holland (1990)
  * [32] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove and D. S. Scott.  Continuous lattices and domains.  Cambridge Univ. Press (2003)
  * [33] R. Hasegawa.  Two applications of analytic functors.  Theoret. Comput. Sci. 272(1-2):113–175 (2002)
  * [34] F. Hausdorff.  _Mengenlehre_.  (3rd ed.), de Gruyter (1935)
  * [35] C. Hermida and B. Jacobs.  Structural induction and coinduction in a fibrational setting.  Inf. Comput. 145(2):107–152 (1998)
  * [36] D. Hofmann and C. D. Reis.  Probabilistic metric spaces as enriched categories.  Fuzzy Sets and Systems 210:1–21 (2013)
  * [37] D. Hofmann, G. J. Seal and W. Tholen (eds.).  Monoidal Topology: A Categorical Approach to Order, Metric and Topology.  Encycl. Math. Appl., Cambridge Univ. Press (2014)
  * [38] J. Hughes and B. Jacobs.  Simulations in coalgebra.  Theor. Comput. Sci. 327(1-2):71–108 (2004)
  * [39] G. M. Kelly.  Doctrinal adjunction.  In: G. M. Kelly (ed.), Category Seminar,  Lect. Notes Math. 420, pp. 257–280. Springer (1974)
  * [40] G. M. Kelly.  Basic concepts of enriched category theory.  London Math. Soc. Lect. Notes Series 64, Cambridge Univ. Press (1982),  also available as Repr. Theory Appl. Categ. 10 (2005)
  * [41] G. M. Kelly and S. Lack.  ${\mathscr{V}}\mbox{-}\hskip 0.9pt{\mathsf{cat}}$ is locally presentable or bounded if ${\mathscr{V}}$ is so.  Theory Appl. Categ. 8(23):555–575 (2001)
  * [42] G. M. Kelly and R. Street.  Review of the elements of 2-categories  In: G. M. Kelly (ed.), Category Seminar,  Lect. Notes Mathem. 420, pp. 75–103,  Springer, Berlin, Heidelberg (1974)
  * [43] A. Kurz and J. Velebil.  Enriched Logical Connections.  Appl. Categ. Structures 21(4):349–377 (2013)
  * [44] A. Kurz and J. Velebil.  Relation lifting, a survey.  J. Log. Alg. Methods Program. 85(4):475–499 (2016)
  * [45] A. Kurz and J. Velebil.  Quasivarieties and varieties of ordered algebras: regularity and exactness.  Math. Struct. Comp. Sci. 27(7): 1153-1194 (2017)
  * [46] K. Kuratowski.  Topology. Vol I. New York-London, Academic Press (1966)
  * [47] F. W. Lawvere.  Metric spaces, generalised logic, and closed categories.  Rend. Sem. Mat. Fis. Milano,  XLIII:135–166 (1973), also available as Repr. Theory Appl. Categ. 1:1–37 (2002)
  * [48] M. Lenisa, J. Power and H. Watanabe.  Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads.  Electr. Notes Theor. Comput. Sci. 33:230–260 (2000)
  * [49] R. Mardare, P. Panangaden and G. D. Plotkin.  Quantitative algebraic reasoning.  In: LICS 2016,  pp. 700-709, ACM (2016)
  * [50] D. Pompeiu.  Sur la continuité des fonctions des variables complexes.  Ann. Fac. Sci. Toulouse 2(7):265–315 (1905),  also available at Numdam.
  * [51] G. N. Raney.  Completely distributive complete lattices.  Proc. Amer. Math. Soc. 3:677–680 (1952)
  * [52] K. I. Rosenthal.  Quantaloids, Enriched Categories and Automata Theory.  Appl. Categ. Structures 3:279–301 (1995)
  * [53] K. I. Rosenthal.  The theory of quantaloids.  Pitman Res. Notes Math. Series 348, Addison Wesley (1996)
  * [54] J. J. M. M. Rutten.  Elements of generalised ultrametric domain theory.  Theoret. Comput. Sci. 170:349–381 (1996)
  * [55] J. J. M. M. Rutten.  Relators and metric bisimulations (extended abstract).  In: B. Jacobs et al (eds.), CMCS 1998, Electr. Notes Theor. Comput. Sci. 11:1–7 (1998)
  * [56] J. J. M. M. Rutten.  Universal coalgebra: a theory of systems.  Theoret. Comput. Sci.,  249:3–80 (2000)
  * [57] D. Scott.  Continuous lattices.  In F. W. Lawvere (ed.), Toposes, Algebraic Geometry and Logic,  Lect. Notes Math. 274, pp. 97–136, Springer (1971)
  * [58] M. B. Smyth and G. D. Plotkin.  The category-theoretic solution of recursive domain equations.  SIAM J. Comput. 11(4):761–783 (1982)
  * [59] M. B. Smyth.  Topology.  In: S. Abramsky et al (eds.), Handbook of Logic in Computer Science. Vol. 1. Background: Mathematical Structures.  Oxford University Press (1992)
  * [60] R. Street.  The formal theory of monads.  J. Pure Appl. Algebra 2:149–168 (1972)
  * [61] I. Stubbe.  “Hausdorff distance” via conical cocompletion.  Cah. Top. Gèom. Diff. Categ. 51(1):51–76 (2010)
  * [62] I. Stubbe.  An introduction to quantaloid-enriched categories.  Fuzzy Sets Syst. 256:95–116 (2014)
  * [63] V. Trnková.  Relational automata in a category and their languages.  In: M. Karpinski (ed.), Fundamentals of Computation Theory,  Lect. Notes Comput. Sci. 56, pp. 340–355,  Springer (1977)
  * [64] D. Turi and J. Rutten.  On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces.  Math. Struct. Comp. Sci. 8:481–540 (1998)
  * [65] J. Velebil and A. Kurz.  Equational presentations of functors and monads.  Math. Struct. Comp. Sci. 21(2):363–381 (2011)
  * [66] D. Verity.  Enriched categories, internal categories and change of base.  PhD thesis, Cambridge University (1992), also available as TAC Reprints (2011)
  * [67] C. Villani.  Optimal transport: old and new,  Springer (2009)
  * [68] K. R. Wagner.  Solving Recursive Domain Equations with Enriched Categories.  PhD thesis, Carnegie Mellon University (1994)
  * [69] H. Wolff.  $V$-cat AND $V$-graph.  J. Pure Appl. Algebra 4(2):123–135 (1974)
  * [70] J. Worrell.  Coinduction for recursive data types: partial order, metric spaces and $\Omega$-categories.  In: H. Reichel (ed.), CMCS 2000, Electr. Notes Theor. Comput. Sci. 33:337–356 (2000)
  * [71] J. Worrell.  On coalgebras and final semantics.  PhD thesis, University of Oxford (2000)