1 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 [2, 6, 14, 24].

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 [33], 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, 38]. Since every lax extension induces a functor lifting in a straightforward way [38] 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 [28, 34]. 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 1 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 (Theorem 3.1).

  • 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 (Theorem 3.9).

  • 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 (Theorem 5.3).

By a recent coalgebraic quantitative Hennessy-Milner theorem that fits this level of generality [12], it follows that given a functor \(\textsf{F}\) 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 (Corollary 5.10). 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 (Theorem 3.18).

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 [34]. Moreover, we do not restrict to symmetric distances, and hence cover also simulation preorders and simulation distances [24].

Fig. 1.
figure 1

Summary of connections (a rigorous categorical interpretation of these connections involves a square of adjunctions (3)).

Full size image

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 [40]. 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, 38]. 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 [39]. There is a line of work on Kantorovich-type coinductive predicates at the level of generality of topological categories [21, 22] (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 [12, 23, 38] by establishing the Kantorovich property they assume.

2 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 3.

2.1 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 [20, 26, 36]. Recall that a coalgebra for a functor \(\textsf{F}:\textsf{C}\rightarrow \textsf{C}\) consists of an object \(X\) of \(\textsf{C}\), thought of as an object of states, and a morphism \(\alpha :X \rightarrow \textsf{F}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 \textsf{C}(X, Y)\) such that \(\beta \cdot f = \textsf{F}f \cdot \alpha \). We will focus on concrete categories over \(\textsf{Set}\), that is categories that come equipped with a faithful functor \({\mathsf {|}{-}\mathsf {|}}:\textsf{C}\rightarrow \textsf{Set}\), which allows speaking about individual states as elements of \({\mathsf {|}{X}\mathsf {|}}\). A lifting of an endofunctor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) to \(\textsf{C}\) is an endofunctor \(\overline{\textsf{F}}:\textsf{C}\rightarrow \textsf{C}\) such that \({\mathsf {|}{-}\mathsf {|}}\cdot \overline{\textsf{F}}= \textsf{F}\cdot {\mathsf {|}{-}\mathsf {|}}\).

Example 2.1

Some functors of interest for coalgebraic modelling are as follows.

  1. 1.

    The finite powerset functor \(\textsf{P}_\omega :\textsf{Set}\rightarrow \textsf{Set}\) maps each set to its finite powerset, and for a map g, \(\textsf{P}_\omega (g)\) takes direct images under g. Given a set \(A\) (of labels), coalgebras for the the functor \(\textsf{P}_\omega (A \times -)\) are finitely branching A-labelled transition systems.

  2. 2.

    The finite distribution functor \(\textsf{D}_\omega :\textsf{Set}\rightarrow \textsf{Set}\) maps a set X to the set \(\textsf{D}_\omega X\) of finitely supported probability distributions on X. Given a finite set \(A\), coalgebras for the functor \((1 + \textsf{D}_\omega )^A\), are probabilistic transition systems [10, 25].

    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 \(\mathfrak {x}\in \textsf{F}X\), there is a finite subset inclusion \(m :A \rightarrow X\) such that \(\mathfrak {x}\) is in the image of \(\textsf{F}m\).

    Standard examples of non-finitary functors are as follows.

  3. 3.

    The (unbounded) powerset functor \(\textsf{P}:\textsf{Set}\rightarrow \textsf{Set}\).

  4. 4.

    The neighbourhood functor \(\textsf{N}:\textsf{Set}\rightarrow \textsf{Set}\) sends a set \(X\) to the set \(\textsf{P}\textsf{P}X\), and a function \(f :X \rightarrow Y\) to the function \(\textsf{N}f :\textsf{N}X \rightarrow \textsf{N}Y\) that assigns to every element \(\mathfrak {x}\in \textsf{N}X\) the set \(\{B \subseteq Y \mid f^{-1} B \in \mathfrak {x}\}\).

2.2 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 \((\mathcal {V},\otimes ,k)\), more precisely a commutative and unital quantale, is a complete lattice \(\mathcal {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 \mathcal {V}\), the map \(u \otimes - :\mathcal {V}\rightarrow \mathcal {V}\) preserves suprema. This entails that every \(u \otimes - \) has a right adjoint \(\hom (u,-) :\mathcal {V}\rightarrow \mathcal {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 \ne \top \), and integral if \(\top = k\).

Example 2.2

  1. 1.

    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 \(\textsf{2}\), the two-element lattice \(\{\bot ,\top \}\) and \(\textsf{1}\), the trivial quantale.

  2. 2.

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

  3. 3.

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

    1. (a)

      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.

    2. (b)

      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.

    3. (c)

      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).

  4. 4.

    Every commutative monoid \((M, \cdot , e)\) generates a quantale on \(\textsf{P}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 \(\mathcal {V}\)-category is pair \((X,a)\) consisting of a set X and a map \(a :X \times X \rightarrow \mathcal {V}\) such that \(k \le a(x,x)\) and \(a(x,y) \otimes a(y,z) \le 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 \(\mathcal {V}\)-category \((X,a)\) is symmetric if \(a(x,y) = a(y,x)\) for all \(x,y \in X\). Every \(\mathcal {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 \(\mathcal {V}\text {-}\textsf{Cat} \rightarrow \textsf{Ord}\). A \(\mathcal {V}\)-category is separated if its natural order is antisymmetric. A \(\mathcal {V}\)-functor \(f :(X,a) \rightarrow (Y,b)\) is a map \(f :X \rightarrow Y\) such that, for all \(x,y \in X\), \( a(x,y) \le b(f(x),f(y)).\) \(\mathcal {V}\)-categories and \(\mathcal {V}\)-functors form the category \(\mathcal {V}\text {-}\textsf{Cat}\), and we denote by \(\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\) the full subcategory of \(\mathcal {V}\text {-}\textsf{Cat}\) determined by the symmetric \(\mathcal {V}\)-categories and by \(\mathcal {V}\text {-}\textsf{Cat}_{\textrm{sym},\textrm{sep}}\) the full subcategory of \(\mathcal {V}\text {-}\textsf{Cat}_{\textrm{sym}}\) determined by the separated symmetric \(\mathcal {V}\)-categories.

Example 2.3

  1. 1.

    The Category \(\textsf{1}\text {-}\textsf{Cat}\) is equivalent to the category \(\textsf{Set}\) of sets and functions.

  2. 2.

    The category \(\textsf{2}\text {-}\textsf{Cat}\) is equivalent to the category \(\textsf{Ord}\) of preordered sets and monotone maps.

  3. 3.

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

    1. (a)

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

    2. (b)

      The category \([0,\infty ]_{\max }\text {-}\textsf{Cat}\) is equivalent to the category \(\textsf{GUMet}\) of generalized ultrametric spaces and non-expansive maps.

    3. (c)

      The category \([0,1]_{\oplus }\text {-}\textsf{Cat}\) is equivalent to the category \(\textsf{BHMet}\) of bounded-by-1 hemimetric spaces and non-expansive maps.

  4. 4.

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

Table 1. \(\mathcal {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.
Full size table

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

A \(\mathcal {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 \(\mathcal {V}\)-category \({(X,a)}^\textrm{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 :X \rightarrow {\mathsf {|}{(X_i,a_i)}\mathsf {|}})_{i\in I}\) of maps into \(\mathcal {V}\)-categories \((X_i,a_i)\), the initial structure \(a :X \times X \rightarrow \mathcal {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) \rightarrow (X_i,a_i))_{i \in I}\) is said to be initial (w.r.t. the forgetful functor \({\mathsf {|}{-}\mathsf {|}} :\mathcal {V}\text {-}\textsf{Cat} \rightarrow \textsf{Set}\)) if \(a\) is the initial structure w.r.t. the structured cone \((X \rightarrow {\mathsf {|}{(X_i,a_i)}\mathsf {|}})_{i \in I}\); a \(\mathcal {V}\)-functor is initial if it forms a singleton initial cone. For every \(\mathcal {V}\)-category \((X,a)\) and every set \(S\), the \(S\)-power \((X,a)^S\) is the \(\mathcal {V}\)-category consisting of the set of all functions from \(S\) to \(X\), equipped with the \(\mathcal {V}\)-category structure \([-,-]\) given by \( [f,g] = \bigwedge _{x \in X} a(f(x),g(x)), \) for all \(f,g :S \rightarrow X\). By equipping its hom-sets with the substructure of the appropriate power, the category \(\mathcal {V}\text {-}\textsf{Cat}\) becames \(\mathcal {V}\text {-}\textsf{Cat}\)-enriched and, hence, also \(\textsf{Ord}\)-enriched w.r.t to the corresponding natural order of \(\mathcal {V}\)-categories. We say that an endofunctor on \(\mathcal {V}\text {-}\textsf{Cat}\) is locally monotone if it preserves this preorder.

Remark 2.4

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

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

Proposition 2.5

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

2.3 Predicate Liftings

Given a cardinal \(\kappa \) and a \(\mathcal {V}\)-category \(X\), a \(\kappa \)-ary \(X\)-valued predicate lifting for a functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) is a natural transformation \( \lambda :\mathcal {V}\text {-}\textsf{Cat}(-,X^\kappa ) \rightarrow \mathcal {V}\text {-}\textsf{Cat}(\textsf{F}-,X). \) When \(\mathcal {V}\) is the trivial quantale, we identify an \(X\)-valued predicate lifting with a natural transformation \( \lambda :\textsf{Set}(-,X^\kappa ) \rightarrow \textsf{Set}(\textsf{F}-,X) \) via the isomorphism \(\textsf{Set}\cong 1\text {-}\textsf{Cat}\). 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.

Remark 2.6

By the Yoneda lemma, every \(\kappa \)-ary \(X\)-valued predicate lifting for a functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat}\rightarrow \mathcal {V}\text {-}\textsf{Cat}\) is determined by a \(\mathcal {V}\)-functor \(\textsf{F}X^\kappa \rightarrow X\). In particular, the collection of all \(X\)-valued \(\kappa \)-ary predicate liftings for a functor is a set.

Example 2.7

  1. 1.

    The Kripke semantics of the standard diamond modality \(\Diamond \) of the modal logic \(K\) is induced (in a way recalled in Section 5) by the unary predicate lifting \(\Diamond _X(A) = \{B \subseteq X \mid A \cap B \ne \varnothing \}\) for the (finite) powerset functor (modulo the isomorphism \(\mathcal {P} X\cong \textsf{Set}(X,\textsf{2})\)).

  2. 2.

    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 \(\textsf{D}_\omega :\textsf{Set}\rightarrow \textsf{Set}\), which we denote by \(\mathbb {E}\).

2.4 Quantale-Enriched Relations and Lax Extensions

The structure of a quantale-enriched category is a particular kind of “enriched relation”. For a quantale \(\mathcal {V}\) and sets X and Y, a \(\mathcal {V}\)-relation from X to Y is a map \(r:X \times Y \rightarrow \mathcal {V}\); we then write . As for ordinary relations, a pair of \(\mathcal {V}\)-relations and 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 \(\mathcal {V}\)-relations between them form a category, denoted \(\mathcal {V}\text {-}\textsf{Rel}\). The identity morphism on a set \(X\) is the \(\mathcal {V}\)-relation that sends every diagonal element to \(k\) and all the others to \(\bot \).

Example 2.8

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

The category \(\mathcal {V}\text {-}\textsf{Rel}\) comes with an involution \( {(-)}^\circ :{\mathcal {V}\text {-}\textsf{Rel}}^\textrm{op}\rightarrow \mathcal {V}\text {-}\textsf{Rel} \) that maps objects identically and sends a \(\mathcal {V}\)-relation to the \(\mathcal {V}\)-relation 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 \(\mathcal {V}\), \(\mathcal {V}\text {-}\textsf{Rel}\) is made into a quantaloid (e.g. [31]), i.e. enriched over complete join semilattices. This entails that there is an optimal way of extending a \(\mathcal {V}\)-relation along a \(\mathcal {V}\)-relation : the (Kan) extension of \(r\) along \(s\) is the \(\mathcal {V}\)-relation defined by the property , for all .

A lax extensionFootnote 1 of a functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) to \(\mathcal {V}\text {-}\textsf{Rel}\) is a lax functor \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Rel} \rightarrow \mathcal {V}\text {-}\textsf{Rel}\) that agrees with \(\textsf{F}\) on sets and whose action on functions is compatible with \(\textsf{F}\). To make the latter requirement precise, we note that a function is interpreted as the \(\mathcal {V}\)-relation that sends every element of its graph to \(k\) and all the others to \(\bot \); then, a lax extension of \(\textsf{F}\) to \(\mathcal {V}\text {-}\textsf{Rel}\), or simply a lax extension, is a map such that:

(L1):

\(r \le r' \implies \widehat{\textsf{F}}r \le \widehat{\textsf{F}}r'\),

(L2):

\(\widehat{\textsf{F}}s\cdot \widehat{\textsf{F}}r\le \widehat{\textsf{F}}(s\cdot r)\),

(L3):

\(\textsf{F}f \le \widehat{\textsf{F}}f\) and \({(\textsf{F}f)}^\circ \le \widehat{\textsf{F}}(f^\circ )\),

for all , and \(f :X \rightarrow Y\).

Example 2.9

The generalized “lower-half” Egli-Milner order between powersets, which for a relation is defined as the relation given by

$$ A (\widehat{\textsf{P}}r) B \iff \forall a \in A.\, \exists b \in B.\, a \mathrel {r} b, $$

defines a lax extension of the powerset functor \(\textsf{P}:\textsf{Set}\rightarrow \textsf{Set}\) to \(\textsf{Rel}\). Similarly, the generalized “upper-half” and the generalized Egli-Milner order define lax extensions of the powerset functor to \(\textsf{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 \( \mathcal {V}\text {-}\textsf{Rel}(\kappa ,X) \rightarrow \mathcal {V}\text {-}\textsf{Rel}(1,\textsf{F}X) \) [16].Footnote 2

Definition 2.10

A \(\kappa \)-ary predicate lifting \(\lambda \) for a functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) is induced by a lax extension \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Rel}\! \rightarrow \! \mathcal {V}\text {-}\textsf{Rel}\) if there is a \(\mathcal {V}\)-relation such that \(\lambda (f) = \widehat{\textsf{F}}f \cdot \mathfrak {r}\), for every \(\mathcal {V}\)-relation .

Example 2.11

By interpreting a subset of a set \(X\) as a relation from \(1\) to \(X\), the unary predicate lifting \(\Diamond \) (see Example 2.7) for the powerset functor \(\textsf{P}:\textsf{Set}\rightarrow \textsf{Set}\) is induced by the lax extension of Example 2.9; indeed, it is determined by the map \(1 \rightarrow \textsf{P}1\) that selects the set \(1\).

Remark 2.12

Every predicate lifting induced by a lax extension is monotone.

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

Definition 2.13

Let \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) be a functor, and \(\varLambda \) a class of monotone predicate liftings for \(\textsf{F}\). The Kantorovich lax extension of \(\textsf{F}\) w.r.t. \(\varLambda \) is the lax extension \( \widehat{\textsf{F}}^\varLambda = \bigwedge _{\lambda \in \varLambda } \widehat{\textsf{F}}^\lambda , \) where for every \(\mathcal {V}\)-relation , the \(\mathcal {V}\)-relation given by .

Example 2.14

The Kantorovich extension of the powerset functor \(\textsf{P}:\textsf{Set}\rightarrow \textsf{Set}\) to \(\textsf{Rel}\) w.r.t the \(\Diamond \) predicate lifting coincides with the extension given by the “lower-half” of the Egli-Milner order (Example 2.9).

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

Theorem 2.15

([16]). Let \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Rel} \rightarrow \mathcal {V}\text {-}\textsf{Rel}\) be a lax extension, and let \(\varLambda \) be the class of all predicate liftings induced by \(\widehat{\textsf{F}}\). Then, \(\widehat{\textsf{F}} = \widehat{\textsf{F}}^\varLambda \).

3 Topological Liftings

It is well-known that every lax extension \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Rel} \rightarrow \mathcal {V}\text {-}\textsf{Rel}\) of a functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) gives rise to a lifting (which we denote by the same symbol) of \(\textsf{F}\) to \(\mathcal {V}\text {-}\textsf{Cat}\) (for instance, see [37]). By definition, liftings are completely determined by their action on objects. In particular, the lifting induced by a lax extension \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Cat}\rightarrow \mathcal {V}\text {-}\textsf{Cat}\) sends a \(\mathcal {V}\)-category \((X,a)\) to the \(\mathcal {V}\)-category \((\textsf{F}X,\widehat{\textsf{F}}a)\). Of course, it does not make sense to talk about functor liftings to the category \(\mathcal {V}\text {-}\textsf{Cat}\) when \(\mathcal {V}\) is trivial, hence we assume from now on that \(\mathcal {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, 29]: To lift a functor \(\textsf{G}:\textsf{A}\rightarrow \textsf{Y}\) along a topological functor \({\mathsf {|}{-}\mathsf {|}} :\textsf{B}\rightarrow \textsf{Y}\), it is enough to give, for every object \(A\) in \(\textsf{A}\), a structured cone

$$\begin{aligned} \mathcal {C}(A)=(\textsf{G}A\xrightarrow {h}{\mathsf {|}{B}\mathsf {|}})_{h,B} \end{aligned}$$
(1)

so that, for every \(h\) in \(\mathcal {C}(A)\) and every \(f :A'\rightarrow A\), the composite \(h\cdot \textsf{G}f\) belongs to the cone \(\mathcal {C}(A')\). Then, for an object \(A\) in \(\textsf{A}\), one defines \(\textsf{G}^I A\) by equipping \(\textsf{G}A\) with the initial structure w.r.t. the structured cone (1). It is easy to see that the assignment \( X \mapsto \textsf{G}^I X \) indeed defines a functor \(\textsf{G}^I :\textsf{A}\rightarrow \textsf{B}\) such that \({\mathsf {|}{-}\mathsf {|}}\cdot \textsf{G}^{I}=\textsf{G}\). This technique has been previously applied in the context of codensity liftings [19, 21, 22, 35] and Kantorovich liftings [5]. We apply this to our situation as follows. Given a functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\), take \(\textsf{G}=\textsf{F}\cdot {\mathsf {|}{-}\mathsf {|}}\); then a lifting of \(\textsf{F}\) to \(\mathcal {V}\text {-}\textsf{Cat}\) can be specified by a class of natural transformations

$$\begin{aligned} \lambda :\mathcal {V}\text {-}\textsf{Cat}(-,A_\lambda ) \longrightarrow \textsf{Set}(\textsf{F}{\mathsf {|}{-}\mathsf {|}},{\mathsf {|}{B_\lambda }\mathsf {|}}), \end{aligned}$$
(2)

(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 \(\mathcal {V}\)-category \(X\), we consider the structured cone consisting of all maps

$$ \lambda (f) :\textsf{F}{\mathsf {|}{X}\mathsf {|}} \longrightarrow {\mathsf {|}{B_\lambda }\mathsf {|}} $$

where \(\lambda \) ranges over the given natural transformations and f over all \(\mathcal {V}\)-functors \(X \rightarrow A_\lambda \). As described above, we obtain a \(\mathcal {V}\)-category \(\textsf{F}^I X\) by equipping \(\textsf{F}|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 (2) to be the \(\mathcal {V}\)-category \((\mathcal {V},\hom )\):

Theorem 3.1

Every lifting of a \(\textsf{Set}\)-functor to \(\mathcal {V}\text {-}\textsf{Cat}\) is topological w.r.t. a class of natural transformations \( \lambda :\mathcal {V}\text {-}\textsf{Cat}(-,A_\lambda ) \longrightarrow \textsf{Set}(\textsf{F}{\mathsf {|}{-}\mathsf {|}},{\mathsf {|}{\mathcal {V}}\mathsf {|}}). \)

In examples, we usually construct a generalized predicate lifting (2) from a \(\kappa \)-ary predicate lifting \(\lambda \) for the set functor \(\textsf{F}\): Choose a pair \((A,B)\) of \(\mathcal {V}\)-categories over the sets \(\mathcal {V}^\kappa \) and \(\mathcal {V}\), respectively (the above theorem allows restricting to \(B=\mathcal {V}\), and the examples we present are of this kind). We can then precompose \(\lambda \) with the inclusion natural transformation \(\mathcal {V}\text {-}\textsf{Cat}(-,A) \longrightarrow \textsf{Set}({\mathsf {|}{-}\mathsf {|}},{\mathsf {|}{A}\mathsf {|}})\), obtaining a natural transformation \(\lambda ^{(A,B)} :\mathcal {V}\text {-}\textsf{Cat}(-,A) \rightarrow \textsf{Set}(\textsf{F}{\mathsf {|}{-}\mathsf {|}},{\mathsf {|}{B}\mathsf {|}})\) that applies \(\lambda \) to maps underlying \(\mathcal {V}\)-functors with codomain \(A\).

Example 3.2

  1. 1.

    The discrete lifting of the identity functor \(\textsf{Id}:\textsf{Set}\rightarrow \textsf{Set}\), which sends every \(\mathcal {V}\)-category to the discrete \(\mathcal {V}\)-category with the same underlying set, can be obtained as a topological lifting constructed from the identity \(\mathcal {V}\)-valued predicate lifting for \(\textsf{Id}\) by choosing \(A\) to be the \(\mathcal {V}\)-category consisting of the set \(\mathcal {V}\) equipped with the indiscrete structure.

  2. 2.

    The lifting of the identity functor \(\textsf{Id}:\textsf{Set}\rightarrow \textsf{Set}\) to \(\textsf{Ord}\) that computes the smallest equivalence relation that contains a given preorder can be obtained as a topological lifting constructed from the \(\textsf{2}\)-valued identity predicate lifting for \(\textsf{Id}\) by choosing \(A\) to be the discrete preordered set with two elements.

  3. 3.

    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 :X \rightarrow [0,1]} \mathbb {E}_X(f)(\upsilon ) \ominus \mathbb {E}_X(f)(\mu )\) (see Example 2.7(2)). Therefore, the total variation distance defines a lifting of the finite distribution functor to \(\textsf{BHMet}\) 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 \(\textsf{BHMet}\) (see Example 3.5) and the discrete lifting of the identity functor to \(\textsf{BHMet}\). By Theorem 3.9 below, precomposing functor liftings with the discrete lifting of the identity functor can be used to derive non-Kantorovich liftings.

Remark 3.3

Theorem 3.1 can be fine-tuned to show that the discrete lifting \(\textsf{F}^d :\textsf{Ord}\rightarrow \textsf{Ord}\) of a finitary functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) is a topological lifting constructed from a set \(\varLambda \) of finitary \(2\)-valued predicate liftings for \(\textsf{F}\). Hence, for every set \(X\), considered as a discrete preordered set, we have that the cone of all maps \( \lambda (f) :\textsf{F}^d(X,1_X) \rightarrow 2, \) for \(\kappa \)-ary predicate liftings \(\lambda \in \varLambda \) and maps \(X \rightarrow 2^\kappa \), is initial. Thus, as \(\textsf{F}^d(X,1_X)\) is antisymmetric, this cone is mono. In this sense, our results subsume the result that every finitary \(\textsf{Set}\)-functor admits a separating set of finitary predicate liftings [34].

3.1 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 (2) are of the shape \( \lambda :\mathcal {V}\text {-}\textsf{Cat}(-,\mathcal {V}^\kappa ) \longrightarrow \textsf{Set}(\textsf{F}{\mathsf {|}{-}\mathsf {|}},{\mathsf {|}{\mathcal {V}}\mathsf {|}}) \), and thus employ \(\mathcal {V}\), equipped with its standard \(\mathcal {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 5). Many functor liftings considered in work on coalgebraic behavioural distance can be understood as topological liftings constructed in this way (e.g. [5, 12, 22, 38, 39]). To simplify notation, in the sequel we often omit the forgetful functor to \(\textsf{Set}\).

Definition 3.4

Let \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) be a functor and \(\varLambda \) a class of \(\mathcal {V}\)-valued predicate liftings for \(\textsf{F}\). The Kantorovich lifting of \(\textsf{F}\) w.r.t. \(\varLambda \) is the topological lifting \(\textsf{F}^\varLambda :\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) that sends a \(\mathcal {V}\)-category \(X\) to the \(\mathcal {V}\)-category \((\textsf{F}X, \textsf{F}^\varLambda a)\), where \(\textsf{F}^\varLambda a\) denotes the initial structure on \(\textsf{F}X\) w.r.t. the structured cone of all functions

$$ \lambda (f) :\textsf{F}{\mathsf {|}{X}\mathsf {|}} \longrightarrow {\mathsf {|}{\mathcal {V}}\mathsf {|}} $$

where \(\lambda \in \varLambda \) is \(\kappa \)-ary and \(f :(X,a) \rightarrow \mathcal {V}^\kappa \) is a \(\mathcal {V}\)-functor. Generally, a lifting \(\mathsf {\overline{F}}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) of \(\textsf{F}\) is Kantorovich if \(\mathsf {\overline{F}}=\textsf{F}^\varLambda \) some class \(\varLambda \) of predicate liftings for \(\textsf{F}\).

Example 3.5

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 \(\textsf{Set}\) to the category \(\textsf{BHMet}\) w.r.t the predicate lifting \(\mathbb {E}\) that computes expected values, i.e. \(\textsf{D}_\omega ^\mathbb {E}(X,a)(\mu ,\upsilon ) = \bigvee _{f :(X,a) \rightarrow [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 \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) and a quantale \(\mathcal {V}\). Consider the partially ordered conglomerate \(\mathsf {Pred(\textsf{F})}\) of classes of \(\mathcal {V}\)-valued predicate liftings for \(\textsf{F}\) ordered by containment, i.e. \( \varLambda \le \varLambda ' \iff \varLambda \supseteq \varLambda '; \) and the partially ordered class \(\mathsf {Lift(\textsf{F})}\) of liftings of \(\textsf{F}\) to \(\mathcal {V}\text {-}\textsf{Cat}\) ordered pointwise, i.e. \( \mathsf {\overline{F}}\le \mathsf {\overline{F}}' \iff \mathsf {\overline{F}}a \le \mathsf {\overline{F}}' a, \) for every \(\mathcal {V}\)-category \((X,a)\).

Definition 3.6

Let \(\mathsf {\overline{F}}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) be a lifting of \(\textsf{F}\). A \(\kappa \)-ary \(\mathcal {V}\)-valued predicate lifting \(\lambda \) for \(\textsf{F}\) is compatible with \(\mathsf {\overline{F}}\) if it restricts to a predicate lifting for \(\mathsf {\overline{F}}\):

figure v

where the vertical arrows denote set inclusions – that is, if \(\lambda \) lifts \(\mathcal {V}\)-functorial predicates on X to \(\mathcal {V}\)-functorial predicates on \(\mathsf {\overline{F}}X\). The class of all predicate liftings compatible with \(\mathsf {\overline{F}}\) is denoted by \(\textsf{P}(\mathsf {\overline{F}})\).

Proposition 3.7

A \(\kappa \)-ary \(\mathcal {V}\)-valued predicate lifting \(\lambda \) for \(\textsf{F}\) is compatible with \(\mathsf {\overline{F}}\) iff the map \(\lambda (1_{{\mathsf {|}{\mathcal {V}^\kappa }\mathsf {|}}}) :\textsf{F}({\mathsf {|}{\mathcal {V}^\kappa }\mathsf {|}}) \rightarrow {\mathsf {|}{\mathcal {V}}\mathsf {|}}\) is a \(\mathcal {V}\)-functor of type \(\mathsf {\overline{F}}\mathcal {V}^\kappa \rightarrow \mathcal {V}\).

The Kantorovich lifting defines a universal construction:

Theorem 3.8

Let \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) be a functor. Assigning to a class of predicate liftings for \(\textsf{F}\) the corresponding Kantorovich lifting yields a right adjoint \(\textsf{F}^{(-)} :\mathsf {Pred(\textsf{F})}\rightarrow \mathsf {Lift(\textsf{F})}\) whose left adjoint \(\textsf{P}:\mathsf {Lift(\textsf{F})}\rightarrow \mathsf {Pred(\textsf{F})}\) maps a lifting of \(\textsf{F}\) to the class \(\textsf{P}(\mathsf {\overline{F}})\) of all \(\mathcal {V}\)-valued predicate liftings for \(\textsf{F}\) 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, 12, 22, 40]).

Theorem 3.9

A lifting of a \(\textsf{Set}\)-functor to \(\mathcal {V}\text {-}\textsf{Cat}\) is Kantorovich iff it preserves initial morphisms.

Corollary 3.10

Every topological lifting of a functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) w.r.t. a class of natural transformations \(\lambda :\mathcal {V}\text {-}\textsf{Cat}(-,A_\lambda ) \rightarrow \textsf{Set}(\textsf{F}-, {\mathsf {|}{B_\lambda }\mathsf {|}})\) where each \(A_\lambda \) is injective in \(\mathcal {V}\text {-}\textsf{Cat}\) w.r.t. initial morphisms is Kantorovich.

Corollary 3.11

The composite of Kantorovich liftings is Kantorovich.

Example 3.12

The characterization of Theorem 3.9 makes it easy to distinguish Kantorovich liftings.

  1. 1.

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

  2. 2.

    The identity functor on \(\textsf{Set}\) has a lifting \( (-)^\circ :\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat} \) that sends every \(\mathcal {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 \(\mathcal {V}\)-valued predicate liftings determined by the representable \(\mathcal {V}\)-functors \(\mathcal {V}^\textrm{op}\rightarrow \mathcal {V}\).

  3. 3.

    The functor \((-)_s :\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\) that symmetrizes \(\mathcal {V}\)-categories gives rise to a lifting \((-)_s :\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) of the identity functor on \(\textsf{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 \(\mathcal {V}\)-valued predicate liftings determined by the representable \(\mathcal {V}\)-functors \(\mathcal {V}_s \rightarrow \mathcal {V}\).

  4. 4.

    The discrete lifting of the identity functor on \(\textsf{Set}\) to \(\mathcal {V}\text {-}\textsf{Cat}\) is not Kantorovich, as it fails to preserve initial morphisms.

  5. 5.

    The lifting of the identity functor on \(\textsf{Set}\) to \(\mathcal {V}\text {-}\textsf{Cat}\) that sends a \(\mathcal {V}\)-category \((X,a)\) to the \(\mathcal {V}\)-category given by the final structure w.r.t. the structured cospan of identity maps \({\mathsf {|}{(X,a)}\mathsf {|}} \rightarrow X \leftarrow {\mathsf {|}{(X,a^\circ )}\mathsf {|}}\) is not Kantorovich. This lifting generalizes Example 3.2(2).

  6. 6.

    The lifting of the finite distribution functor on \(\textsf{Set}\) to \(\textsf{BHMet}\) given by the Kantorovich distance is Kantorovich, while the lifting given by the total variation distance is not Kantorovich.

3.2 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.

Theorem 3.13

Let \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) be a lifting of a functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) induced by a lax extension \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Rel} \rightarrow \mathcal {V}\text {-}\textsf{Rel}\). If \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Rel} \rightarrow \mathcal {V}\text {-}\textsf{Rel}\) is the Kantorovich extension w.r.t. a class \(\varLambda \) of predicate liftings, then the functor \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) is the Kantorovich lifting of \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) w.r.t. \(\varLambda \).

Let \(\mathsf {Lax(\textsf{F})}\) denote the partially ordered class of lax extensions of a functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) to \(\mathcal {V}\text {-}\textsf{Rel}\) ordered pointwise:

$$ \widehat{\textsf{F}}\le \widehat{\textsf{F}}' \iff \forall r \in \mathcal {V}\text {-}\textsf{Rel}. \; \widehat{\textsf{F}}r \le \widehat{\textsf{F}}' r; $$

let \(\mathsf {Lift(\textsf{F})_I}\) denote the partially ordered subclass of \(\mathsf {Lift(\textsf{F})}\) consisting of the liftings that preserve initial morphisms, and let \(\mathsf {Pred(\textsf{F})_M}\) denote the partially ordered subconglomerate of \(\mathsf {Pred(\textsf{F})}\) of monotone predicate liftings. Clearly, the operations of taking Kantorovich extensions \( \widehat{\textsf{F}}^{(-)} :\mathsf {Pred(\textsf{F})_M}\rightarrow \mathsf {Lax(\textsf{F})}, \) and inducing liftings from lax extensions \( \textsf{I}:\mathsf {Lax(\textsf{F})}\rightarrow \mathsf {Lift(\textsf{F})_I}\) define monotone maps. Moreover, as we have seen in Theorem 3.9, the monotone map \(\textsf{F}^{(-)} :\mathsf {Pred(\textsf{F})}\rightarrow \mathsf {Lift(\textsf{F})}\) corestricts to \(\mathsf {Lift(\textsf{F})_I}\). Therefore, our results so far tell us that lax extensions, liftings and predicate liftings are connected through a diagram of monotone maps

figure w

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 \(\widehat{\textsf{F}}^{(-)} :\mathsf {Pred(\textsf{F})_M}\rightarrow \mathsf {Lax(\textsf{F})}\) 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 (Definition 2.10) – in general does not define a monotone map \(\mathsf {Lax(\textsf{F})}\rightarrow \mathsf {Pred(\textsf{F})_M}\). 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.

Example 3.14

The identity functor on \(\textsf{Ord}\) is the lifting induced by the identity functor on \(\textsf{Rel}\) as a lax extension of the identity functor on \(\textsf{Set}\). The constant map into \(\top \) is a monotone map \(2 \rightarrow 2\) and, hence, determines a predicate lifting that is compatible with the identity functor on \(\textsf{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 \(\textsf{Rel}\) [16, Example 3.12].

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 \(\textsf{P}:\mathsf {Lift(\textsf{F})_I}\rightarrow \mathsf {Pred(\textsf{F})}\) does not necessarily corestrict to \(\mathsf {Pred(\textsf{F})_M}\).

Example 3.15

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

Accordingly, we need to “filter the monotone predicate liftings” first. This operation trivially defines the left adjoint \( \textsf{M}:\mathsf {Pred(\textsf{F})}\rightarrow \mathsf {Pred(\textsf{F})_M}\) of the inclusion map \(\mathsf {Pred(\textsf{F})_M}\hookrightarrow \mathsf {Pred(\textsf{F})}\).

Theorem 3.16

Let \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) be a functor. The monotone map \(\textsf{I}:\mathsf {Lax(\textsf{F})}\rightarrow \mathsf {Lift(\textsf{F})_I}\) is order-reflecting and right adjoint to the monotone map \(\widehat{\textsf{F}}^{\textsf{M}\textsf{P}(-)} :\mathsf {Lift(\textsf{F})_I}\rightarrow \mathsf {Lax(\textsf{F})}\).

Corollary 3.17

Let \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) be a functor. The monotone map \(\widehat{\textsf{F}}^{(-)} :\mathsf {Pred(\textsf{F})_M}\rightarrow \mathsf {Lax(\textsf{F})}\) is right adjoint to the order-reflecting monotone map \(\textsf{M}\textsf{P}\textsf{I}:\mathsf {Lax(\textsf{F})}\rightarrow \mathsf {Pred(\textsf{F})_M}\).

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

figure x

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

Theorem 3.18

A lifting \(\widehat{\textsf{F}}\) of a \(\textsf{Set}\)-functor \(\textsf{F}\) to \(\mathcal {V}\text {-}\textsf{Cat}\) is induced by a lax extension of \(\textsf{F}\) to \(\mathcal {V}\text {-}\textsf{Rel}\) iff \(\widehat{\textsf{F}}\) preserves initial morphisms and is locally monotone.

\(\mathcal {V}\)-enriched lax extensions have proved to be crucial to deduce quantitative van Benthem and Hennessy-Milner theorems [38, 39]. We recall that a lax extension of a functor \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) to \(\mathcal {V}\text {-}\textsf{Rel}\) is \(\mathcal {V}\)-enriched [16, 39] if, for all \(u \in \mathcal {V}\), \(u \otimes 1_{\textsf{F}X} \le \widehat{\textsf{F}}(u \otimes 1_X)\); where \(u \otimes r\) denotes the \(\mathcal {V}\)-relation “\(r\) scaled by \(u\)”, that is, \((u \otimes r)(x,y) = u \otimes r(x,y)\).

Theorem 3.19

A lifting \(\widehat{\textsf{F}}\) of a \(\textsf{Set}\)-functor \(\textsf{F}\) to \(\mathcal {V}\text {-}\textsf{Cat}\) is induced by a \(\mathcal {V}\)-enriched lax extension of \(\textsf{F}\) to \(\mathcal {V}\text {-}\textsf{Rel}\) iff \(\widehat{\textsf{F}}\) preserves initial morphisms and is \(\mathcal {V}\text {-}\textsf{Cat}\)-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 3.18 that the liftings \((-)^\circ :\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) and \((-)_s :\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) (see Example 3.12) of the identity functor on \(\textsf{Set}\) to \(\mathcal {V}\text {-}\textsf{Cat}\) 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.

4 Behavioural Distance

One main motivation for lifting functors to metric spaces was to obtain coalgebraic notions of behavioural distance [5, 38]. Indeed, every functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat}\rightarrow \mathcal {V}\text {-}\textsf{Cat}\) gives rise to a notion of distance on a \(\textsf{F}\)-coalgebras:

Definition 4.1

[12] Let \((X,a,\alpha )\) be a coalgebra for a functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\). The behavioural distance \(\textrm{bd}_\alpha ^\textsf{F}(x,y)\) of \(x,y \in X\) is

$$\begin{aligned} \textrm{bd}_\alpha ^\textsf{F}(x,y) = \bigvee \{b(f(x),f(y)) \mid f :(X,a,\alpha ) \rightarrow (Y,b,\beta ) \in \textsf{CoAlg}(\textsf{F})\}. \end{aligned}$$
(4)

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 \(\textsf{Set}\)-based coalgebras. Let \(\textsf{F}:\textsf{Set}\rightarrow \textsf{Set}\) be a functor. A Kantorovich lifting \(\textsf{F}^\varLambda :\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) induces a notion of behavioural distance on an \(\textsf{F}\)-coalgebra \(\alpha :X \rightarrow \textsf{F}X\) as the greatest \(\mathcal {V}\)-categorical structure \((X,a)\) that makes \(\alpha \) a \(\mathcal {V}\)-functor of type \((X,a) \rightarrow \textsf{F}^\varLambda (X,a)\) [5, 22]. From Theorem 3.9 and [12, Proposition 12] (generalized to \(\mathcal {V}\text {-}\textsf{Cat}\), with the same proof), we obtain that this distance coincides with behavioural distance as defined above. On the other hand, every lax extension \(\widehat{\textsf{F}}:\mathcal {V}\text {-}\textsf{Rel} \rightarrow \mathcal {V}\text {-}\textsf{Rel}\) of \(\textsf{F}\) also induces a behavioural distance on an \(\textsf{F}\)-coalgebra \(\alpha :X \rightarrow \textsf{F}X\) as the greatest simulation on \(\alpha \) [13, 32, 38, 40], i.e. the greatest \(\mathcal {V}\)-relation such that \(\alpha \cdot s \le \widehat{\textsf{F}}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 3.13 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. [22]. 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 \(\textsf{N}:\textsf{Set}\rightarrow \textsf{Set}\) does not admit a lax extension to \(\textsf{Rel}\) that preserves converses (\(\widehat{\textsf{F}}(r^\circ ) = (\widehat{\textsf{F}}r)^\circ \)) whose (\(\textsf{2}\)-valued) notion of behavioural distance coincides with behavioural equivalence [27, Theorem 12]. However, from [12, Theorem 34, Proposition A.6] (see also [17]), we can conclude that the (\(\textsf{2}\)-valued) notion of behavioural distance defined by the canonical Kantorovich lifting of \(\textsf{N}\) to \(\textsf{Equ}\) w.r.t. to the predicate lifting induced by the identity natural transformation \(\textsf{N}\rightarrow \textsf{N}\) coincides with behavioural equivalence. (It is easy to see that Marti and Venema’s result holds even if one allows lax extensions of \(\textsf{N}\) that do not preserve converses, and that the situation remains the same in the asymmetric case.)

5 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 \(\mathcal {V}\)-categories. Therefore, we interpret the \(\mathcal {V}\)-categorical notions and results also with \(\mathcal {V}\text {-}\textsf{Cat}_{\textrm{sym}}\) instead of \(\mathcal {V}\text {-}\textsf{Cat}\) and \(\mathcal {V}_{s}\) instead of \(\mathcal {V}\).

We recall a variant [12] of (quantitative) coalgebraic logic [7, 23, 28, 34, 38] that follows the paradigm of interpreting modalities via predicate liftings, in this case of \(\mathcal {V}\)-valued predicates for a \(\mathcal {V}\text {-}\textsf{Cat}\)-functor (Section 2.3). Let \(\varLambda \) be a set of finitary predicate liftings for a functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\rightarrow \mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\). The syntax of quantitative coalgebraic modal logic is then defined by the grammar

$$\begin{aligned}{} & {} \phi :\,\!:=\top \mid \phi _1 \vee \phi _2 \mid \phi _1 \wedge \phi _2 \mid u \otimes \phi \mid \hom _s(u,\phi ) \mid \lambda (\phi _1,\dots ,\phi _n){} & {} (u \in \mathcal {V}, \lambda \in \varLambda ) \end{aligned}$$

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

The semantics is given by assigning to each formula \(\phi \in \mathcal {L}(\varLambda )\) and each coalgebra \(\alpha :X \rightarrow \textsf{F}X\) the interpretation of \(\phi \) over \(\alpha \), i.e. the \(\mathcal {V}\)-functor \(\llbracket {\phi }\rrbracket _\alpha :X \rightarrow \mathcal {V}\) recursively defined as follows:

  • for \(\phi = \top \), we take \(\llbracket {\top }\rrbracket _\alpha \) to be the \(\mathcal {V}\)-functor given by the constant map into \(\top \);

  • for an n-ary propositional operator p, we put \(\llbracket {p(\phi _1, \ldots , \phi _n)}\rrbracket _\alpha = p (\llbracket {\phi _1}\rrbracket _\alpha , \ldots , \llbracket {\phi _n}\rrbracket _\alpha )\), with p interpreted using the lattice structure of \(\mathcal {V}\) and the \(\mathcal {V}\)-categorical structure \(\hom _s\) of \(\mathcal {V}_s\), respectively, on the right-hand side;

  • for \(n\)-ary \(\lambda \in \varLambda \), we put \(\llbracket {\lambda (\phi _1, \ldots , \phi _n)}\rrbracket _\alpha = \lambda (\langle \llbracket {\phi _1}\rrbracket _\alpha , \ldots , \llbracket {\phi _n}\rrbracket _\alpha \rangle ) \cdot \alpha \), where \(\langle \llbracket {\phi _1}\rrbracket _\alpha , \ldots , \llbracket {\phi _n}\rrbracket _\alpha \rangle \) denotes the \(\mathcal {V}\)-functor \((X,a)\rightarrow \mathcal {V}^n\) canonically determined by \(\llbracket {\phi _1}\rrbracket _\alpha , \ldots , \llbracket {\phi _n}\rrbracket _\alpha \).

We then obtain a notion of logical distance:

Definition 5.1

Let \(\varLambda \) be a set of predicate liftings for a functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\). The logical distance \(ld_\alpha ^\varLambda \) on an \(\textsf{F}\)-coalgebra \((X,a,\alpha )\) is the initial structure on \(X\) w.r.t. the structured cone of all maps \( \llbracket {\phi }\rrbracket _\alpha :X \rightarrow {\mathsf {|}{(\mathcal {V},\hom _s)}\mathsf {|}} \) with \(\phi \in \mathcal {L}(\varLambda )\). More explicitly, for all \(x,y \in X\),

$$\begin{aligned}\textstyle ld_\alpha ^\varLambda (x,y) = \bigwedge \{\hom _s(\llbracket {\phi }\rrbracket _\alpha (x),\llbracket {\phi }\rrbracket _\alpha (y)) \mid \phi \in \mathcal {L}(\varLambda )\}. \end{aligned}$$

In the remainder of the paper, we establish criteria under which a \(\mathcal {V}\text {-}\textsf{Cat}_\textrm{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 ^\varLambda \le \textrm{bd}_\alpha ^\textsf{F}\), for every \(\textsf{F}\)-coalgebra \((X,\alpha )\). (It is easy to show that the reverse inequality holds universally [12, Theorem 16]).

Existing expressivity results for quantitative coalgebraic logics for \(\textsf{Set}\)-functors depend crucially on Kantorovich liftings (e.g. [12, 22, 38, 39]). However, it has been shown [12] that the Kantorovich property can be usefully detached from the notion of functor lifting.

Definition 5.2

Let \(\varLambda \) be a class of predicate liftings for a functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\). The functor \(\textsf{F}\) is \(\varLambda \)-Kantorovich if for every \(\mathcal {V}\)-category \(X\), the cone of all \(\mathcal {V}\)-functors \( \lambda (f) :\textsf{F}X \rightarrow \mathcal {V}\), with \(\lambda \in \varLambda \) \(\kappa \)-ary and \(f \in \mathcal {V}\text {-}\textsf{Cat}(X,\mathcal {V}^\kappa )\), is initial. A functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat} \rightarrow \mathcal {V}\text {-}\textsf{Cat}\) is said to be Kantorovich if it is \(\varLambda \)-Kantorovich for some class \(\varLambda \) of predicate liftings for \(\textsf{F}\).

Clearly, every Kantorovich lifting of a \(\textsf{Set}\)-functor to \(\mathcal {V}\text {-}\textsf{Cat}\) w.r.t. a class \(\varLambda \) of predicate liftings is \(\varLambda \)-Kantorovich. Moreover, Theorem 3.9 is easily generalized to Kantorovich functors.

Theorem 5.3

A \(\mathcal {V}\text {-}\textsf{Cat}\)-functor is Kantorovich iff it preserves initial morphisms.

Theorem 5.4

A \(\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\)-functor is Kantorovich iff it preserves initial morphisms.

Example 5.5

  1. 1.

    The inclusion functor \(\mathcal {V}\text {-}\textsf{Cat}_{\textrm{sym},\textrm{sep}} \hookrightarrow \mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\) has a left adjoint \((-)_q :\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\rightarrow \mathcal {V}\text {-}\textsf{Cat}_{\textrm{sym},\textrm{sep}}\) that quotients every \(X\) by its natural preorder, which for symmetric X is an equivalence, and gives rise to a Kantorovich functor on \(\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\).

  2. 2.

    Given a bounded-by-\(1\) pseudometric space \((X,d)\), i.e. an object of \([0,1]_\oplus \text {-}\textsf{Cat}_\textrm{sym}\simeq \textsf{BPMet}\), the Prokhorov distance [30] 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) \le \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) \le \epsilon \}\). It is straightforward to verify that this distance defines a \(\textsf{BPMet}\)-functor (which acts on morphisms by measuring preimages) that preserves isometries and, therefore, it is Kantorovich.

  3. 3.

    For every \(\mathcal {V}\)-category \((X,a)\), the functor \( (X,a)\times - :\mathcal {V}\text {-}\textsf{Cat}\rightarrow \mathcal {V}\text {-}\textsf{Cat} \) is Kantorovich. If the underlying lattice of \(\mathcal {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 \(\mathcal {V}\)-category \(Y=(Y,b)\) to the \(\mathcal {V}\)-category \(Y^{X}=(Y^{X},c)\) with underlying set \( \{\text {all }\mathcal {V}\text {-functors }(1,k)\times (X,a)\rightarrow (Y,b)\} \) and, for \(h,k\in Y^{X}\),

    $$\begin{aligned}\textstyle c(h,k)=\bigwedge _{x_{1},x_{2}\in X}b(h(x_{1}),k(x_{2}))^{a(x_{1},x_{2})}, \end{aligned}$$

    where \((-)^{u}:\mathcal {V}\rightarrow \mathcal {V}\) denotes the right adjoint of \(u\wedge - :\mathcal {V}\rightarrow \mathcal {V}\). For a \(\mathcal {V}\)-functor \(f :(Y_{1},b_{1})\rightarrow (Y_{2},b_{2})\), the \(\mathcal {V}\)-functor \(f^{X}:(Y_{1}^{X},c_{1})\rightarrow (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:

Definition 5.6

A functor \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\rightarrow \mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\) is \(\omega \)-bounded if for every symmetric \(\mathcal {V}\)-category X and every \(t\in \textsf{F}X\), there exists a finite subcategory \(X_0\subseteq X\) and \(t'\in \textsf{F}X_0\) such that \(t=\textsf{F}i(t')\) where i is the inclusion \(X_0\rightarrow X\).

Example 5.7

Every lifting of a finitary \(\textsf{Set}\)-functor to \(\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\) is \(\omega \)-bounded.

Proposition 5.8

Let \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\rightarrow \mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\) be a Kantorovich functor. If \(\textsf{F}\) is \(\omega \)-bounded, then \(\textsf{F}\) is Kantorovich w.r.t. a set of finitary predicate liftings.

Finally, from [12, Theorem 31] we obtain:

Corollary 5.9

Let \(\mathcal {V}\) be a finite quantale, and let \(\textsf{F}:\mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\rightarrow \mathcal {V}\text {-}\textsf{Cat}_\textrm{sym}\) be a lifting of a finitary functor that preserves initial morphisms. Then there is a set \(\varLambda \) of predicate liftings for \(\textsf{F}\) of finite arity such that the coalgebraic logic \(\mathcal {L}(\varLambda )\) is expressive.

Corollary 5.10

Let \(\textsf{F}:\textsf{BPMet}\rightarrow \textsf{BPMet}\) be a functor that preserves isometries, is locally non-expansive, and admits a dense \(\omega \)-bounded subfunctor. Then there is a set \(\varLambda \) of predicate liftings for \(\textsf{F}\) of finite arity such that the coalgebraic logic \(\mathcal {L}(\varLambda )\) is expressive.

These instantiate to results on concrete system types, e.g. ones induced by (sub)functors listed in Example 5.5, 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 5.5(2)) determined by the closure of the set of finitely supported probability measures.

6 Conclusions and Future Work

Quantitative coalgebraic Hennessy-Milner theorems [12, 23, 38] 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 distance.

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.