Identity-Preserving Lax Extensions and Where to Find Them

Goncharov, Sergey; Hofmann, Dirk; Nora, Pedro; Schröder, Lutz; Wild, Paul

doi:10.4230/LIPIcs.STACS.2025.40

Identity-Preserving Lax Extensions
and Where to Find Them

Sergey Goncharov

University of Birmingham, UK Dirk Hofmann

CIDMA, University of Aveiro, Portugal Pedro Nora

Radboud Universiteit, Nijmegen, The Netherlands Lutz Schröder

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany Paul Wild

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Abstract

Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems.

Keywords and phrases:

(Bi-)simulations, lax extensions, modal logics, coalgebra

Funding:

Sergey Goncharov: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 501369690.

Dirk Hofmann: This work is supported by CIDMA under the FCT (Portuguese Foundation for Science and Technology) Multi-Annual Financing Program for R&D Units.

Lutz Schröder: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 531706730.

Paul Wild: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 434050016.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Modal and temporal logics ; Theory of computation

\rightarrow

Concurrency

Editors:

Olaf Beyersdorff, Michał Pilipczuk, Elaine Pimentel, and Nguyễn Kim Thắng

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Branching-time notions of behavioural equivalence of reactive systems are typically cast as notions of bisimilarity, which in turn are based on notions of bisimulation, the paradigmatic example being Park-Milner bisimilarity on labelled transition systems [32]. A key point about this setup is that while bisimilarity is an equivalence on states, individual bisimulations can be much smaller than the full bisimilarity relation, and in particular need not themselves be equivalence relations. In a perspective where one views bisimulations as certificates for bisimilarity, this feature enables smaller certificates.

The concept of bisimilarity via bisimulations can be transferred to many system types beyond basic labelled transition systems, such as monotone neighbourhood systems [21], probabilistic transition systems, or weighted transition systems. In fact, such systems can be treated uniformly within the framework of universal coalgebra [38], in which the system type is encapsulated in the choice of a set functor (the powerset functor for non-deterministic branching, the distribution functor for probabilistic branching etc.). Coalgebraic notions of bisimulation were originally limited to functors that preserve weak pullbacks [38], equivalently admit a strictly functorial extension to the category of relations [5, 44]. They were later extended to functors admitting an identity-preserving or normal lax extension [30, 31] to the category of relations (this is essentially equivalent to notions of bisimilarity based on modal logic [15]). While there is currently no formal general definition of what a notion of bisimulation constitutes except via normal lax extensions, there is a reasonable claim [30, 31] that notions of bisimulation in the proper sense, in particular with bisimulations not required to be equivalence relations but stable under key operations such as relational composition, will not go beyond functors admitting a normal lax extension.

The Barr extension that underlies the original notion of coalgebraic bisimulation for weak-pullback-preserving functors [38] is, in particular, a normal lax extension; that is, preservation of weak pullbacks is sufficient for existence of a normal lax extension. However, this condition is far from being necessary; there are numerous functors that fail to preserve weak pullbacks but do admit a normal lax extension, such as the monotone neighbourhood functor [30, 31]. Using the latter fact, it has been shown that a finitary functor admits a normal lax extension if and only if it admits a separating set of finitary monotone modalities [30, 31], cast as monotone predicate liftings in the paradigm of coalgebraic logic [34, 39] (a similar result holds for unrestricted functors if one considers class-sized collections of infinitary modalities [14]). The latter condition amounts to existence of an expressive modal logic that has monotone modalities [34, 39], and as such admits $\mu$ -calculus-style fixpoint extensions [11]. In a nutshell, a system type admits a good notion of bisimulation if and only if it admits an expressive temporal logic. Both sides of this equivalence, however, need to be witnessed by the construction of a fairly complicated object; what is missing is a characterization via properties of the underlying functor, rather than via the existence of extra structure.

In the present work, we narrow the gap between weak pullback preservation as a sufficient condition for admitting a normal lax extension, and no known necessary pullback preservation condition. On the one hand, we establish a necessary preservation condition, showing that functors admitting a normal lax extension (weakly) preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is isomorphic. (We often put “weakly” in brackets because for many of the pullback types we consider, notably for inverse images and 1/4-iso pullbacks, weak preservation coincides with preservation.) This is a quite natural condition: A key role in the field is played by difunctional relations [36], which may be thought of as relations obtained by chopping the domain of an equivalence in half; for instance, given labelled transition systems $X$ , $Y$ , the bisimilarity relation from $X$ to $Y$ is difunctional. In a nutshell, we show that a functor preserves 1/4-iso pullbacks iff it acts in a well-defined and monotone manner on difunctional relations. A first application of this necessary condition is a very quick proof of the known fact that the neighbourhood functor does not admit a normal lax extension [31].

We then go on to establish two separate sets of sufficient conditions: We show that a functor admits a normal lax extension if it (weakly) preserves either inverse images or both 1/4-iso pullbacks and 4/4-epi pullbacks, i.e. pullbacks in which all morphisms are epi (these are also known as surjective pullbacks [42], and weak preservation of 4/4-epi pullbacks is equivalent to weak preservation of kernel pairs [16]). These sufficient conditions are technically substantially more involved. As indicated above, they imply that finitary functors (weakly) preserving either inverse images or 1/4-iso pullbacks and 4/4-epi pullbacks admit a separating set of finitary monotone modalities; this generalizes a previous result showing the same for functors preserving all weak pullbacks [28]. We summarize our main contributions in Figure 1.

Figure 1: Summary of main results. Solid arrows are present contributions, dashed arrows are trivial. All implications indicated by arrows are non-reversible; in particular, 4.12 shows this for 3.13.

As per the preceding discussion, these necessary and sufficient criteria essentially determine (when applicable) whether or not a given type of systems admits a good notion of bisimulation.

The criterion of weak preservation of 1/4-iso pullbacks and 4/4-epi pullbacks is satisfied by the monotone neighbourhood functor and generalizations thereof (e.g. [42]), and thus in particular reproves the above-mentioned known fact that functors admitting separating sets of monotone modalities have normal lax extensions. The criterion of (weak) preservation of inverse images, in connection with the necessary criterion, implies that a monoid-valued functor for a commutative monoid $M$ (whose coalgebras are $M$ -weighted transition systems) admits a normal lax extension if and only if $M$ is positive (which in turn is equivalent to the functor preserving inverse images [18]).

Related work.

With variations in the axiomatics and terminology, lax extensions go back to an extended strand of work on relation liftings (e.g. [3, 43, 22, 29, 41, 40]). We have already mentioned work by Marti and Venema relating lax extensions to modal logic [30, 31]; at the same time, Marti and Venema prove that the notion of bisimulation induced by a normal lax extension captures the standard notion of behavioural equivalence. Lax relation liftings, constructed for functors carrying a coherent order structure [24], also serve the study of coalgebraic simulation but obey a different axiomatics than lax extensions [31, Remark 4]). Strictly functorial (and converse-preserving) extensions of set functors to the category of sets and relations are known to be unique when they exist, and exist if and only if the functor preserves weak pullbacks [7, 44]; this has been extended to other base categories [3, 8]. There has been both longstanding and recent interest in quantitative notions of relation liftings and lax extensions that act on relations taking values in a quantale, such as the unit interval, in particular with a view to obtaining notions of quantitative bisimulation [37, 47, 23, 13, 45, 46, 14] that witness low behavioural distance (the latter having first been treated in coalgebraic generality by Baldan et al. [4]). The correspondence between normal lax extensions and separating sets of modalities generalizes to the quantitative setting [45, 46, 14].

Organization.

We review material on relations, in particular difunctional relations, and lax extensions in Section 2. In Section 3, we introduce our necessary pullback preservation condition and show that it characterizes well-definedness of the natural functor action on difunctional relations. We prove our main results in Section 4. In Subsection 4.1 we show that a functor that weakly preserves 1/4-iso pullbacks and 4/4-epi pullbacks admits a normal lax extension, and in Subsection 4.2 we show the same for functors that preserve 1/4-mono pullbacks.

2 Preliminaries: Relations and Lax Extensions

We work in the category $\mathsf{Set}$ of sets and functions throughout. We assume basic familiarity with category theory (e.g. [2]). A central role in the development is played by (weak) pullbacks: A commutative square $f\cdot p=g\cdot q$ is a pullback (of $f, g$ ) if for every competing square $f\cdot p^{\prime}=g\cdot q^{\prime}$ , there exists a unique morphism $k$ such that $p\cdot k=p^{\prime}$ and $q\cdot k=q^{\prime}$ ; the notion of weak pullback is defined in the same way except that $k$ is not required to be unique. A functor $\mathsf{F}$ weakly preserves a given pullback if it maps the pullback to a weak pullback; it is known that weak preservation of pullbacks of a given type is equivalent to preservation of weak pullbacks of the same type [17, Corollary 4.4]. Our interest in functors $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ is driven mainly by their role as encapsulating types of transition systems in the paradigm of universal coalgebra [38]: An $\mathsf{F}$ -coalgebra $(X,\alpha)$ consists of a set $X$ of states and a transition map $\alpha\colon X\to\mathsf{F}X$ assigning to each state $x\in X$ a collection $\alpha(x)$ of successors, structured according to $\mathsf{F}$ . For instance, coalgebras for the powerset functor $\mathcal{P}$ assign to each state a set of successors, and hence are just standard relational transition systems, while coalgebras for the distribution functor $\mathcal{D}$ (which maps a set $X$ to the set of discrete probability distributions on $X$ ) assign to each state a distribution on successor states, and are thus probabilistic transition systems.

A morphism $f\colon(X,\alpha)\to(Y,\beta)$ of $\mathsf{F}$ -coalgebras is a map $f\colon X\to Y$ for which $\beta\cdot f={\mathsf{F}f\cdot\alpha}$ . Such morphisms are thought of as preserving the behaviour of states, and correspondingly, states $x$ and $y$ in coalgebras $(X,\alpha)$ and $(Y,\beta)$ , respectively, are behaviourally equivalent if there exist a coalgebra $(Z,\gamma)$ and morphisms $f\colon(X,\alpha)\to(Z,\gamma)$ , $g\colon(Y,\beta)\to(Z,\gamma)$ such that $f(x)=g(y)$ .

Example 2.1.

On relational transition systems, i.e. coalgebras for the powerset functor $\mathcal{P}$ , behavioural equivalence instantiates to the usual notion of bisimilarity. More generally, labelled transition systems with labels taken from a set $\mathcal{A}$ are coalgebras for the functor $\mathcal{P}(\mathcal{A}\times(-))$ , and behavioural equivalence instantiates to Park-Milner bisimilarity [1]. On Markov chains, understood as $\mathcal{D}$ -coalgebras, all states are behaviourally equivalent, as all states are identified in the final coalgebra $1\to\mathcal{D}1\cong 1$ . This triviality is removed in various forms of probabilistic labelled transition systems, for instance in $\mathcal{D}(\mathcal{A}\times(-))$ -coalgebras, on which behavioural equivalence instantiates to standard notions of probabilistic bisimilarity [26].

One is then interested in notions of bisimulation relation that characterize behavioural equivalence in the sense that two states are behaviourally equivalent iff they are related by some bisimulation [38, 31]; this motivates the detailed study of relations and of extensions of $\mathsf{F}$ that act on relations. We write $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ to indicate that $r$ is a relation from the set $X$ to the set $Y$ (i.e. $r\subseteq X\times Y$ ), and we write $x\mathrel{r}y$ when $(x,y)\in r$ . Both for functions and for relations, we use applicative composition, i.e. given $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ and ${s\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08% -15-52-40-1.pdf2svg.svg}Z}$ , their composite is $s\cdot r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025% -05-08-15-52-40-1.pdf2svg.svg}Z$ (defined as $s\cdot r=\{(x,z)\mid\exists y\in Y.\,x\mathrel{r}y\mathrel{s}z\}$ ). We say that $r, s$ of type $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ and ${s\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08% -15-52-40-1.pdf2svg.svg}Z}$ are composable, and we extend this terminology to sequences of relations in the obvious manner. Relations between the same sets are ordered by inclusion, that is $r\leq r^{\prime}\iff r\subseteq r^{\prime}$ . We denote by $1_{X}\colon X\to X$ the identity map (hence relation) on $X$ , and we say that a relation $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}X$ is a subidentity if $r\leq 1_{X}$ . Given a relation $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ , $r^{\circ}\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X$ denotes the corresponding converse relation; in particular, if $f\colon X\to Y$ is a function, then $f^{\circ}\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X$ denotes the converse of the corresponding relation. For a relation $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ , we denote by $\mathop{{\operatorname{\mathsf{dom}}}}r\subseteq X$ and $\mathop{{\operatorname{\mathsf{cod}}}}r\subseteq Y$ the respective domain and codomain (i.e. $\mathop{{\operatorname{\mathsf{dom}}}}r=\{x\in X\mid\exists y\in Y.\,x\mathrel% {r}y\}$ and $\mathop{{\operatorname{\mathsf{cod}}}}r=\{y\in Y\mid\exists x\in X.\,x\mathrel% {r}y\}$ ). A special class of relations of interest are difunctional relations [36], which are relations factorizable as $g^{\circ}\cdot f$ for some functions $f\colon X\to Z$ and $g\colon Y\to Z$ , i.e. $x\leavevmode\nobreak\ r\leavevmode\nobreak\ y$ iff $f(x)=g(y)$ . In the following we record some folklore facts about difunctional relations.

Lemma 2.2.

Let $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ be a relation. Then the following are equivalent:

1.

$r$ is difunctional;
2.

for all $x_{1},x_{2}$ in $X$ and $y_{1},y_{2}\in Y$ , if $x_{1}\mathrel{r}y_{1}\mathrel{r^{\circ}}x_{2}\mathrel{r}y_{2}$ , then $x_{1}\mathrel{r}y_{2}$ .
3.

for every span $X\mathrel{\raisebox{-1.15pt}{$\xleftarrow{\smash{\hskip 3.5pt\raisebox{-2.5pt}% {\makebox(3.0,0.0)[b]{\scriptsize$\pi_{1}$}}\hskip 1.5pt}}$}}R\mathrel{% \raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt}{\makebox% (3.0,0.0)[b]{\scriptsize$\pi_{2}$}}\hskip 2.5pt}}$}}Y$ such that $r=\pi_{2}\cdot\pi_{1}^{\circ}$ , the pushout square

is a weak pullback.

As we can see in 2.2(3) above, difunctional relations are characterized as weak pullbacks, and in this regard we recall that generally, a commutative square $f\cdot p=g\cdot q$ is a weak pullback iff $q\cdot p^{\circ}=g^{\circ}\cdot f$ , equivalently $p\cdot q^{\circ}=f^{\circ}\cdot g$ .

The difunctional closure of a relation $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ is the least difunctional relation $\hat{r}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-% 05-08-15-52-40-1.pdf2svg.svg}Y$ greater than or equal to $r$ . It follows from 2.2 that the difunctional closure of a relation $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ given by a span $X\mathrel{\raisebox{-1.15pt}{$\xleftarrow{\smash{\hskip 3.5pt\raisebox{-2.5pt}% {\makebox(3.0,0.0)[b]{\scriptsize$\pi_{1}$}}\hskip 1.5pt}}$}}R\mathrel{% \raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt}{\makebox% (3.0,0.0)[b]{\scriptsize$\pi_{2}$}}\hskip 2.5pt}}$}}Y$ is obtained by computing its pushout $X\mathrel{\raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt% }{\makebox(3.0,0.0)[b]{\scriptsize$p_{1}$}}\hskip 2.5pt}}$}}O\mathrel{% \raisebox{-1.15pt}{$\xleftarrow{\smash{\hskip 3.5pt\raisebox{-2.5pt}{\makebox(% 3.0,0.0)[b]{\scriptsize$p_{2}$}}\hskip 1.5pt}}$}}Y$ ; i.e., the difunctional closure $\hat{r}$ of $r$ is the relation $p_{2}^{\circ}\cdot p_{1}$ . More explicitly, $\hat{r}=\bigvee_{n\in\mathbb{N}}r\cdot(r^{\circ}\cdot r)^{n}$ (e.g. [36, 20]).

A lax extension $\mathsf{L}$ of an endofunctor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ is a mapping that sends any relation $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ to a relation $\mathsf{L}r\colon\mathsf{F}X\includegraphics{dagpub-standalone-dagpub-svg-% displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}\mathsf{F}Y$ in such a way that

(L1): $r\leq r^{\prime}\implies\mathsf{L}r\leq\mathsf{L}r^{\prime}$ ,
(L2): $\mathsf{L}s\cdot\mathsf{L}r\leq\mathsf{L}(s\cdot r)$ ,
(L3): $\mathsf{F}f\leq\mathsf{L}f$ and ${(\mathsf{F}f)}^{\circ}\leq\mathsf{L}(f^{\circ})$ ,

for all $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ , $s\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Z$ and $f\colon X\to Y$ . We define relax extensions in the same way, without however requiring property (L2). We call a (re)lax extension identity-preserving, or normal, if $\mathsf{L}1_{X}=1_{\mathsf{F}X}$ for every set $X$ , and we say that a (re)lax extension preserves converses if $\mathsf{L}(r^{\circ})=(\mathsf{L}r)^{\circ}$ .

A tactical advantage of using the term “relax extension” is that we can thus refer to constructions that produce lax extensions most of the time, except for some cases when (L2) may fail. A prototypical example of this sort is the Barr extension $\mathsf{\overline{F}}$ [6], which for weak-pullback-preserving $\mathsf{F}$ is even a strict extension, and is defined as follows. Given a relation $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ , choose a factorization $\pi_{2}\cdot\pi_{1}^{\circ}$ for some span $X\mathrel{\raisebox{-1.15pt}{$\xleftarrow{\smash{\hskip 3.5pt\raisebox{-2.5pt}% {\makebox(3.0,0.0)[b]{\scriptsize$\pi_{1}$}}\hskip 1.5pt}}$}}R\mathrel{% \raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt}{\makebox% (3.0,0.0)[b]{\scriptsize$\pi_{2}$}}\hskip 2.5pt}}$}}Y$ and put $\mathsf{\overline{F}}r=\mathsf{F}\pi_{2}\cdot{(\mathsf{F}\pi_{1})}^{\circ}$ . This assignment is independent of the factorization of $r$ , and $r$ admits a canonical factorization which is given by projecting into $X$ and $Y$ the subset of $X\times Y$ of pairs of elements related by $r$ . It is well-known that for every $\mathsf{Set}$ -functor, the Barr extension is a normal relax extension, but it is a lax extension precisely when $\mathsf{F}$ preserves weak pullbacks [27]. In this case, the Barr extension is also the least lax extension of $\mathsf{F}$ , for it follows from (L1)–(L3) that $\mathsf{F}\pi_{2}\cdot{(\mathsf{F}\pi_{1})}^{\circ}\leq\mathsf{L}r$ for every lax extension $\mathsf{L}$ .

Lax extensions have been used extensively to treat the notion of bisimulation coalgebraically (e.g. [22, 29, 31]). Given a lax extension $\mathsf{L}\colon\mathsf{Rel}\to\mathsf{Rel}$ of a functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ , an $\mathsf{L}$ -simulation between $\mathsf{F}$ -coalgebras $(X,\alpha)$ and $(Y,\beta)$ is a relation $s\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ such that $\beta\cdot s\leq\mathsf{L}s\cdot\alpha$ , that is, whenever $x\mathrel{r}y$ , then $\alpha(x)\mathrel{Lr}\beta(y)$ . If $\mathsf{L}$ preserves converses, then $\mathsf{L}$ -simulations are more suitably called $\mathsf{L}$ -bisimulations. Between two given coalgebras, there is a greatest $\mathsf{L}$ -(bi)simulation, which is termed $\mathsf{L}$ -(bi)similarity. It has been shown [31] that if $\mathsf{L}$ is normal and preserves converses, then $\mathsf{L}$ -bisimilarity coincides with coalgebraic behavioural equivalence as recalled above. The axioms of lax extensions guarantee that $L$ -bisimulations are closed under converse and composition and that coalgebra morphisms are (functional) $L$ -bisimulations, so that $L$ -bisimilarity includes behavioural equivalence; that is, $L$ -bisimilarity is complete for behavioural equivalence. Normality of lax extensions ensures that $L$ -bisimulations are sound for behavioural equivalence, i.e. $L$ -bisimilarity is included in behavioural equivalence.

Example 2.3.

1.

For relational transition systems, understood as $\mathcal{P}$ -coalgebras, we have a normal lax extension $L$ of $\mathcal{P}$ given by the standard Barr extension, which in turn coincides with the well-known Egli-Milner extension: Given $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ , $S\in\mathcal{P}X$ , and $T\in\mathcal{P}Y$ , we have $S\mathrel{Lr}T$ iff for all $x\in S$ , there exists $y\in T$ such that $x\mathrel{r}y$ , and symmetrically. An $L$ -bisimulation is then just a bisimulation in the standard sense.
2.

On $F=\mathcal{D}(\mathcal{A}\times(-))$ , we have a normal lax extension $L$ given for $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ , $\mu\in\mathcal{D}(\mathcal{A}\times X)$ , $\nu\in\mathcal{D}(\mathcal{A}\times Y)$ by $\mu\mathrel{Lr}\nu$ iff for all $l\in\mathcal{A},A\in\mathcal{P}X$ , we have $\nu(\{l\}\times r[A])\geq\mu(\{l\}\times A)$ , and symmetrically [15]. The arising notion of $L$ -bisimulation is sound and complete for probabilistic bisimilarity on probabilistic labelled transition systems.

$\blacktriangleright$ Remark 2.4.

As mentioned in the introduction, a functor $\mathsf{F}$ admits a normal lax extension iff $\mathsf{F}$ admits a separating class of monotone predicate liftings [31, 14]. For readability, we discuss only the case where both the functor and the predicate liftings are finitary [31]. An $n$ -ary predicate lifting $\lambda$ for $\mathsf{F}$ is a natural transformation of type $\lambda\colon\mathcal{Q}^{n}\to\mathcal{Q}\cdot\mathsf{F}^{\mathrm{op}}$ where $\mathcal{Q}$ denotes the contravariant powerset functor (given by $\mathcal{Q}X$ being the powerset of a set $X$ , and $\mathcal{Q}f(B)=f^{-1}[B]$ for $f\colon X\to Y$ and $B\in\mathcal{Q}Y$ ); that is, for a set $X$ , $\lambda_{X}$ lifts $n$ predicates on $X$ to a predicate on $\mathsf{F}X$ . Predicate liftings determine modalities in coalgebraic modal logic [34, 39]; a basic example is the unary predicate lifting $\lambda$ for the (covariant) powerset functor $\mathcal{P}$ given by $\lambda_{X}(A)=\{B\in\mathcal{P}X\mid B\subseteq A\}$ for a predicate $A\subseteq X$ , which determines the standard box modality on $\mathcal{P}$ -coalgebras, i.e. on standard relational transition systems. A set of predicate liftings is separating if distinct elements of $\mathsf{F}X$ can be separated by lifted predicates; this condition ensures that the associated instance of coalgebraic modal logic is expressive, i.e. separates behaviourally inequivalent states [34, 39]. Monotonicity of predicate liftings allows the definition of modal fixpoint logics for temporal specification [11]. In the mentioned correspondence between lax extensions and predicate liftings, the construction of predicate liftings from a lax extension $\mathsf{L}$ roughly speaking involves application of $\mathsf{L}$ to the elementhood relation.

3 Functor Actions on Difunctional Relations

Our pullback preservation criterion for existence of normal lax extensions grows from an analysis of how functors act on difunctional relations. To start off, it is well-known that normal lax extensions of a given $\mathsf{Set}$ -functor are given on difunctional relations by the action of the functor (e.g. [31, 23]):

Proposition 3.1.

Let $\mathsf{L}$ be an assignment of relations $\mathsf{L}r\colon\mathsf{F}X\includegraphics{dagpub-standalone-dagpub-svg-% displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}\mathsf{F}Y$ to relations $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ that satisfies (L1), (L2) as well as $1_{\mathsf{F}X}\leq\mathsf{L}1_{X}$ for all $X\in\mathsf{Set}$ . Then $\mathsf{L}$ is a lax extension of $\mathsf{F}$ iff for all functions $f\colon W\to X$ , $g\colon Z\to Y$ and relations $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ , $\mathsf{L}(g^{\circ}\cdot r\cdot f)=(\mathsf{F}g)^{\circ}\cdot\mathsf{L}r\cdot% \mathsf{F}f.$

Corollary 3.2.

All normal lax extensions of a given $\mathsf{Set}$ -functor coincide on difunctional relations. Specifically, for every normal lax extension $\mathsf{L}$ of $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ , $\mathsf{L}(g^{\circ}\cdot f)={\mathsf{F}g}^{\circ}\cdot\mathsf{F}f$ for all $f\colon X\to A$ and $g\colon Y\to A$ .

Therefore, a functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ that admits at least one normal lax extension must be monotone on difunctional relations in the following sense: for all difunctional relations $g^{\circ}\cdot f\colon X\includegraphics{dagpub-standalone-dagpub-svg-% displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}Y$ and $g^{\prime\circ}\cdot f^{\prime}\colon X\includegraphics{dagpub-standalone-% dagpub-svg-displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}Y$ , if $g^{\circ}\cdot f\leq g^{\prime\circ}\cdot f^{\prime}$ then $(\mathsf{F}g)^{\circ}\cdot\mathsf{F}f\leq(\mathsf{F}g^{\prime})^{\circ}\cdot% \mathsf{F}f^{\prime}$ . This property no longer mentions lax extensions, and implies that the functor is well-defined on difunctional relations, i.e. that $\mathsf{F}$ sends cospans that determine the same difunctional relation to cospans that determine the same difunctional relation. In this section, we show that being monotone on difunctional relations is equivalent to preserving 1/4-iso (2/4-mono) pullbacks in the sense defined next; as indicated in the introduction, this allows for a quick proof of the fact that the neighbourhood functor fails to admit a normal lax extension [31]. On this occasion, we also discuss various types of pullbacks and their (weak) preservation in some more breadth for later use in our sufficient criteria (Section 4).

Definition 3.3.

We say that a functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ preserves 1/4-iso 2/4-mono pullbacks, 1/4-iso pullbacks, 1/4-mono pullbacks and inverse images if it sends pullbacks of the following forms, respectively, to pullbacks, with arrows $\rightarrowtail$ and $\mathrel{\raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt}% {\makebox(3.0,0.0)[b]{\scriptsize$\raisebox{1.50694pt}{$\simeq$}$}}\hskip 2.5% pt}}$}}$ indicating injectivity and bijectivity correspondingly.

$\blacktriangleright$ Remark 3.4.

1/4-Iso 2/4-mono pullbacks are special inverse images, characterized by the property that the fibre over every element in the image of the function $B\rightarrowtail Y$ is a singleton. In particular, the inverse image of the empty subset is a 1/4-iso 2/4-mono pullback.

Due to the following proposition, for consistency, we tend to use “preservation of 1/4-mono pullbacks” instead of “preservation of inverse images”.

Proposition 3.5.

A $\mathsf{Set}$ -functor preserves 1/4-mono pullbacks iff it preserves inverse images.

Similarly, we will see in Theorem 3.12 that preservation of 1/4-iso pullbacks is equivalent to preservation of 1/4-iso 2/4-mono pullbacks. We thus tend to use the terms “1/4-iso 2/4-mono pullback preserving” and “1/4-iso pullback preserving” interchangeably. Furthermore, in 3.10 we will see that preservation of 1/4-mono pullbacks is properly stronger than preservation of 1/4-iso pullbacks.

Each of the preservation properties introduced in 3.3 implies preservation of monomorphisms, even if we only require that the corresponding pullbacks are weakly preserved. Hence, as at least one of the projections of the pullbacks is monic, preserving the pullbacks mentioned is equivalent to weakly preserving them, and, therefore, each of the properties is implied by weakly preserving pullbacks. Also, note that weakly preserving limits of a given shape is equivalent to preserving weak limits of that shape (e.g. [17, Corollary 4.4]). Furthermore, weakly preserving pullbacks is known to be sufficient for the existence of a normal lax extension – the Barr extension – and this condition can be decomposed as follows:

Theorem 3.6 ([19, Theorem 2.7]).

A $\mathsf{Set}$ -functor weakly preserves pullbacks iff it weakly preserves inverse images and kernel pairs.

It turns out that weakly preserving kernel pairs is equivalent to weakly preserving 4/4-epi pullbacks as defined next.

Definition 3.7.

We say that a functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ weakly preserves 4/4-epi pullbacks, if it sends pullbacks of the form

with arrows $\twoheadrightarrow$ indicating surjectivity, to weak pullbacks (necessarily of surjections).

Theorem 3.8 ([16, Corollary 5]).

A $\mathsf{Set}$ -functor weakly preserves kernel pairs iff it weakly preserves 4/4-epi pullbacks.

Therefore, the condition of weakly preserving pullbacks can be decomposed as:

Corollary 3.9.

A $\mathsf{Set}$ -functor weakly preserves pullbacks iff it weakly preserves 1/4-mono pullbacks and 4/4-epi pullbacks.

In Section 4, we will show that either preserving 1/4-mono pullbacks or weakly preserving 1/4-iso pullbacks and 4/4-epi pullbacks is sufficient for the existence of a normal lax extension.

Example 3.10.

1.

The subfunctor $(-)^{3}_{2}\colon\mathsf{Set}\to\mathsf{Set}$ of the functor $(-)^{3}\colon\mathsf{Set}\to\mathsf{Set}$ that sends a set $X$ to the set of triples of elements of $X$ consisting of at most two distinct elements does not preserve pullbacks weakly [1] but it preserves inverse images.
2.

The neighbourhood functor $\mathcal{N}\colon\mathsf{Set}\to\mathsf{Set}$ (whose coalgebras are neighbourhood frames [10]) sends a set $X$ to the set $\mathcal{N}X=\mathcal{P}\mathcal{P}X$ of neighbourhood systems over $X$ , and a function $f\colon X\to Y$ to the function $\mathcal{N}f\colon\mathcal{N}X\to\mathcal{N}Y$ that assigns to every element $\mathcal{A}\in\mathcal{N}X$ the set $\{B\subseteq Y\mid f^{-1}[B]\in\mathcal{A}\}$ . The monotone neighbourhood functor $\mathcal{M}\colon\mathsf{Set}\to\mathsf{Set}$ is the subfunctor of the neighbourhood functor that sends a set $X$ to the set of upward-closed subsets of $(\mathcal{P}X,\subseteq)$ . Its coalgebras are monotone neighbourhood frames, which feature, e.g., in the semantics of game logic [33] and concurrent dynamic logic [35]. A closely related functor is the clique functor $\mathcal{C}\colon\mathsf{Set}\to\mathsf{Set}$ , which is the subfunctor of $\mathcal{M}$ given by $\mathcal{C}X=\{\alpha\in\mathcal{M}X\mid\forall A,B\in\alpha.\,A\cap B\neq\emptyset\}$ . The functors $\mathcal{M}$ and $\mathcal{C}$ do not preserve inverse images: Consider the sets $3=\{0,1,2\}$ and $2=\{a,b\}$ . Let $e\colon 3\to 2$ be the function that sends $0,1$ to $a$ and $2$ to $b$ , and $B=\{a\}$ . Then $\mathcal{M}e(\operatorname{\uparrow\!}\{0,1\}\cup\operatorname{\uparrow\!}\{1,% 2\})=\operatorname{\uparrow\!}\{a\}$ , where $\operatorname{\uparrow\!}$ denotes upwards closure, but $e^{-1}[B]=\{0,1\}$ and $\operatorname{\uparrow\!}\{0,1\}\cup\operatorname{\uparrow\!}\{1,2\}$ does not belong to the image of the function $\mathcal{M}i\colon\mathcal{M}\{0,1\}\rightarrowtail\mathcal{M}3$ , where $i\colon\{0,1\}\rightarrowtail 3$ denotes the corresponding inclusion. However, routine calculations show that these functors do preserve 1/4-iso (2/4-mono) pullbacks and weakly preserve 4/4-epi pullbacks (for the first functor, see [42, Proposition 4.4]).
3.

Given a commutative monoid $(M,+,0)$ (or just $M$ ), the monoid-valued functor $M^{(-)}$ maps a set $X$ to the set $M^{(X)}$ of functions $\mu\colon X\to M$ with finite support, i.e. $\mu(x)\neq 0$ for only finitely many $x$ . The coalgebras of $M^{(-)}$ are $M$ -weighted transition systems. It is known that $M^{(-)}$ preserves inverse images iff $M$ is positive, i.e. does not have non-zero invertible elements [18, Theorem 5.13] (the cited theorem shows the equivalence for non-empty inverse images; it is easy to check that in case $M$ is positive, $M^{(-)}$ preserves empty pullbacks). Moreover, $M^{(-)}$ preserves weak pullbacks iff $M$ is positive and refinable, i.e. whenever $m_{1}+m_{2}=n_{1}+n_{2}$ for $m_{1},m_{2},n_{1},n_{2}\in M$ , then there exists a $2\times 2$ -matrix with entries in $M$ whose $i$ -th column sums up to $m_{i}$ and whose $j$ -th row sums up to $n_{j}$ , for $i,j\in\{1,2\}$ [18, Theorem 5.13]. Monoids that are positive but not refinable are fairly common [12]; the simplest example is the additive monoid $\{0,1,2\}$ where $2+1=2$ .

The functor $M^{(-)}$ preserves 1/4-iso (2/4-mono) pullbacks iff it preserves inverse images iff $M$ is positive. Indeed, suppose that $M$ is not positive. Consider the functions $!_{2}\colon 2\to 1$ , $!_{\varnothing}\colon\varnothing\to 1$ . Then, for mutually inverse non-zero elements $u$ and $v$ of $M$ , the function $M^{(!_{2})}$ sends both the pair $(0,0)$ and the pair $(u,v)$ to $0\in M^{(1)}$ , which is in the image of $M^{(!_{\varnothing})}\colon M^{(\varnothing)}\to M^{(1)}$ . Therefore, the functor $M^{(-)}$ does not preserve the (1/4-iso) pullback of $(!_{2},!_{\varnothing})$ : This pullback has vertex $\varnothing$ , and $M^{(\varnothing)}$ has only one element.
4.

In recent work [16], it has been shown that the functor of a monad induced by a variety of algebras preserves inverse images iff whenever a variable $x$ is canceled from a term when identified with other variables, then the term does not actually depend on $x$ . This provides a large reservoir of functors that preserve inverse images but do not always have easily guessable normal lax extensions (whose existence will however be guaranteed by our main results). One example is the functor that maps a set $X$ to the free semigroup over $X$ quotiented by the equation $xxx=xx$ , as neither this equation nor associativity cancel any variables. Notice that this functor does not preserve 4/4-epi pullbacks.

Finally, we show that being monotone on difunctional relations is equivalent to preserving 1/4-iso (2/4-mono) pullbacks. The next lemma connects the order on difunctional relations and pullbacks of such type.

Lemma 3.11.

Let $X\mathrel{\raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt% }{\makebox(3.0,0.0)[b]{\scriptsize$f$}}\hskip 2.5pt}}$}}A\mathrel{\raisebox{-1% .15pt}{$\xleftarrow{\smash{\hskip 3.5pt\raisebox{-2.5pt}{\makebox(3.0,0.0)[b]{% \scriptsize$g$}}\hskip 1.5pt}}$}}Y$ and $X\mathrel{\raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt% }{\makebox(3.0,0.0)[b]{\scriptsize$f^{\prime}$}}\hskip 2.5pt}}$}}A^{\prime}% \mathrel{\raisebox{-1.15pt}{$\xleftarrow{\smash{\hskip 3.5pt\raisebox{-2.5pt}{% \makebox(3.0,0.0)[b]{\scriptsize$g^{\prime}$}}\hskip 1.5pt}}$}}Y$ be cospans for which there is a map $h\colon A\to A^{\prime}$ such that $f^{\prime}=h\cdot f$ and $g^{\prime}=h\cdot g$ . Moreover, consider the commutative square

(3.i)

where $h^{\prime}\colon f[X]\cap g[Y]\to f^{\prime}[X]\cap g^{\prime}[Y]$ is the restriction of $h$ to $f[X]\cap g[Y]$ and the vertical arrows denote subset inclusions.

1.

If $g^{\circ}\cdot f\geq g^{\prime\circ}\cdot f^{\prime}$ , then $h^{\prime}$ is a bijection.
2.

If $g^{\circ}\cdot f\geq g^{\prime\circ}\cdot f^{\prime}$ and the cospan $(f,g)$ is epi, then (3.i) is a pullback.
3.

If $h^{\prime}$ is a bijection and (3.i) is a pullback, then $g^{\circ}\cdot f\geq g^{\prime\circ}\cdot f^{\prime}$ .

(Notice in particular that if $h^{\prime}$ is a bijection and (3.i) is a pullback, then (3.i) is a 1/4-iso pullback.) Using 3.11, one proves the announced characterization:

Theorem 3.12.

The following clauses are equivalent for a functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ :

1.

$\mathsf{F}$ preserves 1/4-iso 2/4-mono pullbacks.
2.

$\mathsf{F}$ is well-defined on difunctional relations.
3.

$\mathsf{F}$ is monotone on difunctional relations.
4.

$\mathsf{F}$ preserves 1/4-iso pullbacks.

Corollary 3.13.

If a $\mathsf{Set}$ -functor admits a normal lax extension, then it preserves 1/4-iso pullbacks.

Therefore, the following functors do not admit a normal lax extension.

Example 3.14.

1.

The neighbourhood functor $\mathcal{N}\colon\mathsf{Set}\to\mathsf{Set}$ (cf. 3.10(2)) does not preserve 1/4-iso pullbacks: the element $\mathcal{P}1\in\mathcal{N}1$ belongs to the image of the function $\mathcal{N}!_{\varnothing}$ , with $!_{\varnothing}\colon\varnothing\rightarrowtail 1$ , however, its fiber w.r.t. $\mathcal{N}!_{2}$ , with $!_{2}\colon 2\to 1$ , is not a singleton.
2.

For every non-positive commutative monoid, the monoid valued functor $M^{(-)}\colon\mathsf{Set}\to\mathsf{Set}$ does not preserve 1/4-iso pullbacks (3.10(3)).
3.

More generally, by (the proof of) [12, Proposition 4.4], the functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ of the monad induced by a variety of algebras that admits a weak form of subtraction (for instance, groups, rings, vector spaces) does not preserve 1/4-iso pullbacks.
4.

For every set $A$ with at least two elements, consider the functor $\mathsf{Set}(A,-)/\sim$ that maps a set $X$ to the quotient of the set $\mathsf{Set}(A,X)$ by the equivalence relation $\sim$ that identifies exactly all non-injective maps, and maps a function $f\colon X\to Y$ to the one sending the equivalence class of $g\colon A\to X$ to that of $f\cdot g$ . This functor does not preserve 1/4-iso pullbacks. For instance, for $A=\{0,1\}$ , consider the sets $3=\{a,b,c\}$ and $B=\{0\}$ . Then, the fibre of each element of $B\subseteq A$ w.r.t. the function $f\colon 3\to A$ that sends $a$ to $0$ and $b, c$ to $1$ is a singleton; however, the fibre of the equivalence class of the constant map into $0$ w.r.t. $\mathsf{Set}(A,f)_{\sim}$ is not a singleton. Similar counterexamples can be constructed for arbitrary $A$ with at least two elements.

$\blacktriangleright$ Remark 3.15.

Every coalgebra can be quotiented by behavioural equivalence (e.g. [25]). Such a quotient can be described by a cocongruence on a given coalgebra, i.e. an equivalence relation that is compatible with the coalgebra structure, and, of course, a cocongruence can be specified by a generating relation that need not itself be an equivalence. For instance, cocongruences have been studied in the context of linear weighted automata [9] (where they are in fact termed bisimulations), and even on neighbourhood frames, one obtains such a notion of equivalence-witnessing relation from the standard Barr extension [31]. All this does not contradict the moral claim that, by 3.14, there are no “good” notions of bisimulation for, e.g., neighbourhood frames or integer-weighted transition systems, as (generating relations of) cocongruences are missing some of the features that we include in the wish list for bisimulations and that $L$ -bisimulations do provide (cf. Section 2). Notably, cocongruences work only on a single coalgebra (while we expect bisimulations to connect two possibly different coalgebras), and they fail to be closed under relational composition.

4 Existence of Normal Lax Extensions

We proceed to present the main results of the paper: a $\mathsf{Set}$ -functor that weakly preserves 1/4-iso pullbacks and 4/4-epi pullbacks, or that preserves 1/4-mono pullbacks admits a normal lax extension. In view of the facts recalled in Section 2, this means that these functors admit a notion of bisimulation that captures behavioural equivalence, or equivalently, that they admit a separating class of monotone predicate liftings.

We begin by showing that the smallest lax extension of a $\mathsf{Set}$ -functor is obtained by “closing its Barr relax extension under composition”. As a consequence, in 4.5 we obtain a criterion to determine if a $\mathsf{Set}$ -functor admits a normal lax extension.

Consider the partially ordered classes $\mathsf{Lax(\mathsf{F})}$ and $\mathsf{ReLax(\mathsf{F})}$ of lax and relax extensions of $\mathsf{F}$ , respectively, ordered pointwise. With the following result we can construct lax extensions from relax extensions in a universal way.

Proposition 4.1.

Let $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ be a functor. The inclusion $\mathsf{Lax(\mathsf{F})}\rightarrowtail\mathsf{ReLax(\mathsf{F})}$ has a left adjoint $(-)^{\bullet}\colon\mathsf{ReLax(\mathsf{F})}\to\mathsf{Lax(\mathsf{F})}$ that sends a relax extension $\mathsf{R}\colon\mathsf{Rel}\to\mathsf{Rel}$ of $\mathsf{F}$ to its laxification $\mathsf{R}^{\bullet}\colon\mathsf{Rel}\to\mathsf{Rel}$ , which is defined on $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ by

\mathsf{R}^{\bullet}r=\bigvee_{\begin{subarray}{c}r_{1},\ldots,r_{n}\colon\\ r_{n}\cdot\ldots\cdot r_{1}\leq r\end{subarray}}\mathsf{R}r_{n}\cdot\ldots% \cdot\mathsf{R}r_{1}.

(4.i)

Furthermore, if a relax extension $\mathsf{R}\colon\mathsf{Set}\to\mathsf{Set}$ preserves converses, then so does its laxification.

Since every lax extension of a functor is greater than or equal to the Barr relax extension (cf. Section 2), we thus have:

Corollary 4.2.

The smallest lax extension of a functor is given by the laxification of its Barr relax extension.

For the Barr relax extension of a $\mathsf{Set}$ -functor, the supremum in the formula (4.i) can be restricted as follows.

Lemma 4.3.

For every composable sequence $r_{1},\ldots,r_{n}$ such that $r_{n}\cdot\ldots\cdot r_{1}\leq r$ , for some relation $r$ , there is a composable sequence $r_{1}^{\prime},\ldots,r_{n}^{\prime}$ such that $r_{n}^{\prime}\cdot\ldots\cdot r_{1}^{\prime}=r$ and $\mathsf{\overline{F}}r_{n}\cdot\ldots\cdot\mathsf{\overline{F}}r_{1}\leq% \mathsf{\overline{F}}r_{n}^{\prime}\cdot\ldots\cdot\mathsf{\overline{F}}r_{1}^% {\prime}$ .

Corollary 4.4.

Let $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ be a functor. For every relation $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ ,

\displaystyle(\mathsf{\overline{F}})^{\bullet}r=\bigvee_{\begin{subarray}{c}r_% {1},\ldots,r_{n}\colon\\ r_{n}\cdot\ldots\cdot r_{1}=r\end{subarray}}\mathsf{\overline{F}}r_{n}\cdot% \ldots\cdot\mathsf{\overline{F}}r_{1}.

Therefore, as normality of a lax extension also implies normality of any lax extension below it, we have

Corollary 4.5.

A functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ admits a normal lax extension iff the laxification of its Barr relax extension is normal. More concretely, a functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ admits a normal lax extension iff for every set $X$ and every composable sequence of relations $r_{1},\ldots,r_{n}$ , whenever $r_{n}\cdot\ldots\cdot r_{1}=1_{X}$ , then $\mathsf{\overline{F}}r_{n}\cdot\ldots\cdot\mathsf{\overline{F}}r_{1}\leq 1_{% \mathsf{F}X}$ .

$\blacktriangleright$ Remark 4.6.

It is well-known [6] that for every functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ and all relations $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ and $s\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Z$ , $\mathsf{\overline{F}}(s\cdot r)\leq\mathsf{\overline{F}}s\cdot\mathsf{% \overline{F}}r$ . Hence, once we show the inequality of 4.5 we actually have equality.

In general terms, our main results follow by showing that in 4.5, under certain conditions on $\mathsf{Set}$ -functors, it suffices to consider composable sequences of relations that satisfy nice properties. In this regard, it is convenient to introduce the following notion.

Definition 4.7.

Let $r_{1},\ldots,r_{n}$ be a composable sequence of relations. A composable sequence $s_{1},\ldots,s_{k}$ is said to be a Barr upper bound of the sequence $r_{1},\ldots,r_{n}$ if $r_{n}\cdot\ldots\cdot r_{1}=s_{k}\cdot\ldots\cdot s_{1}$ and $\mathsf{\overline{F}}r_{n}\cdot\ldots\cdot\mathsf{\overline{F}}r_{1}\leq% \mathsf{\overline{F}}s_{k}\cdot\ldots\cdot\mathsf{\overline{F}}s_{1}$ .

In Section 3 we have seen that every $\mathsf{Set}$ -functor that admits a normal lax extension preserves 1/4-iso pullbacks, or equivalently, it is monotone on difunctional relations (Theorem 3.12). As we show next, the latter condition is also equivalent to satisfying the criterion of 4.5 for pairs of composable relations.

Proposition 4.8.

Let $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ be a functor. The following clauses are equivalent:

(i)

The functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ preserves 1/4-iso pullbacks.
(ii)

For all relations $r_{1}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Y$ , $r_{2}\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}X$ such that $r_{2}\cdot r_{1}\leq 1_{X}$ , $\mathsf{\overline{F}}r_{2}\cdot\mathsf{\overline{F}}r_{1}\leq 1_{\mathsf{F}X}$ .
(iii)

For all relations $r_{1}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Y$ , $r_{2}\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}X$ such that $r_{2}\cdot r_{1}=1_{X}$ , $\mathsf{\overline{F}}r_{2}\cdot\mathsf{\overline{F}}r_{1}\leq 1_{\mathsf{F}X}$ .

Now, suppose that we want to extend the previous result in inductive style to composable triples of relations. Due to the next lemma, a simple idea to reduce the case of composable triples to the case of composable pairs of relations is to take the difunctional closure of the second relation in the sequence.

Lemma 4.9.

Let $r_{1}\colon X_{0}\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X_{1}$ , $r_{2}\colon X_{1}\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X_{2}$ and $r_{3}\colon X_{2}\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X_{3}$ be relations given by spans that form the base of the commutative diagram

Then, with $r_{1}^{\prime}\colon X\includegraphics{dagpub-standalone-dagpub-svg-% displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}O$ and $r_{3}^{\prime}\colon O\includegraphics{dagpub-standalone-dagpub-svg-% displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}X_{3}$ defined by the spans $X_{0}\mathrel{\raisebox{-1.15pt}{$\xleftarrow{\smash{\hskip 3.5pt\raisebox{-2.% 5pt}{\makebox(3.0,0.0)[b]{\scriptsize$\pi_{1}$}}\hskip 1.5pt}}$}}R_{1}\mathrel% {\raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt}{% \makebox(3.0,0.0)[b]{\scriptsize$\rho_{1}^{\prime}$}}\hskip 2.5pt}}$}}O$ and $X_{0}\mathrel{\raisebox{-1.15pt}{$\xleftarrow{\smash{\hskip 3.5pt\raisebox{-2.% 5pt}{\makebox(3.0,0.0)[b]{\scriptsize$\pi_{3}^{\prime}$}}\hskip 1.5pt}}$}}R_{3% }\mathrel{\raisebox{-1.15pt}{$\xrightarrow{\hskip 2.5pt\smash{\raisebox{-2.5pt% }{\makebox(3.0,0.0)[b]{\scriptsize$\rho_{3}$}}\hskip 2.5pt}}$}}X_{3}$ , respectively, $\mathsf{\overline{F}}r_{3}\cdot\mathsf{\overline{F}}r_{2}\cdot\mathsf{% \overline{F}}r_{1}\leq\mathsf{\overline{F}}r_{3}\cdot\mathsf{\overline{F}}\hat% {r}_{2}\cdot\mathsf{\overline{F}}r_{1}\leq\mathsf{\overline{F}}r_{3}^{\prime}% \cdot\mathsf{\overline{F}}r_{1}^{\prime}$ .

Indeed, let $r_{1}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}X_{1}$ , $r_{2}\colon X_{1}\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X_{2}$ and $r_{3}\colon X_{2}\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X$ be relations such that $r_{3}\cdot r_{2}\cdot r_{1}=1_{X}$ . Then, by 4.8 and 4.9, we conclude that $\mathsf{\overline{F}}r_{3}\cdot\mathsf{\overline{F}}r_{2}\cdot\mathsf{% \overline{F}}r_{1}\leq 1_{\mathsf{F}X}$ once we show that $r_{3}^{\prime}\cdot r_{1}^{\prime}=1_{X}$ . Of course, in general, this does not hold. Consider the following example where the arrows depict pairs of related elements.

By taking the difunctional closure $\hat{r}_{2}$ of $r_{2}$ we get

So, $r_{3}\cdot\hat{r}_{2}\cdot r_{1}=r_{3}^{\prime}\cdot r_{1}^{\prime}$ is not a subidentity. Now the property of preserving 1/4-iso pullbacks is helpful again. As we will see in 4.10, under this condition, the sequence below is a Barr upper bound of the first one and it is obtained from it by “splitting” where necessary the elements of $X_{1}$ that do not belong to the codomain of $r_{1}$ and the elements of $X_{2}$ that do not belong to the domain of $r_{3}$ .

In this situation we can apply the difunctional closure to $r_{2}$ (which in this particular example is already difunctional) to reduce the number of relations as discussed in 4.9.

Lemma 4.10.

Let $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ be a functor that preserves 1/4-iso pullbacks, and let $r_{1}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Y$ , $r_{2}\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Z$ and $r_{3}\colon Z\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}W$ be relations. Then, there are relations $s_{1}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Y^{\prime}$ , $s_{2}\colon Y^{\prime}\includegraphics{dagpub-standalone-dagpub-svg-% displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}Z^{\prime}$ and $s_{3}\colon Z^{\prime}\includegraphics{dagpub-standalone-dagpub-svg-% displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}W$ such that $s_{1},s_{2},s_{3}$ is a Barr upper bound of $r_{1},r_{2},r_{3}$ and

1.

for all $y,y^{\prime}\in Y^{\prime}$ and all $z\in Z^{\prime}$ , if $y\neq y^{\prime}$ , $y\mathrel{s_{2}}z$ and $y^{\prime}\mathrel{s_{2}}z$ , then $z\in\mathop{{\operatorname{\mathsf{dom}}}}(s_{3})$ ;
2.

for all $y\in Y^{\prime}$ and $z,z^{\prime}\in Z^{\prime}$ , if $z\neq z^{\prime}$ , $y\mathrel{s_{2}}z$ and $y\mathrel{s_{2}}z^{\prime}$ , then $y\in\mathop{{\operatorname{\mathsf{cod}}}}(s_{1})$ .

The previous lemma essentially closes the argument that we have been crafting so far.

Theorem 4.11.

Let $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ be a functor. The following clauses are equivalent:

(i)

The functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ preserves 1/4-iso pullbacks.
(ii)

For all relations $r_{1}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Y$ , $r_{2}\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Z$ and $r_{3}\colon Z\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}X$ such that $r_{3}\cdot r_{2}\cdot r_{1}\leq 1_{X}$ , $\mathsf{\overline{F}}r_{3}\cdot\mathsf{\overline{F}}r_{2}\cdot\mathsf{% \overline{F}}r_{1}\leq 1_{\mathsf{F}X}$ .
(iii)

For all relations $r_{1}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Y$ , $r_{2}\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}Z$ and $r_{3}\colon Z\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}X$ such that $r_{3}\cdot r_{2}\cdot r_{1}=1_{X}$ , $\mathsf{\overline{F}}r_{3}\cdot\mathsf{\overline{F}}r_{2}\cdot\mathsf{% \overline{F}}r_{1}\leq 1_{\mathsf{F}X}$ .

However, as we see next, Theorem 4.11 is as far as we can go under the assumption of 1/4-iso pullbacks preservation. In other words, the fact that a $\mathsf{Set}$ -functor preserves 1/4-iso pullbacks is not sufficient to conclude that it admits a normal lax extension.

Example 4.12.

Let us define a functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ as a quotient of $\coprod_{n\in\{f,g\}}\{n\}\times X^{5}\cong X^{5}+X^{5}$ under the equivalence defined by the clauses:

$\displaystyle f(y,x,z,x,t)\sim\;$	$\displaystyle f(y^{\prime},x,z^{\prime},x,t^{\prime})$	$\displaystyle f(t,x,x,y,y)\sim\;$	$\displaystyle f(t^{\prime},x,x,y,y)$
$\displaystyle g(y,x,z,x,t)\sim\;$	$\displaystyle g(y^{\prime},x,z^{\prime},x,t^{\prime})$	$\displaystyle g(x,x,y,y,t)\sim\;$	$\displaystyle g(x,x,y,y,t^{\prime})$
$\displaystyle f(y,x,z,x,t)\sim\;$	$\displaystyle g(y^{\prime},x,z^{\prime},x,t^{\prime})$	$\displaystyle f(t,x,z,y,z)\sim\;$	$\displaystyle g(t,x,t,y,z)$

where $f(x_{1},\ldots,x_{5})$ and $g(x_{1},\ldots,x_{5})$ denote the corresponding elements $(f,x_{1},\ldots,x_{5}),\operatorname{}\linebreak[1](g,x_{1},\ldots,x_{5})\in% \coprod_{n\in\{f,g\}}\{n\}\times X^{5}$ . Let $2=\{x,y\}$ and consider the composable sequence of relations depicted below.

Then, $\mathsf{F}$ preserves 1/4-iso pullbacks and $r_{4}\cdot r_{3}\cdot r_{2}\cdot r_{1}=1_{2}$ , however, $\mathsf{\overline{F}}r_{4}\cdot\mathsf{\overline{F}}r_{3}\cdot\mathsf{% \overline{F}}r_{2}\cdot\mathsf{\overline{F}}r_{1}\not\leq 1_{\mathsf{F}2}$ .

4.1 The case of functors that weakly preserve 4/4-epi pullbacks

From Theorem 4.11 it basically follows that a functor that weakly preserves 1/4-iso pullbacks and 4/4-epi pullbacks admits a normal lax extension. But to see this, first we need to sharpen 4.5. The goal is to show that it suffices to consider composable sequences of relations where all relations other than the first and the last are total and surjective. To illustrate how we achieve this, let us consider the sequence of relations depicted below.

Then, by adding new elements $0$ and $1$ to $X_{1},X_{2}$ and $X_{3}$ we can extend this sequence to the sequence

where the dotted arrows indicate pairs of elements that were added to the corresponding relation as follows: for $i=2,3$ , $r^{\prime}_{i}$ relates $0\in X^{\prime}_{i-1}$ to every element of $X_{i}\cup\{0\}$ that does not belong to the codomain of $r_{i}$ and relates every element of $X_{i-1}\cup\{1\}$ that does not belong to the domain of $r_{i}$ to $1\in X^{\prime}_{i}$ . In this way, we guarantee that $r^{\prime}_{2}$ and $r_{3}^{\prime}$ are total and surjective and that $r_{4}^{\prime}\cdot r_{3}^{\prime}\cdot r_{2}^{\prime}\cdot r_{1}^{\prime}=r_{% 4}\cdot r_{3}\cdot r_{2}\cdot r_{1}=1_{X}$ . We could have extended $r_{2}$ and $r_{3}$ to total and surjective relations by adding just a single element $\ast$ to $X_{1}$ , $X_{2}$ and $X_{3}$ that would simultaneously take the role of $0$ and $1$ . However, composing the resulting sequence of relations would not yield the identity relation:

In other words, by splitting $\ast$ in two elements $0$ and $1$ , the former to make the relations $r_{2}$ and $r_{3}$ surjective and the latter to make them total, we obtain a subidentity because we never create paths between elements of $X_{1}$ that are not part of the domain of $r_{2}$ and elements of $X_{3}$ that are not part of the codomain of $r_{3}$ . In the next lemma we formalize this procedure for arbitrary composable sequences of relations and show that it yields Barr upper bounds.

Lemma 4.13.

A functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ that preserves 1/4-iso pullbacks admits a normal lax extension iff for every composable sequence of relations $r_{1},\ldots,r_{n}$ such that $n\geq 4$ and $r_{2},\ldots,r_{n-1}$ are total and surjective, whenever $r_{n}\cdot\ldots\cdot r_{1}=1_{X}$ , for some set $X$ , then $\mathsf{\overline{F}}r_{n}\cdot\ldots\cdot\mathsf{\overline{F}}r_{1}\leq 1_{% \mathsf{F}X}$ .

$\blacktriangleright$ Remark 4.14.

In a composable sequence of relations that satisfies the conditions of 4.13 the first relation is necessarily total while the last one is necessarily surjective.

Now, our first main result follows straightforwardly. Since the composite of total and surjective relations is total and surjective, due to the following fact, every composable sequence of relations where all relations other than the first and the last are total and surjective admits a Barr upper bound consisting of three relations.

Proposition 4.15.

A functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ weakly preserves 4/4-epi pullbacks iff for all relations $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ and $s\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Z$ , whenever $r$ is surjective and $s$ is total, $\mathsf{\overline{F}}s\cdot\mathsf{\overline{F}}r=\mathsf{\overline{F}}(s\cdot r)$ .

Theorem 4.16.

A $\mathsf{Set}$ -functor that weakly preserves 1/4-iso pullbacks and 4/4-epi weak pullbacks admits a normal lax extension.

$\blacktriangleright$ Remark 4.17.

Preservation of 4/4-epi pullbacks plays a role in the analysis of interpolation in coalgebraic logic [42]. In particular, this analysis implies that given a separating set $\Lambda$ of monotone predicate liftings for a finite-set-preserving functor $\leavevmode\nobreak\ \mathsf{F}$ , which induces an expressive modal logic $\mathcal{L}(\Lambda)$ for $\leavevmode\nobreak\ \mathsf{F}$ -coalgebras, the logic $\mathcal{L}(\Lambda)$ has interpolation iff $\mathsf{F}$ weakly preserves 4/4-epi pullbacks [42, Theorem 37]. In connection with the fact that a functor has a normal lax extension iff it has a separating set of monotone predicate liftings [31], we obtain the following application of Theorem 4.16 and 3.13: A finite-set preserving functor $\mathsf{F}$ has a separating set of monotone predicate liftings such that the associated modal logic has uniform interpolation iff $\mathsf{F}$ weakly preserves 1/4-iso pullbacks and 4/4-epi pullbacks.

4.2 The case of functors that preserve 1/4-mono pullbacks

To obtain Theorem 4.16, we refined 4.5 to composable sequences of relations where all relations other than the first and the last are total and surjective. And to achieve this in 4.13, given a composable sequence of relations, we added pairs of related elements to the relations in the sequence. In the sequel, we will show that every functor that preserves 1/4-mono pullbacks admits a normal lax extension. We will see that for these functors it is even possible to refine 4.5 to composable sequences of relations where all relations are total and surjective. However, we will achieve this in 4.19 below by, given a composable sequence of relations, removing pairs of related elements from the relations in the sequence. Our proof strategy is justified by the next fact.

Proposition 4.18.

A functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ preserves 1/4-mono pullbacks iff for all relations $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ and $s\colon Y\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Z$ , whenever $r$ is the converse of a partial function or $s$ is a partial function, $\mathsf{\overline{F}}s\cdot\mathsf{\overline{F}}r=\mathsf{\overline{F}}(s\cdot r)$ .

This result enables a “look ahead and behind” strategy for 4.5. The idea is that, given a composable sequence of relations $r_{1},\ldots,r_{n}$ such that $r_{n}\cdot\ldots\cdot r_{1}=1_{X}$ , then, with $r_{i}\colon X_{i-1}\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2% 025-05-08-15-52-40-1.pdf2svg.svg}X_{i}$ being a relation in the sequence, removing the elements of $X_{i}$ that do not belong to the codomain of $r_{i}\cdot\ldots\cdot r_{1}$ or do not belong to the domain of $r_{n}\cdot\ldots\cdot r_{i+1}$ yields a Barr upper bound of our original sequence. For instance, consider the composable sequence of relations depicted in 4.12, which we used to show that there are functors that preserve 1/4-iso pullbacks but do not admit a normal lax extension. In the next lemma, in particular, we show that for functors that preserve 1/4-mono pullbacks the sequence below of total and surjective relations is a Barr upper bound of this one. The dotted arrows represent pairs of related elements that were removed, and the grey boxes represent the elements of each set that are not removed.

Lemma 4.19.

A functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ that preserves 1/4-mono pullbacks admits a normal lax extension if for every composable sequence of total and surjective relations $r_{1},\ldots,r_{n}$ , whenever $r_{n}\cdot\ldots\cdot r_{1}=1_{X}$ for some set $X$ , then $\mathsf{\overline{F}}r_{n}\cdot\ldots\cdot\mathsf{\overline{F}}r_{1}\leq 1_{% \mathsf{F}X}$ .

It turns out that the sufficient condition of the previous lemma is actually satisfied by every $\mathsf{Set}$ -functor that preserves 1/4-iso pullbacks. Indeed, due to the next result, 4.9 and the fact that surjections are stable under pushouts, every composable sequence of total and surjective relations whose composite is an identity admits a Barr upper bound consisting of three relations.

Lemma 4.20.

Let $r_{1}\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05% -08-15-52-40-1.pdf2svg.svg}X_{1}$ , $r_{2}\colon X_{1}\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X_{2}$ and $r_{3}\colon X_{2}\includegraphics{dagpub-standalone-dagpub-svg-displaymath-202% 5-05-08-15-52-40-1.pdf2svg.svg}X$ be a composable sequence of total and surjective relations, and let $\hat{r}_{2}\colon X_{1}\includegraphics{dagpub-standalone-dagpub-svg-% displaymath-2025-05-08-15-52-40-1.pdf2svg.svg}X_{2}$ be the difunctional closure of $r_{2}$ . If $r_{3}\cdot r_{2}\cdot r_{1}=1_{X}$ , then $r_{3}\cdot\hat{r}_{2}\cdot r_{1}=1_{X}$ .

Proposition 4.21.

Let $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ be a functor that preserves 1/4-iso pullbacks, and let $r_{1},\ldots,r_{n}$ be a composable sequence of total and surjective relations. If $r_{n}\cdot\ldots\cdot r_{1}=1_{X}$ for some set $X$ , then $\mathsf{\overline{F}}r_{n}\cdot\ldots\cdot\mathsf{\overline{F}}r_{1}\leq 1_{% \mathsf{F}X}$ .

Therefore,

Theorem 4.22.

Every $\mathsf{Set}$ -functor that preserves 1/4-mono pullbacks admits a normal lax extension.

In particular, since in 3.10(3) we have seen that for (commutative) monoid-valued functors preserving 1/4-mono pullbacks is equivalent to preserving 1/4-iso pullbacks, as a consequence of Theorem 4.22 and 3.13 we obtain:

Corollary 4.23.

A (commutative) monoid-valued functor admits a normal lax extension iff the monoid is positive.

$\blacktriangleright$ Remark 4.24.

The above result may be equivalently stated as saying that a monoid-valued functor has a separating set of monotone predicate liftings iff the monoid is positive. In this formulation, it improves on a previous result effectively stating the same equivalence under the additional assumption that the monoid is refinable [42, Proposition 22]. For every monoid $M$ , one has a preorder on $M$ given by $m\geq n$ iff $\exists k\in M.\,m=n+k$ , which is a partial order whenever the monoid is cancellative and positive. It is then clear that one has a separating set of monotone predicate liftings $\Diamond_{m}$ , for $m\in M$ , defined by $\Diamond_{m}(A)=\{\mu\in M^{(X)}\mid\mu(A)\geq m\}$ where we write $\mu(A)=\sum_{x\in A}\mu(x)$ . The arising normal lax extension is given for $r\colon X\includegraphics{dagpub-standalone-dagpub-svg-displaymath-2025-05-08-% 15-52-40-1.pdf2svg.svg}Y$ , $\mu\in M^{(X)}$ , $\nu\in M^{(Y)}$ by $\mu\mathrel{Lr}\nu$ iff $\nu(r[A])\geq\mu(A)$ for all $A\subseteq X$ and symmetrically, much like for probabilistic transition systems (2.3(2)). For non-cancellative positive monoids, the description of the normal lax extension and the separating set of monotone predicate liftings whose existence are guaranteed by 4.23 is in general more involved. In particular, the predicate liftings $\Diamond_{m}$ described above may fail to be separating, as witnessed, for instance, by the commutative additive monoid $\{0,1,2\}$ with $1+2=1$ . Specifically, $\mu,\nu\in M^{(\{\star\})}$ given by $\mu(\star)=1$ and $\nu(\star)=2$ cannot be distinguished.

The class of $\mathsf{Set}$ -functors that admit a normal lax extension is closed under subfunctors and several natural constructions such as the sum of functors. This makes it easy to extend the reach of our sufficient conditions, but it also shows that it is easy to provide examples of functors that admit a normal lax extension and do not weakly preserve 1/4-mono pullbacks nor 4/4-epi pullbacks. A quick example is the functor given by the sum of the functor $(-)^{3}_{2}$ and the monotone neighbourhood functor. To conclude this section, we present a less obvious example that is constructed analogously to 4.12. Notice that, as we have seen in 3.14(4), the class of functors that admit a normal lax extension is not closed under quotients.

Example 4.25.

For any set $X$ , let $\mathsf{F}X$ be the quotient of $X^{3}$ under the equivalence relation $\sim$ defined by the clauses $(x,x,y)\sim(x,x,x)\sim(y,x,x)$ . This yields a functor $\mathsf{F}\colon\mathsf{Set}\to\mathsf{Set}$ that neither weakly preserves 1/4-mono pullbacks nor 4/4-epi pullbacks, however, $\mathsf{F}$ admits a normal lax extension.

5 Conclusions

Normal lax extensions of functors play a dual role in the coalgebraic modelling of reactive systems, on the one hand allowing for good notions of bisimulations on functor coalgebras and on the other hand guaranteeing the existence of expressive temporal logics. We have shown on the one hand that every functor admitting a lax extension preserves 1/4-iso pullbacks, and on the other hand that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks or inverse images. These results improve on previous results [28, 30, 31], which combine to imply that weak-pullback-preserving functors admit normal lax extensions. One application of our results implies, roughly, that a given type of monoid-weighted transition systems admits a good notion of bisimulation iff the monoid is positive.

The most obvious issue for future work is to close the remaining gap, i.e. to give a necessary and sufficient criterion for the existence of normal lax extensions in terms of limit preservation. Additionally, the structure of the lattice of normal lax extensions of a functor merits attention, in the sense that larger lax extensions induce more permissive notions of bisimulation.

References

[1] Peter Aczel and Nax Paul Mendler. A final coalgebra theorem. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings, volume 389 of Lecture Notes in Computer Science, pages 357–365. Springer, 1989. doi:10.1007/BFB0018361.
[2] Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and concrete categories: The joy of cats. John Wiley & Sons Inc., 1990. Republished in: Reprints in Theory and Applications of Categories, No. 17 (2006) pp. 1–507. URL: http://tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
[3] Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. Polynomial relators (extended abstract). In Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo, editors, Algebraic Methodology and Software Technology, AMAST 1991, Workshops in Computing, pages 303–326. Springer, 1991.
[4] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:20)2018.
[5] Michael Barr. Relational algebras. In Reports of the Midwest Category Seminar IV, number 137 in Lect. Notes Math., pages 39–55. Springer, 1970. doi:10.1007/BFb0060439.
[6] Michael Barr. Relational algebras. In Reports of the Midwest Category Seminar IV, pages 39–55. Springer, 1970. doi:10.1007/bfb0060439.
[7] Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299–315, 1993. doi:10.1016/0304-3975(93)90076-6.
[8] Richard S. Bird and Oege de Moor. Algebra of programming. Prentice Hall International series in computer science. Prentice Hall, 1997.
[9] Filippo Bonchi, Marcello M. Bonsangue, Michele Boreale, Jan J. M. M. Rutten, and Alexandra Silva. A coalgebraic perspective on linear weighted automata. Inf. Comput., 211:77–105, 2012. doi:10.1016/J.IC.2011.12.002.
[10] Brian F. Chellas. Modal Logic – An Introduction. Cambridge University Press, 1980. doi:10.1017/CBO9780511621192.
[11] Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic mu-calculus. Log. Methods Comput. Sci., 7(3), 2011. doi:10.2168/LMCS-7(3:3)2011.
[12] Maria Manuel Clementino, Dirk Hofmann, and George Janelidze. The monads of classical algebra are seldom weakly cartesian. J. Homotopy and Related Structures, 9(1):175–197, 2014.
[13] Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Anuj Dawar and Erich Grädel, editors, Logic in Computer Science, LICS 2018, pages 452–461. ACM, 2018. doi:10.1145/3209108.3209149.
[14] Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. A point-free perspective on lax extensions and predicate liftings. Mathematical Structures in Computer Science, pages 1–30, 2023. doi:10.1017/S096012952300035X.
[15] Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science, CALCO 2013, volume 8089 of LNCS, pages 253–266. Springer, 2013. doi:10.1007/978-3-642-40206-7_19.
[16] H. Peter Gumm. Free-algebra functors from a coalgebraic perspective. In Daniela Petrisan and Jurriaan Rot, editors, Coalgebraic Methods in Computer Science, CMCS 2020, volume 12094 of LNCS, pages 55–67. Springer, 2020. doi:10.1007/978-3-030-57201-3_4.
[17] H. Peter Gumm and Tobias Schröder. Coalgebraic structure from weak limit preserving functors. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, Berlin, Germany, March 25-26, 2000, volume 33 of Electronic Notes in Theoretical Computer Science, pages 111–131. Elsevier, 2000. doi:10.1016/S1571-0661(05)80346-9.
[18] H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. In Andrea Corradini, Marina Lenisa, and Ugo Montanari, editors, Coalgebraic Methods in Computer Science, CMCS 2001, volume 44(1) of ENTCS, pages 185–204. Elsevier, 2001. doi:10.1016/S1571-0661(04)80908-3.
[19] H. Peter Gumm and Tobias Schröder. Types and coalgebraic structure. Algebra universalis, 53(2–3):229–252, August 2005. doi:10.1007/s00012-005-1888-2.
[20] H. Peter Gumm and Mehdi Zarrad. Coalgebraic simulations and congruences. In Marcello M. Bonsangue, editor, Coalgebraic Methods in Computer Science - 12th IFIP WG 1.3 International Workshop, CMCS 2014, Colocated with ETAPS 2014, Grenoble, France, April 5-6, 2014, Revised Selected Papers, volume 8446 of Lecture Notes in Computer Science, pages 118–134. Springer, 2014. doi:10.1007/978-3-662-44124-4_7.
[21] Helle Hvid Hansen and Clemens Kupke. A coalgebraic perspective on monotone modal logic. In Jirí Adámek and Stefan Milius, editors, Coalgebraic Methods in Computer Science, CMCS 2004, volume 106 of ENTCS, pages 121–143. Elsevier, 2004. doi:10.1016/j.entcs.2004.02.028.
[22] Wim H. Hesselink and Albert Thijs. Fixpoint semantics and simulation. Theor. Comput. Sci., 238(1-2):275–311, 2000. doi:10.1016/S0304-3975(98)00176-5.
[23] Dirk Hofmann, Gavin J. Seal, and Walter Tholen, editors. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology, volume 153 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, July 2014. Authors: Maria Manuel Clementino, Eva Colebunders, Dirk Hofmann, Robert Lowen, Rory Lucyshyn-Wright, Gavin J. Seal and Walter Tholen. doi:10.1017/cbo9781107517288.
[24] Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theor. Comput. Sci., 327(1-2):71–108, 2004. doi:10.1016/J.TCS.2004.07.022.
[25] Thomas Ihringer. Algemeine Algebra. Mit einem Anhang über Universelle Coalgebra von H. P. Gumm, volume 10 of Berliner Studienreihe zur Mathematik. Heldermann Verlag, 2003.
[26] Bartek Klin. Structural operational semantics for weighted transition systems. In Jens Palsberg, editor, Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday, volume 5700 of LNCS, pages 121–139. Springer, 2009. doi:10.1007/978-3-642-04164-8_7.
[27] Clemens Kupke, Alexander Kurz, and Yde Venema. Completeness for the coalgebraic cover modality. Log. Methods Comput. Sci., 8(3), 2012. doi:10.2168/LMCS-8(3:2)2012.
[28] Alexander Kurz and Raul Andres Leal. Modalities in the stone age: A comparison of coalgebraic logics. Theor. Comput. Sci., 430:88–116, 2012. doi:10.1016/J.TCS.2012.03.027.
[29] Paul Blain Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, FOSSACS 2011, volume 6604 of LNCS, pages 27–41. Springer, 2011. doi:10.1007/978-3-642-19805-2_3.
[30] Johannes Marti and Yde Venema. Lax extensions of coalgebra functors. In Dirk Pattinson and Lutz Schröder, editors, Coalgebraic Methods in Computer Science, CMCS 2021, volume 7399 of LNCS, pages 150–169. Springer, 2012. doi:10.1007/978-3-642-32784-1_9.
[31] Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. Journal of Computer and System Sciences, 81(5):880–900, 2015. doi:10.1016/j.jcss.2014.12.006.
[32] Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989.
[33] Rohit Parikh. Propositional game logic. In Foundations of Computer Science, FOCS 1983, pages 195–200. IEEE Computer Society, 1983. doi:10.1109/SFCS.1983.47.
[34] Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45(1):19–33, 2004. doi:10.1305/ndjfl/1094155277.
[35] David Peleg. Concurrent dynamic logic (extended abstract). In Robert Sedgewick, editor, Symposium on Theory of Computing, STOC 1985, pages 232–239. ACM, 1985. doi:10.1145/22145.22172.
[36] Jacques Riguet. Relations binaires, fermetures, correspondances de Galois. Bulletin de la Société Mathématique de France, 76:114–155, 1948. doi:10.24033/bsmf.1401.
[37] Jan J. M. M. Rutten. Relators and metric bisimulations. In Bart Jacobs, Larry Moss, Horst Reichel, and Jan J. M. M. Rutten, editors, Coalgebraic Methods in Computer Science, CMCS 1998, volume 11 of ENTCS, pages 252–258. Elsevier, 1998. doi:10.1016/S1571-0661(04)00063-5.
[38] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.
[39] Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2-3):230–247, January 2008. doi:10.1016/j.tcs.2007.09.023.
[40] Christoph Schubert and Gavin J. Seal. Extensions in the theory of lax algebras. Theory and Applications of Categories, 21(7):118–151, 2008.
[41] Gavin J. Seal. Canonical and op-canonical lax algebras. Theory and Applications of Categories, 14(10):221–243, 2005. URL: http://www.tac.mta.ca/tac/volumes/14/10/14-10abs.html.
[42] Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson. Uniform interpolation in coalgebraic modal logic. In Filippo Bonchi and Barbara König, editors, Algebra and Coalgebra in Computer Science, CALCO 2017, volume 72 of LIPIcs, pages 21:1–21:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPICS.CALCO.2017.21.
[43] Albert Thijs. Simulation and fixpoint semantics. PhD thesis, University of Groningen, 1996.
[44] Věra Trnková. General theory of relational automata. Fund. Inform., 3(2):189–233, 1980. doi:10.3233/FI-1980-3208.
[45] Paul Wild and Lutz Schröder. Characteristic logics for behavioural metrics via fuzzy lax extensions. In Igor Konnov and Laura Kovács, editors, Concurrency Theory, CONCUR 2020, volume 171 of LIPIcs, pages 27:1–27:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPICS.CONCUR.2020.27.
[46] Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci., 18(2), 2022. doi:10.46298/LMCS-18(2:19)2022.
[47] James Worrell. Coinduction for recursive data types: partial orders, metric spaces and $\Omega$ -categories. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, volume 33 of ENTCS, pages 337–356. Elsevier, 2000. doi:10.1016/S1571-0661(05)80356-1.

[bib.bib1] [1] Peter Aczel and Nax Paul Mendler. A final coalgebra theorem. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings, volume 389 of Lecture Notes in Computer Science, pages 357–365. Springer, 1989. doi:10.1007/BFB0018361.

[bib.bib2] [2] Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and concrete categories: The joy of cats. John Wiley & Sons Inc., 1990. Republished in: Reprints in Theory and Applications of Categories, No. 17 (2006) pp. 1–507. URL: http://tac.mta.ca/tac/reprints/articles/17/tr17abs.html.

[bib.bib3] [3] Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. Polynomial relators (extended abstract). In Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo, editors, Algebraic Methodology and Software Technology, AMAST 1991, Workshops in Computing, pages 303–326. Springer, 1991.

[bib.bib4] [4] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:20)2018.

[bib.bib5] [5] Michael Barr. Relational algebras. In Reports of the Midwest Category Seminar IV, number 137 in Lect. Notes Math., pages 39–55. Springer, 1970. doi:10.1007/BFb0060439.

[bib.bib6] [6] Michael Barr. Relational algebras. In Reports of the Midwest Category Seminar IV, pages 39–55. Springer, 1970. doi:10.1007/bfb0060439.

[bib.bib7] [7] Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299–315, 1993. doi:10.1016/0304-3975(93)90076-6.

[bib.bib8] [8] Richard S. Bird and Oege de Moor. Algebra of programming. Prentice Hall International series in computer science. Prentice Hall, 1997.

[bib.bib9] [9] Filippo Bonchi, Marcello M. Bonsangue, Michele Boreale, Jan J. M. M. Rutten, and Alexandra Silva. A coalgebraic perspective on linear weighted automata. Inf. Comput., 211:77–105, 2012. doi:10.1016/J.IC.2011.12.002.

[bib.bib10] [10] Brian F. Chellas. Modal Logic – An Introduction. Cambridge University Press, 1980. doi:10.1017/CBO9780511621192.

[bib.bib11] [11] Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic mu-calculus. Log. Methods Comput. Sci., 7(3), 2011. doi:10.2168/LMCS-7(3:3)2011.

[bib.bib12] [12] Maria Manuel Clementino, Dirk Hofmann, and George Janelidze. The monads of classical algebra are seldom weakly cartesian. J. Homotopy and Related Structures, 9(1):175–197, 2014.

[bib.bib13] [13] Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Anuj Dawar and Erich Grädel, editors, Logic in Computer Science, LICS 2018, pages 452–461. ACM, 2018. doi:10.1145/3209108.3209149.

[bib.bib14] [14] Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. A point-free perspective on lax extensions and predicate liftings. Mathematical Structures in Computer Science, pages 1–30, 2023. doi:10.1017/S096012952300035X.

[bib.bib15] [15] Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science, CALCO 2013, volume 8089 of LNCS, pages 253–266. Springer, 2013. doi:10.1007/978-3-642-40206-7_19.

[bib.bib16] [16] H. Peter Gumm. Free-algebra functors from a coalgebraic perspective. In Daniela Petrisan and Jurriaan Rot, editors, Coalgebraic Methods in Computer Science, CMCS 2020, volume 12094 of LNCS, pages 55–67. Springer, 2020. doi:10.1007/978-3-030-57201-3_4.

[bib.bib17] [17] H. Peter Gumm and Tobias Schröder. Coalgebraic structure from weak limit preserving functors. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, Berlin, Germany, March 25-26, 2000, volume 33 of Electronic Notes in Theoretical Computer Science, pages 111–131. Elsevier, 2000. doi:10.1016/S1571-0661(05)80346-9.

[bib.bib18] [18] H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. In Andrea Corradini, Marina Lenisa, and Ugo Montanari, editors, Coalgebraic Methods in Computer Science, CMCS 2001, volume 44(1) of ENTCS, pages 185–204. Elsevier, 2001. doi:10.1016/S1571-0661(04)80908-3.

[bib.bib19] [19] H. Peter Gumm and Tobias Schröder. Types and coalgebraic structure. Algebra universalis, 53(2–3):229–252, August 2005. doi:10.1007/s00012-005-1888-2.

[bib.bib20] [20] H. Peter Gumm and Mehdi Zarrad. Coalgebraic simulations and congruences. In Marcello M. Bonsangue, editor, Coalgebraic Methods in Computer Science - 12th IFIP WG 1.3 International Workshop, CMCS 2014, Colocated with ETAPS 2014, Grenoble, France, April 5-6, 2014, Revised Selected Papers, volume 8446 of Lecture Notes in Computer Science, pages 118–134. Springer, 2014. doi:10.1007/978-3-662-44124-4_7.

[bib.bib21] [21] Helle Hvid Hansen and Clemens Kupke. A coalgebraic perspective on monotone modal logic. In Jirí Adámek and Stefan Milius, editors, Coalgebraic Methods in Computer Science, CMCS 2004, volume 106 of ENTCS, pages 121–143. Elsevier, 2004. doi:10.1016/j.entcs.2004.02.028.

[bib.bib22] [22] Wim H. Hesselink and Albert Thijs. Fixpoint semantics and simulation. Theor. Comput. Sci., 238(1-2):275–311, 2000. doi:10.1016/S0304-3975(98)00176-5.

[bib.bib23] [23] Dirk Hofmann, Gavin J. Seal, and Walter Tholen, editors. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology, volume 153 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, July 2014. Authors: Maria Manuel Clementino, Eva Colebunders, Dirk Hofmann, Robert Lowen, Rory Lucyshyn-Wright, Gavin J. Seal and Walter Tholen. doi:10.1017/cbo9781107517288.

[bib.bib24] [24] Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theor. Comput. Sci., 327(1-2):71–108, 2004. doi:10.1016/J.TCS.2004.07.022.

[bib.bib25] [25] Thomas Ihringer. Algemeine Algebra. Mit einem Anhang über Universelle Coalgebra von H. P. Gumm, volume 10 of Berliner Studienreihe zur Mathematik. Heldermann Verlag, 2003.

[bib.bib26] [26] Bartek Klin. Structural operational semantics for weighted transition systems. In Jens Palsberg, editor, Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday, volume 5700 of LNCS, pages 121–139. Springer, 2009. doi:10.1007/978-3-642-04164-8_7.

[bib.bib27] [27] Clemens Kupke, Alexander Kurz, and Yde Venema. Completeness for the coalgebraic cover modality. Log. Methods Comput. Sci., 8(3), 2012. doi:10.2168/LMCS-8(3:2)2012.

[bib.bib28] [28] Alexander Kurz and Raul Andres Leal. Modalities in the stone age: A comparison of coalgebraic logics. Theor. Comput. Sci., 430:88–116, 2012. doi:10.1016/J.TCS.2012.03.027.

[bib.bib29] [29] Paul Blain Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, FOSSACS 2011, volume 6604 of LNCS, pages 27–41. Springer, 2011. doi:10.1007/978-3-642-19805-2_3.

[bib.bib30] [30] Johannes Marti and Yde Venema. Lax extensions of coalgebra functors. In Dirk Pattinson and Lutz Schröder, editors, Coalgebraic Methods in Computer Science, CMCS 2021, volume 7399 of LNCS, pages 150–169. Springer, 2012. doi:10.1007/978-3-642-32784-1_9.

[bib.bib31] [31] Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. Journal of Computer and System Sciences, 81(5):880–900, 2015. doi:10.1016/j.jcss.2014.12.006.

[bib.bib32] [32] Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989.

[bib.bib33] [33] Rohit Parikh. Propositional game logic. In Foundations of Computer Science, FOCS 1983, pages 195–200. IEEE Computer Society, 1983. doi:10.1109/SFCS.1983.47.

[bib.bib34] [34] Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45(1):19–33, 2004. doi:10.1305/ndjfl/1094155277.

[bib.bib35] [35] David Peleg. Concurrent dynamic logic (extended abstract). In Robert Sedgewick, editor, Symposium on Theory of Computing, STOC 1985, pages 232–239. ACM, 1985. doi:10.1145/22145.22172.

[bib.bib36] [36] Jacques Riguet. Relations binaires, fermetures, correspondances de Galois. Bulletin de la Société Mathématique de France, 76:114–155, 1948. doi:10.24033/bsmf.1401.

[bib.bib37] [37] Jan J. M. M. Rutten. Relators and metric bisimulations. In Bart Jacobs, Larry Moss, Horst Reichel, and Jan J. M. M. Rutten, editors, Coalgebraic Methods in Computer Science, CMCS 1998, volume 11 of ENTCS, pages 252–258. Elsevier, 1998. doi:10.1016/S1571-0661(04)00063-5.

[bib.bib38] [38] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.

[bib.bib39] [39] Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2-3):230–247, January 2008. doi:10.1016/j.tcs.2007.09.023.

[bib.bib40] [40] Christoph Schubert and Gavin J. Seal. Extensions in the theory of lax algebras. Theory and Applications of Categories, 21(7):118–151, 2008.

[bib.bib41] [41] Gavin J. Seal. Canonical and op-canonical lax algebras. Theory and Applications of Categories, 14(10):221–243, 2005. URL: http://www.tac.mta.ca/tac/volumes/14/10/14-10abs.html.

[bib.bib42] [42] Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson. Uniform interpolation in coalgebraic modal logic. In Filippo Bonchi and Barbara König, editors, Algebra and Coalgebra in Computer Science, CALCO 2017, volume 72 of LIPIcs, pages 21:1–21:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPICS.CALCO.2017.21.

[bib.bib43] [43] Albert Thijs. Simulation and fixpoint semantics. PhD thesis, University of Groningen, 1996.

[bib.bib44] [44] Věra Trnková. General theory of relational automata. Fund. Inform., 3(2):189–233, 1980. doi:10.3233/FI-1980-3208.

[bib.bib45] [45] Paul Wild and Lutz Schröder. Characteristic logics for behavioural metrics via fuzzy lax extensions. In Igor Konnov and Laura Kovács, editors, Concurrency Theory, CONCUR 2020, volume 171 of LIPIcs, pages 27:1–27:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPICS.CONCUR.2020.27.

[bib.bib46] [46] Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci., 18(2), 2022. doi:10.46298/LMCS-18(2:19)2022.

[bib.bib47] [47] James Worrell. Coinduction for recursive data types: partial orders, metric spaces and $\Omega$ -categories. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, volume 33 of ENTCS, pages 337–356. Elsevier, 2000. doi:10.1016/S1571-0661(05)80356-1.