# Transitivity and Difunctionality of Bisimulations

Mehdi Zarrad, H. Peter Gumm

► To cite this version:

Mehdi Zarrad, H. Peter Gumm. Transitivity and Difunctionality of Bisimulations. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. pp.33-52, 10.1007/978-3-319-40370-0_4 . hal-01446032

HAL Id: hal-01446032

https://inria.hal.science/hal-01446032

Submitted on 25 Jan 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Transitivity and Difunctionality of Bisimulations

Mehdi Zarrad and H. Peter Gumm

Philipps-Universität Marburg, Germany

**Abstract** Bisimilarity and observational equivalence are notions that agree in many classical models of coalgebras, such as e.g. Kripke structures. In the general category $Set_F$ of $F$-coalgebras these notions may, however, diverge. In many cases, observational equivalence, being transitive, turns out to be more useful.

In this paper, we shall investigate the role of transitivity for the largest bisimulation of a coalgebra. Passing to relations between two coalgebras, we choose difunctionality as generalization of transitivity. Since in $Set_F$ bisimulations are known to coincide with $\bar{F}$-simulations, we are led to study the notion of $L$-similarity, where $L$ is a relation lifting.

## 1 Introduction

In the 1990s, J. Rutten developed a universal theory for state-based systems. Such systems were represented as coalgebras in [19]. A coalgebra of type $F$ is a pair consisting of a base set $A$ and a structure map $\alpha : A \to F(A)$ where $F$ is any Set-endofunctor. Many of the early structural results, we just exemplarily mention [16], assumed that the type functor $F$ should preserve weak pullbacks. In [5], one of the present authors began studying the role of weak pullback preservation. In [4] and [14] he extended many results from [19] to the case of arbitrary functors, adding new coalgebraic constructions, e.g. for building terminal coalgebras. A systematic study relating preservation properties of functors to structural (coalgebraic) properties of their coalgebras was given in [8]. In particular, preservation properties were related to properties of bisimulations and congruences. For instance, it was shown that bisimulations restrict to subcoalgebras, if and only if the functor $F$ preserves preimages, i.e. pullbacks along regular monos.

Bisimulations, as compatible relations have been introduced by P. Aczel and N. Mendler in [1]. An alternative definition, equivalent for Set-coalgebras was given by C. Hermida and B. Jacobs [13].

A concept, competing with bisimulations is the notion of a congruence relation $\theta$ as a kernel $\ker \varphi$ of a homomorphism $\varphi$. Just as there is always a largest bisimulation $\sim_A$, there is also a largest congruence $\nabla_A$ on every coalgebra $\mathcal{A}$. The disadvantage of $\sim_A$ versus $\nabla_A$ is, that even though $\sim_A$ is reflexive and symmetric, it need not be transitive, hence it is not able to reflect logical equivalence. Since the equivalence hull of any bisimulation is always a congruence relation
[1], we have the implications

$$ \sim_A \subseteq \sim_A^* \subseteq \nabla_A $$

where each of the inclusions may be strict.

Already in [1], bisimulations were defined as relations between two (possible different) coalgebras $\mathcal{A}$ and $\mathcal{B}$. The notion of congruence can as easily be extended to the notion of 2-congruence, defined as the kernel of a sink of two homomorphisms $\varphi: \mathcal{A} \to \mathcal{C}$, and $\psi: \mathcal{B} \to \mathcal{C}$ i.e. as $\ker(\varphi, \psi) := \{(a, b) | \varphi(a) = \psi(b)\}$. (2-congruences were studied by S. Staton [21] under the name of kernel-bisimulations. However they are not necessarily bisimulations in the original sense, so we prefer to call them 2-simulations). Again, for the case of two coalgebras $\mathcal{A}$ and $\mathcal{B}$ it is easy to see that there is again a largest bisimulation $\sim_{\mathcal{A},\mathcal{B}}$ as well as a largest 2-congruence $\nabla_{\mathcal{A},\mathcal{B}}$. The above inequalities do not immediately generalize, since transitivity makes no sense for relations between different sets. An alternative notion, however, is difunctionality as introduced by J. Riguet [18]. The inequality corresponding to the above is then

$$ \sim_{\mathcal{A},\mathcal{B}} \subseteq \sim_{\mathcal{A},\mathcal{B}}^d \subseteq \nabla_{\mathcal{A},\mathcal{B}} $$

where $R^d$ denotes the difunctional closure of a relation $R$.

The definition of bisimulation given by Hermida and Jacobs used the fact that a relation $R \subseteq A \times B$ can easily be lifted to a relation $\bar{F}R \subseteq F(A) \times F(B)$, often called the Barr extension of $R$. Generalizing this to an arbitrary relation lifting $L$ leads to the notion of $L$-simulation as studied by A. Thijs [22] and in a series of papers by I. Venema et al., see e.g. [15].

The congruences which can be obtained as transitive closure of bisimulations are exactly the regular congruences i.e. kernels of coequalizers [8]. In the same paper it was shown that a functor $F$ preserves weak kernel pairs if and only every congruence on a single coalgebra in $Set_F$ is a bisimulation. In the present paper, which subsumes some results obtained in the first author's Master thesis [24], we want to explain further the relationship between bisimulations and 2-congruences and, assuming a monotonic relation lifting $L$, we study the di-functional closure of $L$-similarity. A quite useful tool is provided by a result, giving conditions for a bisimulation to restrict to subcoalgebras without assuming anything about the functor $F$.

## 2 Basic notions

For a product $A \times B$ we denote the projections to the components by $\pi_A$ and $\pi_B$. Given a relation $R \subseteq A \times B$, the restrictions to $R$ of the projections are $\pi_A^R := \pi_A \circ \iota_R$ where $\iota_R: R \hookrightarrow A \times B$ is set inclusion. Given a second relation $S$ with $R \subseteq S \subseteq A \times B$ we note that $\pi_A^R = \pi_A^S \circ \iota_R^S$, where $\iota_R^S: R \hookrightarrow S$ is, again, the inclusion map.

The converse of a relation $R$ is $R^- := \{(b, a) | (a, b) \in R\}$. For a subset $U \subseteq A$, we let $R[U] := \{b \in B | \exists u \in U.(u, b) \in R\}$. A relation $R \subseteq A \times A$
is transitive if for all $x, y, z \in A$ we have $(x, y), (y, z) \in R \implies (x, z) \in R$. Equivalently, $R$ is transitive, if $R \circ R \subseteq R$ where $\circ$ is relational composition. The reflexive transitive closure of $R$ is called $R^*$.

Transitivity makes no sense for relations $R \subseteq A \times B$ between different sets, so difunctionality [18] can be considered as a possible generalization of transitivity:

**Definition 1.** A relation $R \subseteq A \times B$ is called difunctional, if for all $a_1, a_2 \in A$ and for all $b_1, b_2 \in B$ it satisfies:

$$ (a_1, b_1), (a_2, b_1), (a_2, b_2) \in R \implies (a_1, b_2) \in R. $$

This notion can be illustrated by the following figure, which explains why “difunctional” is sometimes called “z-closed”:

<figure><img src="image_2.png" /></figure>

It is elementary to see that the difunctional closure of a relation $R$ is

$$ R^d := R \circ (R^- \circ R)^* = (R \circ R^-)^* \circ R $$

where $R^-$ is the converse relation to $R$. The difunctional closure can also be obtained as the pullback of the pushout of $\pi_A^R$ with $\pi_B^R$ [18],[9].

## 2.1 Categorical notions

We assume only elementary categorical notions and we use the terminology of [2]. Regular monos are equalizers of a parallel pair of morphisms. Analogously, regular epis are coequalizers. Split epis (split monos) i.e. the right-(left-)-invertible morphisms are regular epi (regular mono). We denote the sum of a family $(A_i)_{i \in I}$ of objects and with the canonical injections by $e_{A_i} : A_i \to \Sigma_{i \in I} A_i$. Given a sink $(q_i : A_i \to Q)_{i \in I}$ we denote the induced morphisms from the sum $\sum A_i \to Q$ by $[(q_i)_{i \in I}]$. The following lemma will be needed later. It is obviously true in every category with sums:

**Lemma 1.** For all morphisms $f : A \to B$ the map $[f, id_B] : A + B \to B$ is split epi.

**Definition 2.** A weak limit of a diagram $D$ is a cone over $D$ such that for every other (competing) cone there is at least one morphism making the relevant triangles commutative.

If we replace “at least one” in the above definition with “exactly one”, this is the definition of limit.
**Set-endofunctors** In the following, $F$ will always be a **Set-endofunctor**. $F$ preserves epis, and $F$ preserves monos with nonempty domain. Next, let $D$ a diagram.

**Definition 3.** $F$ weakly preserves $D$-limits if $F$ maps every $D$-limit into a weak $D$-limit.

It is well known that $F$ weakly preserves $D$-limits if and only if it preserves weak $D$-limits, see [5].

An important property of Set-endofunctors is that they preserve finite nonempty intersections [23]. In order to preserve all finite intersections, it might be necessary to redefine $F$ on the empty set and on empty mappings to obtain a (marginally modified) new functor preserving all finite intersections. Therefore, we are safe to only consider functors which preserve all finite intersections.

## 2.2 F-coalgebras

**Definition 4.** Let $F : \mathbf{Set} \to \mathbf{Set}$ be a Set-endofunctor. An $F$-coalgebra $\mathcal{A} = (A, \alpha)$ consists of a set $A$ and a structure map $\alpha : A \to F(A)$. A map $\varphi : A \to B$ between two coalgebras $\mathcal{A} = (A, \alpha)$ and $\mathcal{B} = (B, \beta)$ is called a homomorphism, if $\beta \circ \varphi = F\varphi \circ \alpha$. A subcoalgebra of a coalgebra $\mathcal{A}$ is a subset $U \subseteq A$ with a structure map $\alpha_U$ such that the inclusion map $i_U^X : U \hookrightarrow X$ is a homomorphism.

The class of all $F$-coalgebras with coalgebra homomorphisms forms the category $Set_F$. In [3] it is proved that $Set_F$ is cocomplete i.e. every colimit exists. Epis are exactly the surjective homomorphisms [19]. Monomorphisms in $Set_F$ need not be injective. Regular monos are exactly the injective homomorphisms [6].

## Bisimulations

**Definition 5 (Aczel and Mendler [1]).** A bisimulation between two coalgebras $\mathcal{A}$ and $\mathcal{B}$ is a relation $R \subseteq A \times B$ for which there exists a coalgebra structure $\rho : R \to F(R)$ such that the projections $\pi_A^R : R \to A$ and $\pi_B^R : R \to B$ are homomorphisms. A bisimulation $R$ on a coalgebra $\mathcal{A}$ is a bisimulation between $\mathcal{A}$ and itself.

The union of bisimulations is a bisimulation and $\emptyset$ is always a bisimulation, so that the bisimulations between $\mathcal{A}$ and $\mathcal{B}$ form a complete lattice with largest element called $\sim_{\mathcal{A},\mathcal{B}}$. For the same reason, every relation $R$ between coalgebras $\mathcal{A}$ and $\mathcal{B}$ contains a largest bisimulation, which we denote by $[R]$. It is the union of all bisimulations contained in $R$.

## Congruences and 2-congruences

**Definition 6.** A congruence $\theta$ on a coalgebra $\mathcal{A}$ is the kernel of a homomorphism $\varphi : \mathcal{A} \to \mathcal{C}$, i.e $\theta = \ker \varphi = \{(a, a') \in A \times A \mid \varphi(a) = \varphi(a')\}$.
If $\theta$ is a congruence on $\mathcal{A}$, then there is a structure map on the factor set $A/\theta := \{[a]\theta | a \in A\}$, such that $\pi_{\theta}: \mathcal{A} \to A/\theta$ with $\pi_{\theta}(a) := [a]\theta := \{a' \in A | a\theta a'\}$ becomes a homomorphism. The set of all congruences on a coalgebra $\mathcal{A}$ forms a complete lattice [7] with largest element called $\nabla_{\mathcal{A}}$ and smallest element $\Delta_{\mathcal{A}} = \{(a, a) | a \in A\}$. The supremum of a family of congruences is obtained as the transitive closure of their union. We denote the lattice of all congruences by $\text{Con}(\mathcal{A})$.

Given a bisimulation $R$ on $\mathcal{A}$, its equivalential hull, that is the smallest equivalence relation containing $R$ is a congruence relation [1]. It follows immediately, that $\sim_{\mathcal{A}} \subseteq \nabla_{\mathcal{A}}$. Congruences arising as equivalential hulls of a bisimulation are called regular. This notion is suggested by the following result from [8]:

**Lemma 2.** A morphism $\varphi: \mathcal{A} \to \mathcal{B}$ is mono iff $[\text{ker}\varphi] = \Delta_{\mathcal{A}}$ and regular mono, iff it is injective.

An epi $\varphi: \mathcal{A} \to \mathcal{B}$ is regular epi (in $\text{Set}_F$) iff its kernel is a regular congruence iff $\text{ker}\varphi = [\text{ker}\varphi]^*$.

For technical reasons, we call a homomorphism $\varphi$ strictly regular, if its kernel is a bisimulation, i.e. if $\text{ker}\varphi = [\text{ker}\varphi]$. Notice that this notion is not an abstract categorical one, but a coalgebraic notion.

**Definition 7.** A 2-congruence between two coalgebras $\mathcal{A}$ and $\mathcal{B}$ is the kernel (pullback in the category $\text{Set}$) of two homomorphisms $\varphi: \mathcal{A} \to \mathcal{C}$ and $\psi: \mathcal{B} \to \mathcal{C}$, i.e.

$$ \theta = \text{ker}(\varphi, \psi) := \{(a, b) \in \mathcal{A} \times \mathcal{B} | \varphi(a) = \psi(b)\}. $$

Just as congruences are transitive, 2-congruences are difunctional. The largest 2-congruence between $\mathcal{A}$ and $\mathcal{B}$ is called observational equivalence and written $\nabla_{\mathcal{A},\mathcal{B}}$. For each bisimulation $R$ between $\mathcal{A}$ and $\mathcal{B}$, its difunctional hull $R^d$, being the kernel of the pushout of the components $\pi_{\mathcal{A}}^R$ and $\pi_{\mathcal{B}}^R$ is a 2-congruence, so $R^d \subseteq \nabla_{\mathcal{A},\mathcal{B}}$.

# 3 Observational equivalence and bisimilarity

When $\mathcal{A}$ and $\mathcal{B}$ are coalgebras, elements $a \in \mathcal{A}$ and $b \in \mathcal{B}$ are called bisimilar, if there exists a bisimulation $R$ between $\mathcal{A}$ and $\mathcal{B}$ containing $(a, b)$. This is the same as saying that for some coalgebra $\mathcal{R}$ and homomorphisms $\varphi_{\mathcal{A}}: \mathcal{R} \to \mathcal{A}$ and $\varphi_{\mathcal{B}}: \mathcal{R} \to \mathcal{B}$ there is some $r \in \mathcal{R}$ with $\varphi_{\mathcal{A}}(r) = a$ and $\varphi_{\mathcal{B}}(r) = b$. In short, $a$ and $b$ are bisimilar, if they have a common ancestor.

Dually, $a$ and $b$ are called observationally equivalent, iff they have a common offspring, meaning that there exists a coalgebra $\mathcal{C}$ and homomorphisms $\psi_{\mathcal{A}}: \mathcal{A} \to \mathcal{C}$ and $\psi_{\mathcal{B}}: \mathcal{B} \to \mathcal{C}$ with $\psi_{\mathcal{A}}(a) = \psi_{\mathcal{B}}(b)$. We first study the situation for the case $\mathcal{A} = \mathcal{B}$. Here $a, a'$ are bisimilar iff $(a, a') \in \sim_{\mathcal{A}}$ and observationally equivalent iff $(a, a') \in \nabla_{\mathcal{A}}$.
## 3.1 Nabla and simple coalgebras

**Definition 8.** A coalgebra $\mathcal{A}$ is called simple, if $\nabla_{\mathcal{A}} = \Delta_{\mathcal{A}}$ and extensional, if $\sim_{\mathcal{A}} = \Delta_{\mathcal{A}}$.

It is well known that a coalgebra $\mathcal{A}$ is simple iff each morphism starting in $\mathcal{A}$ is injective [4]. If a terminal coalgebra $\mathcal{T}$ exists, simple coalgebras are precisely the subcoalgebras of $\mathcal{T}$[4]. For every coalgebra $\mathcal{A}$, the factor coalgebra $\mathcal{A}/\nabla_{\mathcal{A}}$ is simple. The notions of simplicity and extensionality differ [7]. The coalgebra of the following example is extensional but not simple.

*Example 1.*

<figure><img src="image_3.png" /></figure>

Consider the above $2 \times \mathbb{P}_{\le 3}$-coalgebra $\mathcal{A} := (\{0,1,2,3\}, \alpha)$ with $\alpha(0) := (0, \{0,1,2\})$, $\alpha(2) := (1, \{0,1,2\})$, $\alpha(1) = (0, \{1,2,3\})$, $\alpha(3) = (1, \{1,2,3\})$. It is easy to check that $\nabla = \{(0,1), (1,0), (2,3), (3,2)\} \cup \Delta_{\mathcal{A}}$. Suppose that $(0,1) \in \sim$. Then there is $(0, M) \in 2 \times \mathbb{P}_{\le 3} \sim$ with $\pi_1[M] = (0,1,2)$ and $\pi_2[M] = (1,2,3)$. Hence $M = \{(0,1), (1,1), (2,2), (2,3)\}$. This is a contradiction, because $|M| = 4$. Similarly $(2,3) \not\in \sim$. We obtain $\sim = \Delta \neq \nabla$.

The following lemma helps us to verify whether a congruence $\theta$ is the largest congruence. It suffices to check that the codomain of a factor is simple.

**Lemma 3.** *Subcoalgebras of simple coalgebras are simple. More generally, if $\varphi: \mathcal{A} \to \mathcal{C}$ is a homomorphism and $\mathcal{C}$ is simple, then $\ker \varphi = \nabla_{\mathcal{A}}$.*

*Proof.* Let $\iota: \mathcal{U} \hookrightarrow \mathcal{C}$ be the inclusion morphism, and assume that $\theta$ is a congruence on $\mathcal{U}$. The pushout of $\iota$ with $\pi_\theta$ yields a homomorphism $\psi: \mathcal{C} \to \mathcal{P}$. Since $\mathcal{C}$ is simple, $\psi$ is injective. It follows that $\pi_\theta$ is injective. This means that $\nabla_{\mathcal{U}} = \Delta_{\mathcal{U}}$. Next, let $\varphi: \mathcal{A} \to \mathcal{C}$ be a homomorphism and $\mathcal{C}$ simple. The image of $\mathcal{A}$ under $\varphi$ is a subcoalgebra of $\mathcal{C}$, which, as we have just seen, must be simple. Thus we may as well assume that $\varphi$ is epi. Obviously, $\ker \varphi \subseteq \nabla_{\mathcal{A}}$, so there is a homomorphism $\psi: \mathcal{C} \to \mathcal{A}/\nabla_{\mathcal{A}}$ with $\pi_{\nabla_{\mathcal{A}}} = \psi \circ \varphi$. So $\psi$ is surjective, and injective, since $\mathcal{C}$ is simple. It follows that $\psi$ is an isomorphism, whence $\ker \varphi = \ker \pi_{\nabla_{\mathcal{A}}} = \nabla_{\mathcal{A}}$.

The following lemma relates observational equivalence between two coalgebras to observational equivalence on their sum:

**Lemma 4 ([14]).** $(a,b) \in \nabla_{\mathcal{A},\mathcal{B}} \iff (e_A(a), e_B(b)) \in \nabla_{\mathcal{A}+\mathcal{B}}$.
Proof.

$$
\begin{align*}
(a, b) \in \nabla_{A,B} &\iff \exists \mathcal{C}, \varphi : \mathcal{A} \to \mathcal{C}, \psi : \mathcal{B} \to \mathcal{C}. \varphi(a) = \psi(b) \\
&\iff \exists \mathcal{C}, \chi : \mathcal{A} + \mathcal{B} \to \mathcal{C}, \chi(e_{\mathcal{A}}(a)) = \chi(e_{\mathcal{B}}(b)) \\
&\iff (e_{\mathcal{A}}(a), e_{\mathcal{B}}(b)) \in \nabla_{\mathcal{A}+\mathcal{B}}.
\end{align*}
$$

We need to extend Lemma 3 to the case of a cospan of two homomorphisms:

**Lemma 5.** If $\varphi : \mathcal{A} \to \mathcal{C}$ and $\psi : \mathcal{B} \to \mathcal{C}$ are homomorphism and $\mathcal{C}$ is simple, then $\ker(\varphi, \psi) = \nabla_{\mathcal{A},\mathcal{B}}$.

*Proof.* Consider $[\varphi, \psi] : \mathcal{A} + \mathcal{B} \to \mathcal{C}$ with $\varphi = [\varphi, \psi] \circ e_{\mathcal{A}}$ and $\psi = [\varphi, \psi] \circ e_{\mathcal{B}}$. By lemma 3, we obtain $\ker[\varphi, \psi] = \nabla_{\mathcal{A}+\mathcal{B}}$, so with this and lemma 4 we calculate:

$$
\begin{align*}
\varphi(a) = \psi(b) &\iff [\varphi, \psi] \circ e_{\mathcal{A}}(a) = [\varphi, \psi] \circ e_{\mathcal{B}}(b) \\
&\iff (e_{\mathcal{A}}(a), e_{\mathcal{B}}(b)) \in \ker[\varphi, \psi] \\
&\iff (e_{\mathcal{A}}(a), e_{\mathcal{B}}(b)) \in \nabla_{\mathcal{A}+\mathcal{B}} \\
&\iff (a, b) \in \nabla_{\mathcal{A},\mathcal{B}}.
\end{align*}
$$

The following construction will be used in various places. It can be used to
change the structure map $\alpha$ of a coalgebra while at the same time preserving
other important properties as seen in the ensuing lemma:

**Definition 9.** Given a coalgebra $\mathcal{A} = (A, \alpha)$, element $x_0 \in \mathcal{A}$ and subset $U \subseteq \mathcal{A}$.
We define a new coalgebra $\mathcal{A}_{x_0}^U := (A, \bar{\alpha})$ on the same base set by constantly
mapping all elements of $U$ to $\alpha(x_0)$ and retaining $\alpha$ on all other elements, i.e.:

$$
\bar{\alpha}(x) := \begin{cases} \alpha(x_0) & \text{if } x \in U \\ \alpha(x) & \text{else.} \end{cases}
$$

**Lemma 6.** Let $\varphi : \mathcal{A} \to \mathcal{C}$ be a homomorphism and $U \subseteq [x_0]$ ker $\varphi$ for some $x_0 \in \mathcal{A}$. Then the map $\varphi : \mathcal{A} \to \mathcal{C}$ is also a homomorphism $\varphi : \bar{\mathcal{A}} \to \mathcal{C}$ where $\bar{\mathcal{A}} := \mathcal{A}_{x_0}^U$. Moreover, $\nabla_{\mathcal{A}} = \nabla_{\bar{\mathcal{A}}}.$

*Proof.* If $x \in U$, then $(F\varphi \circ \bar{\alpha})(x) = (F\varphi)(\alpha_{\mathcal{A}}(x_0)) = \alpha_{\mathcal{C}}(\varphi(x_0)) = \alpha_{\mathcal{C}}(\varphi(x))$. If $x \notin U$, nothing has changed, so $\varphi$ keeps being a homomorphism. With $\mathcal{C} = A/\nabla_{\mathcal{A}}$ and lemma 3, we obtain $\nabla_{\mathcal{A}} = \ker \varphi = \nabla_{\bar{\mathcal{A}}}.$

**3.2 Restricting bisimulations**

For the following we assume that $R \subseteq A_1 \times A_2$ is a bisimulation between coal-
gebras $A_1 = (A, \alpha_1)$ and $A_2 = (A, \alpha_2)$, and $U_i \le A_i$ are subcoalgebras for
$i = 1, 2$.

**Definition 10.** $R$ restricts to $U := U_1 \times U_2$, if $R \upharpoonright U := R \cap (U_1 \times U_2)$ is a bisimulation between $U_1$ and $U_2$.
Without any further assumption, bisimulations will not necessarily restrict to subcoalgebras. In fact in [6] it was shown that all bisimulations restrict to all subcoalgebras, globally throughout Set<sub>F</sub>, if and only if F preserves preimages. In spite of this, here we can identify conditions on R and on the U<sub>i</sub> that guarantee that R restricts to U<sub>1</sub> × U<sub>2</sub> without any condition on F. The main result of this section is the following theorem and its applications:

**Theorem 1.** If there exist κ<sub>i</sub> : A<sub>i</sub> → U<sub>i</sub> left inverses to the inclusion maps, satisfying for all a<sub>1</sub> ∈ A<sub>1</sub>, a<sub>2</sub> ∈ A<sub>2</sub>:

$$ (a_1, a_2) \in R \implies (\kappa_1 a_1, \kappa_2 a_2) \in R $$

then R restricts to U.

Instantiating the existential quantifier in this theorem with particularly natural left inverses to the inclusion maps, we shall obtain the following, easy-to-apply criterion (Here R[U] denotes {y | ∃x ∈ U.(x, y) ∈ R} and R<sup>-</sup> is the converse relation to R):

**Theorem 2.** If R[U<sub>1</sub>] ⊆ U<sub>2</sub> and R<sup>-</sup>[U<sub>2</sub>] ⊆ U<sub>1</sub> then R restricts to a bisimulation between U<sub>1</sub> and U<sub>2</sub>.

The following further specialization with U ≤ A and R a bisimulation on A will likely be the most useful one:

**Corollary 1.** A bisimulation R on A restricts to the subcoalgebra U ≤ A, provided that R[U] ⊆ U and R<sup>-</sup>[U] ⊆ U.

Given an epimorphism ϕ : A → B, the largest bisimulation contained in its kernel reveals, whether ϕ is a regular epi in the category Set<sub>F</sub> or not. We start with [ker ϕ], the largest bisimulation contained in the kernel of ϕ. The criterion found in [8] is, that the transitive hull of [ker ϕ] should be all of ker ϕ. Expressed as a formula this is: [ker ϕ]<sup>*</sup> = ker ϕ. Studying this further, we show the following result, which turns out to be another corollary:

**Corollary 2.** From ϕ<sub>i</sub> : A<sub>i</sub> → B<sub>i</sub> construct ϕ<sub>1</sub> + ϕ<sub>2</sub> : A → B with A := A<sub>1</sub> + A<sub>2</sub> and B := B<sub>1</sub> + B<sub>2</sub>. Consider ker ϕ<sub>i</sub> as subsets of A, then [ker(ϕ<sub>1</sub> + ϕ<sub>2</sub>)] = [ker ϕ<sub>1</sub>] ∪ [ker ϕ<sub>2</sub>].

To see why this follows from corollary 1, choose U<sub>i</sub> := A<sub>i</sub> ≤ A: If R ⊆ ker(ϕ<sub>1</sub> + ϕ<sub>2</sub>) is a bisimulation, then R[A<sub>i</sub>] ⊆ ker(ϕ<sub>1</sub> + ϕ<sub>2</sub>)[A<sub>i</sub>] = A<sub>i</sub> and symmetrically R<sup>-</sup>[A<sub>i</sub>] ⊆ A<sub>i</sub>. Thus R restricts to A<sub>i</sub> ⊆ A<sub>1</sub> + A<sub>2</sub>. This proves that [ker(ϕ<sub>1</sub> + ϕ<sub>2</sub>)] ⊆ [ker ϕ<sub>1</sub>] ∪ [ker ϕ<sub>2</sub>]. The other direction is trivial, since kerϕ<sub>i</sub> ⊆ ker(ϕ<sub>1</sub> + ϕ<sub>2</sub>), hence [kerϕ<sub>i</sub>] ⊆ [ker(ϕ<sub>1</sub> + ϕ<sub>2</sub>)].

We now turn to the proof of theorem 1:

*Proof (of theorem 1 and 2).* Consider the following diagram, where we use ι, possibly with indices, to denote inclusion maps and similarly π<sub>i</sub> or ¯π<sub>i</sub> to denote projection maps to the i-th component, for i = 1, 2. The κ<sub>i</sub> are the mentioned
left inverses to the $\iota_i$ and $\kappa := \kappa_1 \times \kappa_2$. The condition of the theorem guarantees that $\kappa'$s codomain is indeed $R \upharpoonright U$, and by definition, we have:

$$ \bar{\pi}_i \circ \kappa = \kappa_i \circ \pi_i. $$

Simply define

$$ \bar{\rho} := F(\kappa) \circ \rho \circ \iota $$

and chase the following diagram:

<figure><img src="image_4.png" /></figure>

$$ \begin{align*} F\bar{\pi}_i \circ \bar{\rho} &= F\bar{\pi}_i \circ F\kappa \circ \rho \circ \iota \\ &= F\kappa_i \circ F\pi_i \circ \rho \circ \iota \\ &= F\kappa_i \circ \alpha_{A_i} \circ \pi_i \circ \iota \\ &= F\kappa_i \circ \alpha_{A_i} \circ \iota_i \circ \bar{\pi}_i \\ &= F\kappa_i \circ F\iota_i \circ \alpha_{U_i} \circ \bar{\pi}_i \\ &= Fid_{A_i} \circ \alpha_{U_i} \circ \bar{\pi}_i \\ &= \alpha_{U_i} \circ \bar{\pi}_i \end{align*} $$

For the proof of theorem 2, we note that the case where $R \upharpoonright U$ is empty becomes trivial. Otherwise fix any pair $(u_1, u_2) \in R \upharpoonright U$ and define the following inverses $\kappa_i$ to the inclusions $\iota_i : U_i \to A_i$:

$$ \kappa_i(a) := \text{if } (a \in U_i) \text{ then a else } u_i. $$

Given $(a_1, a_2) \in R$, the conditions $R[U_1] \subseteq U_2$ and $R^{-}[U_2] \subseteq U_1$ guarantee that $a_1 \in U_1 \iff a_2 \in U_2$. By definition of $\kappa_i$ then, either $(\kappa_1 a_1, \kappa_2 a_2) = (a_1, a_2)$ or $(\kappa_1 a_1, \kappa_2 a_2) = (u_1, u_2)$.

# 4 Relationships between bisimilarity and observational equivalence

Bisimilarity and observational equivalence need not be distinguished in many classical systems, such as e.g. in Kripke structures. In particular, the famous
Hennessy-Milner theorem [12] relates bisimilarity with logical equivalence. However, the generalization of this result to coalgebras, as given by D. Pattinson [17], demonstrates that logical equivalence should rather be related to observational equivalence. In hindsight, this appears obvious, as bisimilarity need not be transitive, whereas observational equivalence always is transitive, and clearly so is logical equivalence. Thus in the case of the Hennessy-Milner theorem, “luckily” both notions agreed. The reason for this is, that the type functor for Kripke-structures, is rather well behaved, in that it weakly preserves kernel pairs, even arbitrary pullbacks.

## 4.1 Weak preservation of kernel pairs

A kernel pair is the pullback of two equal morphisms. A preimage is a pullback with a regular epimorphism. The role of weak preservation of pullbacks in general, of kernel pairs and of preimages has been studied by H.P. Gumm and T. Schröder [8]. In particular, we recall that:

**Theorem 3 ([8]).** The following are equivalent :

(1) *F weakly preserves kernel pairs (of epis).*

(2) *Every congruence is a bisimulation.*

Thus weak preservation of kernel pairs is equivalent to all epis $\varphi$ being strictly regular, meaning that $[ker \varphi] = ker\varphi$. We shall show below that this is equivalent to all epis just being regular, i.e. $[ker \varphi]^* = ker \varphi$.

A joint result of the second author and C. Henkel, to be found in the latter's Master thesis [11], also turns out to be useful:

**Theorem 4 ([11]).** The following are equivalent:

1. *F weakly preserves kernel pairs*

2. *F weakly preserves pullbacks of epimorphisms.*

In [8], furthermore, the implications (1) $\implies$ (2) $\implies$ (3) have been shown for the following properties:

1. *F weakly preserves kernel pairs*

2. every epi is regular epi

3. every mono is regular mono.

In [20] it was further claimed that (3) $\Rightarrow$ (1), rendering all three properties equivalent. Unfortunately, the proof contained a gap, so until today, (3) $\Rightarrow$ (1) remains open. Nevertheless, we are able to close the loop at (2) $\Rightarrow$ (1) in the following theorem 5, so (1) and (2) indeed turn out to be equivalent. The following innocuous lemma holds a key for the proof.

**Lemma 7.** Let $\varphi$ be the coequalizer of $\psi_1, \psi_2: Q \to A$ and let $x \in A$. If there exists $y \neq x$ with $\varphi(x) = \varphi(y)$ then for some $q$ in $Q$ either $\psi_1(q) = x \neq \psi_2(q)$ or $\psi_2(q) = x \neq \psi_1(q)$.
*Proof.* In the category *Set*, the coequalizer $\varphi$ of $\psi_1$ and $\psi_2$ is obtained by factor-
ing $A$ by the equivalence relation generated by the relation $R = \{(\psi_1(q), \psi_2(q)) \mid q \in
Q\}$. Thus $\ker \varphi = \text{Eq}(R) = (\Delta_A \cup R \cup R^-)^*$. If $x$ $\ker y$ for some $y \neq x$, there
must be therefore be at least some $y' \neq x$ with $xRy'$ or $xR^-y'$.

The following theorem was obtained in the master thesis of the first author:

**Theorem 5 ([24]).** *F weakly preserves kernel pairs iff every epi is regular epi.*

*Proof.* “⇒” is from [8].

"$\Leftarrow$": By theorem 3 it suffices to show, that $F$ preserves weak kernel pairs of epis.
Let $\varphi : A \to C$ be a surjective map, $\tilde{a}, \tilde{b} \in F(A)$ and $\tilde{c} \in F(C)$ with $(F\varphi)\tilde{a} =
\tilde{c} = (F\varphi)\tilde{b}$. We need to find $\tilde{p} \in F(\ker\varphi)$ with $(F\pi_1)\tilde{p} = \tilde{a}$ and $(F\pi_2)\tilde{p} = \tilde{b}$. In
case $\varphi$ is injective, then the pullback of $\varphi$ is an intersection. We have assumed
in this paper that functors preserve intersections. Otherwise there are $x, y \in A$
with $x \neq y$ and $\varphi(x) = \varphi(y)$. We define structure maps $\alpha_A : A \to FA$ and
$\alpha_C : C \to FC$ as follows:

$$
\begin{array}{r@{\,}c@{\,}l@{\quad}l}
\alpha_A(z) & := & \left\{ \begin{array}{ll} \tilde{a} & \text{if } z = x \\ \tilde{b} & \text{otherwise} \end{array} \right. & \text{and} \\
\alpha_C(z) & := & \tilde{c}. &
\end{array}
$$

Clearly $\varphi$ is a surjective homomorphisms, since $(\alpha_C \circ \varphi)(z) = \alpha_C(\varphi(z)) = \tilde{c} = (F\varphi)(\alpha_A(z)) = ((F\varphi) \circ \alpha_A)(z)$ for every $z \in A$. By assumption $\varphi$ is regular epi, so it is the coequalizer of two homomorphisms $\psi_1$ and $\psi_2: Q \to A$. By Lemma 7 there is some $q \in Q$ with $(\psi_1(q) = x$ and $\psi_2(q) \neq x)$ or $(\psi_1(q) \neq x$ and $\psi_2(q) = x)$. Since $\varphi$ is the coequalizer of $\psi_1$ and $\psi_2$, $(Q, \psi_1, \psi_2)$ becomes a competitor for the pullback $(\ker \varphi, \pi_1, \pi_2)$ in *Set*. Thus there is a map $m$ with $\pi_1 \circ m = \psi_1$ and $\pi_2 \circ m = \psi_2$.

<figure><img src="image_5.png" /></figure>

Since $\psi_1(q) = x$ and $\psi_2(q) \neq x$ it follows that $\alpha_A(\psi_1(q)) = \tilde{a}$ and $\alpha_A(\psi_2(q)) = \tilde{b}$.
Then $F\psi_1 \circ \alpha_Q(q) = \tilde{a}$ and $F\psi_2 \circ \alpha_Q(q) = \tilde{b}$ because $\psi_1$ and $\psi_2$ are homo-
morphisms. From property of functor this implies: $F\pi_1 \circ Fm \circ \alpha_Q(q) = \tilde{a}$ and
$F\pi_2 \circ Fm \circ \alpha_Q(q) = \tilde{b}$. Then $F\pi_1(Fm \circ \alpha_Q(q)) = \tilde{a}$ and $F\pi_2(Fm \circ \alpha_Q(q)) = \tilde{b}$.
This shows the existence of some $\tilde{p} \in F\ker \varphi$ with $(F\pi_1)\tilde{p} = \tilde{a}$ and $(F\pi_2)\tilde{p} = \tilde{b}$.
**Lemma 8.** If an epimorphism $\varphi : \mathcal{U} \to \mathcal{B}$ can be factored as $\varphi = \psi \circ e$ with $e : \mathcal{U} \hookrightarrow \mathcal{A}$ a regular mono and $\psi : \mathcal{A} \to \mathcal{B}$ a strictly regular epi, then $\varphi$ is strictly regular epi.

*Proof.* If $U = \emptyset$ then $\ker \varphi = \emptyset$ is a bisimulation, so we may assume that $U \neq \emptyset$. Since $\varphi$ is epi, then $\varphi$ is surjective and the axiom of choice yields a right inverse map $r$ for $\varphi$. With its help we obtain a map $l : A \to U$ as

$$l(x) := \begin{cases} u & \text{if } e(u) = x \\ r(\psi(x)) & \text{otherwise.} \end{cases}$$

It is easy to check that $\varphi \circ l = \psi$.

<figure><img src="image_6.png" /></figure>

(ker $\varphi, e \circ \pi_1, e \circ \pi_2$) is a competitor to the pullback $\ker \psi$. This yields a map $m : \ker \varphi \to \ker \psi$ with $\bar{\pi}_i \circ m = e \circ \pi_i$ for $i = 1, 2$. Similarly, $(\ker \psi, l \circ \bar{\pi}_1, l \circ \bar{\pi}_2)$ is a competitor to the pullback $\ker \varphi$, providing another map $\bar{m} : \ker \psi \to \ker \varphi$ with $l \circ \bar{\pi}_i = \pi_i \circ \bar{m}$. Now let us assume that $\ker \psi$ is a bisimulation, then there exists a structure map $\rho : \ker \psi \to F \ker \psi$ such that $\alpha_A \circ \bar{\pi}_i = F \bar{\pi}_i \circ \rho$ for $i = 1, 2$.

<figure><img src="image_7.png" /></figure>

We claim that $\rho' := F\bar{m} \circ \rho \circ m$ is a structure map witnessing that $\ker \varphi$ is a bisimulation.

$$\begin{align*} F\pi_i \circ \rho' &= F\pi_i \circ F\bar{m} \circ \rho \circ m \\ &= Fl \circ F\bar{\pi}_i \circ \rho \circ m \\ &= Fl \circ \alpha_A \circ \bar{\pi}_i \circ m \\ &= Fl \circ \alpha_A \circ e \circ \pi_i \\ &= Fl \circ Fe \circ \alpha_U \circ \pi_i \\ &= \alpha_U \circ \pi_i \end{align*}$$
**Lemma 9.** Let $\varphi : A \to B$ be an epimorphism. $\varphi$ is strictly regular epi iff $[\varphi, id_B]$ is strictly regular epi.

<figure><img src="image_8.png" /></figure>

*Proof.* "⇒" : $\ker[\varphi, id_B] = \ker\varphi \cup \text{graph}\varphi \cup (\text{graph}\varphi)^- \cup \Delta_{A+B}$. Since $\ker\varphi$ is bisimulation, $\ker[\varphi, id_B]$ is bisimulation, too.

" ⇐ " $[\varphi, id_B]$ is regular epi by lemma 1 and $e_A$ is regular mono since it is injective. The rest follows from lemma 8.

**Proposition 1.** Let $\varphi : A \to B$ and $\psi : C \to D$ be two homomorphisms. $\varphi$ and $\psi$ are regular epi iff $\varphi + \psi$ is regular epi.

*Proof.* "⇒" This holds in every cocomplete category [2].

" ⇐ "By corollary 2 $[\ker(\varphi + \psi)]_{A+C} = [\ker\varphi]_A \cup [\ker\psi]_C$. By lemma 2 $\ker\varphi \cup \ker\psi = \ker(\varphi+\psi) = [\ker(\varphi+\psi)]_{A+C}^* = [\ker\varphi]_A^* \cup [\ker\psi]_C^*$. Then $\ker\varphi = [\ker\varphi]_A^*$ and $\ker\psi = [\ker\psi]_A^*$. From lemma 2 it then follows that $\varphi$ and $\psi$ are regular epi.

<figure><img src="image_9.png" /></figure>

We define an order over all homomorphisms with the same domain by $\varphi \le \psi :\Leftrightarrow \ker\varphi \subseteq \ker\psi$

**Lemma 10.** For any epimorphism $\varphi : A \to B$, the infimum of $id_B + [\varphi, id_B]$ and $[id_B, \varphi] + id_B$ is $id_B + \varphi + id_B$.

*Proof.* Mark the two isomorphic copies of $B$ as $B_1$ and $B_2$ and abbreviate $\psi_1 := id_{B_1} + [\varphi, id_{B_2}]$, $\psi_2 := [id_{B_1}, \varphi] + id_{B_2}$ and $\psi := id_{B_1} + \varphi + id_{B_2}$. We need to check that $\ker\psi = \ker\psi_1 \cap \ker\psi_2$. Given $x \neq y$, then

$$ (x, y) \in \ker \psi_1 \cap \ker \psi_2 \iff \begin{aligned}[t] & \exists(a, a') \in \ker \varphi. x = e_A(a) \land y = e_A(a') \\ & \qquad \iff (x, y) \in \ker \psi. \end{aligned} $$
**Theorem 6.** The following are equivalent:

1. *F preserves weak kernel pairs,*

2. $R^d$ is a bisimulation, whenever $R$ is,

3. $[\theta]$ is difunctional for each 2-congruence $\theta$,

4. $[\theta]$ is transitive for each congruence $\theta$,

5. $[\theta]^* = \theta$ for every congruence $\theta$,

6. the regular congruences form a sublattice of Cong($\mathcal{A}$).

*Proof.* (1)⇒(2) Let $R$ be a bisimulation between two coalgebras $\mathcal{A}_1$ and $\mathcal{A}_2$. We factor the projections $\pi_i^R : R \to \mathcal{A}_i$ into $\iota_i \circ \bar{\pi}_i^R$ as an epi followed by a regular mono and produce the pushout $(p_1, p_2)$ of $(\bar{\pi}_1^R, \bar{\pi}_2^R)$. Then $p_1$ and $p_2$ are epi and. $R^d = \ker(p_1, p_2)$. It follows from theorem 4 that $R^d$ is a bisimulation.

(2) ⇒ (3) is evident

(3) ⇒ (4) If $\theta$ is a congruence, $[\theta]$ also must be reflexive and symmetric. Considered as a 2-congruence between $\mathcal{A}$ and itself, the hypothesis yields that $[\theta]$ is difunctional, too. Difunctionality with reflexivity and symmetry implies transitivity.

(4) ⇒ (5) $\theta = \ker\varphi$ for some epimorphism $\varphi : \mathcal{A} \to \mathcal{B}$. By lemma 1, $\ker[\varphi, id_{\mathcal{B}}]$ is a regular congruence, so $\ker[\varphi, id_{\mathcal{B}}] = [\ker[\varphi, id_{\mathcal{B}}]]^*$. By hypothesis, $[\ker[\varphi, id_{\mathcal{B}}]]$ is transitive, so in fact $\ker[\varphi, id_{\mathcal{B}}] = [\ker[\varphi, id_{\mathcal{B}}]]$, witnessing that $\ker[\varphi, id_{\mathcal{B}}]$ is a bisimulation. From lemma 9, we can conclude now, that $\ker \varphi = \theta$ is a bisimulation, too. Consequently, $\theta = [\theta]$ and a fortiori $\theta = \theta^* = [\theta]^*$.

(5) ⇒ (6) is evident, because all congruences are regular.

(6) ⇒ (1) Let $\varphi : A \to B$ be an epimorphism. Let $\psi_1 : B + A + B \to B + B$, $\psi_2 : B + A + B \to B + B$ and $\psi : B + A + B \to B + B + B$ be defined as $\psi_1 := id_B + [\varphi, id_B]$, $\psi_2 := [id_B, \varphi] + id_B$ and $\psi := id_B + \varphi + id_B$. From lemma 1 and proposition 1 we obtain that $\psi_1$ and $\psi_2$ are regular epis. From the hypothesis it follows that the infimum of $\psi_1$ and $\psi_2$ is regular epi. By lemma 10 then $\psi$ is regular epi. By lemma 1 then $\varphi$ is again regular epi.

## 4.2 Transitivity of ~

The next theorem clarifies which properties assure the transitivity of bisimilarity. The equivalence (1) ⇔ (3) appears in [8] under the additional assumption that $F$ should preserve preimages. Its proof will need a simple lemma allowing us to extend bisimulations in certain situations.

**Theorem 7.** The following are equivalent:

(1) $\sim_A = \nabla_A$ for each $F$-coalgebra $\mathcal{A}$.

(2) $\sim_A^* = \nabla_A$ for each $F$-coalgebra $\mathcal{A}$.

(3) $\sim_A$ is transitive for each $F$-coalgebra $\mathcal{A}$:

*Proof.* (1) ⇒ (2) and (1) ⇒ (3) are evident, since $\nabla_A$ is transitive.

(2) ⇒ (1): Given $\mathcal{A} = (A, \alpha)$, we have to show that $\nabla_A$ is a bisimulation. Hence for arbitrary $(x_0, y_0) \in \nabla_A$ we need to find some $p \in F\nabla_A$ with $F\pi_1(p) = \alpha(x_0)$ and $F\pi_2(p) = \alpha(y_0)$ where $\pi_1, \pi_2 : \nabla_A \to A$ are the projection maps.
If $x_0 = y_0$ then $(x_0, y_0) \in \Delta_A$ which is already a bisimulation contained in $\nabla_A$. But for each bisimulation $S$ contained in $\nabla_A$ with $(x_0, y_0) \in S$ there is already some $q \in F(S)$ with $F\pi_A^S(q) = \alpha(x_0)$ and $F\pi_A^S(q) = \alpha(x_0)$. The inclusion map $i_S^\nabla: S \hookrightarrow \nabla_A$ yields an element $p := F i_S^\nabla(q) \in F(\nabla_A)$ for which $F\pi_1(p) = F\pi_1(Fi_S^\nabla(q)) = F(\pi_1 \circ i_S^\nabla)(q) = F(\pi_1^S)(q) = \alpha(x_0)$, and likewise $F\pi_2(p) = \alpha(y_0)$.

If $x_0 \neq y_0$, we consider $\bar{\mathcal{A}} := \mathcal{A}_{x_0}^U$ (see def.9), where we choose $U := \{x \mid x_0 \nabla_A x \neq y_0\}$. Invoking lemma 6 with $\pi_{\nabla_A}: \mathcal{A} \to \mathcal{A}/\nabla_A$ and recalling that $\mathcal{A}/\nabla_A$ is simple, we obtain $\nabla_{\bar{\mathcal{A}}} = \nabla_A =: \nabla$. By assumption (2), there is a bisimulation $S$ on $\bar{\mathcal{A}}$ with $S^* = \nabla$, so in particular $x_0 S^* y_0$. As $x_0 \neq y_0$, there is some $z \neq y_0$ with $x_0 S^* z S y_0$ and a fortiori $x_0 \nabla z S y_0$. Since $S$ is a bisimulation on $\bar{\mathcal{A}}$, there is some $q \in F(S)$ with $F\pi_1(q) = \bar{\alpha}(z) = \alpha(x_0)$ and $F\pi_2(q) = \bar{\alpha}(y_0) = \alpha(y_0)$.

$$ (3) \Rightarrow (1): $$

<figure><img src="image_10.png" /></figure>

By lemma 1 $[\pi_\nabla, id_{A/\nabla}]$ is regular epi. From theorem 2 we obtain $\sim_{A+A_\nabla}^* = \nabla_{A+A/\nabla}$. Then

$$ \begin{align*} [\ker[\pi_\nabla, id_{A_\nabla}]] &= [\nabla_{A+A/\nabla}] && \text{lemma 3} \\ &= \sim_{A+A_\nabla} \\ &= \sim_{A+A_\nabla}^* && \text{hypothesis} \\ &= \ker[\pi_\nabla, id_{A/\nabla}]. \end{align*} $$

Therefore, $\ker[\pi_\nabla, id_{A/\nabla}]$ is a bisimulation, and by lemma 9, $\nabla$ is a bisimulation.

For image finite Kripke structures $\mathcal{A}$, i.e. coalgebras for $D \times \mathbb{P}_{fin}$ where $D$ is a fixed output set and $\mathbb{P}_{fin}$ the finite-powerset functor, it is well known that $\sim_{\mathcal{A}} = \nabla_{\mathcal{A}}$. However, considered as a coalgebra of $D \times \mathbb{P}_{\leq k}$ where $\mathbb{P}_{\leq k}X := \{U \subseteq X \mid |U| \leq k\}$ the same Kripke structure may fail to satisfy $\sim_{\mathcal{A}} = \nabla_{\mathcal{A}}$. The fact that for $k \geq 3$ the functor $\mathbb{P}_{\leq k}$, defined as a subfunctor of $\mathbb{P}$, does not preserve weak kernel pairs was noticed in [8].

## 4.3 Difunctionality of $\sim$

In an attempt to generalize the results of the previous subsection to relations between two coalgebras, we consider the following conditions:

1. For all $F$-coalgebras $\mathcal{A}, \mathcal{B}: \sim_{\mathcal{A}, \mathcal{B}} = \nabla_{\mathcal{A}, \mathcal{B}}$

2. For all $F$-coalgebras $\mathcal{A}, \mathcal{B}: \sim_{\mathcal{A}, \mathcal{B}}^d = \nabla_{\mathcal{A}, \mathcal{B}}$
3. For all $F$-coalgebras $\mathcal{A}, \mathcal{B}: \sim_{\mathcal{A},\mathcal{B}}$ is difunctional.

We will show in the next section that the direction (2) ⇒ (1) holds more gener-
ally, yet the implication (3) ⇒ (1) fails in general. We provide a counterexample
(example 2) in the next section. We will use the following characterization of
preimages preservation.

**Theorem 8 ([6]).** The following are equivalent:

(1) *F preserves preimages*

(2) If $\mathcal{U}$, $\mathcal{V}$ are subcoalgebras of $\mathcal{A}$, $\mathcal{B}$ then bisimulations between $\mathcal{U}$ and $\mathcal{V}$ are just the restrictions to $\mathcal{U} \times \mathcal{V}$ of bisimulations between $\mathcal{A}$ and $\mathcal{B}$.

Under the assumption that $F$ should preserves preimages we will see that
difunctionality and transitivity of bisimulations are equivalent.

**Theorem 9.** If $F$ preserves preimages, then the following are equivalent:

(1) For all $F$-coalgebras $\mathcal{A}, \mathcal{B}: \sim_{\mathcal{A},\mathcal{B}} = \nabla_{\mathcal{A},\mathcal{B}}$

(2) For all $F$-coalgebras $\mathcal{A}, \mathcal{B}: \sim_{\mathcal{A},\mathcal{B}}$ is difunctional.

(3) For all $F$-coalgebras $\mathcal{A}: \sim_{\mathcal{A}} = \nabla_{\mathcal{A}}$.

*Proof.* (1) ⇒ (2) is evident because $\nabla_{\mathcal{A},\mathcal{B}}$ is difunctional.

(2) ⇒ (3) From the hypothesis it follows that $\sim_A$ is transitive for all $F$-coalgebras $\mathcal{A}$, because $\sim_A$ is reflexive and symmetric. By theorem 7 we obtain that for all $F$-coalgebras $\mathcal{A}: \sim_A = \nabla_A$.

(3) ⇒ (1) Let $\mathcal{A} = (A, \alpha)$ and $\mathcal{B} = (B, \beta)$ two coalgebra. We have to show $\sim_{\mathcal{A},\mathcal{B}} = \nabla_{\mathcal{A},\mathcal{B}}$.

$$
\begin{align*}
(a, b) \in \nabla_{\mathcal{A}, \mathcal{B}} &\iff (e_A(a), e_B(b)) \in \nabla_{\mathcal{A}+\mathcal{B}} && \text{by lemma 4} \\
&\iff (e_A(a), e_B(b)) \in \sim_{\mathcal{A}+\mathcal{B}} && \text{by hypothesis} \\
&\iff (a, b) \sim_{\mathcal{A}, \mathcal{B}} && \text{by theorem 8.}
\end{align*}
$$

**4.4 Relation liftings**

An alternative definition of bisimulation was given by C. Hermida and B. Jacobs
in [13]. The idea is to define a bisimulation $R$ as a relation $R \subseteq A \times B$ satisfying:

$$
xRy \implies \alpha(x) \bar{F}(R) \alpha(y)
$$

where $\bar{F}$ is the “lifting” of the relation $R \subseteq A \times B$ to a relation $\bar{F}(R) \subseteq F(A) \times F(B)$, known as Barr-extension:

$$
\bar{F}(R) := \{(F\pi_A^R(u), F\pi_B^R(u)) \mid u \in F(R)\}.
$$

Choosing the Barr-extension may be one particular method for extending a
relation between $\mathcal{A}$ and $\mathcal{B}$ to a relation between $F(\mathcal{A})$ and $F(\mathcal{B})$, but there might
likely be others, so we define:
**Definition 11.** A relation lifting $L$ is a transformation sending every relation $R \subseteq A \times A$ into a relation $L(R) \subseteq FA \times FB$. It is called monotonic, if $R \subseteq S$ implies $L(R) \subseteq L(S)$. For a given relation lifting $L$ and coalgebras $\mathcal{A} = (A, \alpha_A)$ and $\mathcal{B} = (B, \alpha_B)$, an $L$-simulation is a relation $R \subseteq A \times B$ such

$$x R y \implies \alpha(x) L(R) \alpha(y).$$

Diagrammatically, $R$ is an $L$-simulation if and only if the map sending $(x, y)$ to $(\alpha_A(x), \alpha_B(y))$ factors through $L(R)$, which is the same as saying that there exists a map $m$ such that the following diagram commutes:

<figure><img src="image_11.png" /></figure>

Thus a Hermida-Jacobs-bisimulation is the same as an $L$-simulation where $L = \bar{F}$. Observe, that categorically, $\bar{F}(R)$ arises by applying the functor $F$ to the source $\pi_A^R : R \to A$ and $\pi_B^R : R \to B$, then factoring the resulting source $F\pi_A^R : F(R) \to F(A)$ and $F\pi_B^R : F(R) \to F(B)$, into an epi $q$ followed by a mono-source:

<figure><img src="image_12.png" /></figure>

This diagram can be readily used to demonstrate the well known fact that our earlier definition of bisimulation agrees with that of Hermida and Jacobs in the presence of the axiom of choice. When $L = \bar{F}$, we can paste it to the bottom line of the previous diagram in order to see that any bisimulation $\rho : R \to F(R)$ yields an $\bar{F}$-simulation and conversely, any choice of right inverse $e$ for $q$ yields a bisimulation $\rho := e \circ m$.

Thijs in [22] defined relators as relation liftings with additional properties and generalized the notion of coalgebraic simulation. In [15] Marti and Venema introduced further properties, in an attempt to achieve that $L$-similarity should capture observational equivalence. The union of all $L$-simulations between given coalgebra $\mathcal{A}$ and $\mathcal{B}$ is denoted by $\approx_{\mathcal{A},\mathcal{B}}^L$. If $L$ is monotonic then $\approx_{\mathcal{A},\mathcal{B}}^L$ is again an $L$-simulation. For $L = \bar{F}$, of course, $\approx_{\mathcal{A},\mathcal{B}}^L$ agrees with $\sim_{\mathcal{A},\mathcal{B}}$.

In [15] it was also shown that there is no relation lifting $L$ for the neighborhood functor which captures observational equivalence in the sense that $\approx_{\mathcal{A},\mathcal{B}}^L = \nabla_{\mathcal{A},\mathcal{B}}$ for all coalgebras $\mathcal{A}, \mathcal{B}$. In particular, for this functor there are coalgebras $\mathcal{A}$ and $\mathcal{B}$ such that $\sim_{\mathcal{A},\mathcal{B}} \neq \nabla_{\mathcal{A},\mathcal{B}}$.

**Example 2.** Consider the neighborhood functor $2^{2^-}$. From theorem 6 $\sim_{\mathcal{A},\mathcal{B}}$ is difunctional for all coalgebras $\mathcal{A}, \mathcal{B}$, since $2^{2^-}$ weakly preserves kernel pairs [10]. But $\sim_{\mathcal{A},\mathcal{B}} = \nabla_{\mathcal{A},\mathcal{B}}$ does not hold.
In [9] we have shown, that bisimulations can be enlarged as long as the structure maps are not affected in the following sense:

**Proposition 2 ([9]).** Let $\mathcal{A}_1$ and $\mathcal{A}_2$ be coalgebras with corresponding structure maps $\alpha_1$ and $\alpha_2$. Let $R \subseteq \mathcal{A}_1 \times \mathcal{A}_2$ be a bisimulation and $R'$ an enlargement i.e. $R \subseteq R' \subseteq \ker \alpha_1 \circ R \circ \ker \alpha_2$. Then $R'$ is also a bisimulation.

A relation lifting L is called *extensible*, if for all coalgebras $\mathcal{A}_1$ and $\mathcal{A}_2$ the statement of the above proposition holds with “bisimulation” replaced by “L-simulation”. It turns out, that this property precisely captures monotonicity, i.e.:

**Proposition 3.** *A relation lifting L is monotonic iff it is extensible.*

*Proof.* The proof of the *if*-direction closely follows, but is not identical to, the proof of proposition 2 from [9]: $R$ is a *L-simulation*, so there exists a map $\rho: R \to L(R)$ with $\alpha_i \circ \pi_i^R = \pi_i^{LR} \circ \rho$. Let $\iota: R \to R'$ be the inclusion map, then clearly $\pi_i^R = \pi_i^{R'} \circ \iota$. By assumption, we find for every $(x', y') \in R'$ a pair $(x, y) \in R$ such that $\alpha_1(x) = \alpha_1(x')$ and $\alpha_2(y) = \alpha_2(y')$. The axiom of choice provides for a map $\mu: R' \to R$ satisfying

$$ \alpha_i \circ \pi_i^{R'} \circ \iota \circ \mu = \alpha_i \circ \pi_i^{R'}. $$

We now define $\rho': R' \to L(R')$ by $\rho' := \subseteq \circ \rho \circ \mu$.

<figure><img src="image_13.png" /></figure>

For the *only-if* direction, let $R \subseteq R' \subseteq A_1 \times A_2$ and $(\tilde{x}, \tilde{y}) \in LR$. We have to show $(\tilde{x}, \tilde{y}) \in LR'$. Since $(\tilde{x}, \tilde{y}) \in LR$ then $R$ is a *L-simulation* between $(A_1, c_{\tilde{x}})$ and $(A_2, c_{\tilde{y}})$. By the hypothesis $R'$ is also a *L-simulation*. Then $(\tilde{x}, \tilde{y}) \in LR'$.

With the help of this proposition, we can now somehow simplify the task of proving that $\approx_{A,B}^L$ captures observational equivalence, provided that L is monotonic:

**Theorem 10.** For a monotonic relation lifting L, the following are equivalent:

1. For all coalgebras $\mathcal{A}, \mathcal{B}: \approx_{\mathcal{A},\mathcal{B}} = \nabla_{\mathcal{A},\mathcal{B}}$

2. For all coalgebras $\mathcal{A}, \mathcal{B}: \approx_{\mathcal{A},\mathcal{B}}^d = \nabla_{\mathcal{A},\mathcal{B}}$
Proof. (1) ⇒ (2) is evident as $\nabla_{A,B}$ is difunctional.

(2) ⇒ (1): For any $\mathcal{A} = (A, \alpha)$ and $\mathcal{B} = (B, \beta)$, we have to show that $\nabla_{A,B}$ is an $L$-simulation. Given $(x_0, y_0) \in \nabla_{A,B}$, let $U := [x_0]\nabla_A$ and $V := [y_0]\nabla_B$, let $\varphi := \pi_{\nabla_{A+B}} \circ e_A$ and $\psi := \pi_{\nabla_{A+B}} \circ e_B$. Since $\mathcal{A} + \mathcal{B}/\nabla_{A+B}$ is simple, it follows from lemma 5 that $\ker \varphi = \nabla_A$ and $\ker \psi = \nabla_B$. We define now two coalgebras $\tilde{\mathcal{A}} := \mathcal{A}_{x_0}^U$ and $\tilde{\mathcal{B}} := \mathcal{B}_{y_0}^V$ as in definition 9. Since $U \subseteq [x_0]\ker \varphi$ and $V \subseteq [x_0]\ker \psi$, we can use lemma 6 to see that both $\varphi : \tilde{\mathcal{A}} \to \mathcal{A} + \mathcal{B}/\nabla_{A+B}$ and $\psi : \tilde{\mathcal{B}} \to \mathcal{A} + \mathcal{B}/\nabla_{A+B}$ are homomorphisms to a simple coalgebra, so by lemma 5, $\nabla_{\tilde{\mathcal{A}},\tilde{\mathcal{B}}} = \ker(\varphi, \psi) = \nabla_{A,B}$. By hypothesis $(x_0, y_0) \in \approx_{\tilde{\mathcal{A}},\tilde{\mathcal{B}}}^d$, so there is $x_1 \in A$ with $x_1 \approx_{\tilde{\mathcal{A}},\tilde{\mathcal{B}}} y_0$. From $\approx_{\tilde{\mathcal{A}},\tilde{\mathcal{B}}}^d = \nabla_{A,B}$ it follows that $\approx_{\tilde{\mathcal{A}},\tilde{\mathcal{B}}} \subseteq \nabla_{A,B}$, so $(x_1, y_0) \in \nabla_{A,B}$. Hence $\varphi(x_1) = \psi(y_0) = \varphi(x_0)$ and consequently $(x_0, x_1) \in \ker \varphi = \nabla_A$. By construction of $\tilde{\mathcal{A}}$ then $\tilde{\alpha}(x_1) = \alpha(x_0) = \tilde{\alpha}(x_0)$. With the help of proposition 3 we obtain $x_0 \approx_{\tilde{\mathcal{A}},\tilde{\mathcal{B}}} y_0$. Hence $(\tilde{\alpha}(x_0), \tilde{\beta}(y_0)) \in L \approx_{\tilde{\mathcal{A}},\tilde{\mathcal{B}}}$ and finally $(\alpha(x_0), \beta(y_0)) \in L\nabla_{A,B}$ since $\approx_{\tilde{\mathcal{A}},\tilde{\mathcal{B}}} \subseteq \nabla_{A,B}$ and $L$ is monotonic.

The Barr extension $\tilde{F}$ is an example of a monotonic relation lifting, so we obtain:

**Corollary 3.** The following are equivalent:

1. For all coalgebras $\mathcal{A}, \mathcal{B}: \sim_{\mathcal{A},\mathcal{B}} = \nabla_{\mathcal{A},\mathcal{B}}$.

2. For all coalgebras $\mathcal{A}, \mathcal{B}: \sim_{\mathcal{A},\mathcal{B}}^d = \nabla_{\mathcal{A},\mathcal{B}}$.

# 5 Conclusion and further work

In this paper we exhibited conditions under which bisimulations restrict to sub-coalgebras without requiring the type functor to preserve preimages. Further, we have shown that if the transitive, resp. difunctional hull of bisimilarity covers observational equivalence then bisimilarity and observational equivalence agree. If bisimilarity is transitive for all $F$-coalgebras, then it agrees with observational equivalence.

A negative result is that difunctionality is not enough to cover observational equivalence between two coalgebras. Assuming preimage preservation for the type functor $F$, transitivity and difunctionality of bisimilarity are equivalent.

We also show that $F$ weakly preserves kernel pairs if and only if every epi is regular epi. While it is known that this implies that every mono is regular mono, the converse remains an open question.

A further open question is: If every extensional coalgebra is simple, does this mean that $\sim_A = \nabla_A$ for all coalgebras $\mathcal{A}$? In order to put this question into a more general framework, we plan to investigate $L$-extensionality for arbitrary relation liftings $L$.

# References

1. P. Aczel and N. Mendler. A final coalgebra theorem. In D.H. Pitt et al., editors, *Proceedings category theory and computer science*, Lecture Notes in Computer Science, pages 357–365. Springer, 1989.
2. J. Adámek, H. Herrlich, and G.E. Strecker. *Abstract and Concrete Categories*. John Wiley & Sons, 1990.

3. M. Barr. Terminal coalgebras in well-founded set theory. *Theoretical Computer Science*, (144(2)):299–315, 1993.

4. H.P. Gumm. Elements of the general theory of coalgebras. LUATCS 99, Rand Afrikaans University, Johannesburg, South Africa, 1999.

5. H.P. Gumm. Functors for coalgebras. *Algebra Universalis*, 45:135–147, 2001.

6. H.P. Gumm and T. Schröder. Coalgebraic Structure from Weak Limit Preserving Functors. *Electronic Notes in Theoretical Computer Science*, (33):113–133, 2000.

7. H.P. Gumm and T. Schröder. Products of coalgebras. *Algebra Universalis*, 46:163–185, 2001.

8. H.P. Gumm and T. Schröder. Types and Coalgebraic Structure. *Algebra Universalis*, 53:229–252, 2005.

9. H.P. Gumm and M. Zarrad. Coalgebraic simulations and congruences. *Coalgebra Methods in Computer Science*, 16:118–134, 2014.

10. C. Kupke H. Hansen and E. Pacuit. Bisimulations for neighbourhood structures. algebra and coalgebra in computer science. *Lecture Notes in Computer Science*, pages 279–293, 2007.

11. C. Henkel. Klassifikation coalgebraischer Typfunktoren. Diplomarbeit, Universität Marburg, 2010.

12. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. *J. Assoc. Comput. Mach.*, 32:137–161, 1985.

13. C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting. *Inform. and Comput.*, 145(2):107–152, 1998.

14. Th. Ihringer and H.P.Gumm. *Allgemeine Algebra*. Heldermann Verlag, 2003.

15. J. Marti and Y. Venema. Lax extensions of coalgebra functors. *Coalgebraic Methods in Computer Science*, (LNCS 73):150–169, 2012.

16. Lawrence S. Moss. Coalgebraic logic. *Annals of Pure and Applied Logic*, 96:277–317, 1999.

17. D. Pattinson. Expressive logics for coalgebras via terminal sequence induction. *Notre Dame J. Formal Logic*, 45:19–33, 2004.

18. J. Riguet. Relations binaires, fermetures, correspondances de Galois. *Bulletin de la Societe Mathematique de France*, 76:114–155, 1948.

19. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. *Theoretical Computer Science*, 249(1):3–80, 2000.

20. T. Schröder. Coalgebren und Funktoren. Doktorarbeit, Universität Marburg, 2001.

21. S. Staton. Relating coalgebraic notions of bisimulaions. *Logical Methods in Computer Science*, 7(1), 2011.

22. A. Thijs. *Simulation and Fixpoint Semantics*. PhD thesis, University of Groningen, 1996.

23. V. Trnková. Some properties of set functors. *Comm. Math. Univ. Carolinae*, (10,2):323–352, 1969.

24. M. Zarrad. Verträgliche Relationen auf Coalgebren. Diplomarbeit, Universität Marburg, 2012.