A point-free perspective on lax extensions and predicate liftings

Abstract

Lax extensions of set functors play a key role in various areas, including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is induced by a class of predicate liftings; we discuss several implications of this result.

1. Introduction

A lax extension of a given $\mathsf{Set}$ -functor $\mathsf{F}$ acts on relations in a way that is (laxly) compatible on the one hand with the action of $\mathsf{F}$ on sets and maps and on the other hand with the algebraic structure on relations, in particular composition. Lax extensions are a well-established tool in mathematics and computer science. For example, they are essential in the theory of monoidal topology to encode the type of a space (Hofmann et al. 2014); and in the theory of coalgebras, they encode the type of a simulation (Hughes and Jacobs 2004) as well as the type of a cover modality, in the semantics of Moss-type coalgebraic logics (Marti and Venema 2015).

A more expressive form of coalgebraic modal logic is based on the notion of predicate lifting, which allows capturing the standard syntax and semantics of many forms of modal logic found in the literature in a uniform fashion (Cîrstea et al. 2011). The connection between the two approaches to coalgebraic modal logic is governed by the connection between lax extensions and predicate liftings. Special predicate liftings, the so-called Moss liftings, can be extracted from the Barr extension (Kurz and Leal 2009; Leal 2008). This principle has been extended to a large class of lax extensions (Marti and Venema 2015) and further to the quantative setting (Wild and Schröder 2020). Conversely, lax extensions can be constructed from predicate liftings using the so-called Kantorovich extension (Wild and Schröder 2020), even in quantalic generality (Wild and Schröder 2021). Finally, Moss liftings and the Kantorovich extension lead to a representation theorem (see Theorem 1 below) for specific “fuzzy” (i.e., [0,1]-valued) lax extensions (Wild and Schröder 2020), which is instrumental in deriving a quantitative Hennessy–Milner-type theorem stating essentially that behavioral distance on coalgebraic systems coincides with logical distance under suitable bounding assumptions on the functor (Forster et al. 2023; König and Mika-Michalski 2018; Wild and Schröder 2022).

Although lax extensions apply to relations, the connection between lax extensions and predicate liftings has previously been expressed primarily in the language of functions. In contrast, the cornerstone of the present work is the principle that the connection between lax extensions and predicate liftings is best expressed in the language of relations. More specifically, we work in the language of quantale-enriched relations as a way of unifying the work developed in the classical setting and the emerging work in quantitative settings.

1.1 Main contributions

The main contribution of this paper is to show that every quantale-valued lax extension of an arbitrary $\mathsf{Set}$ -functor is induced by its class of Moss liftings. This generalizes results in the literature that rely on specific properties of the unit interval and on cardinality constraints on $\mathsf{Set}$ -functors (Marti and Venema 2015;Wild and Schröder 2020, 2021). By tackling this problem from the point of view of relations instead of functions, we obtain elegant proofs and new insights. For instance, we introduce the notion of predicate lifting for a lax extension which leads to a simple description of Moss lifting that goes beyond the realm of accessible functors and is independent of functor presentations, which feature centrally in previous approaches (Leal 2008;Marti and Venema 2015; Wild and Schröder 2020).

The representation result obtained here explains the importance of the canonical extensions of generalized monotone neighborhood functors in the process of constructing quantale-valued lax extensions (in analogy to the two-valued case Marti and Venema 2015); it is a stepping stone to connecting the coalgebraic approaches to behavioral distance via quantale-valued lax extensions and via liftings to categories of quantale-enriched categories, respectively (Goncharov et al. 2023), and similarly to connecting – in quantalic generality – the approaches to coalgebraic logics via lax extensions and via predicate liftings; and it helps pave the way to obtaining expressive (monotone) quantale-valued coalgebraic modal logics (Forster et al. 2023; Goncharov et al. 2023).

1.2 Roadmap

After briefly reviewing the necessary background in Section 2, we show in Section 3 how to extract predicate liftings from a lax extension in a canonical way. This leads to the notion of predicate lifting of a lax extension, which generalizes the notion of Moss lifting. We characterize the predicate liftings of a lax extension as the ones that obey a Yoneda-type formula involving the lax extension and conclude that the Moss liftings correspond to special representable $\mathcal{V}$ -functors.

In Sections 4 and 5, we revisit the Kantorovich extension (Wild and Schröder 2020, 2021). The main technical contributions of these sections are connected with one of the main results of ofWild and Schröder (2020):

Theorem 1. Every finitarily separable fuzzy lax extension of a $\mathsf{Set}$ -functor is induced by its set of Moss liftings.

A simpler version of this result states that every fuzzy lax extension of a finitary $\mathsf{Set}$ -functor is induced by its set of Moss liftings. Intuitively, a finitarily separable lax extension is a lax extension under which the functor can be approximated by its finitary part.

In this regard, we show in Section 4 that every lax extension is induced by its class of infinitary Moss liftings, and in Section 5 that the role of $\lambda$ -accessibility is to ensure that it is sufficient to consider a set of Moss liftings of arity less than $\lambda$ . Consequently, we obtain that every lax extension of an arbitrary functor is an initial lift of canonical extensions of generalized monotone neighborhood functors (Corollary 62), a generalization of Theorem 1 above – whose proof was tied to the unit interval – to arbitrary (commutative) quantales (Corollary 79), as well as a generalization of the following key result (Marti and Venema 2015) to arbitrary (commutative) quantales and functors (Corollary 64):

Theorem 2. A finitary $\mathsf{Set}$ -functor admits a lax extension to $\mathsf{Rel}$ that preserves identities if and only if it admits a separating set of monotone predicate liftings.

2. Preliminaries

We briefly review the theory of quantale-enriched categories from the point of view of quantale-enriched relations, as well as lax extensions and predicate liftings, and establish some notation and basic results. We warn the reader that there are several approaches to these topics in the literature, often with particular notations and nomenclature; we follow the conventions of Hofmann et al. (2014).

2.1 Quantale-enriched relations and categories

A quantale, more precisely a commutative unital quantale, is a complete lattice $\mathcal{V}$ that carries the structure of a commutative monoid $(\mathcal{V},\otimes,k)$ such that for every $u \in \mathcal{V}$ the map $u \otimes - \colon \mathcal{V}\to \mathcal{V}$ preserves suprema. Therefore, in a quantale, every map $u \otimes -\colon \mathcal{V} \to \mathcal{V}$ has a right adjoint $\hom(u,-) \colon \mathcal{V} \to \mathcal{V}$ , which is characterized by:

\[ u \otimes v \le w \iff v \le \hom(u,w),\]

for all $v, w \in \mathcal{V}$ . A quantale is nontrivial if the least element $\bot$ of $\mathcal{V}$ does not coincide with the greatest element $\top$ . Moreover, a quantale is integral if $\top$ is the unit of the monoid operation $\otimes$ of $\mathcal{V}$ , which we refer to as tensor or multiplication.

Remark 3. In categorical parlance, a quantale is a commutative monoid in the monoidal category of complete lattices and suprema-preserving maps.

Examples: 4. Quantales are common in mathematics and computer science.

1. (1) Every frame becomes a quantale with $\otimes = \wedge$ and $k = \top$ .

2. (2) Every left continuous t-norm (Alsina et al. 2006) defines a quantale on the unit interval equipped with its natural order. The following are some typical examples.

   1. a. The product t-norm has tensor given by multiplication and

      \[ \hom(u,v) = \begin{cases} \min(\frac{v}{u},1) & \text{if $u \neq 0$,} \\ 1 & \text{otherwise.} \end{cases} \]
      Via the map $[0,\infty]\to[0,1],u \mapsto e^{-u}$ , this quantale is isomorphic to the quantale $[0,\infty]$ of extended nonnegative real numbers used by Lawvere (1973) to define (generalized) metric spaces.

   2. b. The infimum t-norm has tensor given by infimum and

      \[ \hom(u,v) = \begin{cases} 1 & \text{if $u \le v$,} \\ v & \text{otherwise.} \end{cases} \]

   3. c. The Łukasiewicz t-norm has tensor given by $u \otimes v = \max(0,u+v-1)$ and $\hom(u,v) = \min(1,1-u+v)$ . This quantale is isomorphic to the quantale that is used implicitly in the usual treatment of 1-bounded metric spaces. More concretly, this quantale is isomorphic to the quantale based on the unit interval equipped with the dual of the natural order and with tensor given by truncated addition, $u\oplus v = \min(u+v,1)$ ; the map $[0,1] \to [0,1] \colon u \mapsto 1-u$ provides an isomorphism.

3. (3) Every commutative monoid $(M, \cdot, e)$ generates a quantale structure on $(\mathsf{P} M, \bigcup)$ , the free quantale on M. The tensor $\otimes$ on $\mathsf{P} M$ is defined by:

   \[ 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\}$ .

For a quantale $\mathcal{V}$ and sets X, Y, a $\mathcal{V}$ -relation – an enriched relation – from X to Y is a map $X \times Y \to \mathcal{V}$ ; we let denote the space of such maps, and in particular write to indicate that r is a $\mathcal{V}$ -relation from X to Y. As for ordinary relations, $\mathcal{V}$ -relations can be composed via “matrix multiplication.” That is, for and , the composite is calculated pointwise by:

\[ (s \cdot r)(x,z)=\bigvee_{y \in Y} r(x,y) \otimes s(y,z),\]

for $x \in X$ and $z \in Z$ . The collection of all sets and $\mathcal{V}$ -relations between them forms the category $\mathcal{V}\text{-}\mathsf{Rel}$ . For each set X, the identity morphism on X is the $\mathcal{V}$ -relation that sends every diagonal element to k and all the others to $\bot$ .

Examples: 5. The category of relations enriched in the two-element frame is the usual category $\mathsf{Rel}$ of sets and relations. Relations enriched in left continuous t-norms are often called fuzzy or quantitative relations.

We can compare $\mathcal{V}$ -relations of type using the pointwise order:

\[ r \leq s \iff \forall (x,y) \in X \times Y,\, r(x,y) \leq s(x,y).\]

Every hom-set of $\mathcal{V}\text{-}\mathsf{Rel}$ becomes a complete lattice when equipped with this order, and an easy calculation shows that $\mathcal{V}$ -relational composition preserves suprema in each variable. Therefore, $\mathcal{V}\text{-}\mathsf{Rel}$ is a quantaloid and enjoys pleasant properties inherited from $\mathcal{V}$ . In particular, precomposition and poscomposition with a $\mathcal{V}$ -relation define maps with right adjoints that compute Kan lifts and extensions, respectively. The lift of a $\mathcal{V}$ -relation along -relation defined by the property:

for every

We can compute lifts explicitly as:

Dually, the extension of a $\mathcal{V}$ -relation along is the $\mathcal{V}$ -relation defined by the property:

for every

Elementwise, we obtain

Being a quantaloid, $\mathcal{V}\text{-}\mathsf{Rel}$ is a 2-category and, therefore, it makes sense to talk about adjoint $\mathcal{V}$ -relations; as usual, is left adjoint to , written $l \dashv r$ , if $l \cdot r \leq 1_Y$ and $1_X \leq r \cdot l $ .

Proposition 6. Consider $\mathcal{V}$ -relations , , and .

1. (1)

2. (2)

3. (3)

4. (4)

Proof. All claims follow straightforwardly from the universal properties of lifts and extensions.

If $\mathcal{V}$ is nontrivial, we can see $\mathcal{V}\text{-}\mathsf{Rel}$ as an extension of $\mathsf{Set}$ through the faithful functor ${(-)}_\circ \colon \mathsf{Set} \to \mathcal{V}\text{-}\mathsf{Rel}$ that acts as identity on objects and interprets a function $f \colon X \to Y$ as the $\mathcal{V}$ -relation that sends every element of the graph of f to k and all the others to $\bot$ . To avoid unnecessary use of subscripts usually, we write f instead of $f_\circ$ .

The canonical isomorphism $X \times Y \simeq Y \times X$ in $\mathsf{Set}$ induces a contravariant involution in $\mathcal{V}\text{-}\mathsf{Rel}$ :

\[ {(-)}^\circ \colon {\mathcal{V}\text{-}\mathsf{Rel}}^\mathrm{op} \longrightarrow \mathcal{V}\text{-}\mathsf{Rel}\]

that maps objects identically and sends a $\mathcal{V}$ -relation to the $\mathcal{V}$ -relation defined by $r^\circ(y,x) = r(x,y)$ , the converse of r.

Remark 7. The converse of a function $f \colon X \to Y$ yields an adjunction $f \dashv f^\circ$ in $\mathcal{V}\text{-}\mathsf{Rel}$ (and this property of functions distinguishes them among $\mathcal{V}$ -relations precisely when the quantale $\mathcal{V}$ is integral and lean Hofmann et al. 2014, Proposition III.1.2.1). For every set Z, this adjunction extends to the following ones:

1. (1) $ f \cdot (-) \dashv f^\circ \cdot (-) \colon \mathcal{V}\text{-}\mathsf{Rel}(Z,X) \to \mathcal{V}\text{-}\mathsf{Rel}(Z,Y)$ ;

2. (2) $(-) \cdot f^\circ \dashv (-) \cdot f \colon \mathcal{V}\text{-}\mathsf{Rel}(X,Z) \to \mathcal{V}\text{-}\mathsf{Rel}(Y,Z)$ .

The next results collect some useful facts about the interplay between extensions, functions, relations, and involution.

Proposition 8. Let and be $\mathcal{V}$ -relations, and let $f \colon A \to X$ and $g \colon B \to Y$ be functions. Then the following holds.

1. (1)

2. (2) ;

3. (3) .

Proof. All claims are consequences of the uniqueness of adjoints. For example, to show 2 it is sufficient to observe that from Remark 7, it follows that both and are right adjoint to $(s\cdot g)\cdot-$ .

Proposition 9. Let and be $\mathcal{V}$ -relations. Then,

Where $a^\circ$ denotes the converse of the map $a \colon 1 \to A$ that selects the element a.

Corollary 10. Let , be $\mathcal{V}$ -relations, and $y \colon 1 \to Y$ a function. Then,

Proposition 11. Let and be $\mathcal{V}$ -relations, and let $f \colon X \to A$ and $g \colon Y \to B$ be functions such that $g \cdot r \leq s \cdot f $ . Then, $r \cdot f^\circ \leq g^\circ \cdot s$ .

Proof. $r \cdot f^\circ \leq g^\circ \cdot g \cdot r \cdot f^\circ \leq g^\circ \cdot s \cdot f \cdot f^\circ \leq g^\circ \cdot s$ .

Category theory underlines preordered sets as the fundamental ordered structures. For an arbitrary quantale $\mathcal{V}$ , the same role is taken by $\mathcal{V}$ -categories. Analogously to the classical case, we say that a $\mathcal{V}$ -relation is reflexive if $1_X \leq r$ , and transitive if $ r \cdot r \leq r$ . A $\mathcal{V}$ -category is a pair (X,a) consisting of a set X of objects and a reflexive and transitive $\mathcal{V}$ -relation ; a $\mathcal{V}$ -functor $(X,a) \to (Y,b)$ is map $f \colon X \to Y $ such that $f \cdot a \leq b \cdot f$ . Clearly, $\mathcal{V}$ -categories and $\mathcal{V}$ -functors define a category, denoted as $\mathcal{V}\text{-}\mathsf{Cat}$ .

Remark 12. As the nomenclature suggests, the notions of $\mathcal{V}$ -category and $\mathcal{V}$ -functor come from enriched category theory (Kelly 1982; Lawvere 1973; Stubbe 2014). In fact, unravelling the definition of reflexive and transitive $\mathcal{V}$ -relation yields the typical definition of quantale-enriched category: a pair (X,a) consisting of a set X and a map $a \colon X \times X \to \mathcal{V}$ that satisfies the inequalities:

\begin{align*} k \le a(x,x) && \text{and} && a(x,y) \otimes a(y,z) \leq a(x,z) \end{align*}

for all $x,y,z \in X$ . Similarly, a $\mathcal{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)). \]

Examples: 13. The following are some familiar examples of quantale-enriched categories.

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

2. (2) Metric, ultrametric, and bounded metric spaces à la Lawvere (1973) can be seen as categories enriched in left continuous t-norms:

   1. a. With multiplication $*$ , $[0,1]_*\text{-}\mathsf{Cat}$ is equivalent to the category $\mathsf{Met}$ of (generalized) metric spaces and non-expansive maps.

   2. b. With infimum $\wedge$ , $[0,1]_\wedge\text{-}\mathsf{Cat}$ is equivalent to the category $\mathsf{UMet}$ of (generalized) ultrametric spaces and non-expansive maps.

   3. c. With the Łukasiewicz tensor $\odot$ , $[0,1]_{\odot}\text{-}\mathsf{Cat}$ is equivalent to the category $\mathsf{BMet}$ of (generalized) bounded-by-1 metric spaces and non-expansive maps.

3. (3) Categories enriched in a free quantale $\mathsf{P} M$ on a monoid M (such as $M=\Sigma^*$ for some alphabet $\Sigma$ ) can be interpreted as labeled transition systems with labels in M: in a $\mathsf{P} M$ -category (X,a), the objects represent the states of the system, and we can read $m\in a(x,y)$ as an m-labeled transition from x to y.

Definition 14. The dual of a $\mathcal{V}$ -category (X,a) is the $\mathcal{V}$ -category ${(X,a)}^\mathrm{op} = (X,a^\circ)$ .

Remark 15. The quantale $\mathcal{V}$ becomes a $\mathcal{V}$ -category under the canonical structure $\hom \colon \mathcal{V} \times \mathcal{V} \to \mathcal{V}$ . In fact, for every set S, we can form the S-power $\mathcal{V}^S$ of $\mathcal{V}$ which has as underlying set all functions $h \colon S \to \mathcal{V}$ and $\mathcal{V}$ -category structure $[-,-]$ given by:

\[ [h,l] = \bigwedge_{s \in S} \hom(h(s),l(s)), \]

for all $h,l \colon S \to \mathcal{V}$ . For instance, for the quantale $([0,1],\oplus,0)$ , where [0, 1] is equipped with the dual of the natural ordering (Example 4(2c)), this distance on $[0,1]\text{-}\mathsf{Rel}(X,Y)=[0,1]^{X\times Y}$ is given in terms of the natural order on [0, 1] by:

\[ [r,s] = \sup \big\{\max(s(x,y)-r(x,y),0) \mid (x,y) \in X \times Y\big\}. \]

Every $\mathcal{V}$ -category (X,a) carries a natural order defined by:

\[ x \le y \text{ if } k \le a(x,y),\]

which induces a faithful functor $\mathcal{V}\text{-}\mathsf{Cat} \to \mathsf{Ord}$ . A $\mathcal{V}$ -category (X,a) is separated if

\begin{equation} (k\le a(x,y)\quad\&\quad k\leq a(y,x))\implies x=y\end{equation}

for all $x,y\in X$ . That is, (X,a) is separated if the natural order defined above is anti-symmetric.

Remark 16. The natural order of the $\mathcal{V}$ -category $\mathcal{V}$ is just the order of the quantale $\mathcal{V}$ . The natural order of $\mathcal{V}^S$ is calculated pointwise, and as such is complete. Furthermore, the $\mathcal{V}$ -category $\mathcal{V}^{S}$ is complete in the sense of enriched category theory; in particular, $\mathcal{V}^{S}$ has tensors, which are given by $(u\otimes h)(s)=u\otimes h(s)$ , for $u\in\mathcal{V}$ and $h\in\mathcal{V}^{S}$ . Tensors are compatible with composition, that is, $(u \otimes f) \cdot g = u \otimes (f \cdot g)$ for all $u \in \mathcal{V}$ , $f \colon S \to \mathcal{V}$ , and $g \colon S' \to S$ . Here, we recall that a $\mathcal{V}$ -category (X,a) is tensored if, for every $x\in X$ , the $\mathcal{V}$ -functor $a(x,-)\colon X\to\mathcal{V}$ has a left adjoint $-\otimes x \colon\mathcal{V}\to X$ in $\mathcal{V}\text{-}\mathsf{Cat}$ . We also note that $\mathcal{V}$ -functors between tensored $\mathcal{V}$ -categories are characterized by a pleasant property: a map $f \colon X\to Y$ between tensored $\mathcal{V}$ -categories X and Y is a $\mathcal{V}$ -functor if and only if f is monotone and, for all $u\in\mathcal{V}$ and $x\in X$ , $u\otimes f(x)\le f(u\otimes x)$ (Stubbe 2006).

2.2 Lax extensions

A lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ to $\mathcal{V}\text{-}\mathsf{Rel}$ consists of a map:

such that

(L1) $r \le r' \implies \mathsf{L} r \le \mathsf{L} r'$ ,

(L2) $\mathsf{L} s\cdot\mathsf{L} r\le\mathsf{L} (s\cdot r)$ ,

(L3) $\mathsf{F} f \le \mathsf{L} f$ and ${(\mathsf{F} f)}^\circ\le\mathsf{L}(f^\circ)$

for all , , and $f \colon X \to Y$ . The first condition means precisely that $\mathsf{L}$ induces a monotone map:

(1) \begin{equation} \mathsf{L}_{X,Y} \colon \mathcal{V}\text{-}\mathsf{Rel}(X,Y) \longrightarrow \mathcal{V}\text{-}\mathsf{Rel}(\mathsf{F} X, \mathsf{F} Y),\end{equation}

for all sets X and Y. We say that a lax extension is $\mathcal{V}$ -enriched if this map satisfies the stronger condition of being a $\mathcal{V}$ -functor, for all sets X and Y (see Remark 15):

(L1’) $[r,r'] \leq [\mathsf{L} r, \mathsf{L} r']$

for all . A lax extension $\mathsf{L}$ is identity-preserving if $\mathsf{L} 1_X = 1_{\mathsf{F} X}$ for every set X.

Remark 17. It is common to refer to various forms of extensions of $\mathsf{Set}$ -functors to $\mathsf{Rel}$ as relators, relational liftings, or lax relational liftings.

Example 18. The prototypical example of a lax extension is the Barr extension to $\mathsf{Rel}$ of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ that preserves weak pullbacks. Taking advantage of the fact that every relation can be described as a span:

the Barr extension of $\mathsf{F}$ sends r to the relation $\mathsf{F} p_2 \cdot {\mathsf{F} p_1}^\circ$ .

Kurz and Velebil (2016) provide a concise survey-oriented toward applications of lax extensions in coalgebra and logic that deals mostly with lax extensions to $\mathsf{Rel}$ . Regarding lax extensions to $\mathcal{V}\text{-}\mathsf{Rel}$ , work within the framework of monoidal topology (Clementino and Hofmann 2004; Schubert and Seal 2008; Seal 2005) encompasses a substantial amount of results.

Our main motivation to study lax extensions stems from the fact that they provide a framework for the coalgebraic treatment of various notions of quantale-valued (bi)simulation (Gavazzo 2018; Goncharov et al. 2023; Hughes and Jacobs 2004; Marti and Venema 2015; Rutten 1998;Wild and Schröder 2020, 2021). Recall that an $\mathsf{F}$ -coalgebra for a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ is a pair $(X,\alpha)$ consisting of a set X of states and a transition map $\alpha\colon X\to\mathsf{F} X$ ; such coalgebras are viewed as transition systems, with $\mathsf{F}$ determining the transition type (e.g., if $\mathsf{F}$ is just powerset, then $\mathsf{F}$ -coalgebras are relational transition systems in the usual sense). Now given a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ of $\mathsf{F}$ , an $\mathsf{L}$ -simulation between $\mathsf{F}$ -coalgebras $(X,\alpha)$ and $(Y,\beta)$ is a $\mathcal{V}$ -relation such that

\[ \beta \cdot s \leq \mathsf{L} s \cdot \alpha.\]

If the lax extension $\mathsf{L}$ preserves converse, then $\mathsf{L}$ -simulations are more suitably called $\mathsf{L}$ -bisimulations. Since $\mathcal{V}\text{-}\mathsf{Rel}$ is a quantaloid, there is the largest $\mathsf{L}$ -(bi)simulation between two given coalgebras, which is termed $\mathsf{L}$ -(bi)similarity. In the two-valued case, it has been shown by Marti and Venema (2015) that the notion of $\mathsf{L}$ -bisimilarity arising from an identity-preserving lax extension that preserves converse coincides with the standard coalgebraic notion of behavioral equivalence. On the other hand, the notion of $\mathcal{V}$ -enriched lax extension has been instrumental in establishing quantitative Hennessy-Milner and van Benthem-type theorems (Wild and Schröder 2020, 2021). It has been introduced with $\mathcal{V}$ -enrichment replaced with (L1) together with the condition:

(L4) For every set X and every $u\in\mathcal{V}$ , $u\otimes 1_{\mathsf{F} X}\le \mathsf{L}(u\otimes 1_{X})$ ,

where $u \otimes 1_A$ denotes the tensor of u and $1_A$ as defined in Remark 16 (and this condition is shown to be equivalent to a variant of $\mathcal{V}$ -enrichment where $\mathcal{V}$ is equipped with the symmetrized distance). The next result records the equivalence of these and other conditions.

Theorem 19. For a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ , the following assertions are equivalent.

1. (i) $\mathsf{L}$ is $\mathcal{V}$ -enriched.

2. (ii) For every set X and every $u\in\mathcal{V}$ , $u\leq[1_{\mathsf{F} X},\mathsf{L}(u\otimes 1_{X})]$ .

3. (iii) For every set X and every $u\in\mathcal{V}$ , $u\otimes 1_{\mathsf{F} X}\le \mathsf{L}(u\otimes 1_{X})$ .

4. (iv) For every $\mathcal{V}$ -relation and every $u\in\mathcal{V}$ , $u\otimes\mathsf{L} r\le\mathsf{L}(u\otimes r)$ .

Proof. Note that a lax extension satisfies the monotonicity condition (L1); therefore, the statements (i) and (iv) are equivalent by general results about tensored $\mathcal{V}$ -categories recalled in Remark 16. Now assume (i). Then, for every $u\in\mathcal{V}$ ,

\begin{equation} u\le [1_{X},u\otimes 1_{X}]\le [\mathsf{L} 1_{X},\mathsf{L}(u\otimes 1_{X})]\le [1_{\mathsf{F} X},\mathsf{L}(u\otimes 1_{X})]. \end{equation}

The implication (ii) $\Rightarrow$ (iii) follows from the adjunction $-\otimes 1_{\mathsf{F} X}\dashv[1_{\mathsf{F} X},-]$ . Finally, assume (iii). Then, for every $u\in\mathcal{V}$ and ,

\begin{equation} \mathsf{L}(u\otimes r) =\mathsf{L}(u\otimes (r\cdot 1_{X})) =\mathsf{L}(r\cdot (u\otimes 1_{X})) \geq \mathsf{L} r\cdot \mathsf{L}(u\otimes 1_{X}) \geq \mathsf{L} r\cdot (u\otimes 1_{\mathsf{F} X}) =u\otimes \mathsf{L} r. \end{equation}

Remark 20. If $k=\top$ in $\mathcal{V}$ , then $u\otimes 1_{X}\le 1_{X}$ and therefore $[u\otimes 1_{X},1_{X}]=k=\top$ . Hence,

\begin{equation} [1_{X},u\otimes 1_{X}]=[1_{X},u\otimes 1_{X}]\wedge [u\otimes 1_{X},1_{X}], \end{equation}

and $\mathcal{V}$ -enrichment of a lax extension can be equivalently expressed using the symmetrization of the canonical structure on $\mathcal{V}$ .

Remark 21. For the quantale [0, 1] of Example 4(2c), Wild and Schröder (2020) prove the equivalence (i) $\Leftrightarrow$ (iii) of Theorem 19, but with non-expansiveness of (1) defined with respect to the symmetric Euclidean metric on [0, 1] and with $\Delta_{\varepsilon,X}$ denoting $\varepsilon\otimes 1_{X}$ . Since this quantale is integral, Remark 20 ensures that this is equivalent to considering the asymmetric distance.

In the remainder of this subsection, we collect some useful properties of lax extensions. First, we note that they preserve certain composites of $\mathcal{V}$ -relations and functions strictly.

Proposition 22. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension, and let $f \colon X \to Y$ , $g \colon W \to Z$ be functions and a $\mathcal{V}$ -relation. Then,

1. (1) $\mathsf{L} (s\cdot f)=\mathsf{L} s\cdot\mathsf{L} f=\mathsf{L} s\cdot \mathsf{F} f$ ,

2. (2) $\mathsf{L} (g^\circ\cdot s)= \mathsf{L}(g^{\circ})\cdot\mathsf{L} s={(\mathsf{F} g)}^\circ\cdot\mathsf{L} s$ .

Proof. See, for example, Hofmann et al. (2014, Proposition III.1.4.4).

Proposition 23. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax functor. Then, items 5 and 5 of Proposition 5 are equivalent as conditions on $\mathsf{L}$ . If $\mathsf{L}$ satisfies them, then $\mathsf{L}$ is a lax extension of $\mathsf{F}$ .

Proof. See, for example, Hofmann et al. (2014, Proposition III.1.4.3).

A morphism of lax extensions $\alpha \colon (\mathsf{G}, \mathsf{L}) \to (\mathsf{F},\mathsf{L}_\mathsf{F})$ is a natural transformation $\alpha \colon \mathsf{G} \to \mathsf{F}$ that is oplax as a transformation $\alpha \colon \mathsf{L}_\mathsf{G} \to \mathsf{L}_\mathsf{F}$ ; that is, for every ,

\[ \alpha_Y \cdot \mathsf{L}_\mathsf{G} r \leq \mathsf{L}_\mathsf{F} r \cdot \alpha_X.\]

When no ambiguities arise, we simply write $\alpha \colon \mathsf{L}_\mathsf{G} \to \mathsf{L}_\mathsf{F}$ .

Disregarding size constraints, we have that lax extensions and their morphisms form a category which is topological over the category of endofunctors on $\mathsf{Set}$ (Schubert and Seal 2008, Remark 3.5). Given a family $\alpha = {(\alpha_i \colon \mathsf{F} \to \mathsf{F}_i)}_{i \in I}$ of natural transformations where each $\mathsf{F}_i$ carries a lax extension $\mathsf{L}_i$ to $\mathcal{V}\text{-}\mathsf{Rel}$ , the initial extension $\mathsf{L}_\alpha$ is defined by:

\[ \mathsf{L}_\alpha r = \bigwedge_{i \in I} \alpha_Y^\circ \cdot \mathsf{L}_i r \cdot \alpha_X,\]

for . In particular, the supremum and infimum over a class of lax extensions of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ is a lax extension of $\mathsf{F}$ .

Every lax extension has a dual as introduced by Seal (2005). The dual lax extension $\mathsf{L}^\circ \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ of a lax extension $\mathsf{L}\colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ is the lax extension of $\mathsf{F} \colon \mathsf{Set} \to\mathsf{Set}$ that is defined by the assignment:

\[ r \longmapsto {\mathsf{L} (r^\circ)}^\circ.\]

Notably, this means that we can symmetrize lax extensions. The symmetrization ${\widehat{\mathsf{F}}}^s \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ of a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ is the lax extension obtained as the meet of $\mathsf{L}$ and ${\mathsf{L}}^\circ$ .

Finally, an important application of lax extensions of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ to $\mathcal{V}\text{-}\mathsf{Rel}$ is to construct liftings of $\mathsf{F}$ to $\mathcal{V}\text{-}\mathsf{Cat}$ ; that is, endofunctors on $\mathcal{V}\text{-}\mathsf{Cat}$ that make the following diagram commute, where the vertical arrows represent the forgetful functor:

The lifting $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Cat} \to \mathcal{V}\text{-}\mathsf{Cat}$ induced by a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ sends a $\mathcal{V}$ -category (X,a) to the $\mathcal{V}$ -category $(\mathsf{F} X, \mathsf{L} a)$ .

2.3 Predicate liftings

Given a cardinal $\kappa$ , a $\kappa$ -ary predicate lifting for a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ is a natural transformation:

\[ \mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \longrightarrow \mathsf{Q}_\mathcal{V} \mathsf{F},\]

where, for a set Y, $\mathsf{Q}_Y \colon \mathsf{Set}^\mathrm{op} \to \mathsf{Set}$ denotes the functor:

\[ \mathsf{Set}(-,Y) \colon \mathsf{Set}^\mathrm{op} \to \mathsf{Set};\]

that is, we can think of elements of $\mathsf{Q}_{\mathcal{V}^\kappa} X$ as $\kappa$ -indexed families of $\mathcal{V}$ -valued predicates on X. We say that $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa}\to \mathsf{Q}_\mathcal{V} \mathsf{F}$ is monotone if for every set X the map:

\[ \mu_X \colon \mathsf{Set}(X,\mathcal{V}^\kappa) \to \mathsf{Set}(\mathsf{F} X,\mathcal{V})\]

is monotone w.r.t the pointwise orders induced by the corresponding powers of the complete lattice $\mathcal{V}$ , and $\mathcal{V}$ -enriched if this map is actually a $\mathcal{V}$ -functor w.r.t to the $\mathcal{V}$ -categorical structures induced by the corresponding powers of the $\mathcal{V}$ -category $\mathcal{V}$ (see Remark 15). Note that when talking about monotone or $\mathcal{V}$ -enriched predicate liftings, instead of $\mathsf{Q}_{\mathcal{V}^\kappa}\colon\mathsf{Set}^{\mathrm{op}}\to\mathsf{Set}$ we actually consider the functors $\mathsf{Q}_{\mathcal{V}^\kappa}\colon\mathsf{Set}^{\mathrm{op}}\to\mathsf{Pos}$ and $\mathsf{Q}_{\mathcal{V}^\kappa}\colon\mathsf{Set}^{\mathrm{op}}\to\mathcal{V}\text{-}\mathsf{Cat}$ , respectively. In any case, the functors $\mathsf{Q}_{\mathcal{V}^\kappa}$ are part of an adjunction: in general, for a category $\mathsf{A}$ and an object A with powers in $\mathsf{A}$ , we have

Moreover, for all functors $\mathsf{G} \colon \mathsf{Set}^{\mathrm{op}}\to\mathsf{A}$ and $\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ , the adjunction above induces a bijection between natural transformations $\mathsf{G}\to\mathsf{Q}_{A}\mathsf{F}$ and natural transformations $\mathsf{F}\to\mathsf{A}(\mathsf{G},A)$ . In particular, a $\kappa$ -ary predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa}\to\mathsf{Q}_\mathcal{V}\mathsf{F}$ corresponds to a natural transformation:

(2) \begin{equation} \overline{\mu}\colon\mathsf{F} \longrightarrow\mathsf{A}(\mathsf{Q}_{\mathcal{V}^\kappa},\mathcal{V}). \end{equation}

For $\mathsf{A}=\mathsf{Set}$ (respectively $\mathsf{A}=\mathsf{Pos}$ ) and $\mathcal{V}=\mathsf{2}$ , the codomain of $\overline{\mu}$ is the generalized (monotone) neighborhood functor (Marti and Venema 2015; Schröder and Pattinson 2010). A collection M of predicate liftings is separating if the cone

\begin{equation} (\overline{\mu}_{X}\colon \mathsf{F} X\longrightarrow\mathsf{Set}(\mathsf{Q}_{\mathcal{V}^\kappa} X,\mathcal{V}))_{\mu\in M} \end{equation}

(with $\overline\mu$ as per (2)) is mono (i.e., jointy injective) for every set X.

Remark 24. Predicate liftings are instrumental in coalgebraic logic (Cîrstea et al. 2011; Pattinson 2004; Schröder 2008). As a basic example, consider the Kripke semantics of modal logic. Coalgebras for the covariant powerset functor $\mathsf{P} \colon \mathsf{Set} \to \mathsf{Set}$ correspond precisely to Kripke frames. In coalgebraic modal logic, the Kripke semantics of the modal logic K is recovered by interpreting the modal operator $\Diamond$ as the predicate lifting $\Diamond \colon \mathsf{Q}_2 \to \mathsf{Q}_2\mathsf{P}$ whose X-component is defined by:

\[ \Diamond_X(A)= \{B \subseteq X \mid A \cap B \neq \varnothing\}, \]

or by interpreting the modal operator $\Box$ as the predicate lifting $\Box \colon \mathsf{Q}_2 \to \mathsf{Q}_2\mathsf{P}$ whose X-component is defined by:

\[ \Box_X(A)= \{B \subseteq X \mid B \subseteq A\}. \]

Both $\Diamond$ and $\Box$ are monotone (= $\mathsf{2}$ -enriched) predicate liftings, and both $\{\Diamond\}$ and $\{\Box\}$ are separating for $\mathsf{P}$ . Similarly, $\mathcal{V}$ -valued predicate liftings provide the semantical framework for modal operators in $\mathcal{V}$ -valued coalgebraic modal logic (Forster et al. 2023; Goncharov et al. 2023; Wild and Schröder 2020, 2021). In inductive definitions of the semantics of (coalgebraic) modal logics over a coalgebra $(X,\alpha)$ , formulae are typically interpreted as subsets of the state set X. If $\heartsuit$ is the predicate lifting interpreting a modality $\heartsuit$ , and $Y\subseteq X$ is the interpretation of a formula $\phi$ , then the formula $\heartsuit\phi$ is interpreted by the set $\alpha^{-1}[\heartsuit_X(Y)]$ . For instance, the interpretation of $\Diamond\phi$ in a $\mathsf{P}$ -coalgebra $(X,\alpha)$ , again with $Y\subseteq X$ being the interpretation of $\phi$ , consists of all $x\in X$ such that $\alpha(x)\cap Y\neq\emptyset$ , that is, of all states that have some successor satisfying $\phi$ .

Remark 25. Generalizing a corresponding observation for the $\mathsf{2}$ -valued case (Schröder 2008), we note that by the Yoneda lemma, a predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ is equivalently given by a morphism of type $\mathsf{F} \mathcal{V}^\kappa \to \mathcal{V}$ , the image of the identity map on $\mathcal{V}^\kappa$ under $\mu_{\mathcal{V}^\kappa}$ . In particular, for given $\kappa$ , the collection of all $\kappa$ -ary predicate liftings is small. The X-component $\mu_X \colon \mathsf{Q}_{\mathcal{V}^\kappa} X \to \mathsf{Q}_\mathcal{V} \mathsf{F} X $ of the predicate lifting induced by a morphism $g\colon \mathsf{F} \mathcal{V}^\kappa \to \mathcal{V}$ is defined by:

\[ \mu_X(f)= g \cdot \mathsf{F} f. \]

In the two-valued case, it has been shown that separating sets of finitary predicate liftings for a finitary $\mathsf{Set}$ -functor give rise to expressive coalgebraic modal logics (Schröder 2008), and that a finitary $\mathsf{Set}$ -functor admits a separating set of finitary monotone predicate liftings if and only if the functor admits an identity-preserving lax extension to $\mathsf{Rel}$ (Marti and Venema 2015). On the other hand, sets of $\mathcal{V}$ -enriched predicate liftings satisfying a quantitative analogue of separation feature in expressiveness results for quantitative coalgebraic modal logics for behavioral distances (Forster et al. 2023; König and Mika-Michalski 2018; Wild and Schröder 2020, 2021, 2022). We conclude this subsection with a characterization of $\mathcal{V}$ -enriched predicate liftings, which corresponds to Theorem 19 and can be shown similarly.

Theorem 26. For a predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V}\mathsf{F}$ , the following are equivalent.

1. (i) $\mu$ is $\mathcal{V}$ -enriched.

2. (ii) $\mu$ is monotone and for every $u\in\mathcal{V}$ , $u\leq[\mu(1_{\mathcal{V}^\kappa}),\mu(u\otimes 1_{\mathcal{V}^\kappa})]$ .

3. (iii) $\mu$ is monotone and for every $u\in\mathcal{V}$ , $u\otimes \mu(1_{\mathcal{V}^\kappa}) \le \mu(u\otimes 1_{\mathcal{V}^\kappa})$ .

$\mu$ is monotone and for every function $f \colon X \to \mathcal{V}^\kappa$ and every $u\in\mathcal{V}$ , $u\otimes\mu(f) \le \mu(u\otimes f)$ .

Remark 27. Analogously to Remark 20, if $k = \top$ , then $\mathcal{V}$ -enrichment of predicate liftings can be equivalently expressed using the symmetrization of the canonical structure on $\mathcal{V}$ .

3. From Lax Extensions to Predicate Liftings

We proceed to investigate the relationship between lax extensions and predicate liftings, using $\mathcal{V}$ -relations as a natural language to express their interaction. We begin by expressing predicate liftings in terms of $\mathcal{V}$ -relations, with an view to constructing predicate liftings from lax extensions.

We recall that the category $\mathsf{Set}$ is Cartesian-closed. In particular, this means that for every set I, the evaluation map $\mathrm{ev}_I \colon \mathcal{V}^I \times I \to \mathcal{V}$ , which we think of as a $\mathcal{V}$ -relation defined by $\mathrm{ev}_I(f,i) = f(i)$ , exhibits the function space $\mathcal{V}^I$ as an exponential object. Therefore, for every set X, currying/uncurrying defines an isomorphism:

\[ \mathcal{V}\text{-}\mathsf{Rel}(X,I) \simeq \mathsf{Set}(X,\mathcal{V}^I).\]

We denote the right adjunct of a $\mathcal{V}$ -relation by $r^\sharp \colon X \to \mathcal{V}^I$ and the left adjunct of a function $f \colon X \to \mathcal{V}^I$ by .

Remark 28. For every $\mathcal{V}$ -relation , the universal property of $\mathrm{ev}_I \colon \mathcal{V}^I \times I \to \mathcal{V}$ interpreted in $\mathcal{V}\text{-}\mathsf{Rel}$ implies $ r = \mathrm{ev}_I \cdot r^\sharp. $

Lemma 29. Let $\mathcal{V}$ be a quantale and I a set. For all functions $f \colon X \to Y$ and $g \colon Y \to \mathcal{V}^I$ ,

\[ (g \cdot f)^\flat = g^\flat \cdot f_\circ. \]

Proof. Let $x \in X$ and $i \in I$ . Then, by definition,

$$(g \cdot f)^\flat (x,i) = (g \cdot f)(x)(i) = g(f(x))(i) = g^\flat(f(x),i) = (g^\flat \cdot f_\circ) (x,i).$$

In the sequel, given a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ and a cardinal $\kappa$ , let $\mathcal{V}\text{-}\mathsf{Rel}_\circ(\mathsf{F} -, \kappa) \colon \mathsf{Set}^\mathrm{op} \to \mathsf{Set}$ denote the composite functor:

The above lemma says essentially that the uncurrying bijection $(-)^\flat$ is natural, so we immediately obtain the following:

Proposition 30. For every set I and every functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ , the functor $\mathsf{Q}_{\mathcal{V}^I} \mathsf{F} \colon \mathsf{Set}^\mathrm{op} \to \mathsf{Set}$ is isomorphic to the functor $\mathcal{V}\text{-}\mathsf{Rel}_\circ(\mathsf{F} -, I) \colon \mathsf{Set}^\mathrm{op} \to \mathsf{Set}$ .

Therefore, we mainly view predicate liftings as natural transformations $\mathcal{V}\text{-}\mathsf{Rel}_\circ(-,\kappa) \to \mathcal{V}\text{-}\mathsf{Rel}_\circ(\mathsf{F} -,1)$ from now on, although to keep the notation simple we still write $\mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ . Explicitly, naturality of a transformation $\mu\colon\mathcal{V}\text{-}\mathsf{Rel}_\circ(-,\kappa) \to \mathcal{V}\text{-}\mathsf{Rel}_\circ(\mathsf{F} -,1)$ means that for $f\colon X\to Y$ and , we have

\begin{equation*} \mu_X(r\cdot f) = \mu_Y(r)\cdot \mathsf{F} f.\end{equation*}

Now, it is easy to see that every lax extension induces natural transformations with the desired domain:

Proposition 31. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax functor and $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ a functor. Then, $\mathsf{L}$ is a lax extension of $\mathsf{F}$ if and only if $\mathsf{L}$ agrees with $\mathsf{F}$ on objects, and for every set I, $\mathsf{L}$ induces a natural transformation $\mathsf{L}_{-,I} \colon \mathcal{V}\text{-}\mathsf{Rel}_\circ (-,I) \to \mathcal{V}\text{-}\mathsf{Rel}_\circ(\mathsf{F} -, \mathsf{F} I)$ .

Proof. By Propositions 22(1) and 23.

This description suggests that to construct $\kappa$ -ary predicate liftings from a lax extension, we should construct natural transformations $\mathcal{V}\text{-}\mathsf{Rel}_\circ (\mathsf{F} -, F\kappa) \to \mathcal{V}\text{-}\mathsf{Rel}_\circ (\mathsf{F} -, 1)$ . The easiest way to do so is to select a $\mathcal{V}$ -relation . Then, each component of the resulting predicate lifting $\mathcal{V}\text{-}\mathsf{Rel}_\circ (-,\kappa) \to \mathcal{V}\text{-}\mathsf{Rel}_\circ (\mathsf{F} -, 1)$ is computed as:

\[ f \longmapsto \textbf{r} \cdot \mathsf{L} f.\]

This motivates our notion of predicate lifting induced by a lax extension, which, as we shall explain at the end of this section, generalizes the notion of Moss lifting (Kurz and Leal 2009; Leal 2008; Marti and Venema 2015;Wild and Schröder 2021).

Definition 32. A predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ is induced by a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ , or just a predicate lifting for $\mathsf{L}$ , if there exists a $\mathcal{V}$ -relation such that $\mu(f) = \textbf{r} \cdot \mathsf{L} f $ , for every $\mathcal{V}$ -relation . If $\textbf{r}$ is the converse of an element $\textbf{k} \colon 1 \to \mathsf{F} \kappa$ , then we say that $\mu$ is a Moss lifting of $\mathsf{L}$ and emphasize this by using the notation $\mu^\textbf{k} \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ .

Immediately from the definition, we have:

Proposition 33. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension. Every predicate lifting induced by $\mathsf{L}$ is monotone. If $\mathsf{L}$ is $\mathcal{V}$ -enriched, then every predicate lifting induced by $\mathsf{L}$ is $\mathcal{V}$ -enriched.

Example 34. Consider the lax extension of the covariant powerset functor $\mathsf{P} \colon \mathsf{Set} \to \mathsf{Set}$ to $\mathsf{Rel}$ given by:

\[ B (\widehat{\mathsf{P}}r) C \iff \forall c \in C, \exists b \in B,\, b \mathrel{r} c. \]

The unary Moss lifting for $\widehat{\mathsf{P}}$ determined by the element $1 \in \mathsf{P} 1$ is the predicate lifting $\Diamond \colon \mathsf{Q}_\mathcal{V} \to \mathsf{Q}_\mathcal{V}\mathsf{P}$ whose X-component is defined by:

\[ A \longmapsto \{B \subseteq X \mid A \cap B \neq \varnothing\}. \]

The Moss lifting for the dual extension of $\widehat{\mathsf{P}}$ determined by the element $1 \in \mathsf{P} 1$ is the predicate lifting $\Box \colon \mathsf{Q}_\mathcal{V} \to \mathsf{Q}_\mathcal{V}\mathsf{P}$ whose X-component is computed as:

\[ A \longmapsto \{B \subseteq X \mid B \subseteq A\}. \]

On the other hand, the unary Moss lifting for the Barr extension $\bar{\mathsf{P}}$ of $\mathsf{P}$ (the symmetrization of $\widehat{\mathsf{P}}$ ) determined by the element $1 \in \mathsf{P} 1$ is the predicate lifting $\nabla \colon \mathsf{Q}_\mathcal{V} \to \mathsf{Q}_\mathcal{V}\mathsf{P}$ whose X-component is defined by:

\[ A \longmapsto \{B \subseteq X \mid B \neq\varnothing \wedge B \subseteq A\}. \]

As mentioned in Remark 25, by the Yoneda Lemma, $\kappa$ -ary predicate liftings for a functor are completely determined by their action on the identity function on $\mathcal{V}^\kappa$ and the action of the functor. In the relational point of view, this means that $\kappa$ -ary predicate liftings are completely determined by the image of the evaluation relation . In the following, we will see that $\kappa$ -ary predicate liftings induced by a lax extension are completely determined by their action on the identity $\mathcal{V}$ -relation $1_\kappa \colon \kappa \to \kappa$ and the action of the lax extension. This characterization makes it easy to construct, detect, and manipulate predicate liftings induced by lax extensions (see Corollary 37, Lemma 77, and Proposition 39).

Lemma 35. Let $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ be a predicate lifting and $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ a lax extension. Then the following are equivalent:

1. (i) $\mu$ is induced by $\mathsf{L}$ ;

2. (ii) $\mu(\mathrm{ev}_\kappa) = \textbf{r} \cdot \mathsf{L}\,\mathrm{ev}_\kappa$ , for some ;

3. (iii) $\mu(\mathrm{ev}_\kappa) = \mu(1_\kappa) \cdot \mathsf{L}\,\mathrm{ev}_\kappa$ ;

4. (iv)

Proof. Let be a $\mathcal{V}$ -relation.

(i)⇒(ii) By definition.

(ii)⇒(iii) $ \mu(\mathrm{ev}_\kappa) = \textbf{r} \cdot \mathsf{L}\,\mathrm{ev}_\kappa = \textbf{r} \cdot \mathsf{L}1_\kappa \cdot \mathsf{L}\,\mathrm{ev}_\kappa = \mu(1_\kappa) \cdot \mathsf{L}\,\mathrm{ev}_\kappa. $

(iii)⇒(iv) By adjointness, the assumption implies that so we obtain .

(iv)⇒(i) Put . Then, since $\mu$ is a natural transformation,

\begin{align*} \mu(f) = \mu(\mathrm{ev}_\kappa \cdot f^\sharp) & = \mu(\mathrm{ev}_\kappa) \cdot \mathsf{F} f^\sharp \\ & = \textbf{r} \cdot \mathsf{L}\,\mathrm{ev}_\kappa \cdot \mathsf{F} f^\sharp = \textbf{r} \cdot \mathsf{L} f \end{align*}

where the last equality is by Proposition 22.

We crystallize the above into a Yoneda-style characterization of predicate liftings that is analogous to the one mentioned in Remark 25 but uses the lax extension instead of the underlying set functor:

Theorem 36. A predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V}\mathsf{F}$ is induced by a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ if and only if it is defined from $\mu(1_\kappa)$ (in the $\mathcal{V}$ -relational view) by:

\[ \mu(f)= \mu(1_\kappa) \cdot \mathsf{L}(f). \]

Proof. “If” is immediate by Condition (iii) in Lemma 35; we prove “only if.” Varying the calculation in the proof of (iv) $\implies$ (i) in Lemma 35 and using condition (iii) of the lemma, we have

\begin{equation*} \mu(f) = \mu(\mathrm{ev}_\kappa \cdot f^\sharp) = \mu(\mathrm{ev}_\kappa) \cdot \mathsf{F} f^\sharp \overset{\text(iii)}{=}\mu(1_\kappa) \cdot \mathsf{L}\,\mathrm{ev}_\kappa\cdot \mathsf{F} f^\sharp=\mu(1_\kappa)\cdot \mathsf{L} f. \end{equation*}

Corollary 37. A predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V}\mathsf{F}$ is induced by a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ if and only if for every relation and every function $g \colon \kappa \to Y$ ,

\[ \mu(g^\circ \cdot r) = \mu(g^\circ) \cdot \mathsf{L} r. \]

Proof. For “if,” just apply the assumption to $g=\mathrm{id}_\kappa$ and use Theorem 36. For “only if,” apply Theorem 36 to $g^\circ \cdot r$ , obtaining

\begin{equation*} \mu(g^\circ \cdot r)= \mu(1_\kappa) \cdot \mathsf{L}(g^\circ \cdot r)=\mu(1_\kappa) \cdot \mathsf{L}(g^\circ) \cdot \mathsf{L} r = \mu(g^\circ)\cdot \mathsf{L} r \end{equation*}

where the second equality is by Proposition 22.

Remark 38. Given a $\kappa$ -ary predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V}\mathsf{F}$ induced by a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ of $\mathsf{F}$ , it follows from Theorem 36 that is the largest $\mathcal{V}$ -relation that induces $\mu$ , but it may not be the only $\mathcal{V}$ -relation with this property if $\mathsf{L}$ does not preserve identities. For instance, in Example 34, we have seen that $\Box \colon \mathsf{Q}_2 \to \mathsf{Q}_2\mathsf{P}$ is the Moss lifting given by $1 \in \mathsf{P} 1$ for the dual lax exntesion of $\widehat{\mathsf{P}}$ but $\Box(1_1) = \top_{2,1}$ .

In Section 4, we will see that every lax extension is induced by its class of Moss liftings and turn now to the question of characterizing the Moss liftings induced by a lax extension in the usual point of view.

Lemma 39. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ , and $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V}\mathsf{F}$ a predicate lifting induced by $\mathsf{L}$ . Let denote the structure of the $\mathcal{V}$ -category ${(\mathcal{V}^\kappa)}^\mathrm{op}$ . Then,

\begin{equation*} \mu(\mathrm{ev}_\kappa) = \mu(1_\kappa) \cdot {(\mathsf{F} 1_\kappa^\sharp)}^\circ \cdot \mathsf{L} h. \end{equation*}

Proof. Observe that $\mathrm{ev}_\kappa = {(1_\kappa^\sharp)}^\circ \cdot h$ . Thus, we have

\begin{equation*} \mu(\mathrm{ev}_\kappa)=\mu({(1_\kappa^\sharp)}^\circ \cdot h)=\mu({(1_\kappa^\sharp)}^\circ)\cdot\mathsf{L}(h)=\mu(1_\kappa) \cdot \mathsf{L} ((1_\kappa^\sharp)^\circ) \cdot \mathsf{L} h=\mu(1_\kappa) \cdot {(\mathsf{F} 1_\kappa^\sharp)}^\circ \cdot \mathsf{L} h, \end{equation*}

using Corollary 37, Theorem 36, and Proposition 22, in that order.

Theorem 40. Let $\kappa$ be a cardinal and be the structure of the $\mathcal{V}$ -category ${(\mathcal{V}^\kappa)}^\mathrm{op}$ (see Remark 15). Furthermore, let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ . The $\kappa$ -ary Moss liftings induced by $\mathsf{L}$ correspond precisely to the representable $\mathcal{V}$ -functors $(\mathsf{F}\mathcal{V}^\kappa, \mathsf{L} h) \to \mathcal{V}^\mathrm{op}$ with representing objects in the image of the map $\mathsf{F}1_\kappa^\sharp \colon \mathsf{F}\kappa \to \mathsf{F}\mathcal{V}^\kappa$ .

Proof. Let $\mu^\textbf{k} \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V}\mathsf{F}$ be a Moss lifting induced by $\mathsf{L}$ . Note that $\mu(1_\kappa) \cdot {(\mathsf{F} 1_\kappa^\sharp)}^\circ \cdot \mathsf{L} h = \textbf{k}^\circ \cdot {(\mathsf{F} 1_\kappa^\sharp)}^\circ \cdot \mathsf{L} h$ . Hence, from Lemma 39, we conclude that under the isomorphism between $\kappa$ -ary predicate liftings for $\mathsf{F}$ and maps of type $\mathsf{F}\mathcal{V}^\kappa \to \mathcal{V}$ (see Remark 25), the predicate lifting $\mu^\textbf{k}$ corresponds to the map $\mathsf{F}\mathcal{V}^\kappa \to \mathcal{V}$ defined by:

\[ \textbf{v} \longmapsto \mathsf{L} h(\textbf{v},\mathsf{F} 1_\kappa^\sharp(\textbf{k})). \]

That is, $\mu^\textbf{k}$ corresponds to the representable $\mathcal{V}$ -functor $(\mathsf{F}\mathcal{V}^\kappa, \mathsf{L} h) \to \mathcal{V}^\mathrm{op}$ with representing object $\mathsf{F}1_\kappa^\sharp(\textbf{k})$ . On the other hand, this also makes it clear that every representable $\mathcal{V}$ -functor $(\mathsf{F}\mathcal{V}^\kappa, \mathsf{L} h) \to \mathcal{V}^\mathrm{op}$ with representing object in the image of the map $\mathsf{F}1_\kappa^\sharp \colon \mathsf{F}\kappa \to \mathsf{F}\mathcal{V}^\kappa$ corresponds to a Moss lifting.

By Lemma 35, the predicate liftings induced by a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ are determined by the fixed points of the monotone map:

which are precisely the $\mathcal{V}$ -relations that can be factorized as $\textbf{r} \cdot \mathsf{L}\,\mathrm{ev}_\kappa$ for some $\mathcal{V}$ -relation . Therefore, the least fixed point is obtained by composing the $\mathcal{V}$ -relation with the $\mathcal{V}$ -relation , the constant function into $\bot$ . The corresponding $\kappa$ -ary predicate lifting sends a $\mathcal{V}$ -relation to the $\mathcal{V}$ -relation , the constant function into $\bot$ . This is the smallest predicate lifting with respect to the pointwise order of $\kappa$ -ary predicate liftings, which is defined by:

Similarly, the greatest fixed point is obtained by composing the $\mathcal{V}$ -relation with the $\mathcal{V}$ -relation $\top_{\mathsf{F}\kappa,1}$ , the constant function into $\top$ . However, the greatest predicate lifting induced by a lax extension is not necessarily the greatest predicate lifting.

Example 41. Consider the identity functor $1_\mathsf{Rel} \colon \mathsf{Rel} \to \mathsf{Rel}$ which is a lax extension to $\mathsf{Rel}$ of the identity functor $1_\mathsf{Set} \colon \mathsf{Set} \to \mathsf{Set}$ . Then, the greatest unary predicate lifting of $1_\mathsf{Set}$ induced by $1_\mathsf{Rel}$ is the identity natural transformation $\mathsf{Q}_2 \to \mathsf{Q}_2$ , while the greatest unary predicate lifting for $1_\mathsf{Set}$ sends a relation to the greatest relation .

The definition of Moss lifting of a lax extension used in the literature is seemingly different from the one presented here (Kurz and Leal 2009; Leal 2008; Marti and Venema 2015; Wild and Schröder 2020). To conclude this section, we show that both definitions are computed in the same way.

We recall that every accessible $\mathsf{Set}$ -functor admits a presentation (e.g., Adámek et al. 2010, Proposition 3.9 and Theorem 68) as follows. A $\lambda$ -ary presentation of a $\lambda$ -accessible functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ consists of a $\lambda$ -ary signature $\Sigma$ , that is, a set of operations of arity less than $\lambda$ , and for each operation $\sigma \in \Sigma$ of arity $\kappa$ , a natural transformation $\sigma \colon {(-)}^\kappa \to \mathsf{F}$ such that, for every $X \in \mathsf{Set}$ , the cocone ${(\sigma_X \colon X^\kappa \to \mathsf{F} X)}_{\sigma \in \Sigma}$ is epi. Every functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ has a $\lambda$ -accessible subfunctor $\mathsf{F}_\lambda \colon \mathsf{Set} \to \mathsf{Set}$ (Adámek et al. 2010) that maps a set X to the set:

The notion of Moss lifting of a lax extension $\mathsf{L} \colon\mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ was introduced by Marti and Venema (2015). They think of predicate liftings for a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ as natural transformations:

\[ {(\mathsf{Q}_\mathcal{V})}^n \longrightarrow \mathsf{Q}_\mathcal{V} \mathsf{F},\]

where n is a natural number and ${(\mathsf{Q}_\mathcal{V}})^n$ denotes the n-fold product of $\mathsf{Q}_\mathcal{V}$ . Then, given a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ and a finitary presentation of $\mathsf{F}_\omega$ with signature $\Sigma$ , each n-ary $\sigma \in \Sigma$ induces a n-ary predicate lifting for $\mathsf{F}$ — a Moss lifting — whose X-component is defined by the assignment:

\[ (f_1, \dots, f_n ) \longmapsto (\textbf{x} \mapsto \mathsf{L}({\mathrm{ev}_X}^\circ)(\textbf{x}, \sigma_{\mathsf{Q}_\mathcal{V} X}(f_1, \dots, f_n)).\]

Of course, the functors $\mathsf{Q}_{\mathcal{V}^\kappa}$ and ${(\mathsf{Q}_\mathcal{V})}^\kappa$ are isomorphic, and the next proposition shows that both definitions of Moss lifting agree.

Proposition 42. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ , $\Sigma$ the signature of a $\lambda$ -ary presentation of $\mathsf{F}_\lambda$ , and $\kappa$ a cardinal. Let $\sigma \colon {(-)}^\kappa \to \mathsf{F}_\lambda \to \mathsf{F}$ be the natural transformation induced by a $\kappa$ -ary operation symbol $\sigma \in \Sigma$ . Then, for every $\mathcal{V}$ -relation ,

\[ \mu^{\sigma_\kappa(1_\kappa)} (f) = {\sigma_{P_\mathcal{V} X} (\,^\ulcorner\! f^\urcorner)}^\circ \cdot \mathsf{L}({\mathrm{ev}}^\circ), \]

where $\,^\ulcorner\! f^\urcorner$ represents the $\mathcal{V}$ -relation f as a function of type $\kappa \to \mathsf{Q}_\mathcal{V} X$ .

Proof. Note that by definition of ${\mathrm{ev}_X}^\circ$ , $f = {\,^\ulcorner\! f^\urcorner}^\circ \cdot {\mathrm{ev}_X}^\circ$ . Hence, $\mathsf{L} f = {\mathsf{F} \,^\ulcorner\! f^\urcorner}^\circ \cdot \mathsf{L}(\mathrm{ev}^\circ)$ . Moreover, ${\,^\ulcorner\! f^\urcorner}^\kappa (1_\kappa) = \,^\ulcorner\! f^\urcorner$ by definition of the functor ${(-)}^\kappa \colon \mathsf{Set} \to \mathsf{Set}$ ; or with $\mathrm{id}_\kappa \colon 1 \to \kappa^\kappa$ denoting the function that selects the identity morphism on $\kappa$ , ${\,^\ulcorner\! f^\urcorner}^\kappa \cdot \mathrm{id}_\kappa = \,^\ulcorner\! f^\urcorner$ . Therefore, since $\sigma \colon {(-)}^\kappa \to \mathsf{F}$ is a natural transformation,

\begin{align*} \mu^{\sigma_\kappa(1_\kappa)} (f) & = {\mathrm{id}_\kappa}^\circ \cdot \sigma_\kappa^\circ \cdot \mathsf{L} f \\ & = {\mathrm{id}_\kappa}^\circ \cdot \sigma_\kappa^\circ \cdot {\mathsf{F} \,^\ulcorner\! f^\urcorner}^\circ \cdot \mathsf{L} ({\mathrm{ev}_X}^\circ) \\ & = {\mathrm{id}_\kappa}^\circ \cdot {{\,^\ulcorner\! f^\urcorner}^\kappa}^\circ \cdot \sigma_{\mathsf{Q}_\mathcal{V} X}^\circ \cdot \mathsf{L} ({\mathrm{ev}_X}^\circ) \\ & = {\sigma_{\mathsf{Q}_\mathcal{V} X} (\,^\ulcorner\! f^\urcorner)}^\circ \cdot \mathsf{L}({\mathrm{ev}_X}^\circ). \end{align*}

Therefore, $\kappa$ -ary Moss liftings are constructed in a very simple way. From the usual point of view, a Moss lifting $\mu^\textbf{k} \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ of a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ , for $\textbf{k} \colon 1 \to \mathsf{F} \kappa$ , is just the map that sends a function $f \colon X \to \mathcal{V}^\kappa$ (with left adjunct to the function $\mathsf{L} f^\flat (-,\textbf{k}) \colon \mathsf{F} X \to \mathcal{V}$ .

Remark 43. Marti and Venema (2015) consider lax extensions of $\mathsf{Set}$ -functors that are not necessarily finitary; however, to construct Moss liftings, they restrict the functor to its finitary part. That is, the element $\textbf{k}$ inducing a Moss lifting $\mu^\textbf{k}$ belongs to $\mathsf{F}_\omega \kappa \subseteq \mathsf{F} \kappa$ .

In terms of maps of type $\mathsf{F} \mathcal{V}^\kappa \to \mathcal{V}$ , Proposition 39 tells us that $\mu^\textbf{k}$ is determined by the map $\mu(1_{\mathcal{V}^\kappa}) \colon \mathsf{F}\mathcal{V}^\kappa \to \mathcal{V}$ defined by:

\[ \textbf{x} \longmapsto \mathsf{L} h(\textbf{x},\mathsf{F} 1_\kappa^\sharp(\textbf{k})),\]

where is the structure of the $\mathcal{V}$ -category ${(\mathcal{V}^\kappa)}^\mathrm{op}$ (see Remark 15). In other words, $\kappa$ -ary Moss liftings correspond precisely to the representable $\mathcal{V}$ -functors $(\mathsf{F}\mathcal{V}^\kappa, \mathsf{L} h) \to \mathcal{V}^\mathrm{op}$ with representing objects in the image of the map $\mathsf{F}1_\kappa^\sharp \colon \mathsf{F}\kappa \to\mathsf{F}\mathcal{V}^\kappa$ .

4. From Predicate Liftings to Lax Extensions

The main goal of this section is to provide a way to construct lax extensions to $\mathcal{V}\text{-}\mathsf{Rel}$ from predicate liftings and to understand which lax extensions arise in such way. The first task has already been discharged in earlier work (Wild and Schröder 2020, 2021). In the following, we describe the Kantorovich extension of a collection of monotone predicate liftings (Wild and Schröder 2020, 2021), but completely from the point of view of $\mathcal{V}$ -relations. In Theorem 49, we show that every Kantorovich extension arises as an initial extension w.r.t to canonical extensions of generalized monotone neighborhood functors.

Given a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ and a predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ , this perspective makes it intuitive to construct a $\mathcal{V}$ -relation from a $\mathcal{V}$ -relation :

Theorem 44. Let $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F} $ be a $\kappa$ -ary predicate lifting. For every $\mathcal{V}$ -relation , consider the $\mathcal{V}$ -relation given by:

(3)

If $\mu$ is monotone, then the assignment $r \mapsto \mathsf{L}^\mu r $ defines a lax extension $\mathsf{L}^\mu \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel} $ , which is $\mathcal{V}$ -enriched whenever $\mu$ is $\mathcal{V}$ -enriched.

Proof. (L1)/(L1’) Monotonicity is immediate from the fact that

\begin{equation} \mathsf{L}^{\mu}(-)\colon\mathcal{V}\text{-}\mathsf{Rel}(X,Y) \longrightarrow\mathcal{V}\text{-}\mathsf{Rel}(\mathsf{F} X,\mathsf{F} Y) \end{equation}

is a composite of monotone maps; similarly for $\mathcal{V}$ -enrichment.

(L2) Let and be $\mathcal{V}$ -relations. We have to show that $\mathsf{L} s\cdot\mathsf{L} r\le\mathsf{L} (s\cdot r)$ . Let $h \colon Z \to \kappa$ . By definition, we have

Therefore, by Proposition 6(3)

which implies the claim.

(L3) Let $f\colon X\to Y$ . First, observe that since $\mu$ is a natural transformation, we have $\mu(g)\cdot \mathsf{F} f=\mu(g\cdot f)$ , and therefore

for all . Hence, $\mathsf{F} f \leq \mathsf{L}^\mu f$ . Second, note that because $\mu$ is monotone and natural, we have

for all . Therefore, by Proposition 11, $\mu(i)\cdot(\mathsf{F} f)^\circ\le \mu(i \cdot f^\circ)$ , and hence

Thus, $(\mathsf{F} f^\circ)\le \mathsf{L}^\mu (f^\circ)$ .

The formula (3) of Theorem 44 is entailed by the view of predicate liftings as natural transformations of type ${\mathcal{V}\text{-}\mathsf{Rel}}_\circ(-,\kappa) \to {\mathcal{V}\text{-}\mathsf{Rel}}_\circ(\mathsf{F} -,1)$ . By applying the involution on $\mathcal{V}\text{-}\mathsf{Rel}$ , we could also think of predicate liftings as natural transformations ${\mathcal{V}\text{-}\mathsf{Rel}}^\circ(\kappa,-) \to {\mathcal{V}\text{-}\mathsf{Rel}}^\circ(1, \mathsf{F} -)$ between functors defined according to the schema:

This point of view would lead us to the dual extension of (3).

Proposition 45. Let $\mu \colon \mathcal{V}\text{-}\mathsf{Rel}_\circ(-,\kappa) \to \mathcal{V}\text{-}\mathsf{Rel}_\circ(\mathsf{F} -, 1)$ be a predicate lifting and $\bar{\mu} \colon \mathcal{V}\text{-}\mathsf{Rel}^\circ(\kappa,-) \to \mathcal{V}\text{-}\mathsf{Rel}^\circ(1,\mathsf{F} -)$ be the natural transformation defined by:

\[ r \longmapsto {\mu(r^\circ)}^\circ. \]

Then,

Proof. Taking into account Proposition 6(1) and the fact that $(-)^\circ$ preserves infima, we have

Definition 46. Let $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ be a functor and M a class of monotone predicate liftings. The Kantorovich lax extension of $\mathsf{F}$ with respect to M is the lax extension:

\[ \mathsf{L}^M = \bigwedge_{\mu \in M} \mathsf{L}^\mu. \]

Examples: 47. Let $\mathcal{V}$ be a quantale.

1. (1) The identity functor on $\mathcal{V}\text{-}\mathsf{Rel}$ is the Kantorovich extension of the identity functor on $\mathsf{Set}$ with respect to the identity natural transformation $\mathsf{Q}_\mathcal{V} \to \mathsf{Q}_\mathcal{V}$ .

2. (2) The largest extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ to $\mathcal{V}\text{-}\mathsf{Rel}$ arises as the Kantorovich extension of $\mathsf{F}$ with respect to the natural transformation $\top \colon \mathsf{Q}_\mathcal{V} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ that sends every map to the constant map $\top$ and also as the Kantorovich extension with respect to the natural transformation $\bot \colon \mathsf{Q}_\mathcal{V} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ that sends every map to the constant map $\bot$ .

3. (3) For a subquantale $\mathcal{W}$ of $\mathcal{V}$ (i.e., $\mathcal{W}$ is a submonoid of $\mathcal{V}$ closed under suprema), it is easy to construct a unary predicate lifting of the covariant $\mathcal{W}$ -powerset functor $\mathsf{P} \colon \mathsf{Set} \to \mathsf{Set}$ , which, in terms of $\mathcal{V}$ -relations, is defined by:

   \begin{align*} \mathsf{P} X & =\mathcal{W}\text{-}\mathsf{Rel}(X, 1) \subseteq \mathcal{V}\text{-}\mathsf{Rel}(X,1), \\ \mathsf{P} f & = (-) \cdot f^\circ. \end{align*}
   A straightforward calculation shows that “evaluating” induces a predicate lifting $\Diamond \colon \mathsf{Q}_\mathcal{V} \to \mathsf{Q}_\mathcal{V} \mathsf{P}$ whose X-component is defined by:
   \begin{align*} \Diamond_X \colon \mathcal{V}\text{-}\mathsf{Rel}(X,1) & \longrightarrow \mathcal{V}\text{-}\mathsf{Rel}(\mathsf{P} X, 1). \\ \phi & \longmapsto \phi \cdot \mathrm{ev}_{\mathcal{W},X} \end{align*}

   Then, by Proposition 6(4) and Corollary 9,

   

   for every $\mathcal{V}$ -relation . Therefore, for $\mathcal{W}$ -relations and ,

   \[ \widehat{\mathsf{P}}^\Diamond r (\phi, \psi) = \bigwedge_{y \in Y} \hom(\psi(y), \bigvee_{x \in X} r(x,y) \otimes \phi(x)). \]
   Furthermore, for $\mathcal{W} = \mathsf{2}$ this formula simplifies to
   \[ \widehat{\mathsf{P}}^\Diamond r (A,B) = \bigwedge_{b \in B} \bigvee_{a \in A} r(a,b). \]

   1. a. For $\mathcal{W} = \mathcal{V} = \mathsf{2}$ we obtain a generalization of the upper half of the Egli–Milner order: for every , and all $A \in \mathsf{P} X$ and $B \in \mathsf{P} Y$ ,

      \[ A (\widehat{\mathsf{P}}^\Diamond r) B \iff \forall b \in B, \exists a \in A, a\, r\, b. \]

   2. b. For $\mathcal{W} = 2$ and $\mathcal{V}$ a left continuous t-norm, we obtain a generalization of the upper half of the Hausdorff metric: for every , and all $A \in \mathsf{P} X$ and $B \in \mathsf{P} Y$ ,

      \[ \widehat{\mathsf{P}}^\Diamond r (A,B) = \bigwedge_{b \in B} \bigvee_{a \in A} r(a,b). \]

4. (4) The dual lax extensions of the extensions 47(3a) and 47(3b) are generalizations of the lower half of the Egli–Milner order and of the lower half of the Hausdorff metric, respectively. Therefore, the symmetrization of these lax extensions are generalizations of the Egli–Milner order and the Hausdorff metric.

5. (5) Let us now consider a faithful functor ${\mathsf{|}{-}\mathsf{|}} \colon\mathsf{A}\to\mathsf{Pos}$ with some $\mathsf{A}$ -object $\mathcal{V}$ over the partially ordered set $\mathcal{V}$ and the functor ${{}^{\kappa}\mathsf{U}}=\mathsf{A}(\mathsf{Q}_{\mathcal{V}^\kappa},\mathcal{V})\colon\mathsf{Set}\to\mathsf{Set}$ . Some typical examples are $\mathsf{A}=\mathsf{Pos}$ and $\mathsf{A}=\mathcal{V}\text{-}\mathsf{Cat}$ ; for instance, for $\mathsf{A}=\mathsf{Pos}$ and $\mathcal{V}=\mathsf{2}$ , we obtain the generalized monotone neighborhood functor ${{}^{\kappa}\mathsf{U}}\colon\mathsf{Set}\to\mathsf{Set}$ . There is a canonical predicate lifting corresponding to the identity transformation $1 \colon {{}^{\kappa}\mathsf{U}}\to{{}^{\kappa}\mathsf{U}}$ , and we denote the induced extension as $\widehat{{{}^{\kappa}\mathsf{U}}}$ . Then, for a $\mathcal{V}$ -relation and for $\Phi \colon \mathsf{Q}_{\mathcal{V}^\kappa} X\to\mathcal{V}$ and $\Psi \colon \mathsf{Q}_{\mathcal{V}^\kappa} Y\to\mathcal{V}$ ,

This extension coincides with the one considered by Schubert and Seal (2008) for the classical monotone neighborhood functor. In particular, it follows that, for the identity , the $\mathcal{V}$ -category $({{}^{\kappa}\mathsf{U}} X,\widehat{{{}^{\kappa}\mathsf{U}}} 1_{X})$ is separated.

Remark 48. To see that the Kantorovich extension defined by Wild and Schröder (2020) coincides with the one presented here, note that Theorem 44 requires $\mu$ to be monotone; hence, we can define $\mathsf{F}^\mu$ with respect to $\mathcal{V}$ -relations of type with the same result, that is,

Moreover, in the language of Wild and Schröder (2020), a pair (f,g) of $\kappa$ -indexed families of maps of type $X \to \mathcal{V}$ is r-non-expansive precisely when , when interpreting f and g as $\mathcal{V}$ -relations.

The following result explains the distinguished role of the canonical extensions of generalized monotone neighborhood functors in the process of constructing lax extensions.

Theorem 49. Let M be a collection of predicate liftings for a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ . The Kantorovich extension $\mathsf{L}^{M}$ is the initial extension of $\mathsf{F}$ with respect to the cone:

\begin{equation} (\overline{\mu}\colon\mathsf{F} \longrightarrow{{}^{\kappa}\mathsf{U}})_{\mu\in M} \end{equation}

(with $\overline\mu$ as per (2)) and the lax extensions $\widehat{{{}^{\kappa}\mathsf{U}}}$ of ${{}^{\kappa}\mathsf{U}}$ described in Examples 47(5). Also, note that if all predicate liftings in M are even $\mathcal{V}$ -enriched, then so is $\mathsf{L}^{M}$ .

Proof. Let $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F} $ be a $\kappa$ -ary predicate lifting in M. Then, for a $\mathcal{V}$ -relation and $\textbf{x}\in\mathsf{F} X$ and $\textbf{y}\in\mathsf{F} Y$ ,

That is, $\mathsf{L}^{\mu}$ is the initial extension with respect to $\overline{\mu}\colon\mathsf{F}\to{{}^{\kappa}\mathsf{U}}$ and the lax extension $\widehat{{{}^{\kappa}\mathsf{U}}}$ of ${{}^{\kappa}\mathsf{U}}$ .

We proceed to collect some properties of Kantorovich extensions. We begin by observing that Kantorovich extensions are compatible with initial extensions along a natural transformation. This property will be particularly useful in Section 5 to generalize Theorem 1.

Proposition 50. Let $\mathsf{L}_\mathsf{F} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ , and let $i \colon \mathsf{G}\to \mathsf{F}$ be a natural transformation. Consider the initial lax extension $\mathsf{L}_i \colon\mathcal{V}\text{-}\mathsf{Rel}\to\mathcal{V}\text{-}\mathsf{Rel}$ of $\mathsf{G}$ with respect to $i \colon \mathsf{G}\to \mathsf{F}$ . If $\mathsf{L}_\mathsf{F}$ is Kantorovich w.r.t a class M of monotone predicate liftings, then $\mathsf{L}_i$ is Kantorovich w.r.t to the class of monotone predicate liftings:

\[ M_i = \{ (\mathsf{Q}_\mathcal{V} i) \cdot \mu \mid \mu \in M \}. \]

Proof. Clearly, every predicate lifting in $M_i$ is monotone. Now, let be a $\mathcal{V}$ -relation. Then,

Therefore, by Corollary 8,

Example 51. We recall that an endofunctor on $\mathsf{Set}$ is called taut if it preserves inverse images (Manes 2002). Every taut functor $\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ admits a natural transformation:

\begin{equation} \mathrm{supp} \colon \mathsf{F} \longrightarrow\mathsf{U} \end{equation}

into the monotone neighborhood functor with X-component:

\begin{equation} \mathrm{supp}_{X}\colon \mathsf{F} X \longrightarrow\mathsf{U} X,\quad \textbf{x} \longmapsto \{A\subseteq X\mid \textbf{x}\in \mathsf{F} A\}. \end{equation}

We note that every $\mathrm{supp}_{X}(\textbf{x})$ is actually a filter (Gumm 2005; Manes 2002). As observed by Schubert and Seal (2008), the op-canonical extension (Seal 2005) of a taut functor is the initial lift with respect to supp of the extension $\widehat{\mathsf{U}}$ of the monotone neighborhood functor $\mathsf{U} \colon\mathsf{Set}\to\mathsf{Set}$ of Example 47(5), that is, the extension induced by the predicate lifting $\mu$ corresponding to the identity transformation $1 \colon\mathsf{U}\to\mathsf{U}$ . Hence, by Proposition 50, the op-canonical extension of a taut functor $\mathsf{F}$ is induced by the predicate lifting:

\begin{equation} \mathsf{Q}_\mathcal{V}\mathrm{supp} \cdot \mu, \end{equation}

which, by adjunction, corresponds to the natural transformation:

\begin{equation} \mathrm{supp} \colon\mathsf{F} \longrightarrow\mathsf{U}. \end{equation}

The next result entails that we can use the Kantorovich extension to major a lax extension by extracting all predicate liftings induced by the lax extension. This is the first step toward representing lax extensions by collections of predicate liftings.

Proposition 52. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension and $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ a predicate lifting induced by $\mathsf{L}$ . Then, $\mathsf{L} \leq \mathsf{L}^\mu$ .

Proof. Let be a $\mathcal{V}$ -relation. Then, by (L2),

Corollary 53. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension and $\mu^\textbf{k} \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ a Moss lifting of $\mathsf{L}$ . Then, $\mathsf{L} \leq \mathsf{L}^{\mu^\textbf{k}}$ .

Notably, as a consequence of the previous results, we can use the Kantorovich extension to detect predicate liftings induced by lax extensions.

Proposition 54. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension and $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa} \to \mathsf{Q}_\mathcal{V} \mathsf{F}$ a predicate lifting induced by $\mathsf{L}$ . Then, the predicate lifting $\mu$ is induced by $\mathsf{L}^\mu$ .

Proof. According to Lemma 35, it suffices to show $\mu(\mathrm{ev}_\kappa) = \mu(1_\kappa) \cdot \mathsf{L}^\mu\mathrm{ev}_\kappa$ . First, observe that by Proposition 52 and Lemma 35((iii)) we have

\[ \mu(\mathrm{ev}_\kappa) = \mu(1_\kappa) \cdot \mathsf{L}(\mathrm{ev}_\kappa) \leq \mu(1_\kappa) \cdot \mathsf{L}^\mu(\mathrm{ev}_\kappa). \]

Second, note that by definition of $\mathsf{L}^\mu$ , we obtain

Example 55. The predicate lifting $\Diamond \colon \mathsf{Q}_\mathcal{V} \to \mathsf{Q}_\mathcal{V}\mathsf{P}$ of Example 47(3) is induced by the lax extension $\widehat{\mathsf{P}}^\Diamond \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ . With $k \colon 1 \to \mathcal{W}$ denoting the function that selects the element $k \in \mathcal{W}$ , we have

\[ \Diamond(f) = k^\circ \cdot \widehat{\mathsf{P}}^\Diamond f \]

for every $\mathcal{V}$ -relation .

We already know from Proposition 33 that every predicate lifting induced by a lax extension is monotone. The next example shows that the converse statement does not hold.

Example 56. Let [0, 1] denote the quantale consisting of the unit interval equipped with the usual order and multiplication. Consider the unary monotone predicate lifting for the identity functor $\mu \colon \mathsf{P}_{[0,1]} \to \mathsf{P}_{[0,1]}$ determined by the map $\mu(\mathrm{ev}_1) \colon [0,1] \to [0,1]$ defined by:

\[ \mu(\mathrm{ev}_1)(v) = \begin{cases} 0\;\;\;\; \text{ if } v \leq \frac{1}{2}; \\ 1\;\;\;\; \text{ otherwise}. \end{cases} \]

Given that [0, 1] is an integral quantale and $\mu$ is a unary predicate lifting in order to be induced by $\mathsf{L}^\mu$ , $\mu$ would need to satisfy the condition:

\[ \mu(\mathrm{ev}_1) \leq \mathsf{L}^\mu(\mathrm{ev}_1); \]

that is, for every ,

However, with $g = \frac{2}{3}$ and $v = \frac{3}{4}$ ,

Finally, we tackle the problem of recovering a lax extension to $\mathcal{V}\text{-}\mathsf{Rel}$ as the Kantorovich extension w.r.t. some class of predicate liftings.

Definition 57. A lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ is induced by a class of monotone predicate liftings $\Lambda$ for $\mathsf{F}$ if $\mathsf{L}$ is the Kantorovich extension w.r.t. $\Lambda$ .

Lemma 58. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ , $\kappa$ a cardinal, and $i \colon Y \to \kappa$ a function. For every $\textbf{y} \in \mathsf{F} Y$ and $\textbf{k} = \mathsf{F} i(\textbf{y})$ , and all $\mathcal{V}$ -relations and ,

1. (1) $\mu^\textbf{k}(s) = \textbf{y}^\circ \cdot \mathsf{L}(i^\circ \cdot s)$ ;

2. (2) if i is a monomorphism, then

   1. a. $\mu^{\textbf{k}}(i \cdot r) = \textbf{y}^\circ \cdot \mathsf{L} r$ ;

   2. b.

Proof. Note that $\textbf{k} = \mathsf{F} i(\textbf{y})$ means $\textbf{k} = \mathsf{F} i \cdot \textbf{y}$ , when considering elements as functions.

1. (1) $ \mu^\textbf{k} (s) = \textbf{k}^\circ \cdot \mathsf{L} s = \textbf{y}^\circ \cdot {\mathsf{F} i}^\circ \cdot \mathsf{L} s = \textbf{y}^\circ \cdot \mathsf{L} (i^\circ \cdot s) $ .

2. (2)

   1. a. Since i is a monomorphism, $i^\circ \cdot i = 1_Y$ . Therefore, the claim follows by applying 1 with $s = i \cdot r$ .

   2. b. Applying 2a, and recalling Proposition 6(2) and Condition (L3), yields

Corollary 59. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ , $i\colon \lambda \to \kappa$ a function between cardinals, $\textbf{l}$ an element of $\mathsf{F} \lambda$ , and $\textbf{k} = \mathsf{F} i (\textbf{l})$ .

1. (1) $\mathsf{L}^{\mu^\textbf{l}} \leq \mathsf{L}^{\mu^\textbf{k}}$ .

2. (2) If i is mono, then $\mathsf{L}^{\mu^\textbf{l}} = \mathsf{L}^{\mu^\textbf{k}}$ .

Lemma 58 allows approximating a lax extension with respect to the cardinality of the codomain of $\mathcal{V}$ -relations.

Corollary 60. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ , $\kappa$ a cardinal, and Y a set such that $|Y| \leq \kappa$ . Consider the set $M = \{ \mu^\textbf{k} \mid \textbf{k} \in \mathsf{F} \kappa \}$ . Then, for every $\mathcal{V}$ -relation , $\mathsf{L} r = \mathsf{L}^M r$ .

Therefore, as the collection of all Moss liftings of a lax extension is not larger than the class of all sets,

Theorem 61. Every lax extension of a $\mathsf{Set}$ -functor to $\mathcal{V}\text{-}\mathsf{Rel}$ is induced by its class of Moss liftings.

From Theorem 49, we obtain

Corollary 62. Every lax extension of a $\mathsf{Set}$ -functor to $\mathcal{V}\text{-}\mathsf{Rel}$ is an initial extension with respect to the lax extensions of the functors ${{}^{\kappa}\mathsf{U}} \colon \mathsf{Set} \to \mathsf{Set}$ (see Theorem 49).

From Proposition 33, we obtain

Corollary 63. Every $\mathcal{V}$ -enriched lax extension of a $\mathsf{Set}$ -functor to $\mathcal{V}\text{-}\mathsf{Rel}$ is induced by a class of $\mathcal{V}$ -enriched predicate liftings.

The next result is a generalization of Theorem 2 mentioned in the introduction. Note that, for $\mathcal{V}=\mathsf{2}$ and a lax extension $\mathsf{L}\colon \mathcal{V}\text{-}\mathsf{Rel}\to \mathcal{V}\text{-}\mathsf{Rel}$ that preserves converses, $\mathsf{L} 1_{X}$ is an equivalence relation on X. Hence, $\mathsf{L}$ is identity-preserving if and only if the ordered set $(\mathsf{F} X,\mathsf{L}1_{X})$ is anti-symmetric.

Corollary 64. A functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ has a separating class of $\mathcal{V}$ -valued monotone predicate liftings if and only if there is a lax extension $\mathsf{L}\colon \mathcal{V}\text{-}\mathsf{Rel}\to \mathcal{V}\text{-}\mathsf{Rel}$ such that, for all sets X, the $\mathcal{V}$ -category $(\mathsf{F} X,\mathsf{L}1_{X})$ is separated.

Proof. Suppose that there is such a lax extension $\mathsf{L}\colon \mathcal{V}\text{-}\mathsf{Rel}\to \mathcal{V}\text{-}\mathsf{Rel}$ . Let X be a set and $\textbf{x},\textbf{y}\in\mathsf{F} X$ with $\textbf{x}\neq\textbf{y}$ . By assumption, then have w.l.o.g. that $k\nleq\mathsf{L} 1_{X}(\textbf{x},\textbf{y})$ . Hence, by Theorem 61, there is a predicate lifting $\mu \colon \mathsf{Q}_{\mathcal{V}^\kappa}\to\mathsf{Q}_\mathcal{V}\mathsf{F}$ such that

\begin{equation} k\nleq{{}^{\kappa}\mathsf{U}}(\overline{\mu}(\textbf{x}),\overline{\mu}(\textbf{y})), \end{equation}

and therefore $\overline{\mu}(\textbf{x})\neq\overline{\mu}(\textbf{y})$ (see Example 47(5)). On the other hand, if $\mathsf{F}$ has a separating class of monotone predicate liftings, then the Kantorovich extension of $\mathsf{F}$ with respect to this class has the desired property by Example 47(5).

To conclude this section, we note that quantale-valued lax extensions that preserve converses and satisfy the condition of Corollary 64 lead to quantale-valued notions of bisimilarity that extend the canonical coalgebraic notion of behavioral equivalence.

Proposition 65. Let $\mathcal{V}$ be a nontrivial quantale, and let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ that preserves converses and such that, for all sets X, the $\mathcal{V}$ -category $(\mathsf{F} X,\mathsf{L}1_{X})$ is separated. Then two states in an $\mathsf{F}$ -coalgebra are behaviorally equivalent if and only if their $\mathsf{L}$ -bisimilarity is greater or equal than k.

Proof. Consider the lax homomorphisms of quantales $\phi \colon \mathsf{2} \to \mathcal{V}$ defined by $\phi(0) = \bot$ and $\phi(1) = k$ , and $\psi \colon \mathcal{V} \to \mathsf{2}$ defined by $\psi(v) = 1$ if $k \leq v$ and $\psi(v) = 0$ , otherwise. It is well known that lax homomorphisms of quantales give rive to lax functors between the corresponding categories of $\mathcal{V}$ -relations (Hofmann et al. 2014). Hence, we obtain lax functors:

\[ \phi \colon \mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel} \text{ and } \psi \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathsf{Rel} \]

that act identically on sets and postcompose the lax homomorphisms of quantales with relations (interpreted as maps into the quantales). It is easy to see that if we start with a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ of $\mathsf{F}$ that satisfies the conditions of the proposition, then, as $\mathcal{V}$ is nontrivial, we obtain an identity-preserving lax extension $\mathsf{L}_2 \colon \mathsf{Rel} \to \mathsf{Rel}$ of $\mathsf{F}$ that preserves converses as the composite:

Therefore, by Marti and Venema (2015, Theorem 14), $\mathsf{L}_2$ -bisimilarity coincides with behavioural equivalence. Moreover, as $\mathsf{L}$ -bisimilarity is itself an $\mathsf{L}$ -bisimulation, it follows that two states in an $\mathsf{F}$ -coalgebra are $\mathsf{L}_2$ -bisimilar if and only if their $\mathsf{L}$ -bisimilarity is greater or equal than k.

5. Small Lax Extensions

We next discuss the possibility of recovering a lax extension from a set of predicate liftings.

Definition 66. Let $\lambda$ be a regular cardinal. A lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ of a functor $\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ is $\lambda$ -small if it can be obtained as the Kantorovich extension of a set of $\kappa$ -ary predicate liftings with $\kappa<\lambda$ . We call $\mathsf{L}$ small if it is $\lambda$ -small for some regular cardinal $\lambda$ .

We will see next that every lax extension of an accessible functor is small. We recall that, for a regular cardinal $\lambda$ , a functor $\mathsf{F}\colon \mathsf{Set}\to \mathsf{Set} $ is called $\lambda$ -accessible if $\mathsf{F}$ preserves $\lambda$ -directed colimits. Furthermore, a functor $\mathsf{F}\colon \mathsf{Set}\to \mathsf{Set} $ is called accessible if $\mathsf{F}$ is $\lambda$ -accessible for some regular cardinal $\lambda$ .

Clearly, every $\lambda$ -accessible functor $\mathsf{F}\colon \mathsf{Set}\to \mathsf{Set} $ is $\lambda$ -bounded, that is, for every set X and every $\textbf{x}\in \mathsf{F} X$ , there exists a subset $m \colon A\to X$ with $|A|<\lambda$ and $\textbf{x}$ is in the image of $\mathsf{F} m$ . This property is in fact equivalent to accessibility:

Theorem 67. (Adámek et al. 2019) A functor $\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ is $\lambda$ -accessible if and only if $\mathsf{F}$ is $\lambda$ -bounded.

An immediate consequence of the result above is an algebraic presentation of accessible functors.

Theorem 68. (Adámek et al. 2015) Let $\lambda$ be a regular cardinal and $\mathsf{F}\colon \mathsf{Set}\to \mathsf{Set} $ be a functor. The following assertions are equivalent.

1. (i) $\mathsf{F}$ is $\lambda$ -bounded

2. (ii) $\mathsf{F}$ is a colimit of representable functors $\hom(X,-)$ where $|X|<\lambda$ .

3. (iii) There exists a small epi-cocone:

   \begin{equation} {(\!\hom(X_{i},-) \longrightarrow\mathsf{F})}_{i\in I} \end{equation}
   where, for each $i\in I$ , $|X_{i}|<\lambda$ .

Remark 69. The implication (i) $\implies$ (ii) above can be justified as follows. First, recall (MacLane 1998) that $\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ is a colimit of the (large) diagram

\begin{equation} {(\text{elements $(X,\textbf{x})$ of $\mathsf{F}$})}^{\mathrm{op}} \longrightarrow [\mathsf{Set},\mathsf{Set}]. \end{equation}

By (i),

\begin{equation} {(\text{elements $(X,\textbf{x})$ of $\mathsf{F}$ where $|X|<\lambda$})}^{\mathrm{op}} \longrightarrow {(\text{elements $(X,\textbf{x})$ of $\mathsf{F}$})}^{\mathrm{op}} \end{equation}

is cofinal.

Proposition 70. Every lax extension of an $\lambda$ -accessible functor is $\lambda$ -small. In fact, $\mathsf{L}=\mathsf{L}^{M_{\lambda}}$ for

\begin{equation} M_{\lambda}=\{\text{all $\alpha$-ary Moss-liftings, $\alpha<\lambda$}\}. \end{equation}

Proof. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of an accessible functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ . By Theorem 61, $\mathsf{L}=\mathsf{L}^{M}$ for the class M of all Moss liftings. Let $\kappa\geq\lambda$ be a cardinal and $\textbf{k}\in\mathsf{F}\kappa$ . Since $\mathsf{F}$ is $\lambda$ -accessible, there is some cardinal $\alpha<\lambda$ with inclusion $i \colon\alpha\to\kappa$ and some $\textbf{a}\in\mathsf{F}\alpha$ with $\mathsf{F} i(\textbf{a})=\textbf{k}$ . By Corollary 59, $\mathsf{L}^{\mu^{\textbf{a}}}=\mathsf{L}^{\mu^{\textbf{k}}}$ . Therefore, $\mathsf{L}=\mathsf{L}^{M_{\lambda}}$ .

Example 71. Every lax extension of the finite powerset functor can be recovered from a countable set of predicate liftings.

Corollary 72. Let $\mathsf{F}\colon \mathsf{Set}\to \mathsf{Set} $ be a $\lambda$ -accessible functor with a lax extension $\mathsf{L}\colon \mathcal{V}\text{-}\mathsf{Rel}\to \mathcal{V}\text{-}\mathsf{Rel}$ such that, for all sets X with $|X|<\lambda$ , the $\mathcal{V}$ -category $(\mathsf{F} X,\mathsf{L}1_{X})$ is separated. Then the set

\begin{equation} M_{\lambda}=\{\text{all $\alpha$-ary Moss liftings, $\alpha<\lambda$}\} \end{equation}

is separating.

Proof. Same as for Corollary 64, using Proposition 70.

Proposition 73. Let $\mathsf{L}_\mathsf{F} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ and $i \colon \mathsf{G}\to \mathsf{F}$ be a natural transformation. Furthermore, let $\mathsf{L}_i \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be the initial lax extension with respect to $i \colon \mathsf{G}\to \mathsf{F}$ . If $\mathsf{L}_\mathsf{F}$ is $\lambda$ -small, then $\mathsf{L}_i$ is $\lambda$ -small.

Proof. Follows from Proposition 50.

We can relax slightly the condition of Proposition 70 by taking advantage of the structure of $\mathcal{V}$ -category.

Definition 74. Let (X,a) be a $\mathcal{V}$ -category. A map $i \colon A\to X$ is dense in (X,a) if $a = a \cdot i \cdot i^\circ \cdot a$ .

Remark 75. A map $i \colon A \to X$ is dense in (X,a) if and only if the image of A is dense in (X,a) with respect to the closure operator $\overline{(-)}$ on $\mathcal{V}\text{-}\mathsf{Cat}$ introduced by Hofmann and Tholen (2010). We recall that for every $x \in X$ and $M \subseteq X$ ,

\begin{equation} x \in \overline{M} \iff k \le \bigvee_{z\in M} a(x,z) \otimes a(z,x). \end{equation}

This closure operator generalizes the one induced by the usual topology associated with a metric space. In fact, one can show that for categories enriched in a value quantale, such as metric spaces, this closure operator coincides with the one induced by the symmetric topology considered by Flagg (1992).

Definition 76. A natural transformation $i \colon \mathsf{G}\to \mathsf{F}$ between functors $\mathsf{G},\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ is called dense with respect to a lax extension $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ of $\mathsf{F}$ if, for each set X, $i_{X}\colon \mathsf{G} X\to\mathsf{F} X$ is dense in the $\mathcal{V}$ -category $(\mathsf{F} X,\mathsf{L} 1_{X})$ .

The following lemma records that dense maps are compatible with Moss liftings (see Theorem 36); in the sense that to determine the action of a $\kappa$ -ary Moss lifting, it suffices to focus on a dense subset of $(\mathsf{F} \kappa, \mathsf{L} 1_\kappa)$ .

Lemma 77. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of a functor $\mathsf{F} \colon \mathsf{Set} \to \mathsf{Set}$ . Furthermore, let be a $\mathcal{V}$ -relation, $\textbf{k}$ be an element of $\mathsf{F}\kappa$ , and $i \colon A \to \mathsf{F}\kappa$ be a dense map in $(\mathsf{F}\kappa,\mathsf{L} 1_{\kappa})$ . Then,

\begin{equation} \mu^{\textbf{k}}(\varphi)= \mu^\textbf{k}(1_\kappa) \cdot i \cdot i^\circ \cdot \mathsf{L}(\varphi). \end{equation}

Theorem 78. Let $i \colon \mathsf{G}\to \mathsf{F}$ be a natural transformation between functors $\mathsf{G},\mathsf{F} \colon\mathsf{Set}\to\mathsf{Set}$ , and let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension of $\mathsf{F}$ such that i is dense with respect to $\mathsf{L}$ . If $\mathsf{G}$ is $\lambda$ -accessible, then $\mathsf{L}$ is $\lambda$ -small.

Proof. Let be a $\mathcal{V}$ -relation, $\textbf{k}\in\mathsf{F}\kappa$ , and consider $i_{\kappa} \colon \mathsf{G} \kappa \to \mathsf{F} \kappa$ . Then, by Lemma 77, for all ,

Hence, by Propositions 6(4) and 9,

Now, the claim follows from the fact that $\mathsf{G}$ is $\lambda$ -accessible.

Finally, we obtain a generalization of Theorem 1 mentioned in the introduction.

Corollary 79. Let $\mathsf{L} \colon \mathcal{V}\text{-}\mathsf{Rel} \to \mathcal{V}\text{-}\mathsf{Rel}$ be a lax extension. If there is a regular cardinal $\lambda$ such that the natural transformation $\mathsf{F}_\lambda \hookrightarrow \mathsf{F}$ is dense, then $\mathsf{L}$ is $\lambda$ -small.

6. Conclusions

We have argued that the language of relations is a natural system to express the connection between predicate liftings and lax extensions by showing that it provides a point-free perspective in which many fundamental notions and results arise naturally and proofs become very elementary. Using this perspective, we were able to remove several technical restrictions that feature centrally in previous approaches which were confined to classical or [0, 1]-valued relations and accessible $\mathsf{Set}$ -functors (Leal 2008; Marti and Venema 2015; Wild and Schröder 2020). Indeed, our constructions and results are valid for arbitrary $\mathsf{Set}$ -functors and lax extensions to categories of quantale-enriched relations. In particular, we have introduced a new way of extracting predicate liftings from a lax extension that is independent of functor presentations, and indeed we provide an intrinsic characterization of predicate liftings that are induced in this sense by a given lax extension. This leads to a very simple description of Moss liftings, which has made it straightforward to show – in quantalic generality – that every lax extension is induced by its class of Moss liftings, and that the role of accessibility is to ensure that it suffices to consider a set of Moss liftings. Consequently, we have obtained the fact that every lax extension of a $\mathsf{Set}$ -functor is an initial extension of canonical extensions of generalized monotone neighborhood functors, as well as a generalization of the fact that the finitary functors that admit an identity-preserving lax extension are precisely the ones that admit a separating set of monotone predicate liftings. Furthermore, we have lifted the result that every finitarily separable [0, 1]-valued lax extension of a $\mathsf{Set}$ -functor is induced by a set of predicate liftings (Wild and Schröder 2020) to quantalic generality. Here, we have avoided restrictions on the quantale that are needed when classical notions of density (Flagg 1997) are used (like in recent results on quantalic van Benthem and Hennessy-Milner theorems Wild and Schröder 2021), by employing instead a categorical closure operator available on all quantale-enriched categories.