Kantorovich Functors and Characteristic Logics for Behavioural Distances

Sergey Goncharov10000-0001-6924-8766Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 501369690, Dirk Hofmann 20000-0002-1082-6135Funded by The Center for Research and Development in Mathematics and Applications (CIDMA) through the Portuguese Foundation for Science and Technology (FCT) – project numbers UIDB/04106/2020 and UIDP/04106/2020, Pedro Nora 10000-0001-8581-0675Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 259234802, Lutz Schröder 10000-0002-3146-5906Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 434050016 and Paul Wild 10000-0001-9796-9675

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany Center for Research and Development in Mathematics and Applications, University of Aveiro, Portugal

S. Goncharov et al.

Behavioural distances measure the deviation between states in
quantitative systems, such as probabilistic or weighted systems.
There is growing interest in generic approaches to behavioural
distances.  In particular, coalgebraic methods capture variations in
the system type (nondeterministic, probabilistic, game-based etc.),
and the notion of quantale abstracts over the actual values
distances take, thus covering, e.g., two-valued equivalences,
(pseudo)metrics, and probabilistic (pseudo)metrics.  Coalgebraic
behavioural distances have been based either on liftings of
\(\SET\)-functors to categories of metric spaces, or on lax
extensions of \(\SET\)-functors to categories of quantitative
relations. Every lax extension induces a functor lifting but not
every lifting comes from a lax extension.

It was shown recently that every lax extension is Kantorovich, i.e. induced by a
suitable choice of monotone predicate liftings, implying via a
quantitative coalgebraic Hennessy-Milner theorem that behavioural
distances induced by lax extensions can be characterized by
quantitative modal logics. Here, we essentially show
the same in the more general setting of behavioural distances
induced by functor liftings. In particular, we show that every
functor lifting, and indeed every functor on (quantale-valued)
metric spaces, that preserves isometries
is Kantorovich, so that the induced behavioural distance (on systems
of suitably restricted branching degree) can be characterized by a
quantitative modal logic.

§ INTRODUCTION

Qualitative transition systems, such as standard labelled transition
systems, are typically compared under two-valued notions of
behavioural equivalence, such as Park-Milner bisimilarity. For
quantitative systems, such as probabilistic, weighted, or metric
transition systems, notions of behavioural distance allow for a
more fine-grained comparison, in particular give a numerical measure
of the deviation between inequivalent states, instead of just flagging
them as inequivalent [14, 6, 2, 26].

The variation found in the mentioned system types calls for unifying
methods, and correspondingly has given rise to generic notions of
behavioural distance based on universal
coalgebra [35], a framework for state-based systems in
which the transition type of systems is encapsulated as an
(endo-)functor on a suitable base category.  Coalgebraic behavioural
distances have been defined on the one hand using liftings of
given set functors to the category of metric spaces [5], and
on the other hand using lax extensions, i.e. extensions of set
functors to categories of quantitative
relations [13, 40]. Since every lax extension induces a
functor lifting in a straightforward way [40] but on the other
hand not every functor lifting is induced by a lax extension, the
approach via liftings is more widely applicable. On the other hand, it
has been shown that every lax extension is Kantorovich, i.e.induced by a suitable choice of modalities, modelled as predicate
liftings in the spirit of coalgebraic logic [30, 36]. Using
quantitative coalgebraic Hennessy-Milner theorems, it follows
that under expected conditions on the functor and the lax extension,
behavioural distance coincides with logical distance.

Roughly speaking, our main contribution in the present paper is to
show that the same holds for functor liftings and their induced
behavioural distances. In more detail, we have the following (cf. Figure <ref> for a graphical summary):

* Every lifting of a set functor is topological,
i.e. induced by a generalized form of predicate liftings in which
one may need to switch to non-standard spaces of truth values for
the predicates involved (<ref>).

* Functor liftings that preserve  isometries are Kantorovich, i.e. induced by (possibly
polyadic) predicate liftings. (Here, we understand predicate
liftings as involving only the standard space of truth values –
that is, the unit interval, in the case of $1$-bounded metric
spaces). In fact, preservation of isometries is also
necessary (<ref>).

* Lastly, we detach the technical development from set functors,
and show that a functor on (pseudo)metric spaces is
Kantorovich, in the sense that the distance of its elements
can be characterized by predicate liftings, iff it preserves isometries (<ref>).

By a recent coalgebraic quantitative Hennessy-Milner theorem that fits
this level of generality [12], it follows that given a
functor $\ftF$ on (pseudo<)metric spaces that preserves isometries, acts non-expansively on morphisms, and admits a dense
finitary subfunctor, behavioural distance can be characterized by
quantitative modal logic (<ref>). In additional
results, we further clarify the relationship between functor liftings
and lax extensions, and in particular characterize the functor
liftings that are induced by lax extensions (<ref>).

Indeed, we conduct the main technical development not only in
coalgebraic generality, but also parametric in a
quantale, hence abstracting both over distances and over truth
values. One benefit of this generality is that our results cover the
two-valued case, captured by the two-element quantale. In particular,
one instance of our results is the fact that every finitary set
functor has a separating set of finitary predicate liftings, and hence
admits a modal logic having the Hennessy-Milner
property [36]. Moreover, we do
not restrict to symmetric distances, and hence cover also simulation
preorders and simulation distances [26].

\[
\begin{tikzcd}[cells={nodes={draw=gray}},column sep=20ex, row sep=6ex,style={every label/.append style={scale=.9},cells={nodes={scale=.9}}}]
\parbox[][5ex][c]{2.5cm}{\centering monotone\\ predicate liftings}
\ar[r,hook]
\dar["\text{[40], \autoref{p:62}}"',xshift=-3ex] &
\parbox[][5ex][c]{2.5cm}{\centering predicate liftings}
\dar[xshift=-3ex,"\text{[5], \autoref{p:51}}"']\\
\parbox[][5ex][c]{2.5cm}{\centering lax extensions\\{}}
\rar[yshift=-1ex,hook, "\text{\autoref{p:61}}"']
\uar["\text{[40]}"',xshift=3ex] &
\parbox[][5ex][c]{2.5cm}{\centering functor liftings\\{}}
\lar[yshift=1ex, "\text{\autoref{p:19}}"']
\uar[xshift=3ex,"\parbox{5em}{\tiny\autoref{p:53},\\ \autoref{p:54}}"']
\end{tikzcd}
\]

Summary of connections (a rigorous categorical interpretation of these
connections involves a square of adjunctions (<ref>)).

*Related Work Quantale-valued quantitative notions of
bisimulation for functors that already live on generalized metric
spaces (rather than being lifted from functors on sets) have been
considered early on [42]. We have already mentioned previous
work on coalgebraic behavioural metrics, for functors originally
living on sets, via metric liftings [5] and via lax
extensions [13, 40].
Existing work that combines coalgebraic and quantalic generality and
accommodates asymmetric distances, like the present work, has so far
concentrated on establishing so-called van Benthem theorems, concerned
with characterizing (coalgebraic) quantitative modal logics by
bisimulation invariance [41]. There is a line of work on
Kantorovich-type coinductive predicates at the level of generality of
topological categories [22, 23] (phrased in fibrational
terminology), with results including a game characterization and
expressive logics for coinductive predicates already assumed to be
Kantorovich in a general sense, i.e. induced by variants of predicate
liftings. In this work, the condition of preserving isometries
already shows up as fiberedness, and indeed  the
condition already appears in work on metric liftings [5]. As
mentioned in the above discussion, we complement existing work on
quantitative coalgebraic Hennessy-Milner
theorems [24, 40, 12] by establishing the Kantorovich
property they assume.

§ PRELIMINARIES

We will need a fair amount of material on coalgebra, quantales and
quantale-enriched categories (generalizing metric spaces), predicate
liftings, and lax extension, which we recall in the sequel. New
material starts in Section <ref>.

§.§ Categories and Coalgebras

We assume basic familiarity with category theory [1, 4].
More specifically, we make extensive use of topological categories [1] and quantale-enriched categories [28, 21, 38].
Recall that a coalgebra for a functor \(\ftF \colon \catC \to \catC\)
consists of an object \(X\) of \(\catC\), thought of as an object of
states, and a morphism $\alpha \colon X \rightarrow \ftF X$, thought of
as assigning structured collections (sets, distributions, etc.) of successors to
states. A coalgebra morphism from \((X, \alpha)\) to \((Y, \beta)\) is a
morphism $f \in \catC(X, Y)$ such that \(\beta \cdot f = \ftF f \cdot \alpha\).
We will focus on concrete categories over \(\SET\), that is categories that
come equipped with a faithful functor $\ftII{-}\colon \catC \rightarrow \SET$,
which allows speaking about individual states as elements of $\ftII{X}$.
A lifting of an endofunctor $\ftF\colon\SET\to\SET$ to $\catC$ is an endofunctor
$\overline{\ftF}\colon\catC\to\catC$ such that $\ftII{-}\cdot\overline\ftF =
\ftF\cdot\ftII{-}$.

Some functors of interest for coalgebraic modelling are as follows.

* The finite powerset functor \(\ftP_\omega \colon \SET \to \SET\) maps each set to its finite powerset, and for a map $g$, $\ftP_\omega(g)$ takes direct images under $g$.
Given a set \(A\) (of labels), coalgebras for the the functor \(\ftP_\omega(A \times -)\)
are finitely branching $A$-labelled transition systems.

*  The finite distribution functor \(\ftD_\omega \colon \SET \to \SET\) maps a set $X$
to the set $\ftD_\omega X$ of finitely supported probability distributions on $X$.
Given a finite set \(A\), coalgebras for the functor \((1 + \ftD_\omega)^A\), are probabilistic transition 		systems [27, 10].

Finitary functors are those which are determined by their action on finite sets.
More precisely, a functor is finitary if for every set \(X\) and
every \(\fx \in \ftF X\), there is a finite subset inclusion \(m \colon A \to X\) such
that \(\fx\) is in the image of \(\ftF m\).

Standard examples of non-finitary functors are as follows.

* The (unbounded) powerset functor \(\ftP \colon \SET \to \SET\).

* The neighbourhood functor \(\ftN \colon \SET \to \SET\) sends a set \(X\) to the set \(\ftP\ftP
X\), and a function \(f \colon X \to Y\) to the function \(\ftN f \colon
\ftN X \to \ftN Y\) that assigns to every element \(\fx \in \ftN X\) the set
\(\{B \subseteq Y \mid f^{-1} B \in \fx \}\).

§.§ Quantales and Quantale-Enriched Categories

A central notion of our development is that of a quantale, which will
serve as a parameter determining the range of truth values and
distances.  A quantale \((\V,\otimes,k)\), more precisely a
commutative and unital quantale, is a complete lattice $\V$ – with
joins and meets denoted by $\bigvee$ and $\bigwedge$, respectively –
that carries the structure of a commutative monoid with
tensor $\otimes$ and unit $k$, such that for every
$u \in \V$, the map $u \otimes - \colon \V\to \V$ preserves suprema.
This entails that every $u \otimes - $ has a right
adjoint $\hom(u,-) \colon \V \to \V$, characterized by the property
\( u \otimes v \le w \iff v \le \hom(u,w).  \) We denote by $\top$ and
$\bot$ the greatest and the least element of a quantale, respectively.
A quantale is non-trivial if $\bot\neq\top$, and integral if
\(\top = k\).

*  Every frame (i.e. a complete lattice in which binary meets distribute over
infinite joins) is a quantale with \(\otimes = \wedge\) and \(k = \top\).
In particular, every finite distributive lattice is a quantale, prominently \(\two\), the two-element lattice $\{\bot,\top\}$ and \(\one\), the trivial quantale.

* Every left continuous \(t\)-norm [3] defines a quantale on the unit interval equipped with its natural order.

*  The previous clause (up to isomorphism) further specializes as follows:

* The quantale \([0,\infty]_+ = ([0,\infty], \inf, +, 0)\) of non-negative real numbers with infinity, ordered by the greater or equal relation, and with tensor given by addition.

* The quantale \([0,\infty]_{\max} = ([0,\infty], \inf, \max, 0)\) of non-negative real numbers with infinity, ordered by the greater or equal relation, and with tensor given by maximum.

*  The quantale \([0,1]_\oplus = ([0,1], \inf, \oplus, 0)\) of the unit interval, ordered by the greater or equal order, and with tensor given by truncated addition.

(Note that the quantalic order here is dual to the standard numeric order).

* Every commutative monoid \((M, \cdot, e)\) generates a quantale on \(\ftP M\)
(the free quantale over \(M\)) w.r.t. set inclusion and with the tensor
\(
A \otimes B = \{ a \cdot b \mid a \in A \text{ and } b \in B\},
\)
for all \(A,B \subseteq M\).
The unit of this multiplication is the set \(\{e\}\).

A \(\V\)-category
is pair \((X,a)\) consisting of a set $X$ and a map
$a \colon X \times X \to \V$ such that \(k \le a(x,x)\) and
\(a(x,y) \otimes a(y,z) \leq a(x,z)\) for all $x,y,z \in X$. We view
$a$ as a (not necessarily symmetric) distance function, noting however that objects with `greater' distance should be seen as being closer together. A \(\V\)-category \((X,a)\) is
symmetric if \(a(x,y) = a(y,x)\) for all \(x,y \in X\).
Every $\V$-category \((X,a)\) carries a natural order defined by
\(
x \le y \text{ whenever } k \le a(x,y),
\)
which induces a faithful functor $\Cats{\V} \to \ORD$.
A \(\V\)-category is separated if its natural order is antisymmetric.
A $\V$-functor $f \colon (X,a) \to (Y,b)$ is a map $f \colon X \to Y$ such that, for all $x,y \in X$, \( a(x,y) \le b(f(x),f(y)).\)
\(\V\)-categories and \(\V\)-functors form the category \(\Cats{\V}\), and we denote by \(\Cats{\V}_\sym\) the full subcategory of \(\Cats{\V}\) determined by the symmetric \(\V\)-categories and by \(\Cats{\V}_{\sym,\sep}\) the full subcategory of \(\Cats{\V}_{\sym}\) determined by the separated symmetric \(\V\)-categories.

* The Category \(\Cats{\one}\) is equivalent to the category \(\SET\) of sets and functions.

* The category $\Cats{\two}$ is equivalent to the category $\ORD$ of preordered sets and monotone maps.

* Metric, ultrametric and bounded metric spaces à la Lawvere [28] can be seen as quantale-enriched categories:

* The category \(\Cats{[0,\infty]_+}\) is equivalent to the category \(\MET\) of generalized metric spaces and non-expansive maps.

* The category \(\Cats{[0,\infty]_{\max}}\) is equivalent to the category $\UMET$ of generalized ultrametric spaces and non-expansive maps.

* The category $\Cats{[0,1]_{\oplus}}$ is equivalent to the category $\BMET$ of bounded-by-$1$ hemimetric spaces and non-expansive maps.

* Categories enriched in a free quantale \(\ftP M\) on a monoid \(M\) can be interpreted as sets equipped with a non-deterministic \(M\)-valued structure.

General $\V$                Qualitative ($\V=2$)                       Quantitative ($\V=[0,1]_\oplus$)
$\V$-category               preorder                                   bounded-by-1 hemimetric space

symmetric $\V$-category     equivalence                                bounded-by-1 pseudometric space

$\V$-functor                monotone map                               non-expansive map

initial $\V$-functor        order-reflectingmonotone  map     isometry

$\V$-categorical notions in the qualitative and the quantitative setting. The prefix `pseudo' refers to absence of separatedness, and the prefix `hemi' additionally indicates absence
of symmetry.

We focus on $\V=\two$ and $\V=[0,1]_\oplus$, which we will use to capture classical (qualitative) and metric (quantitative) aspects of system behaviour, respectively..
Table <ref> provides some instances of generic quantale-based concepts (either introduced above or to be introduced presently) in these two cases, for further reference.

A $\V$-category $(X,a)$ is discrete if $a=1_X$, and indiscrete if $a(x,y)=\top$ for all $x,y\in X$. The dual of \((X,a)\) is the
\(\V\)-category \({(X,a)}^\op = (X,a^\circ)\) given by
$a^\circ(x,y)=a(y,x)$. Given a set $X$ and a structured cone,
i.e. a family \((f_i \colon X \to \ftII{(X_i,a_i)})_{i\in I}\) of
maps into $\V$-categories $(X_i,a_i)$, the initial structure
\(a \colon X \times X \to \V\) on $X$ is defined by
\( a(x,y) = \bigwedge_{i\in I}a_i(f_i(x),f_i(y)), \) for all
$x,y\in X$.  A cone \(((X,a) \to (X_i,a_i))_{i \in I}\) is said to be
initial (w.r.t. the forgetful functor
\(\ftII{-} \colon \Cats{\V} \to \SET\)) if \(a\) is the initial
structure w.r.t. the structured cone
\((X \to \ftII{(X_i,a_i)})_{i \in I}\); a \(\V\)-functor is initial if
it forms a singleton initial cone.  For every \(\V\)-category \((X,a)\) and
every set \(S\), the \(S\)-power \((X,a)^S\) is the
\(\V\)-category consisting of the set of all functions from \(S\) to
\(X\), equipped with the \(\V\)-category structure \([-,-]\) given by
\( [f,g] = \bigwedge_{x \in X} a(f(x),g(x)), \) for all
\(f,g \colon S \to X\).  By equipping its hom-sets with the
substructure of the appropriate power, the category \(\Cats{\V}\)
becames \(\Cats{\V}\)-enriched and, hence, also \(\ORD\)-enriched
w.r.t to the corresponding natural order of \(\V\)-categories.  We say
that an endofunctor on \(\Cats{\V}\) is locally monotone if it
preserves this preorder.

Let us briefly outline the connections between \(\Cats{\V}\) and \(\Cats{\V}_\sym\), which for real-valued $\V$ correspond to hemimetric and pseudometric spaces, respectively.
By virtue of the above construction of initial structures, the categories \(\Cats{\V}\) and  \(\Cats{\V}_\sym\) are topological over \(\SET\) [1];
in particular, both categories are complete and cocomplete.
Moreover,  \(\Cats{\V}_\sym\) is a (reflective and) coreflective full subcategory of \(\Cats{\V}\).
The coreflector \((-)_s \colon \Cats{\V} \to \Cats{\V}_\sym\) is identity on morphisms and sends every \((X,a)\) to its symmetrization, the \(\V\)-category \((X,a_s)\) where \(a_s(x,y)= a(x,y) \wedge a(y,x)\) (keep in mind that in <ref>.<ref>, the order is the dual of the numeric order).

Finally, we note that for every quantale $\V$, $(\V,\hom)$ is a $\V$-category, which for simplicity we also denote by \(\V\).
The following result records two fundamental properties of the \(\V\)-category \(\V\).

The \(\V\)-category \(\V=(\V,\hom)\) is injective w.r.t. initial morphisms, and for every \(\V\)-category \(X\),
the cone \((f \colon X \to \V)_{f}\) is initial.

§.§ Predicate Liftings

Given a cardinal \(\kappa\) and a \(\V\)-category \(X\), a \(\kappa\)-ary \(X\)-valued predicate lifting for a functor \(\ftF \colon \Cats{\V} \to \Cats{\V}\) is a natural transformation
\(
\lambda \colon\Cats{\V}(-,X^\kappa) \to \Cats{\V}(\ftF-,X).
\)
When \(\V\) is the trivial quantale, we identify an \(X\)-valued predicate lifting with a natural transformation
\(
\lambda \colon \SET(-,X^\kappa) \to \SET(\ftF-,X)
\)
via the isomorphism \(\SET \cong \Cats{1}\).
In this case, we are primarily interested in predicate liftings valued in the underlying set of another quantale, and we say that such predicate liftings are monotone if each of its components is a monotone map w.r.t. the pointwise order induced by that quantale.

By the Yoneda lemma, every \(\kappa\)-ary \(X\)-valued predicate lifting for a functor \(\ftF \colon \Cats{\V}\to \Cats{\V}\) is  determined by a \(\V\)-functor \(\ftF X^\kappa \to X\).
In particular, the collection of all \(X\)-valued \(\kappa\)-ary predicate liftings for a functor is a set.

* The Kripke semantics of the standard diamond modality \(\Diamond\) of the modal logic \(K\) is induced (in a way recalled in Section <ref>) by the unary predicate lifting $\Diamond_X(A) = \{B \subseteq X \mid A \cap B \neq \varnothing\}$ for the (finite) powerset functor (modulo the isomorphism $\mathcal{P} X\cong\SET(X,\two)$).

*  Computing the expected value for a given $[0,1]$-valued function with respect to each probability distribution defines a unary \([0,1]\)-valued predicate lifting for the functor \(\ftD_\omega \colon \SET \to \SET\), which we denote by \(\mathbb{E}\).

§.§ Quantale-Enriched Relations and Lax Extensions

The structure of a quantale-enriched category is a particular kind of “enriched relation”.
For a quantale $\V$ and sets $X$ and $Y$, a $\V$-relation from $X$ to $Y$ is a map $r\colon X \times Y \to \V$; we then write $r\colon X \relto Y$.
As for ordinary relations, a pair of $\V$-relations \(r \colon X \relto Y\) and \(s \colon Y \relto Z\) can be composed via “matrix multiplication”:
\(
(s \cdot r)(x,z)=\bigvee_{y \in Y} r(x,y) \otimes s(y,z)
\)
for \(x \in X\), \(z \in Z\).
With this composition, the collection of all sets and \(\V\)-relations between them form a category, denoted \(\Rels{\V}\).
The identity morphism on a set \(X\) is the \(\V\)-relation \(1_X \colon X \relto X\) that sends every diagonal element to \(k\) and all the others to \(\bot\).

The category of $2$-relations is the usual category \(\REL\) of sets and relations.
Quantitative or “fuzzy” relations are usually defined as \([0,1]_\oplus\)-relations (e.g. [40, 5]).

The category \(\Rels{\V}\) comes with an involution
\(
{(-)}^\circ \colon {\Rels{\V}}^\op \to \Rels{\V}
\)
that maps objects identically and sends a \(\V\)-relation \({r \colon X \relto Y}\) to the \(\V\)-relation \(r^\circ \colon Y \relto X\) given by \(r^\circ(y,x) = r(x,y)\), the converse of \(r\).
Moreover, by equipping its hom-sets with the pointwise order induced by \(\V\), \(\Rels{\V}\) is made into a quantaloid (e.g. [33]), i.e. enriched over complete join semilattices.
This entails that there is an optimal way of extending a \(\V\)-relation \(r \colon X \relto Y\) along a \(\V\)-relation \(s \colon X \relto Z\):
the (Kan) extension of \(r\) along \(s\) is the \(\V\)-relation  \(r \multimapdotinv s \colon Z \relto Y\)  defined by the property
\(
t \cdot s \leq r \iff t \leq r \multimapdotinv s,
\)
for all \(t \colon Z \relto Y\).

A lax extension
Extensions of \(\SET\)-functors to \(\REL\) are also commonly referred to as “relators”, “relational liftings” or “lax relational liftings”.
of a functor \(\ftF \colon \SET \to \SET\) to \(\Rels{\V}\) is a lax functor \(\eF \colon \Rels{\V} \to \Rels{\V}\) that agrees with \(\ftF\) on sets and whose action on functions is compatible with \(\ftF\).
To make the latter requirement precise, we note that a function is interpreted as the \(\V\)-relation that sends every element of its graph to \(k\) and all the others to \(\bot\);
then, a lax extension of \(\ftF\) to \(\Rels{\V}\), or simply a lax extension, is a map
\(
(r \colon X \relto Y) \longmapsto (\eF r \colon \ftF X \relto \ftF Y)
\)
such that:

p:102(L1) $r \le r' \implies \eF r \le \eF r'$,

p:26(L2) $\eF s\cdot\eF r\le\eF (s\cdot r)$,

p:0(L3) $\ftF f \le \eF f$ and
${(\ftF f)}^\circ\le\eF(f^\circ)$,

for all \(r \colon X \relto Y\), \(s \colon Y \relto Z \) and \(f \colon X \to Y\).

The generalized “lower-half” Egli-Milner order between powersets, which for a relation \(r \colon X \relto Y\) is defined as the relation \(\widehat{\ftP}r \colon \ftP X \relto \ftP Y\) given by

\[
A (\widehat{\ftP}r) B \iff \forall a \in A.\, \exists b \in B.\, a \mathrel{r} b,
\]

defines a lax extension of the powerset functor \(\ftP \colon \SET \to \SET\) to \(\REL\).
Similarly, the generalized “upper-half” and the generalized Egli-Milner order define lax extensions of the powerset functor to \(\REL\).

Lax extensions are deeply connected with monotone predicate liftings.
To realize this, it is convenient to think of the \(X\)-component of a \(\kappa\)-ary predicate lifting as a map of type
\(
\Rels{\V}(\kappa,X) \to \Rels{\V}(1,\ftF X)
\)

[Note that Goncharov et. al. consider as their main point of view the dual of the one considered here <cit.>.
Our choice prevents a harmless mismatch between the Kantorovich liftings and Kantorovich extensions in Theorem <ref>.]

A \(\kappa\)-ary predicate lifting \(\lambda\) for a functor
\(\ftF \colon \SET \to \SET\) is induced by a lax extension
\(\eF \colon \Rels{\V}\! \to\! \Rels{\V}\) if there is a \(\V\)-relation
\(\fr \colon 1\! \relto\! \ftF \kappa\)
such that
\(\lambda(f) = \eF f \cdot \fr \),
for every \(\V\)-relation
\(f \colon \kappa \relto X\).

By interpreting a subset of a set \(X\) as a relation from \(1\) to \(X\), the unary predicate lifting \(\Diamond\) (see Example <ref>) for the powerset functor \(\ftP \colon \SET \to \SET\) is induced by the lax extension of Example <ref>; indeed, it is determined by the map \(1 \to \ftP 1\) that selects the set \(1\).

Every predicate lifting induced by a lax extension is monotone.

Lax extensions have been instrumental in coalgebraic notions of behavioural distance (e.g. [13, 40, 41]), and the notion of Kantorovich extension has been crucial to connect such notions with coalgebraic modal logic [7].

Let \(\ftF \colon \SET \to \SET\) be a functor, and \(\Lambda\) a class of monotone predicate liftings for \(\ftF\).
The Kantorovich lax extension of \(\ftF\) w.r.t. \(\Lambda\) is the lax extension
\(
\eF^\Lambda = \bigwedge_{\lambda \in \Lambda} \eF^\lambda,
\)
where for every \(\V\)-relation \(r \colon X \relto Y\), the \(\V\)-relation \(\eF^\lambda r \colon \ftF X \relto \ftF Y\) given by
\(
\label{p:44}
\eF^\lambda r
= \bigwedge_{g \colon \kappa \relto X} \lambda(r \cdot g) \multimapdotinv \lambda (g).
\)

The Kantorovich extension of the powerset functor \(\ftP \colon \SET \to \SET\) to \(\REL\) w.r.t the \(\Diamond\) predicate lifting coincides with the extension given by the “lower-half” of the Egli-Milner order (Example <ref>).

As suggested by the previous example, the Kantorovich extension leads to a representation theorem that plays an important role in Section <ref>.

Let \(\eF \colon \Rels{\V} \to \Rels{\V}\) be a lax extension, and let \(\Lambda\) be the class of all predicate liftings induced by \(\eF\).
Then, \(\widehat \ftF = \eF^\Lambda\).

§ TOPOLOGICAL LIFTINGS

It is well-known that every lax extension \(\eF \colon \Rels{\V} \to \Rels{\V}\) of a functor \(\ftF \colon \SET \to \SET\) gives rise to a lifting (which we denote by the same symbol) of $\ftF$ to $\Cats{\V}$ (for instance, see [39]).
By definition, liftings are completely determined by their action on objects.
In particular, the lifting induced by a lax extension \(\eF \colon \Cats{\V}\to\Cats{\V}\) sends a \(\V\)-category \((X,a)\) to the \(\V\)-category \((\ftF X,\eF a)\).
Of course, it does not make sense to talk about functor liftings to the category \(\Cats{\V}\) when \(\V\) is trivial, hence we assume from now on that $\V$ is non-trivial.

Predicate liftings also induce functor
liftings, via a simple construction available on all topological
categories that goes back, at least, to work in categorical duality theory
[11, 31]: To lift a functor
\(\ftG \colon\catA\to\catY\) along a topological functor
\(\ftII{-} \colon\catB\to\catY\), it is enough to give, for every
object \(A\) in \(\catA\), a structured cone

\begin{equation}
\label{d:eq:4}
\mathcal{C}(A)=(\ftG A\xrightarrow{h}\ftII{B})_{h,B}
\end{equation}

so that, for every \(h\) in \(\mathcal{C}(A)\) and every
\(f \colon A'\to A\), the composite \(h\cdot\ftG f\) belongs to the
cone \(\mathcal{C}(A')\).  Then, for an object \(A\) in \(\catA\), one
defines \(\ftG^I A\) by equipping \(\ftG A\) with the initial
structure w.r.t. the structured cone (<ref>).  It is easy to
see that the assignment \( X \mapsto \ftG^I X \) indeed defines a
functor \(\ftG^I \colon\catA\to\catB\) such that
\(\ftII{-}\cdot\ftG^{I}=\ftG\).  This technique has been previously
applied in the context of codensity liftings
[22, 23, 37, 20] and Kantorovich liftings
[5].  We apply this to our situation as follows. Given a
functor \(\ftF \colon \SET \to \SET\), take \(\ftG=\ftF\cdot \ftII{-}\); then a lifting of $\ftF$ to \(\Cats{\V}\) can be specified by a class of natural transformations

\begin{equation}\label{eq:gen-pl}
\lambda \colon \Cats{\V}(-,A_\lambda) \longrightarrow \SET(\ftF\ftII{-},\ftII{B_\lambda}),
\end{equation}

(which may be thought of as generalized predicate liftings, in that they lift $A_\lambda$-valued predicates to $B_\lambda$-valued ones).
Namely, given a \(\V\)-category \(X\), we consider the structured cone consisting of all maps

\[
\lambda(f) \colon \ftF \ftII{X} \longrightarrow \ftII{B_\lambda}
\]

where \(\lambda\) ranges over the given natural transformations
and $f$ over all \(\V\)-functors \(X \to A_\lambda\).  As described
above, we obtain a \(\V\)-category \(\ftF^I X\) by equipping
\(\ftF |X|\) with the initial structure w.r.t. this cone.  We call
functor liftings constructed in this way topological. Indeed, it
turns out that every functor lifting is topological, even when
one restricts $B_\lambda$ in (<ref>) to be the $\V$-category
\((\V,\hom)\):

Every lifting of a \(\SET\)-functor to \(\Cats{\V}\) is topological w.r.t. a class of natural transformations
\(
\lambda \colon \Cats{\V}(-,A_\lambda) \longrightarrow \SET(\ftF\ftII{-},\ftII{\V}).
\)

In examples, we usually construct a generalized predicate
lifting (<ref>) from a $\kappa$-ary predicate
lifting $\lambda$ for the set functor $\ftF$: Choose a pair \((A,B)\)
of \(\V\)-categories over the sets \(\V^\kappa\) and \(\V\),
respectively (the above theorem allows restricting to $B=\V$, and the
examples we present are of this kind). We can then precompose
$\lambda$ with the inclusion natural transformation
$\Cats{\V}(-,A) \longrightarrow \SET(\ftII{-},\ftII{A})$, obtaining a
natural transformation
\(\lambda^{(A,B)} \colon \Cats{\V}(-,A) \to
\SET(\ftF\ftII{-},\ftII{B})\) that applies \(\lambda\) to maps
underlying \(\V\)-functors with codomain \(A\).

* The discrete lifting of the identity functor \(\ftId \colon \SET \to \SET\), which sends every \(\V\)-category to the discrete \(\V\)-category with the same underlying set, can be obtained as a topological lifting constructed from the identity \(\V\)-valued predicate lifting for \(\ftId\) by choosing \(A\) to be the \(\V\)-category consisting of the set \(\V\) equipped with the indiscrete structure.

*  The lifting of the identity functor \(\ftId \colon \SET \to \SET\) to \(\ORD\) that computes the smallest equivalence relation that contains a given preorder can be obtained as a topological lifting constructed from the \(\two\)-valued identity predicate lifting for \(\ftId\) by choosing \(A\) to be the discrete preordered set with two elements.

* It is well-known that the total variation distance between finite distributions \(\mu,\upsilon\) on a set \(X\) coincides with the Kantorovich distance on the discrete bounded-by-\(1\) metric space \(X\) (e.g. [15]);
that is, \(d^{TV}(\mu,\upsilon) = \bigvee_{f \colon X \to [0,1]} \mathbb{E}_X(f)(\upsilon) \ominus \mathbb{E}_X(f)(\mu)\) (see Example <ref>(<ref>)).
Therefore, the total variation distance defines a lifting of the finite distribution functor to \(\BMET\) that can be obtained as the topological lifting constructed from the predicate lifting \(\mathbb{E}\) by choosing \(A\) to be the indiscrete space \([0,1]\).
This example is closely related to the first one. Indeed, this lifting is the composite of the Kantorovich lifting of the finite distribution functor to \(\BMET\) (see Example <ref>) and the discrete lifting of the identity functor to \(\BMET\). By Theorem <ref> below,  precomposing functor liftings with the discrete lifting of the identity functor can be used to derive non-Kantorovich s.

Theorem <ref> can be fine-tuned to show that the discrete lifting \(\ftF^d \colon \ORD \to \ORD\) of a finitary functor \(\ftF \colon \SET \to \SET\) is a topological lifting constructed from a set \(\Lambda\) of finitary \(2\)-valued predicate liftings for \(\ftF\).
Hence, for every set \(X\), considered as a discrete preordered set, we have that the cone of all maps
\(
\lambda(f) \colon \ftF^d(X,1_X) \to 2,
\)
for \(\kappa\)-ary predicate liftings \(\lambda\in\Lambda\) and maps \(X \to 2^\kappa\), is initial.
Thus, as \(\ftF^d(X,1_X)\) is antisymmetric, this cone is mono.
In this sense, our results subsume the result that every finitary \(\SET\)-functor admits a separating set of finitary predicate liftings [36].

§.§ Kantorovich Liftings

For our present purposes, we are primarily interested in topological
liftings induced by predicate liftings in the standard sense,
i.e. the natural transformations (<ref>) are of
the shape
\( \lambda \colon \Cats{\V}(-,\V^\kappa) \longrightarrow
\SET(\ftF\ftII{-},\ftII{\V}) \), and thus employ $\V$, equipped with
its standard $\V$-category structure, as the object of truth values
throughout. In particular, this format is needed to use predicate
liftings as modalities in existing frameworks for quantitative
coalgebraic logic (Section <ref>). Many functor liftings
considered in work on coalgebraic behavioural distance can be
understood as topological liftings constructed in this way
(e.g. [5, 23, 40, 41, 12]).
To simplify notation, in the sequel we often omit the forgetful functor to \(\SET\).

Let \(\ftF \colon \SET \to \SET\) be a functor and \(\Lambda\) a class of \(\V\)-valued predicate liftings for \(\ftF\).
The Kantorovich lifting of \(\ftF\) w.r.t. \(\Lambda\) is the topological lifting \(\ftF^\Lambda \colon \Cats{\V} \to \Cats{\V}\) that sends a \(\V\)-category \(X\) to the \(\V\)-category \((\ftF X, \ftF^\Lambda a)\), where \(\ftF^\Lambda a\) denotes the initial structure on \(\ftF X\) w.r.t. the structured cone of all functions

\[
\lambda(f) \colon \ftF \ftII{X} \longrightarrow \ftII{\V}
\]

where \(\lambda\in\Lambda\) is \(\kappa\)-ary and \(f \colon (X,a) \to \V^\kappa\) is a \(\V\)-functor.
Generally, a lifting \(\ftbF \colon \Cats{\V} \to \Cats{\V}\) of $\ftF$ is  Kantorovich if $\ftbF=\ftF^\Lambda$ some class $\Lambda$ of predicate liftings for \(\ftF\).

As the name suggests, the prototypical example of a Kantorovich lifting is given by the (non-symmetric) Kantorovich distance between finite distributions, which arises as the Kantorovich lifting of the finite distribution functor on \(\SET\) to the category \(\BMET\) w.r.t the predicate lifting \(\mathbb{E}\) that computes expected values, i.e. \(\ftD_\omega^\mathbb{E}(X,a)(\mu,\upsilon) = \bigvee_{f \colon (X,a) \to [0,1]} \mathbb{E}_X(f)(\upsilon) \ominus \mathbb{E}_X(f)(\mu)\).

We go on to exploit the universal property of initial lifts of cones to characterize the liftings that are Kantorovich.
In the following, fix a functor \(\ftF \colon \SET \to \SET\) and a quantale \(\V\). Consider the partially ordered conglomerate \(\PredF\) of classes of \(\V\)-valued predicate liftings for \(\ftF\) ordered by containment, i.e.
\(
\Lambda \leq\Lambda' \iff\Lambda \supseteq \Lambda';
\)
and the partially ordered class \(\LiftF\) of liftings of \(\ftF\) to \(\Cats{\V}\) ordered pointwise, i.e.
\(
\ftbF \leq \ftbF'
\iff \ftbF a \leq \ftbF' a,
\)
for every \(\V\)-category \((X,a)\).

Let \(\ftbF \colon \Cats{\V} \to \Cats{\V}\) be a lifting of \(\ftF\).
A \(\kappa\)-ary \(\V\)-valued predicate lifting \(\lambda\) for \(\ftF\) is compatible with \(\ftbF\) if it restricts to a predicate lifting for \(\ftbF\):

[row sep=2ex]
(-,^κ)     (-,)

(-,^κ)    (-, )
[from=1-1, to=1-2, "λ", dotted]
[from=1-1, to=2-1, ]
[from=1-1, to=2-2, "=", phantom]
[from=1-2, to=2-2, ]
[from=2-1, to=2-2, "λ"']

where the vertical arrows denote set inclusions – that is, if $\lambda$ lifts $\V$-functorial predicates on $X$ to $\V$-functorial predicates on $\ftbF X$.
The class of all predicate liftings compatible with \(\ftbF\) is denoted by \(\ftP(\ftbF)\).

A \(\kappa\)-ary \(\V\)-valued predicate lifting \(\lambda\) for \(\ftF\) is compatible with \(\ftbF\) iff the map \(\lambda(1_{\ftII{\V^\kappa}}) \colon \ftF (\ftII{\V^\kappa}) \to \ftII{\V}\) is a \(\V\)-functor of type \(\ftbF \V^\kappa \to \V\).

The Kantorovich lifting defines a universal construction:

Let \(\ftF \colon \SET \to \SET\) be a functor.
Assigning to a class of predicate liftings for \(\ftF\) the corresponding Kantorovich lifting yields a right adjoint \(\ftF^{(-)} \colon \PredF \to \LiftF\) whose left
adjoint \(\ftP \colon \LiftF \to \PredF\) maps a lifting of \(\ftF\) to the class \(\ftP(\ftbF)\) of all \(\V\)-valued predicate liftings for \(\ftF\) that are compatible with the lifting.

The following result shows that Kantorovich liftings are characterized by a pleasant property that is required in multiple results in the context of coalgebraic approaches to behavioural distance (e.g. [5, 23, 12, 42]).

A lifting of a \(\SET\)-functor to \(\Cats{\V}\) is Kantorovich iff it preserves initial morphisms.

Every topological lifting of a functor \(\ftF \colon \SET \to \SET\) w.r.t. a class of natural transformations \(\lambda \colon \Cats{\V}(-,A_\lambda) \to \SET(\ftF -, \ftII{B_\lambda})\) where each \(A_\lambda\) is injective in \(\Cats{\V}\) w.r.t. initial morphisms is Kantorovich.

The composite of Kantorovich liftings is Kantorovich.

The characterization of Theorem <ref> makes it easy to distinguish Kantorovich liftings.

*  It is an elementary fact that every lifting induced by a lax extension preserves initial morphisms (e.g. <cit.>).
In particular, the Wasserstein lifting [5] is Kantorovich.

The identity functor on \(\SET\)  has a lifting
\(
(-)^\circ \colon \Cats{\V} \to \Cats{\V}
\)
that sends every \(\V\)-category to its dual.
Clearly, this lifting preserves initial morphisms, and hence it is Kantorovich. Indeed, one can show that it is the Kantorovich lifting of the identity functor w.r.t. the set of \(\V\)-valued predicate liftings determined by the representable \(\V\)-functors \(\V^\op \to \V\).

*  The functor \((-)_s \colon \Cats{\V} \to \Cats{\V}_\sym\) that symmetrizes \(\V\)-categories gives rise to a lifting \((-)_s \colon \Cats{\V} \to \Cats{\V}\) of the identity functor on \(\SET\).
Clearly, this functor preserves initial morphisms, and hence it is Kantorovich. Indeed, one can show that it is the Kantorovich lifting of the identity functor w.r.t. the set of all \(\V\)-valued predicate liftings determined by the representable \(\V\)-functors \(\V_s \to \V\).

* The discrete lifting of the identity functor on \(\SET\) to \(\Cats{\V}\) is not Kantorovich, as it fails to preserve initial morphisms.

* The lifting of the identity functor on \(\SET\) to \(\Cats{\V}\) that sends a \(\V\)-category \((X,a)\) to the \(\V\)-category given by the final structure w.r.t. the structured cospan of identity maps \(\ftII{(X,a)} \rightarrow X \leftarrow \ftII{(X,a^\circ)}\) is not Kantorovich.
This lifting generalizes Example <ref>(<ref>).

* The lifting of the finite distribution functor on \(\SET\) to \(\BMET\) given by the Kantorovich distance is Kantorovich, while the lifting given by the total variation distance is not Kantorovich.

§.§ Liftings Induced by Lax Extensions

We  show next that lax extensions, functor liftings, and predicate liftings are linked by adjunctions, and characterize the liftings induced by lax extensions.
We begin by showing that the Kantorovich extension and the Kantorovich lifting are compatible.

Let \(\eF \colon \Cats{\V} \to \Cats{\V}\) be a lifting of a functor \(\ftF \colon \SET \to \SET\)
induced by a lax extension \(\eF \colon \Rels{\V} \to \Rels{\V}\).
If \(\eF \colon \Rels{\V} \to \Rels{\V}\) is the Kantorovich extension w.r.t. a class \(\Lambda\) of predicate liftings, then the functor \(\eF \colon \Cats{\V} \to \Cats{\V}\) is the Kantorovich lifting of \(\ftF \colon \SET \to \SET\) w.r.t. \(\Lambda\).

Let \(\LaxF\) denote the partially ordered class of lax extensions of a functor \(\ftF \colon \SET \to \SET\) to \(\Rels{\V}\) ordered pointwise:

\[
\eF \leq \eF'
\iff \forall r \in \Rels{\V}. \; \eF r \leq \eF' r;
\]

let \(\LiftFi\) denote the partially ordered subclass of \(\LiftF\) consisting of the liftings that preserve initial morphisms, and let \(\PredFm\) denote the partially ordered subconglomerate of \(\PredF\) of monotone predicate liftings.
Clearly, the operations of taking Kantorovich extensions
\(
\eF^{(-)} \colon \PredFm \to \LaxF,
\)
and inducing liftings from lax extensions
\(
\ftI \colon \LaxF \to \LiftFi
\)
define monotone maps.
Moreover, as we have seen in Theorem <ref>, the monotone map \(\ftF^{(-)} \colon \PredF \to \LiftF\) corestricts to \(\LiftFi\).
Therefore, our results so far tell us that lax extensions, liftings and predicate liftings are connected through a diagram of monotone maps

[row sep=large, column sep=scriptsize]

[from=1-1, to=1-2, ""]
[from=1-2, to=2-2, "", bend left]
[from=2-1, to=2-2, hookrightarrow]
[from=2-1, to=1-1, "^(-)"]
[from=2-2, to=1-2, "^(-)", bend left]
[from=2-2, to=1-2, "⊢", phantom]

which commutes if the left adjoint is ignored.
In the sequel, we will see that every monotone map in this diagram is an adjoint.
In particular, it might not be immediately obvious that the monotone map \(\eF^{(-)} \colon \PredFm \to \LaxF\) is a right adjoint without  first thinking in terms of functor liftings induced by lax extensions, because the obvious guess – taking the predicate liftings induced by a lax extension (<ref>) – in general does not define a monotone map \(\LaxF \to \PredFm\).
The next example illustrates this as well as the fact that there are predicate liftings compatible with a functor lifting induced by a lax extension that are not induced by the lax extension.

The identity functor on \(\ORD\) is the lifting induced by the identity functor on \(\REL\) as a lax extension of the identity functor on \(\SET\).
The constant map into \(\top\) is a monotone map \(2 \to 2\) and, hence, determines a predicate lifting that is compatible with the identity functor on \(\ORD\).
It is easy to see that this predicate lifting is induced by the largest extension of the identity functor, however, it is not induced by the identity functor on \(\REL\) <cit.>.

It should also be noted that the predicate liftings compatible with a functor lifting that preserves initial morphisms are not necessarily monotone.
That is, the map \(\ftP \colon \LiftFi \to \PredF\) does not necessarily corestrict to \(\PredFm\).

Consider the lifting \({(-)}^\circ \colon \ORD \to \ORD\) of the identity functor on \(\SET\) that sends each preordered set to its dual.
Then, the predicate lifting for \({(-)}^\circ\) determined by the \(\V\)-functor \(\hom(-,0) \colon {(2,\hom)}^\op \to (2,\hom)\) is not monotone since it sends the constant map \(0 \colon 1 \to 2\) to the constant map \(1 \colon 1 \to 2\).

Accordingly, we need to “filter the monotone predicate liftings” first.
This operation trivially defines the left adjoint
\(
\ftM \colon \PredF \to \PredFm
\)
of the inclusion map \(\PredFm \hookrightarrow \PredF\).

Let \(\ftF \colon \SET \to \SET\) be a functor.
The monotone map \(\ftI \colon \LaxF \to \LiftFi\) is order-reflecting and right adjoint to the monotone map \(\eF^{\ftM\ftP(-)} \colon \LiftFi \to \LaxF\).

Let \(\ftF \colon \SET \to \SET\) be a functor.
The monotone map \(\eF^{(-)} \colon \PredFm \to \LaxF\) is right adjoint to the order-reflecting monotone map \(\ftM\ftP\ftI \colon \LaxF \to \PredFm\).

Therefore, the interplay between lax extensions, liftings and predicate liftings is captured by the diagram

\begin{equation}\label{eq:adjunctions}
\begin{tikzcd}[row sep=large, column sep=normal]
\LaxF  & \LiftFi \\
\PredFm & \PredF
\ar[from=1-1, to=1-2, "\ftI"']
\ar[from=1-1, to=2-1, "\ftM\ftP\ftI"', bend right]
\ar[from=1-1, to=2-1, "\dashv"', phantom]
\ar[from=1-2, to=2-2, "\ftP", bend left]
\ar[from=1-2, to=1-1, "\eF^{\ftM\ftP(-)}"', bend right]
\ar[from=1-2, to=1-1, "\tdash"', phantom, bend right=12]
\ar[from=2-1, to=1-1, "\eF^{(-)}"', bend right]
\ar[from=2-1, to=2-2, hookrightarrow]
\ar[from=2-2, to=1-2, "\ftF^{(-)}", bend left]
\ar[from=2-2, to=1-2, "\vdash", phantom]
\ar[from=2-2, to=2-1, "\ftM", bend left]
\ar[from=2-2, to=2-1, "\dasht", phantom, bend left=12]
\end{tikzcd}
\end{equation}

which commutes when only the right adjoints or only the left adjoints are considered.
Finally, we characterize the liftings induced by lax extensions.

A lifting $\eF$ of a \(\SET\)-functor $\ftF$ to \(\Cats{\V}\) is induced by a lax extension of $\ftF$ to \(\Rels{\V}\)  iff $\eF$ preserves initial morphisms and is locally monotone.

\(\V\)-enriched lax extensions have proved to be crucial to deduce quantitative van Benthem and Hennessy-Milner theorems [40, 41].
We recall that a lax extension of a functor \(\ftF \colon \SET \to \SET\) to \(\Rels{\V}\) is \(\V\)-enriched [41, 16] if, for all \(u \in \V\), \(u \otimes 1_{\ftF X} \leq \eF(u \otimes 1_X)\); where \(u \otimes r\) denotes the \(\V\)-relation “\(r\) scaled by \(u\)”, that is, \((u \otimes r)(x,y) = u \otimes r(x,y)\).

A lifting $\eF$ of a \(\SET\)-functor $\ftF$ to \(\Cats{\V}\) is induced by a \(\V\)-enriched lax extension of $\ftF$ to \(\Rels{\V}\) iff $\eF$ preserves initial morphisms and is \(\Cats{\V}\)-enriched.

Our characterization of lax extensions makes it clear that there is a large collection of Kantorovich liftings that are not induced by lax extensions.
For instance, it follows from Theorem <ref> that the liftings \((-)^\circ \colon \Cats{\V} \to \Cats{\V}\) and \((-)_s \colon \Cats{\V} \to \Cats{\V}\) (see Example <ref>) of the identity functor on \(\SET\) to \(\Cats{\V}\) are Kantorovich but are not induced by lax extensions.
Furthermore, as the composite of Kantorovich liftings is Kantorovich, in many situations it is possible to compose these functors with other Kantorovich liftings to generate liftings that are not induced by lax extensions.

§ BEHAVIOURAL DISTANCE

One main motivation for lifting functors to metric spaces was to obtain coalgebraic notions of behavioural distance [5, 40]. Indeed,
every functor \(\ftF \colon \Cats{\V}\to \Cats{\V}\) gives rise to a notion of distance on a \(\ftF\)-coalgebras:

Let \((X,a,\alpha)\) be a coalgebra for a functor \(\ftF \colon \Cats{\V} \to \Cats{\V}\).
The behavioural distance \(\bd_\alpha^\ftF(x,y)\) of \(x,y \in X\) is

\begin{align}\label{eq:bd-form}
\bd_\alpha^\ftF(x,y) = \bigvee \{b(f(x),f(y)) \mid f \colon (X,a,\alpha) \to (Y,b,\beta) \in \Coalg{\ftF}\}.
\end{align}

Notice the analogy with the standard notion of behavioural
equivalence: Two states are behaviourally equivalent if they can be
made equal under some coalgebra morphism; and according to the above
definition,  two states in a metric coalgebra have low behavioural distance if they can be
made to have low distance under some coalgebra morphism.

Kantorovich liftings and lax extensions are key ingredients in mentioned alternative coalgebraic approaches to behavioural distance on \(\SET\)-based coalgebras.
Let \(\ftF \colon \SET \to \SET\) be a functor.
A Kantorovich lifting \(\ftF^\Lambda \colon \Cats{\V} \to \Cats{\V}\) induces a notion of behavioural distance on an \(\ftF\)-coalgebra \(\alpha \colon X \to \ftF X\) as the greatest \(\V\)-categorical structure \((X,a)\) that makes \(\alpha\) a \(\V\)-functor of type \((X,a) \to \ftF^\Lambda (X,a)\) [5, 23].
From Theorem <ref> and <cit.> (generalized to \(\Cats{\V}\), with the same proof), we obtain that this distance coincides with behavioural distance as defined above.
On the other hand, every lax extension \(\eF \colon \Rels{\V} \to \Rels{\V}\) of \(\ftF\) also induces a behavioural distance on an \(\ftF\)-coalgebra \(\alpha \colon X \to \ftF X\) as the greatest simulation on \(\alpha\) [34, 42, 13, 40],
i.e. the greatest \(\V\)-relation \(s \colon X \relto X\) such that \(\alpha \cdot s \leq \eF s \cdot \alpha\). It follows by routine calculation that this distance coincides with the distance defined via the lifting induced by the lax extension and, hence, Theorem <ref> ensures that, if we start with a collection of monotone predicate liftings, then the corresponding Kantorovich extension and Kantorovich lifting yield the same notion of behavioural distance.
This allows including the approach to behavioural distance via lax extensions in the categorical framework for indistinguishability introduced recently by Komorida et al. [23].

On the other hand, there are notions of behavioural distance defined via Kantorovich liftings that do not arise via lax extensions.
Indeed, it has been shown that the neighbourhood functor \(\ftN \colon \SET \to \SET\) does not admit a lax extension to \(\REL\) that preserves converses (\(\eF (r^\circ) = (\eF r)^\circ\)) whose (\(\two\)-valued) notion of behavioural distance coincides with behavioural equivalence <cit.>.
However, from <cit.> (see also [17]), we can conclude that the (\(\two\)-valued) notion of behavioural distance defined by the canonical Kantorovich lifting  of \(\ftN\) to \(\EQ\) w.r.t. to the predicate lifting induced by the identity natural transformation \(\ftN \to \ftN\) coincides with behavioural equivalence.
(It is easy to see that Marti and Venema's result holds even if one allows lax extensions of \(\ftN\) that do not preserve converses, and that the situation remains the same in the asymmetric case.)

§ EXPRESSIVITY OF QUANTITATIVE COALGEBRAIC LOGICS

We proceed to connect the characterization of Kantorovich functors
with existing expressivity results for quantitative coalgebraic logic,
focusing from now on on symmetric \(\V\)-categories. Therefore, we
interpret the \(\V\)-categorical notions and results also with
\(\Cats{\V}_{\sym}\) instead of \(\Cats{\V}\) and \(\V_{s}\) instead
of \(\V\).

We recall a variant [12] of
(quantitative) coalgebraic
logic [30, 36, 7, 25, 40] that follows the
paradigm of interpreting modalities via predicate liftings, in this case of
$\V$-valued predicates for a \(\Cats{\V}\)-functor (Section <ref>). Let \(\Lambda\) be a set of finitary predicate liftings for a functor \(\ftF \colon \Cats{\V}_\sym \to \Cats{\V}_\sym\).
The syntax of quantitative coalgebraic modal logic is then defined by the grammar

ϕ⊤|ϕ_1 ∨ϕ_2 |ϕ_1 ∧ϕ_2 |u ⊗ϕ|_s(u,ϕ) |λ(ϕ_1,…,ϕ_n)          (u ∈, λ∈Λ)

where $\Lambda$ is a set of modalities of finite arity, which we identify, by abuse of notation, with the given set \(\Lambda\) of predicate liftings.
We view all other connectives as propositional operators.
Let $\calL(\Lambda)$ be the set of modal formulas thus defined.

The semantics is given by assigning to each formula \(\phi \in \calL(\Lambda)\) and each coalgebra \(\alpha \colon X \to \ftF X\) the interpretation of $\phi$ over $\alpha$,
i.e. the \(\V\)-functor \(\Sema{\phi} \colon X \to \V\) recursively defined as follows:

* for \(\phi = \top\), we take \(\Sema{\top}\) to be the \(\V\)-functor given by the constant map into \(\top\);

* for an $n$-ary propositional operator $p$, we put $\Sema{p(\phi_1, \ldots, \phi_n)} = p (\Sema{\phi_1}, \ldots, \Sema{\phi_n})$, with $p$ interpreted using the lattice structure of $\V$ and the \(\V\)-categorical structure \(\hom_s\) of \(\V_s\), respectively, on the right-hand side;

* for  \(n\)-ary $\lambda \in \Lambda$, we put $\Sema{\lambda(\phi_1, \ldots, \phi_n)} = \lambda (\langle\Sema{\phi_1}, \ldots, \Sema{\phi_n}\rangle) \cdot \alpha$, where \(\langle \Sema{\phi_1}, \ldots, \Sema{\phi_n}\rangle\) denotes the  \(\V\)-functor \((X,a)\to\V^n\) canonically determined by \(\Sema{\phi_1}, \ldots, \Sema{\phi_n}\).

We then obtain a notion of logical distance:

Let \(\Lambda\) be a set of predicate liftings for a functor \(\ftF \colon \Cats{\V} \to \Cats{\V}\).
The logical distance \(ld_\alpha^\Lambda\) on an \(\ftF\)-coalgebra \((X,a,\alpha)\) is the initial structure on \(X\) w.r.t. the structured cone of all maps
\(
\Sema{\phi} \colon X \to \ftII{(\V,\hom_s)}
\)
with \(\phi \in \calL(\Lambda)\).
More explicitly, for all \(x,y \in X\),
ld_α^Λ(x,y) = ⋀{_s(ϕ(x),ϕ(y)) |ϕ∈(Λ)}.

In the remainder of the paper, we establish criteria under which a \(\Cats{\V}_\sym\)-functor admits a set of predicate liftings for which logical and behavioural distances coincide.
Recall that a (quantitative) coalgebraic logic is expressive if \(ld_\alpha^\Lambda \leq \bd_\alpha^\ftF\), for every \(\ftF\)-coalgebra \((X,\alpha)\).
(It is easy to show that the reverse inequality holds universally <cit.>).

Existing expressivity results for quantitative coalgebraic logics for \(\SET\)-functors depend crucially on Kantorovich liftings (e.g. [40, 41, 23, 12]).
However, it has been shown [12] that the Kantorovich property can be usefully detached from the notion of functor lifting.

Let \(\Lambda\) be a class of predicate liftings for a functor \(\ftF \colon \Cats{\V} \to \Cats{\V}\).
The functor \(\ftF\) is \(\Lambda\)-Kantorovich if for every \(\V\)-category \(X\), the cone of all \(\V\)-functors
\(
\lambda(f) \colon \ftF X \to \V
\),
with \(\lambda\in \Lambda\) \(\kappa\)-ary and \(f \in \Cats{\V}(X,\V^\kappa)\), is initial.
A functor \(\ftF \colon \Cats{\V} \to \Cats{\V}\) is said to be Kantorovich if it is \(\Lambda\)-Kantorovich for some class \(\Lambda\) of predicate liftings for \(\ftF\).

Clearly, every Kantorovich lifting of a \(\SET\)-functor to \(\Cats{\V}\) w.r.t. a class \(\Lambda\) of predicate liftings is \(\Lambda\)-Kantorovich.
Moreover, Theorem <ref> is easily generalized to Kantorovich functors.

A \(\Cats{\V}\)-functor is Kantorovich iff it preserves initial morphisms.

A \(\Cats{\V}_\sym\)-functor is Kantorovich iff it preserves initial morphisms.

* The inclusion functor \(\Cats{\V}_{\sym,\sep} \hookrightarrow \Cats{\V}_\sym\) has a
left adjoint \((-)_q \colon \Cats{\V}_\sym \to \Cats{\V}_{\sym,\sep}\) that quotients every \(X\) by its natural preorder, which for  symmetric $X$ is an equivalence, and gives rise to a Kantorovich functor on \(\Cats{\V}_\sym\).

*  Given a bounded-by-\(1\) pseudometric space \((X,d)\), i.e. an object of \(\Cats{[0,1]_\oplus}_\sym \simeq \PBMET\), the Prokhorov distance [32] for probability measures on the measurable space of Borel sets of \((X,d)\) is defined by \(d^P(\mu,\upsilon) = \inf\{\epsilon > 0 \mid \mu(A) \leq \upsilon (A^\epsilon) + \epsilon \text{ for all Borel sets $A\subseteq X$}\}\), where \(A^\epsilon = \{x \in X \mid \inf_{y \in A} d(x,y) \leq \epsilon\}\).
It is straightforward to verify that this distance defines a \(\PBMET\)-functor (which acts on morphisms by measuring preimages) that preserves isometries and, therefore, it is Kantorovich.

*  For every \(\V\)-category \((X,a)\), the functor
\(
(X,a)\times- \colon\Cats{\V}\to\Cats{\V}
\)
is Kantorovich.
If the underlying lattice of \(\V\) is Heyting, then under certain conditions this functor has a right adjoint [8, 9]
which is Kantorovich as well.
Here, for \(X=(X,a)\) exponentiable, the right adjoint \((-)^{X}\) of \(X\times-\) sends a
\(\V\)-category \(Y=(Y,b)\) to the \(\V\)-category \(Y^{X}=(Y^{X},c)\) with
underlying set
\(
\{\text{all \(\V\)-functors \((1,k)\times(X,a)\to(Y,b)\)}\}
\)
and, for \(h,k\in Y^{X}\),

where \((-)^{u}\colon\V\to\V\) denotes the right adjoint of \(u\wedge- \colon\V\to\V\).
For a \(\V\)-functor \(f \colon (Y_{1},b_{1})\to(Y_{2},b_{2})\), the
\(\V\)-functor \(f^{X}\colon (Y_{1}^{X},c_{1})\to (Y_{2}^{X},c_{2})\) sends
\(h\in Y_{1}^{X}\) to \(f\cdot h\).

To ensure that a Kantorovich functor is represented by finitary predicate liftings, we need to impose a size constraint:

A functor $\ftF\colon\Cats{\V}_\sym \to\Cats{\V}_\sym$ is \(\omega\)-bounded if for every symmetric $\V$-category $X$ and every $t\in\ftF X$, there exists a finite subcategory $X_0\subseteq X$ and $t'\in\ftF X_0$ such that $t=\ftF i(t')$ where $i$ is the inclusion $X_0\to X$.

Every lifting of a finitary \(\SET\)-functor to \(\Cats{\V}_\sym\) is \(\omega\)-bounded.

Let \(\ftF \colon \Cats{\V}_\sym \to \Cats{\V}_\sym\) be a Kantorovich functor.
If \(\ftF\) is \(\omega\)-bounded, then \(\ftF\) is Kantorovich w.r.t. a set of finitary predicate liftings.

Finally, from <cit.> we obtain:

Let \(\V\) be a finite quantale, and let \(\ftF \colon \Cats{\V}_\sym \to \Cats{\V}_\sym\) be a lifting of a finitary functor that preserves initial morphisms.
Then there is a set \(\Lambda\) of predicate liftings for \(\ftF\) of finite arity such that the coalgebraic logic \(\calL(\Lambda)\) is expressive.

Let \(\ftF \colon \PBMET \to \PBMET\) be a functor that preserves isometries, is locally non-expansive, and admits a dense \(\omega\)-bounded subfunctor.
Then there is a set \(\Lambda\) of predicate liftings for \(\ftF\) of finite arity such that the coalgebraic logic \(\calL(\Lambda)\) is expressive.

These instantiate to results on concrete system types, e.g. ones induced by (sub)functors listed in Example <ref>, such as probabilistic transition systems equipped with a behavioural distance induced by the functor that sends a bounded metric space \(X\) to the subspace of the space of all probability measures on \(X\) equipped with the Prokhorov distance (see Example <ref>(<ref>)) determined by the closure of the set of finitely supported probability measures.

§ CONCLUSIONS AND FUTURE WORK

Quantitative coalgebraic Hennessy-Milner
theorems [24, 40, 12] assume that the functor (on
metric spaces) describing the system type is Kantorovich,
i.e. canonically induced by a suitable choice of – not necessarily
monotone – predicate liftings, which then serve as the modalities of
a logic that characterizes behavioural distance. We have shown as one
of our main results that a functor on (quantale-valued) metric spaces
is Kantorovich iff it preserves initial morphisms
(i.e. isometries). As soon as such a functor additionally adheres to
the expected size and continuity constraints (which replace the
condition of finite branching found in the classical Hennessy-Milner
theorem for labelled transition systems), one thus has a logical
characterization of behavioural distance in coalgebras for the
functor, in the sense that behavioural distance equals logical

In fact we have shown that every functor on metric spaces can
be captured by a generalized form of predicate liftings where the
object of truth values may change along the lifting. A simple example
is the discretization functor, which is characterized by a predicate
lifting in which the truth value object for the input predicates is
equipped with the indiscrete pseudometric, so that the lifting accepts
all predicates instead of only non-expansive ones. This hints
at a perspective to design heterogeneous modal logics that
characterize behavioural distance for such functors, with modalities
connecting different types of formulas (e.g. non-expansive
vs. unrestricted), which we will pursue in future work. One
application scenario for such a logic are behavioural distances on
probabilistic systems involving total variation distance, which may be
seen as a composite of the usual probabilistic Kantorovich functor and
the discretization functor.

[1]
Adámek, J., Herrlich, H., Strecker, G.E.: Abstract and concrete categories:
The joy of cats. Pure and Applied Mathematics (New York), John Wiley &
Sons Inc., New York (1990),
<http://tac.mta.ca/tac/reprints/articles/17/tr17abs.html>, republished
in: Reprints in Theory and Applications of Categories, No. 17 (2006)
pp. 1–507

[2]
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and Branching System
Metrics. IEEE Transactions on Software Engineering  35(2),
258–273 (mar 2009). 10.1109/TSE.2008.106

[3]
Alsina, C., Frank, M.J., Schweizer, B.: Associative functions. Triangular norms
and copulas. Hackensack, NJ: World Scientific (2006).

[4]
Awodey, S.: Category Theory. Oxford University Press, 2nd edn. (2010)

[5]
Baldan, P., Bonchi, F., Kerstan, H., König, B.: Coalgebraic Behavioral
Metrics. Log. Methods Comput. Sci.  14(3),  1860–5974 (2018).

[6]
van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic
transition systems. Theoretical Computer Science  331(1),  115–142
(feb 2005). 10.1016/j.tcs.2004.09.035

[7]
Cîrstea, C., Kurz, A., Pattinson, D., Schröder, L., Venema, Y.:
Modal Logics are Coalgebraic. Computer Journal  54(1),  31–41
(2011). 10.1093/comjnl/bxp004

[8]
Clementino, M.M., Hofmann, D.: Exponentiation in $V$-categories. Topology and
its Applications  153(16),  3113–3128 (Oct 2006).

[9]
Clementino, M.M., Hofmann, D., Stubbe, I.: Exponentiable functors between
quantaloid-enriched categories. Applied Categorical Structures
17(1),  91–101 (Sep 2009). 10.1007/s10485-007-9104-5

[10]
Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled markov
processes. Inf. Comput.  179(2),  163–193 (2002).

[11]
Dimov, G.D., Tholen, W.: A characterization of representable dualities. In:
Adámek, J., MacLane, S. (eds.) Categorical topology and its relation to
analysis, algebra and combinatorics: Prague, Czechoslovakia, 22-27 August
1988, pp. 336–357. World Scientific (1989)

[12]
Forster, J., Goncharov, S., Hofmann, D., Nora, P., Schröder, L., Wild, P.:
Quantitative Hennessy-Milner theorems via notions of density. In: Klin,
B., Pimentel, E. (eds.) Computer Science Logic, CSL 2023. LIPIcs, Schloss
Dagstuhl – Leibniz-Zentrum für Informatik (2023), to appear. Preprint
avaible on arXiv under <https://doi.org/10.48550/arXiv.2207.09187>

[13]
Gavazzo, F.: Quantitative behavioural reasoning for higher-order effectful
programs: Applicative distances. In: Dawar, A., Grädel, E. (eds.) Logic
in Computer Science, LICS 2018. pp. 452–461. ACM (2018).

[14]
Giacalone, A., Jou, C., Smolka, S.A.: Algebraic Reasoning for Probabilistic
Concurrent Systems. In: Broy, M., Jones, C.B. (eds.) Programming concepts
and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working
Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5
April, 1990. pp. 443–458. North-Holland (1990)

[15]
Gibbs, A.L., Su, F.E.: On choosing and bounding probability metrics.
International statistical review  70(3),  419–435 (2002)

[16]
Goncharov, S., Hofmann, D., Nora, P., Schröder, L., Wild, P.: A
point-free perspective on lax extensions and predicate liftings. CoRR
abs/2112.12681 (2021), <https://arxiv.org/abs/2112.12681>

[17]
Hansen, H.H., Kupke, C., Pacuit, E.: Neighbourhood structures: Bisimilarity and
basic model theory. Log. Methods Comput. Sci.  5(2) (2009),

[18]
Hofmann, D., Nora, P.: Hausdorff Coalgebras. Applied Categorical Structures
28(5),  773–806 (Apr 2020). 10.1007/s10485-020-09597-8

[19]
Huber, P.: Robust Statistics. Wiley Series in Probability and Statistics, Wiley
(1981), <https://books.google.de/books?id=hVbhlwEACAAJ>

[20]
Katsumata, S.: A semantic formulation of tt-lifting and logical predicates for
computational metalanguage. In: Ong, C.L. (ed.) Computer Science Logic, 19th
International Workshop, CSL 2005, 14th Annual Conference of the EACSL,
Oxford, UK, August 22-25, 2005, Proceedings. Lecture Notes in Computer
Science, vol. 3634, pp. 87–102. Springer (2005). 10.1007/11538363_8,

[21]
Kelly, G.M.: Basic concepts of enriched category theory, London Mathematical
Society Lecture Note Series, vol. 64. Cambridge University Press, Cambridge
(1982), Republished in: Reprints in Theory and Applications of Categories.
No. 10 (2005), 1–136

[22]
Komorida, Y., Katsumata, S., Hu, N., Klin, B., Hasuo, I.: Codensity Games for
Bisimilarity. In: 34th Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. pp. 1–13.
IEEE (2019). 10.1109/LICS.2019.8785691

[23]
Komorida, Y., Katsumata, S., Kupke, C., Rot, J., Hasuo, I.: Expressivity of
Quantitative Modal Logics : Categorical Foundations via Codensity
and Approximation. In: 36th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp.
1–14. IEEE (2021). 10.1109/LICS52264.2021.9470656

[24]
König, B., Mika-Michalski, C.: (metric) bisimulation games and
real-valued modal logics for coalgebras. In: Schewe, S., Zhang, L. (eds.)
29th International Conference on Concurrency Theory, CONCUR 2018, September
4-7, 2018, Beijing, China. LIPIcs, vol. 118, pp. 37:1–37:17. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik (2018).

[25]
König, B., Mika-Michalski, C.: (metric) bisimulation games and
real-valued modal logics for coalgebras. In: Schewe, S., Zhang, L. (eds.)
Concurrency Theory, CONCUR 2018. LIPIcs, vol. 118, pp. 37:1–37:17. Schloss
Dagstuhl – Leibniz-Zentrum für Informatik (2018).

[26]
Larsen, K.G., Fahrenberg, U., Thrane, C.R.: Metrics for weighted transition
systems: Axiomatization and complexity. Theor. Comput. Sci.
412(28),  3358–3369 (2011). 10.1016/j.tcs.2011.04.003

[27]
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf.  Comput.  94(1),  1–28 (1991). 10.1016/0890-5401(91)90030-6

[28]
Lawvere, F.W.: Metric spaces, generalized logic, and closed categories.
Rendiconti del Seminario Matemàtico e Fisico di Milano  43(1),
135–166 (Dec 1973). 10.1007/bf02924844, Republished in: Reprints in
Theory and Applications of Categories, No. 1 (2002), 1–37

[29]
Marti, J., Venema, Y.: Lax extensions of coalgebra functors and their logic.
Journal of Computer and System Sciences  81(5),  880–900 (2015).

[30]
Pattinson, D.: Expressive logics for coalgebras via terminal sequence
induction. Notre Dame J. Formal Log.  45(1),  19–33 (jan 2004).

[31]
Porst, H.E., Tholen, W.: Concrete dualities. In: Herrlich, H., Porst, H.E.
(eds.) Category theory at work, Research and Exposition in Mathematics,
vol. 18, pp. 111–136. Heldermann Verlag, Berlin (1991),
<http://www.heldermann.de/R   E/RAE18/ctw07.pdf>, with Cartoons by Marcel

[32]
Prokhorov, Y.V.: Convergence of random processes and limit theorems in
probability theory. Theory of Probability & Its Applications  1(2),
157–214 (1956). 10.1137/1101016,

[33]
Rosenthal, K.: Quantaloids, enriched categories and automata theory. Appl.  Cat. Struct.  3,  279–301 (1995). 10.1007/BF00878445

[34]
Rutten, J.: Relators and Metric Bisimulations. Electronic Notes in
Theoretical Computer Science  11,  252–258 (1998).

[35]
Rutten, J.: Universal coalgebra: a theory of systems. Theoretical Computer
Science  249(1),  3–80 (Oct 2000).

[36]
Schröder, L.: Expressivity of coalgebraic modal logic: The limits and
beyond. Theor. Comput. Sci.  390(2-3),  230–247 (jan 2008).

[37]
Sprunger, D., Katsumata, S., Dubut, J., Hasuo, I.: Fibrational bisimulations
and quantitative reasoning: Extended version. J. Log. Comput.
31(6),  1526–1559 (2021). 10.1093/logcom/exab051,

[38]
Stubbe, I.: An introduction to quantaloid-enriched categories. Fuzzy Sets and
Systems  256,  95–116 (Dec 2014). 10.1016/j.fss.2013.08.009,
special Issue on Enriched Category Theory and Related Topics (Selected papers
from the 33rd Linz Seminar on Fuzzy Set Theory, 2012)

[39]
Tholen, W.: Ordered topological structures. Topology and its Applications
156(12),  2148–2157 (Jul 2009). 10.1016/j.topol.2009.03.038

[40]
Wild, P., Schröder, L.: Characteristic logics for behavioural metrics via
fuzzy lax extensions. In: Konnov, I., Kovács, L. (eds.) Concurrency
Theory, CONCUR 2020. LIPIcs, vol. 171, pp. 27:1–27:23. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik (2020).
10.4230/LIPIcs.CONCUR.2020.27, extended version in Log. Methods
Comput. Sci. 18(2), 2022

[41]
Wild, P., Schröder, L.: A Quantified Coalgebraic van Benthem
Theorem. In: Kiefer, S., Tasson, C. (eds.) Foundations of Software Science
and Computation Structures, FOSSACS 2021. LNCS, vol. 12650, pp. 551–571.
Springer (2021). 10.1007/978-3-030-71995-1_28

[42]
Worrell, J.: Coinduction for recursive data types: partial orders, metric
spaces and $\Omega$-categories. In: Reichel, H. (ed.) Coalgebraic Methods
in Computer Science, CMCS 2000, Berlin, Germany, March 25-26, 2000.
Electronic Notes in Theoretical Computer Science, vol. 33, pp. 337–356.
Elsevier (2000). 10.1016/S1571-0661(05)80356-1

§ APPENDIX: OMITTED PROOFS AND DETAILS

§.§ Proof of <ref>

Let \(\ftbF \colon \Cats{\V} \to \Cats{\V}\) be a lifting of a functor \(\ftF \colon \SET \to \SET\), \(X\) be a \(\V\)-category and \(\Lambda\) be a class of natural transformations

\[
\lambda \colon \Cats{\V}(-,A_\lambda) \longrightarrow \Cats{\V}(\ftbF -, \V).
\]

If the cocone

\[
\big(\lambda_{X} \colon \Cats{\V}(X,A_\lambda) \longrightarrow \Cats{\V}(\ftbF X, \V)\big)_{\lambda \in \Lambda}
\]

is jointly epic, then the topological lifting w.r.t. the class of all natural transformations

\[
\lambda \colon \Cats{\V}(-,A_\lambda) \longrightarrow \SET(\ftF\ftII{-}, \ftII{\V})
\]

that factor as

(-,A_λ)     (-,)

(-, )
[from=1-1, to=1-2, "λ"]
[from=1-1, to=2-2, "λ"']
[from=1-2, to=2-2, "-_-,"]

for some \(\lambda \in \Lambda\) coincides with \(\ftbF\) on \(X\).

It follows by hypothesis that the topological lifting maps the \(\V\)-category \(X\) to the domain of the initial lift of the structured cone

\[
(\ftII{f} \colon \ftF\ftII{X} \longrightarrow \ftII{\V})_{f \in \Cats{\V}(\ftbF X, \V)}.
\]

Therefore, the claim is consequence of the fact that the cone
\(\Cats{\V}(\ftbF X, \V)\) is initial (see Remark <ref>).

The Yoneda lemma guarantees that there is an epi-cocone of natural transformations

\[
\lambda \colon \Cats{\V}(-,A_\lambda) \longrightarrow \Cats{\V}(\ftbF -, \V)
\]

determined by every \(\V\)-category \(A\) and every \(\V\)-functor \(\lambda \colon \ftbF A \to \V\).

§.§ Details of Example <ref>(<ref>)

Consider the discrete preordered set with two elements \((2=\{0,1\},1_2)\) and the preordered set \((3=\{0,1,2\},\vee)\) with three elements generated by \(2 \leq 1\) and \(2 \leq 0\).
Then, the inclusion \((2,1_2) \hookrightarrow (3,\vee)\) is initial, however its image under the lifting it is not, since the lifting acts as identity on \((2,1_2)\) but sends \((3,\vee)\) to the indiscrete preordered set with three elements.
To see that this is a topological lifting of identity functor on \(\SET\) constructed from the \(\two\)-valued identity predicate lifting for \(\ftId \colon \SET \to \SET\) by choosing \(A=(2,1_2)\), note that for every preordered set \((X,r)\), \(x\) is equivalent to \(y\) w.r.t to the smallest equivalence relation that contains \(r\) if and only if there is a zigzag between \(x\) and \(y\) in \((X,r)\) if and only if for every monotone map \(f \colon (X,r) \to (2,1_2)\), \(f(x) = f(y)\).

§.§ Proof of <ref>

Let \(\ftbF \colon \Cats{\V} \to \Cats{\V}\) be a lifting of \(\ftF\) and \(S\) be a set of predicate liftings for \(\ftF\).
We claim that \(\ftP(\ftbF) \supseteq S\) iff \(\ftbF \leq \ftF^S\).
Suppose that \(\ftP(\ftbF) \supseteq S\).
Then, since every \(\kappa\)-ary predicate lifting in \(S\) is compatible with \(\ftbF\), for every \(\V\)-functor \(f \colon (X,a) \to \V^\kappa\), the map

(X,a)     (^κ)    [from=1-1, to=1-2, "f"']
[from=1-2, to=1-3, "λ(1_^κ)"']
[from=1-1, to=1-3, bend left, "λ(f)"]

is a \(\V\)-functor.
Therefore, \(\ftbF(X,a) \leq \ftF^S (X,a)\).

On the other hand, suppose that \(\ftbF \leq \ftF^S\).
By definition of Kantorovich lifting, every predicate lifting in \(S\) is compatible with \(\ftF^S\).
Hence, for every \(\lambda \colon \ftF^S(\V^\kappa) \to \V\) determined by a \(\kappa\)-ary predicate lifting \(\lambda\) in \(S\),

(^κ)     ^S(^κ)    [from=1-1, to=1-2, "1_^κ"']
[from=1-2, to=1-3, "λ"']
[from=1-1, to=1-3, bend left, "λ"]

is a \(\V\)-functor.

§.§ Proof of <ref>

Firstly, we show that every Kantorovich lifting of a functor \(\ftF \colon \SET \to \SET\) preserves initial morphisms.

Let \(i \colon (X,a) \to (Y,b)\) be an initial morphism,
\(\Lambda\) a class of predicate liftings for \(\ftF\),
\(j \colon (Z,c) \to \ftF^\Lambda(Y,b)\) a \(\V\)-functor, and
\(h \colon Z \to \ftF X\) a map such that \(j = \ftF i \cdot h\).

By definition of \(\ftF^\Lambda\) it is sufficient to show that for every
\(\kappa\)-ary predicate lifting for \(\ftF\) in \(\Lambda\) and every \(\V\)-functor
\(f \colon (X,a) \to \V^\kappa\), \(\lambda(f) \cdot h\) is a \(\V\)-functor.
Since \(\V\) is injective in \(\Cats{\V}\) w.r.t. initial
morphisms, \(\V^\kappa\) is also injective in \(\Cats{\V}\) with respect
to initial morphisms.
Hence, for every \(\V\)-functor
\(f \colon (X,a) \to \V^\kappa\) there is a \(\V\)-functor
\(g \colon (Y,b) \to \V^\kappa\) such that \(f = g \cdot i\).

\[
\lambda(f) \cdot h
= \lambda(g \cdot i) \cdot h
= \lambda(g) \cdot \ftF i \cdot h
= \lambda(g) \cdot j
\]

is a \(\V\)-functor.

Secondly, we show that the converse statement holds. Suppose that \(\ftbF\)
is a lifting that preserves initial morphisms. We already know from
Theorem <ref> that \(\ftbF \leq \ftF^{\ftP(\ftbF)}\). To prove that under
our assumption the reverse inequality also holds, let \((X,a)\) be a
\(\V\)-category and \(\kappa = |X|\). Then, the Yoneda embedding \((X,a)
\to [(X,a)^\op,\V]\) gives us an initial morphism

(X,a)     [(X,a)^,]     ^X     ^κ.
[from=1-1, to=1-2]
[from=1-2, to=1-3, hookrightarrow]
[from=1-1, to=1-4, bend left, ""]
[from=1-3, to=1-4, "∼"]

Hence, since \(\ftbF\) preserves initial morphisms,
\(\ftbF \yoneda \colon \ftbF(X,a) \to \ftbF(\V^\kappa)\)
is initial. Now, let \(\ftP_\kappa(\ftbF)\) denote the set of all
\(\kappa\)-ary predicate liftings in \(\ftP(\ftbF)\).
Given that the cone of all \(\V\)-functors

\[
\ftbF(\V^\kappa) \longrightarrow \V
\]

is initial and the composition of initial cones is initial, the cone

\[
(\lambda(\yoneda) \colon \ftbF(X,a) \longrightarrow \V)_{\lambda \in \ftP_\kappa(\ftbF)}
\]

is initial. Therefore, \(\ftF^{\ftP(\ftbF)} (X,a) \leq \ftbF (X,a)\).

§.§ Proof of <ref>

To obtain this result it is useful to express the Kantorovich lifting in the language of \(\V\)-relations [16].
In the sequel, given a \(\V\)-functor \(f \colon X \to \V^\kappa\), we denote by \(f^\flat \colon \kappa \relto X\) the \(\V\)-relation defined by \(f^\flat(k,x) = f(x)(k)\), for all \(k \in \kappa\) and \(x \in X\).
Also, we recall that a \(\V\)-relation \(r \colon X \relto Y\) is a distributor \(r \colon (X,a) \modto (Y,b)\) if \(r \cdot a \leq r\) and \(b \cdot r \leq r\).

Let \((X,a)\) be a \(\V\)-category, \(\kappa\) a cardinal and
\(f \colon X \to \V^\kappa\) a function. The following propositions are

* \(f \colon (X, a) \to \V^\kappa\) is a \(\V\)-functor;

* \(a \leq f^\flat \multimapdotinv f^\flat\);

*  \(a \cdot f^\flat = f^\flat\);

* \(f^\flat \colon (\kappa, 1_\kappa) \relto (X,a)\) is a \(\V\)-distributor.

Let \(\calC = (f_i \colon X \to |\V^\kappa|)_{i \in I}\) be a structured cone.
The initial  \(\V\)-category on \(X\) w.r.t. \(\calC\) is given by

\[
\bigwedge_{i \in I} {f_i}^\flat \multimapdotinv {f_i}^\flat.
\]

Let \(\lambda\) be a \(\kappa\)-ary \(\V\)-valued predicate lifting for a functor \(\ftF \colon \SET \to \SET\).
The Kantorovich lifting \(\ftF^\lambda \colon \Cats{\V} \to \Cats{\V}\) of \(\ftF\) w.r.t. \(\lambda\) sends a \(\V\)-category \((X,a)\) to the \(\V\)-category \((\ftF X, \ftF^\lambda a)\), where

\[
\ftF^\lambda a
= \bigwedge_{r \colon (\kappa,1_\kappa) \modto (X,a)} \lambda(r) \multimapdotinv \lambda(r).
\]

Therefore, the Kantorovich lifting of a class of predicate liftings \(\Lambda\) sends a
\(\V\)-category \((X,a)\) to the \(\V\)-category \((\ftF X, \ftF^\Lambda a)\), where
\(
\ftF^\Lambda a
= \bigwedge_{\lambda \in \Lambda} \ftF^\lambda a.
\)

Now, Theorem <ref> is an immediate consequence of the following lemma.

Let \(\lambda\) be a \(\kappa\)-ary \(\V\)-valued monotone predicate lifting for a functor \(\ftF \colon \SET \to \SET\), and let \((X,a)\) be a \(\V\)-category.

\[
\bigwedge_{g \colon \kappa \relto X} \lambda(a \cdot g) \multimapdotinv \lambda(g)
= \bigwedge_{r \colon (\kappa,1_\kappa) \modto (X, a)} \lambda(r) \multimapdotinv \lambda(r).
\]

Let \(g \colon \kappa \relto X\) be a \(\V\)-relation.
Since \(1_X \leq a\), we have \(g \leq a \cdot g\).
Also, given that \(a \cdot a \leq a\),
we obtain that \(a \cdot g \colon (\kappa,1_\kappa) \modto (X, a)\) is a \(\V\)-distributor.
Therefore, because \(\lambda\) is monotone,

\[
\lambda(a \cdot g) \multimapdotinv \lambda(a \cdot g) \leq
\lambda(a \cdot g) \multimapdotinv \lambda(g).
\]

The other inequality is an immediate consequence of
Proposition <ref>(<ref>).

§.§ Proof of <ref>

In the sequel, given a \(\V\)-relation \(r \colon X \relto Y\), we denote by \(r^\sharp \colon Y \to \V^X\) the function that sends each \(y \in Y\) to the function \(r(-,y) \colon X \to \V\).
Moreover, for every set \(S\), we denote the structure of the \(\V\)-category \(\V^S\) by \(h^S\).

Every predicate lifting induced by a lax extension of a \(\SET\)-functor to \(\Rels{\V}\) is compatible with the lifting to \(\Cats{\V}\) induced by the lax extension.

Let \(\lambda\) be a \(\kappa\)-ary \(\V\)-valued predicate lifting for a functor \(\ftF \colon \SET \to \SET\) that is induced by a lax extension \(\eF \colon \Rels{\V} \to \Rels{\V}\) of \(\ftF\).
Then, by <cit.>,

\begin{align*}
\eF h^\kappa \cdot \lambda(\ev_\kappa)
& = \eF h^\kappa \cdot \lambda(h^\kappa \cdot 1_\kappa^\sharp)                     \\
& = \eF h^\kappa \cdot \eF h^\kappa \cdot \ftF(1_\kappa^\sharp) \cdot \lambda(1_k) \\
& = \eF h^\kappa \cdot \ftF(1_\kappa^\sharp) \cdot \lambda(1_k)                    \\
& = \lambda (\ev_\kappa).
\end{align*}

Therefore, the claim follows from Propositions <ref> and <ref>.

Let \(\ftF \colon \SET \to \SET\) be a functor.
The monotone map \(\ftI \colon \LaxF \to \LiftF_\ftI\) is order-reflecting.

Note that every \(\V\)-relation \(r \colon X \relto Y\) can be factorized as \(r = (r^\sharp)^\circ \cdot h^X \cdot 1_X^\sharp\).

Let  \(\eF \colon \Rels{\V} \to \Rels{\V}\) be a lax extension of \(\ftF\).
Then, by Propositions <ref> and Remark <ref>, \(\ftM\ftP\ftI(\eF)\)
contains the all predicate liftings induced \(\eF\).
Hence, by Theorem <ref>,

\[
\eF^{\ftM\ftP\ftI(\eF)} \leq \eF.
\]

On the other hand, let \(\ftbF \colon \Cats{\V} \to \Cats{\V}\) be a lifting of \(\ftF\) that preserves initial morphisms.
Then, by Theorem <ref> and the fact that \(\ftM\ftP \colon \LiftFi \to \PredFm\) is left adjoint to \(\ftF^{(-)} \colon \PredFm \to \LiftFi\),

\[
\ftbF \leq \ftF^{\ftM\ftP(\ftbF)} = \ftI(\eF^{\ftM\ftP(\ftbF)}).
\]

§.§ Proof of <ref> and <ref>

We will show <ref> as <ref> follows identically by taking into account <cit.> and <cit.>.
We already observed that every lifting induced by a lax extension preserves initial morphisms, and the fact that it is also locally monotone follows immediately from L1 and L3 since \(f \leq g\) in \(\Cats{\V}((X,a),(Y,b))\) iff \(1_X \leq g^\circ \cdot b \cdot f\).

On the other hand, suppose that \(\ftbF \colon \Cats{\V} \to \Cats{\V}\) is a lifting of \(\ftF\) that preserves initial morphisms and is locally monotone.
Then, since every \(\V\)-functor is monotone, we have that every \(\kappa\)-ary \(\V\)-valued predicate lifting \(\lambda\) for \(\ftF\) compatible with \(\ftbF\) is monotone, as each \(X\)-component is given by the composite of monotone maps

((X,1_X),^κ)     ((X,1_X),(^κ))

[from=1-1, to=1-2, "(-)"]
[from=1-2, to=2-2, "λ(1_^κ) ·-"]
[from=1-1, to=2-2, "λ_X"']

Therefore, by Theorem <ref> and the proof of Theorem <ref>, we conclude that \(\ftbF = \eF^{\ftP(\ftbF)}\).

§.§ Details of <ref>

Let \(\ftbF \colon \Cats{\V} \to \Cats{\V}\) be a lifting of a functor \(\ftF \colon \SET \to \SET\) that preserves initial morphisms and corestricts to \(\Cats{\V}_\sym\).
Then, for every \(\ftF\)-coalgebra \(\alpha \colon X \to \ftF X\), \(\bd_\alpha^\ftbF\) is symmetric.

Let \(\alpha \colon X \to \ftF X\) be an \(\ftF\)-coalgebra.
Since the lifting preserves initial morphisms, then by <cit.> (the same proof holds for the non-symmetric case), \(\bd_\alpha^\ftF\) is the greatest \(\V\)-categorical structure that makes \(\alpha \colon (X,\bd_\alpha^\ftF) \to \ftbF(X,\bd_\alpha^\ftF)\) a \(\V\)-functor.
In particular, this means that \(\alpha \colon (X,\bd_\alpha^\ftF) \to \ftbF (X,\bd_\alpha^\ftF)\) is initial.
Therefore, as \(\ftbF\) corestricts to \(\Cats{\V}_\sym\) and this category is closed under initial cones in \(\Cats{\V}\), we conclude that \(\bd_\alpha^\ftF\) is symmetric.

Let \(\eF \colon \Rels{\V} \to \Rels{\V}\) be a lax extension of a functor \(\ftF \colon \SET \to \SET\) and let \(\alpha \colon X \to \ftF X\) be an \(\ftF\)-coalgebra.
Every symmetric \(\eF\)-simulation on \(\alpha\) is also a \(\eF^s\)-(bi)simulation.

Let \(s\) be a symmetric \(\eF\)-simulation on \(\alpha\).

\begin{align*}
& \alpha \cdot s \leq \eF s \cdot \alpha                           \\
\Longleftrightarrow & s^\circ \cdot \alpha^\circ \leq \alpha^\circ \cdot (\eF s)^\circ \\
\Longrightarrow     & s \cdot \alpha^\circ \leq \alpha^\circ \cdot (\eF s)^\circ       \\
\Longleftrightarrow & \alpha \cdot s \leq (\eF s)^\circ \cdot \alpha.
\end{align*}

Therefore, \(\alpha \cdot s \leq (\eF s \wedge (\eF s)^\circ) \cdot \alpha = \eF^s s \cdot \alpha\), since the map \(-\cdot \alpha\) preserves infima.

§.§ Details of <ref>(<ref>)

The usual proof shows that the Prokhorov distance defines a pseudometric (e.g. <cit.>), and to see that “measuring preimages” define non-expansive maps w.r.t. this pseudometric, note that for every non-expansive map \(f \colon X \to Y\),
\(
(f^{-1}B)^\epsilon \subseteq f^{-1}(B^\epsilon),
\)
for all \(B \subseteq Y\) and \(\epsilon \in [0,1]\).
Therefore, the Prokhorov pseudometric defines a functor \(\ftD^P \colon \PBMET \to \PBMET\).
Now, suppose that \(f \colon X \to Y\) is an isometry.
Let  \(\mu, \upsilon\) be probablity measures on \(X\), and let \(\epsilon \in (0,1]\) such that for every Borel set \(B \subseteq Y\), \(\mu(B) \leq \upsilon(B^\epsilon) + \epsilon\).
Consider a Borel set \(A \subseteq X\).
Then, \(\overline{fA} \subseteq Y\) is a Borel set which, by hypothesis, yields \(\mu(A) \leq \upsilon(f^{-1}(\overline{fA})^\epsilon) + \epsilon\).
By <cit.>, \({(\overline{fA})}^\epsilon = ({fA})^\epsilon\), and since \(f\) is initial \(f^{-1}(fA)^\epsilon = A^\epsilon\).
Hence, \(\mu(A) \leq \upsilon(A^\epsilon) + \epsilon\).
Therefore, \(d_X^P(\mu,\upsilon) \leq d_Y^P(\ftD f(\mu),\ftD f(\upsilon))\).

§.§ Details of <ref>(<ref>)

For every \(\V\)-category \((X,a)\), the functor
\(
(X,a)\times- \colon\Cats{\V}\to\Cats{\V}
\)
is Kantorovich. Under certain conditions, this functor has a right adjoint
which is Kantorovich as well. To see that, assume now that the underlying
lattice of \(\V\) is Heyting, and we denote the right adjoint of
\(u\wedge- \colon\V\to\V\) by \((-)^{u}\colon\V\to\V\). It has been shown
[8, 9] that \((X,a)\times-\) is left adjoint if and only if, for
all \(x,z\in X\) and \(u,v\in\V\),

For such \(X=(X,a)\), the right adjoint \((-)^{X}\) of \(X\times-\) sends a
\(\V\)-category \(Y=(Y,b)\) to the \(\V\)-category \(Y^{X}=(Y^{X},c)\) with
underlying set

{all \(\V\)-functors \((1,k)\times(X,a)\to(Y,b)\)}

and, for \(h,k\in Y^{X}\),

For a \(\V\)-functor \(f \colon (Y_{1},b_{1})\to(Y_{2},b_{2})\), the
\(\V\)-functor \(f^{X}\colon (Y_{1}^{X},c_{1})\to (Y_{2}^{X},c_{2})\) sends
\(h\in Y_{1}^{X}\) to \(f\cdot h\), moreover, if \(f\) is initial, then, for
all \(h,k\in Y_{1}^{X}\),

\begin{align*}
& =\bigwedge_{x_{1},x_{2}\in X}b_{1}(h(x_{1}),k(x_{2}))^{a(x_{1},x_{2})}       \\
& =\bigwedge_{x_{1},x_{2}\in X}b_{2}(f(h(x_{1})),f(k(x_{2})))^{a(x_{1},x_{2})}
\end{align*}

§.§ Proof of <ref> and <ref>

See proof of <ref>.

§.§ Proof of <ref>

Let \(f \colon (X,a) \to (Z,c)\), \(g \colon (Y,b) \to (Z,c)\) and \(h \colon (X,a) \to (Y,b)\) be \(\V\)-functors such that \(f = g \cdot h\).
If \(f\) is initial, then for all \(x,x' \in X\), \(a(x,x') = b(h(x),h(x'))\).

Let \(x,x' \in X\).
\(a(x,x') \leq b(h(x),h(x')) \leq c(g \cdot h (x),g \cdot h(x')) = c(f(x),f(x')) = a(x,x').\)

Let \(\ftF \colon \Cats{\V}_\sym \to \Cats{\V}_\sym\) be an \(\omega\)-bounded functor that preserves initial morphisms, and let \(\Lambda\) be the set of all finitary predicate liftings for \(\ftF\).
We claim that \(\ftF\) is \(\Lambda\)-Kantorovich.
Suppose that \(X\) is a symmetric \(\V\)-category and \(\fx,\fy\) are elements of \(\ftF X\).
Then, since \(\ftF\) is \(\omega\)-bounded, there is a finite subcategory \(i \colon X_0 \hookrightarrow X\) and \(\fx',\fy' \in \ftF X_0\) such that \(\fx = \ftF i (\fx')\) and \(\fy = \ftF i(\fy')\).
Moreover, given that \(i\) is initial and for every cardinal \(\kappa\) the \(\V\)-category \(\V_s^\kappa\) is injective in \(\Cats{\V}_\sym\) w.r.t. to initial morphisms, every \(\V\)-functor \(f \colon X_0 \to \V^\kappa\) can be factorized as \(\overline{f} \cdot i\), for some \(\V\)-functor \(\overline{f} \colon X \to \V_s^\kappa\).
Hence, for every \(\kappa\)-ary \(\lambda\) in \(\Lambda\), and every \(\V\)-functor \(f \colon X_0 \to \V_s^\kappa\), \(\lambda(f) = \lambda(\overline{f}) \cdot \ftF i\).
Therefore, as the cone of all \(\V\)-functors \(\lambda(f) \colon \ftF X_0 \to \V_s\) determined by each \(\kappa\)-ary \(\lambda\) in \(\Lambda\) and every \(\V\)-functor \(f \colon X_0 \to \V^\kappa\) is initial (see the proof of Theorem <ref>), by Lemma <ref> we obtain

\begin{align*}
\ftF X(\fx,\fy) & = \bigwedge_{\lambda \in \Lambda}\bigwedge_{\overline{f} \colon X \to \V_s^{\ar(\lambda)}} \hom_s(\lambda(\overline{f})(\fx),\lambda(\overline{f})(\fy)) \\
& \geq \bigwedge_{\lambda \in \Lambda}\bigwedge_{g \colon X \to \V_s^{\ar(\lambda)}} \hom_s(\lambda(g)(\fx),\lambda(g)(\fy)),
\end{align*}

where \(\ar(\lambda)\) denotes the arity of the predicate lifting \(\lambda\).