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

HAL
open science

# Familial Monads and Structural Operational Semantics

Tom Hirschowitz

► To cite this version:

Tom Hirschowitz. Familial Monads and Structural Operational Semantics. Proceedings of the ACM on Programming Languages, 2019, 3 (POPL), pp.1-28. 10.1145/3290334. hal-01815328v4

HAL Id: hal-01815328

https://hal.science/hal-01815328v4

Submitted on 13 Nov 2019

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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Familial Monads and Structural Operational Semantics

TOM HIRSCHOWITZ, Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, France

We propose a categorical framework for structural operational semantics, in which we prove that under suitable hypotheses bisimilarity is a congruence. We then refine the framework to prove soundness of bisimulation up to context, an efficient method for reducing the size of bisimulation relations. Finally, we demonstrate the flexibility of our approach by reproving known results in three variants of the π-calculus.

CCS Concepts: • **Theory of computation** → **Denotational semantics; Operational semantics; Process calculi; Categorical semantics;**

Additional Key Words and Phrases: Structural operational semantics, category theory, familial monads

**ACM Reference Format:**

Tom Hirschowitz. 2019. Familial Monads and Structural Operational Semantics. *Proc. ACM Program. Lang.* 3, POPL, Article 21 (January 2019), 28 pages. https://doi.org/10.1145/3290334

# 1 INTRODUCTION

## 1.1 Motivation

*Structural operational semantics* [Plotkin 1981] is a method for specifying the dynamics of programming languages by induction on their syntax. This means that one describes the behaviour of a program in terms of its components, a feature often called *compositionality*. An important issue in structural operational semantics is the extent to which compositionality entails good behaviour of the generated labelled transition system. In this paper, we consider two particular questions: *congruence of bisimilarity* and *soundness of bisimulation up to context*.

The former is a long-standing problem in structural operational semantics. Bisimilarity is one of the most widely used behavioural equivalences, and congruence of bisimilarity essentially amounts to substitutivity: given two bisimilar program fragments *P* and *Q* (which we denote by *P* ~ *Q*), do we have *C[P] ~ C[Q]* for any context *C*. Bisimilarity is famously known not to be a congruence in general, e.g., in the π-calculus [Sangiorgi and Walker 2001, §2.2.1].

Our second object of study is bisimulation up to context [Pous and Sangiorgi 2011; Sangiorgi and Walker 2001], an efficient variant of bisimulation, which often produces the same results using simpler relations. However, it is sometimes unsound, in the sense that bisimilarity up to context may not entail bisimilarity. Just like congruence of bisimilarity, soundness of bisimulation up to context has proved to be a subtle matter.

The difficulty of such questions, particularly the former, led to a rich variety of syntactic formats [Mousavi et al. 2007], which ensure good behaviour of the generated labelled transition system, up to some constraints on the considered specification. Despite their diversity, these formats have a lot in common, both in definitions and in proof schemes.

This commonality motivated *functorial operational semantics* [Klin 2011; Turi and Plotkin 1997], a unifying theory of formats, in which specifications are recast as distributive laws of a comonad

Author's address: Tom Hirschowitz, Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, Chambéry, France.

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

This work is licensed under a Creative Commons Attribution 4.0 International License.

© 2019 Copyright held by the owner/author(s).

2475-1421/2019/1-ART21

https://doi.org/10.1145/3290334

21
over a monad. The approach has been deeply developed in the set-based case, particularly for congruence of bisimilarity [Mousavi et al. 2007], but also, among other questions, for soundness of bisimulation up to context [Bonchi et al. 2016]. A few attempts have also been made to cover languages with variable binding [Fiore and Staton 2006; Fiore and Turi 2001; Staton 2008].

However, despite its generality and power, functorial operational semantics, in particular in its variants with variable binding, has not caught on as widely as one might have hoped among more practical operational semanticists. A first reason, already noticed by Staton, is that it is “too abstract”. Specifically, although it is very powerful for proving general results, “one must really squint hard to view a distributive law as a collection of rules” [Staton 2008]. Otherwise said, functorial operational semantics is better at reasoning in the large than in the small. Another possible reason for functorial operational semantics not being more widely adopted might be that we should distinguish between two different goals, both of which are crucial for a theory of structural operational semantics to be adopted by the community: (1) the first goal is a high-level abstract language for reasoning on structural operational semantics, as close as possible to concrete intuitions; (2) the second is a generic toolbox for producing well-behaved structural operational semantics from more basic data. It seems fair to say that, until now, most work on the first goal was done with a view to the second one, i.e., with formats in mind. In this paper, instead, our aim is to find the right level of generality, by proposing a new theory of structural operational semantics which attempts to get closer to operational intuitions, while still proving useful abstract results – specifically, congruence of bisimilarity and soundness of bisimulation up to context.

## 1.2 Contributions

Our first contribution is the introduction of transition categories, which are categories equipped with a distinguished class of cospans, thought of as the set of transition labels. Transition categories support a notion of bisimulation defined by lifting, much as in Joyal et al. [1993]. A structural operational semantics specification is then a monad $\mathcal{T}$ on the considered transition category, which embodies the syntax and proof rules for transitions. Models of the specification $\mathcal{T}$ are thus simply $\mathcal{T}$-algebras. The Kleisli category of $\mathcal{T}$ is a high-level, flexible environment for reasoning about terms and (partial) transition proofs, where composition models plugging partial proofs (and terms) into one another. The approach thus lends itself to reasoning in the small. Our first main result (Corollary 4.30) is about reasoning in the large: it states that whenever $\mathcal{T}$ satisfies a certain familiality property [Carboni and Johnstone 1995; Diers 1978; Garner and Hirschowitz 2018; Weber 2007] and the considered $\mathcal{T}$-algebras, say $X$ and $Y$, are compositional, in the sense that both structure maps $\mathcal{T}(X) \to X$ and $\mathcal{T}(Y) \to Y$ are functional bisimulations, then bisimilarity (between states of $X$ and $Y$) is a congruence.

We then turn to soundness of bisimulation up to context in §5. Bisimulation up to context requires the introduction of an intermediate notion, pre-bisimulation, which, instead of relying on lifting, paraphrases the standard definition of bisimulation. We relate pre-bisimulation to bisimulation by showing that it also may be defined by lifting, though in the cospans category of the ambient transition category. Furthermore, under a mild additional hypothesis and using a suitable weak factorisation system, we show that any pre-bisimulation embeds into some bisimulation. We then define pre-bisimulation up to context, which agrees with standard bisimulation up to context in examples. Our second main result (Corollary 5.15) is that, up to a refinement of the familiality hypothesis, any pre-bisimulation up to context embeds into some bisimulation, i.e., pre-bisimulation up to context is sound. This is, to our knowledge, the first categorical soundness result for bisimulation up to context covering calculi with variable binding.
Finally, we demonstrate the flexibility of our framework in §6 by analysing the failure of bisimilarity to be a congruence in the π-calculus. We first pinpoint where the hypotheses of Corollary 4.30 fail, namely: the structure map $\mathcal{T}(Pi) \to Pi$ is not a functional bisimulation. We then recast in our setting two standard ways of working around this issue: (1) prove the weaker claim that bisimilarity is a non-input congruence [Sangiorgi and Walker 2001]; (2) restrict attention to a more constrained notion, wide-open bisimulation [Fiore and Staton 2006; Sangiorgi and Walker 2001; Staton 2008], to which Corollary 4.30 applies.

## 1.3 Related Work

We know of only two other abstract accounts of structural operational semantics covering both syntax and models (≈ categorical accounts), and proving congruence of bisimilarity: functorial operational semantics and Staton [2008]. The clearest novelty of our approach compared to them is that, to our knowledge, they do not cover soundness of bisimulation up to context in the presence of binding. Another distinctive feature is the crucial role of familiality. In particular, Staton [2008, Theorem 12] is very close in spirit to our Corollary 4.30, but beyond the fact that it lives in a different setting, it merely assumes that the considered monad preserves functional bisimulations, while familiality allows us to prove it. Less closely related work includes presheaf models and their generalisations [Cattani et al. 1998; Joyal et al. 1993], which emphasise semantical, rather than operational aspects. Furthermore, their representation of labelled transition systems as presheaves markedly differs from ours, in that, e.g., any finite but cyclic labelled transition system may be finitely represented in our approach, while it has to be represented by an infinite presheaf in theirs. Our approach is also more economical for defining bisimulation, by only lifting against one morphism per label, instead of one morphism per trace extension. Finally, our T<sub>s</sub>-familial monads are related to cellular analytic functors [Garner and Hirschowitz 2018], and the relationship between our pre-bisimulations and bisimulations (§5.2) is closely related to Dubut et al. [2016].

## 1.4 Plan

We start in §2 with a non-technical overview of the new framework, trying to show that it is more practical and intuitive than previous approaches. In §3, relying on the examples of combinatory logic and CCS, we recast structural operational semantics and congruence in the setting of monads on transition categories. In §4, we prove that compositionality and familiality entail congruence of bisimilarity. In §5, we investigate soundness of bisimulation up to context. In §6, we analyse bisimilarity in the π-calculus using our framework. Finally, we conclude in §7.

## 1.5 Notation and Preliminaries

We assume basic familiarity with category theory [Mac Lane 1998]. For any small category $C$, we denote by $\tilde{C}$ the category of presheaves on $C$, i.e., contravariant functors to sets (Set) and natural transformations between them. For any $f : c \to c'$ in $C$ and $X \in \tilde{C}$ the action $X(f) : X(c') \to X(c)$ is denoted by $x \mapsto x \cdot f$. The Yoneda embedding is denoted by $y: C \to \tilde{C}$, and often left implicit.

We denote by $el(X)$ the category of elements [Mac Lane and Moerdijk 1992] of any presheaf $X$: it has as objects all pairs $(c, x)$ with $x \in X(c)$, and as morphisms $(c, x) \to (c', x')$ all morphisms $f: c \to c'$ in $C$ such that $x' \cdot f = x$. We denote the corresponding morphism by $f \upharpoonright x'$. Furthermore, we often abbreviate $(c, x)$ to $x$.

Finally, we often denote by $n$ the finite set $\{1, ..., n\}$.
# 2 OVERVIEW

## 2.1 Bisimulation by Lifting

Before delving into details, let us give a non-technical overview. A transition category is much like the category of labelled transition systems (over a fixed set of labels), with functional simulations as morphisms. Sticking to the untyped case for simplicity, there is thus an object, say $★$, consisting of just one state. Similarly, for each label $α$, there is an object consisting of just one $α$-transition between two states. Thus, giving a morphism $★ \to X$ to any object $X$ is equivalent to choosing a state in $X$, and likewise giving a morphism $e: α \to X$ is equivalent to choosing an $α$-transition in $X$. Furthermore, taking the source of $e$ is just pre-composing with the source morphism $s: ★ \to α$.

So the source of $e$ is $e \circ s$. Symmetrically, its target is $★ \xrightarrow{t} α \xrightarrow{e} X$.

Now, we may define bisimulation diagrammatically, as follows. A relation $R \hookrightarrow X \times Y$ is a bisimulation iff both projections $p: R \to X$ and $q: R \to Y$ are functional bisimulations, where, e.g., $p$ is a functional bisimulation iff for all labels $α$ and commuting squares as below left, there is a lifting $k$ that makes both triangles commute.

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

$$ v = (x, y) \mathrel{\substack{| \\ \xrightarrow{k'}} \mathrel{\substack{\xrightarrow{p} \\ \vdots \\ \xrightarrow{e} \\ \vdots \\ \xrightarrow{p'}}}} x \quad (1) $$

Indeed, as we saw, $v$ denotes a state in $R$, i.e., a related pair $(x, y)$, $e$ an $α$-transition in $X$, and commutation of the square says that $p(v) = x$ is the source of $e$, so that $e: x \xrightarrow{α} x'$. We are thus in a situation like above right. Existence of $k$ then says that there is an $α$-transition $k$ in $R$ with source $v$, mapped by $p$ to $e$, i.e., a pair $(e, f): (x, y) \xrightarrow{α} (x', y')$ of related transitions as above right, just as in the standard definition of bisimulation.

## 2.2 Structural Operational Semantics Specifications as Monads

The next step is to view structural operational semantics specifications as monads $\mathcal{T}$ on the considered transition category. A specification consists of proof rules for inductively constructing transitions. Intuitively, $\mathcal{T}(X)$ is obtained by saturating its argument $X$ by the considered proof rules, i.e., it augments $X$ with new, formal transitions constructed using the rules. A model for the considered structural operational semantics specification is thus merely a $\mathcal{T}$-algebra, i.e., an object $X$ respecting the rules, formally a map $\mathcal{T}(X) \to X$ satisfying certain conditions.

The Kleisli category of $\mathcal{T}$ provides a high-level, flexible environment for manipulating terms and (partial) proofs, including plugging them into one another, at a fine level which is not directly available in functorial operational semantics.

**Remark 2.1.** This is not really surprising: monads are a generalisation of algebraic theories, and the Kleisli category (or rather its opposite) is the corresponding generalisation [Berger et al. 2012] of Lawvere's [1963] syntactic category.

**Example 2.2.** In the case of labelled transition systems, if $\mathcal{T}$ is the monad for CCS terms and rules: morphisms $★ \to \mathcal{T}(X)$ are in one-to-one correspondence with CCS terms with free variables (a.k.a. constants, or indeterminates) in $X$. Similarly, for any label $α$, morphisms $α \to \mathcal{T}(X)$ correspond to proofs of $α$-transitions with variables in $X$, meaning that transitions in $X$ are treated as axioms in the proof system. E.g., consider a labelled transition system $X \cong \bar{a} + a$ consisting of
just two transitions $e: x \xrightarrow{\bar{a}} x'$ and $f: y \xrightarrow{a} y'$. Then, the left-hand proof below yields a morphism $\tau \to \mathcal{T}(X)$, and the right-hand one yields a morphism $\bar{a} \to \mathcal{T}(X)$.

$$ \begin{array}{c} \begin{array}{c} \overline{e} \\ \xrightarrow{\bar{a}} x' \end{array} \qquad \begin{array}{c} \overline{f} \\ \xrightarrow{a} y' \end{array} \\ \hline (x|y) \xrightarrow{\tau} (x'|y') \end{array} \qquad \begin{array}{c} \overline{e} \\ \xrightarrow{\bar{a}} x' \end{array} \qquad \begin{array}{c} \overline{(x|y) \xrightarrow{\bar{a}} (x'|y)} \\ (x|y|y) \xrightarrow{\bar{a}} (x'|y|y) \end{array} \qquad (2) $$

The left-hand proof is linear, i.e., each bit of X is used exactly once. In such cases, the identity of these bits does not really matter, so we may represent proofs a bit more abstractly as transition contexts, i.e., partial proof trees, as below left.

$$ \begin{array}{c} \begin{array}{c} \Box_1 \xrightarrow{\bar{a}} \Box'_1 \end{array} \qquad \begin{array}{c} \Box_2 \xrightarrow{a} \Box'_2 \end{array} \\ \hline (\Box_1|\Box_2) \xrightarrow{\tau} (\Box'_1|\Box'_2) \end{array} \qquad \begin{array}{c} \Box \\ \xrightarrow{\bar{a}\Box} \Box \end{array} \qquad \begin{array}{c} \Box_2 \xrightarrow{a} \Box'_2 \end{array} \qquad \begin{array}{c} (\bar{a}\Box|\Box_2) \xrightarrow{\tau} (\Box|\Box'_2) \end{array} \qquad (3) $$

Such a transition context $E: \tau \to \mathcal{T}(\bar{a} + a)$ may be thought of as a term of type $\tau$ with two free variables of respective types $\bar{a}$ and $a$. Let us now assume that one wants to instantiate, say, the first variable in $E$ with the output rule $\bar{a}.\Box \xrightarrow{\bar{a}} \Box$ (which still depends on a process variable, $\Box$). Then they may compose $E$ in the Kleisli category with the morphism

$$ \bar{a} + a \xrightarrow{output+\eta} \mathcal{T}(\star) + \mathcal{T}(a) \xrightarrow{[\mathcal{T}(in_l), \mathcal{T}(in_r)]} \mathcal{T}(\star + a), $$

where $\eta: a \to \mathcal{T}(a)$ just picks the given variable, output is the map $\bar{a} \to \mathcal{T}(\star)$ corresponding to the output axiom, and $in_l$ and $in_r$ denote the coproduct injections $\star \hookrightarrow \star + a \hookleftarrow a$. Concretely, the composite in the Kleisli category is the transition context on the right in (3), where we explicitly leave $\Box$ as an open-ended branch to emphasise that it might be further instantiated with some (potentially open) process $P: \star \to \mathcal{T}(Y)$.

## 2.3 Congruence of Bisimilarity, Contexts, and Familiality

Now that we have explained why monads on transition categories model structural operational semantics specifications and how terms and partial transition proofs may be manipulated in the Kleisli category, let us consider congruence of bisimilarity. Essentially, this amounts to the fact that given any bisimulation $R$ relating the states of labelled transition systems $X$ and $Y$, the relation consisting of all pairs of the form $(C[x_1, ..., x_n], C[y_1, ..., y_n])$, for any context $C$ with $(x_i, y_i) \in R$ for all $i$, is again a bisimulation. The standard, operational approach for proving this [Bernstein 1998; Bloom et al. 1995; Bol and Groote 1996; Middelburg 2001; Mousavi et al. 2005; Sangiorgi 1994; Sangiorgi and Walker 2001] goes by induction on $C$, but the key underlying intuition is that any transition proof $e: C[x_1, ..., x_n] \xrightarrow{a} x'$ decomposes into a partial transition proof by the context $C$ and transition proofs by some $x_i$s. The categorical framework provides a high-level language to describe this, which leads to a more algebraic proof (by computation instead of by induction).

In our case, the key lemma will state that given algebras $a: \mathcal{T}(X) \to X$ and $b: \mathcal{T}(Y) \to Y$, together with a bisimulation $R$ as above, $\mathcal{T}(R)$ is again a bisimulation, in the sense that the composite $\mathcal{T}(R) \xrightarrow{\mathcal{T}(p)} \mathcal{T}(X) \xrightarrow{a} X$ and its symmetric variant with $Y$ satisfy the same lifting property (1)
as *p* above. First of all, it suffices to prove that both *a* and $\mathcal{T}(p)$ are functional bisimulations, so we consider them separately. The general framework does not have much to say about the former: as we will see in §4.1, it intuitively corresponds to the considered algebra being compositional.

For $\mathcal{T}(p)$, the first step is to be able to talk about contexts, i.e., terms which make linear use of their free variables. Among morphisms in the Kleisli category, contexts will be those satisfying a universal property called genericness, described at the beginning of §4.2. The monad $\mathcal{T}$ is familial just when any morphism $X \to \mathcal{T}(Y)$ canonically factors as

$$X \xrightarrow{C} \mathcal{T}(A) \xrightarrow{\mathcal{T}(f)} \mathcal{T}(Y)$$

with *C* generic, which corresponds to the standard fact that any term with free variables in *Y* decomposes as a context, here *C*, equipped with a map from its holes to *Y*, here *f*. The morphism $\mathcal{T}(A) \to \mathcal{T}(Y)$, being in the image of $\mathcal{T}$, is called free, and we generally refer to such factorisations as generic-free. The middle object *A* is called the *arity* of *C*.

**Example 2.3.** In the case of CCS, for any variable $x: \star \to X$, the term $(x|x)$ factors as

$$\star \xrightarrow{C} \mathcal{T}(\star + \star) \xrightarrow{\mathcal{T}[x,x]} \mathcal{T}(X),$$

where *C* is the context $(\square_1|\square_2)$. General generic transitions $\alpha \to \mathcal{T}(A)$ are essentially the transition contexts of Example 2.2.

The factorisation property of familial monads applies uniformly to terms, transitions, and more (i.e., any object). An important feature of generic-free factorisations in our examples is that they also prescribe how to compute the source and target of transition contexts. The source of a transition, i.e., of a (not necessarily generic) morphism $E: \alpha \to \mathcal{T}(Y)$, is just the composite $\star \xrightarrow{s} \alpha \xrightarrow{E} \mathcal{T}(Y)$. So if we start with a generic $E$, and take the generic-free factorisation of $E \circ s$, we get a commuting square

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

**Example 2.4.** When $E$ is as on the left of (3), factoring $E \circ s$ yields $C := (\square_1|\square_2): \star \to \mathcal{T}(\star + \star)$ with $f = s + s: \star + \star \to \bar{a} + a$. Please note that when $E$ is instantiated, say with $h: \bar{a} + a \to Z, f$ gives the desired instantiation of *C*, namely the composite $\star + \star \xrightarrow{s+s} \bar{a} + a \xrightarrow{h} Z$, which correctly models the fact that the source of any transition $z_1|z_2 \xrightarrow{\tau} z'_1|z'_2$ of this form is indeed $z_1|z_2$.

Returning to the proof that $\mathcal{T}(p)$ is a functional bisimulation when $p$ is, we need to prove that any commuting square as the exterior below admits a lifting. Using familiality of $\mathcal{T}$, we take generic-free factorisations of both *e* and *r* (morally: the given transition and pair of terms, respectively), as in the solid part of

<figure><img src="image_6.png" /></figure>
Genericness of C (see §4.2 for details) then yields *l* making both squares commute (with $p \circ k = h \circ l$). Intuitively, the left-hand square should be just as in Example 2.4, so *l* should merely be a coproduct of source maps. Because *p* is a functional bisimulation, we should thus find a lifting for each one of them, hence *j* by cotupling, which yields the desired lifting $\mathcal{T}(j) \circ E$. In order to enforce this property that the obtained *l* still admits liftings w.r.t. functional bisimulations, we need to impose a further hypothesis on $\mathcal{T}$, which is essentially a specialisation of cellularity [Garner and Hirschowitz 2018]. This is called $T_s$-familiality and explained in detail in §4.3.

## 2.4 Summary

We hope that the present overview demonstrates that the Kleisli category of a monad on a transition category is a high-level, flexible algebraic framework for reasoning about structural operational semantics. It is finer-grained than functorial operational semantics, in the sense that it directly models terms and (partial) transition proofs. Yet, it is a convenient language for proving properties like congruence of bisimilarity. Notably, the language of familial monads brings us closer to intuitions underlying the standard proof by induction over context, and proceed algebraically instead of logically. Similar benefits are observed for bisimulation up to context in §5, using much the same language except that lifting is done in the more complex category of cospans in the ambient transition category. This makes the development a bit more verbose, so we refrain from exposing it here, and move on to the technical development.

# 3 STRUCTURAL OPERATIONAL SEMANTICS SPECIFICATIONS AS MONADS

In this section, we essentially fill in the technical details of §2, up to the abstract statement of congruence of bisimilarity. We first explain how labelled transition systems may be viewed as presheaves, and how bisimulation may be defined by lifting (§3.1). We then abstract over this to define transition categories and bisimulation therein. We then show how structural operational semantics specifications naturally yield monads (§3.2), an observation originally due to Staton [2008]. We finally define congruence in this setting.

## 3.1 Labelled Transition Systems as Objects in Transition Categories

Let us first view labelled transition systems as presheaves in concrete examples, and then abstract over what we did and define transition categories and bisimulation therein.

**3.1.1 Labelled Transition Systems.** The simplest kind of labelled transition system, the one with just one label, is suitably modelled by **Gph**, the category of (directed, multi) graphs, i.e., presheaves over the category $★ \xrightarrow[s]{\underset{l}{\smash{\rightleftharpoons}}} [1]$ (provided one accepts the extra generality of allowing distinct, parallel transitions between nodes). More generally, let us show that transition systems labelled in a set $L$ may also be viewed as presheaves. As a first step, they may be defined as graph morphisms to the graph $A_L$ with one vertex and one endo-edge for each label $l \in L$. So the relevant category is the slice **Gph**/*A*/*L*. But as is well known, for any $A$, **Gph**/*A* is equivalent to $\overline{el(A)}$, presheaves over the category of elements of $A$.

*Example 3.1.* In CCS, labels are elements of $L_{CCS} = \{\tau\} \cup \bigcup_{a \in \mathcal{A}} \{a, \bar{a}\}$, where $\mathcal{A}$ denotes a fixed, infinite set of names, for example the natural numbers $\mathbb{N}$. The relevant base category $C_{CCS} := el(A_{L_{CCS}})$ is freely generated by the graph with vertices in $\{★\} \uplus L_{CCS}$, plus, for all $\alpha \in L_{CCS}$, two edges $★ \xrightarrow{s|\alpha} \alpha \iff \alpha \xrightarrow{t|\alpha} ★$, which we often abbreviate to *s* and *t*. E.g., the labelled transition system $x \leftarrow \bar{a} \quad y \iff \begin{array}{l} b \\ b \end{array} \quad z \leftarrow^a \emptyset$ is modelled by the presheaf X with
$$
\begin{align*}
X(\star) = \{x, y, z\} & \qquad X(\bar{a}) = \{e\} & x = e \cdot t \\
X(b) = \{f, f'\} & \qquad y = e \cdot s = f \cdot s = f' \cdot s \\
X(a) = \{g\} & \qquad z = f \cdot t = f' \cdot t = g \cdot s = g \cdot t.
\end{align*}
$$

3.1.2 Bisimulation. Having seen how presheaves on C$_{CS}$ generalise labelled transition systems, let us now define functional bisimulation by lifting, as sketched in the overview. We will use the following efficient, standard notation [Riehl 2014]. In any category A , a lifting problem for mor- phisms f and g is a commuting square as the solid part below. A solution to the lifting problem is a lifting as shown (dashed) making both triangles commute.

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

Definition 3.2. Let f ⧸ g iff all lifting problems for f and g have at least one solution.

When f ⧸ g , we say that g has the right lifting property w.r.t. f , or symmetrically that f has the left lifting property w.r.t. g . We moreover let f ⧸ denote the class of all morphisms that have the right lifting property w.r.t. f . Similarly, for any class D of morphisms, let D ⧸ = ⋂ f ∈D f ⧸ . We define ⧸ g and ⧸ D symmetrically.

PROPOSITION 3.3. A morphism p : R → X in C̄$_{CS}$ is a functional bisimulation (according to the standard definition) iff it has the right lifting property w.r.t. all maps of the form s : ★ → α for α a label, i.e., iff p ∈ T̄$_{s}$ , where T$_{s}$ denotes the set of all maps s : ★ → α .

Indeed, this is just as in § 2.1, which should now make technical sense.

General (potentially non-functional) bisimulations may be defined as spans X ← l R → r Y where l and r are functional bisimulations. Such bisimulations may have non-monic pairings R → X × Y , but if we consider their epi-mono factorisations R ← s im(R) ⊢ m X × Y , we have:

Proposition 3.4. The monic factor of any bisimulation is again a bisimulation.

Proof. Consider any factorisation m ◦ e as above. Because ★ is representable, its covariant hom- functor preserves epis, i.e., if f : A → B is epi, so is the set map C̄$_{CS}$(★, A ) C̄$_{CS}$(★, f ) C̄$_{CS}$(★, B ). Thus every lifting problem for any s : ★ → α and im ( R ) ⊢ m X × Y π X induces a lifting problem for s and the composite π ◦ m ◦ e . The latter has a lifting by hypothesis, which yields a lifting for π ◦ m . Everything works symmetrically for the projection to Y . □

Definition 3.5. Isomorphism classes of monic bisimulations, i.e., subobjects of X × Y that are bisimulations, are called bisimulation relations.

Bisimulation relations are ordered by inclusion and for any set I we may define the union of relations R$_{i}$ ↪ → X × Y , for i ∈ I , as the image of their (wide) cotupling ∑$_{i}$ R$_{i}$ → X × Y . We have:

Proposition 3.6. Bisimulation relations are closed under union, and admit a maximum, called bisimilarity.

Proof. As before the covariant hom-functor of ★ preserves epis. Thus, every lifting problem for any s : ★ → α and a given union ⋃$_{i}$ R$_{i}$ ↪ → X × Y π X yields one for some R$_{i}$ ↪ → X × Y → X , which has a lifting by hypothesis. Finally, presheaf categories are well-powered , i.e., each object has only a set of subobjects. We thus in particular only have a set of bisimulation relations. This set being closed under unions, it has a maximum. □
### 3.1.3 Transition Categories.
Let us now abstract away from the particular example of $\overline{\mathbb{C}_{\mathrm{CCS}}}$.
The structure and properties we need for deriving abstract analogues of Propositions 3.4 and 3.6 are:

**Definition 3.7.** A transition category is a cocomplete, finitely complete, well-powered category $\mathcal{A}$ with images (i.e., initial factorisations through some mono), equipped with

* two sets $\mathbf{P}$ and $\mathbf{L}$ of objects called *process types* and *label types*, respectively, and

* a set $\mathbf{T}$ of cospans $P \xrightarrow{s} L \xleftarrow{t} Q$ called *transition types*, in which $P, Q \in \mathbf{P}$ and $L \in \mathbf{L}$, such that process types are *tiny*, i.e., their covariant hom-functors preserve colimits.

**Notation 3.8.** We generally denote a transition category by just $\mathcal{A}$, leaving $\mathbf{P}$, $\mathbf{L}$, and $\mathbf{T}$ implicit.

**Remark 3.9.** In any initial factorisation $A \xrightarrow{e} B \xrightarrow{m} C$ with $m$ mono, $e$ is epi, because if $f \circ e = g \circ e$ then $e$ factors through the equaliser of $f$ and $g$, which thus has to be an iso [Johnstone 2002, p20].

**Remark 3.10.** Tininess entails that covariant hom-functors of process types preserve epis.

In examples, tininess follows from:

**Remark 3.11.** If $\mathcal{A}$ is a presheaf category, then all representable presheaves are tiny.

Let us now abstractly replay the above development of bisimulation and bisimilarity.

**Definition 3.12.** For any transition category $\mathcal{A}$, a morphism $f: R \to X$ is a *functional bisimulation* iff it is in $T_s^\square$, where $T_s$ denotes the class of morphisms appearing as $s$ in some transition type. Given any two objects $X$ and $Y$, a *bisimulation* is a span $X \leftarrow^s R \xrightarrow{t} Y$, or equivalently a map $R \xrightarrow{\langle s,t \rangle} X \times Y$ such that $s$ and $t$ are both functional bisimulations. Isomorphism classes of monic bisimulations are called *bisimulation relations*.

**PROPOSITION 3.13.** In any transition category $\mathcal{A}$, bisimulations are closed under images, i.e., if $r: R \to X \times Y$ is a bisimulation, then so is $m$ in its epi-mono factorisation $R \stackrel{q}{\to} im(R) \xrightarrow{m} X \times Y$.

**PROPOSITION 3.14.** In any transition category, bisimulation relations $R \hookrightarrow X \times Y$ are closed under unions, hence admit a maximum, called *bisimilarity* and denoted by $\sim_{X,Y}$, or simply $\sim$ when $X$ and $Y$ are clear from context.

As expected we have:

**Example 3.15 (Graphs).** Graphs form a transition category with $\mathbf{P} = \{\mathbf{y}_\star\}$, $\mathbf{L} = \{\mathbf{y}_{[1]}\}$, and the cospan $\star \xrightarrow{s} [1] \xleftarrow{t} \star$ as unique transition type (omitting the Yoneda embedding).

**Example 3.16 (CCS labels).** The category $\overline{\mathbb{C}_{\mathrm{CCS}}}$ forms a transition category with $\star$ as only process type, all other representables as label types, and all cospans $\star \xrightarrow{s} \alpha \xleftarrow{t} \star$ as transition types.

## 3.2 Specifications as Monads on Transition Categories

In the previous section, we have defined transition categories and bisimulation therein, which abstract over standard labelled transition systems. Let us now further explain how structural operational semantics specifications may be viewed as monads on transition categories, again starting with examples and then abstracting away.
### 3.2.1 First Example: Combinatory Logic.
To get a feel for why monads on transition categories are relevant to operational semantics, let us consider the example of combinatory logic, viewed as a labelled transition system on just one label, i.e., a graph.

Let $\mathcal{T}_{CL}$ denote the functor on **Gph** mapping any graph $G$ to the one with

* as vertices all terms generated by the grammar $M, N ::= (x) | S | K | MN$, where $x$ ranges over $G(\star)$, $S$ and $K$ are constants, and $MN$ stands for the application of a binary function symbol (called "application") to $M$ and $N$;

* edges inductively defined by the following rules, with the given sources and targets.

$$ \begin{array}{ccc} \frac{e \in G(x, y)}{(e) : (x) \to (y)} & \overline{s_{M,N,P} : SMNP \to (MN)(MP)} & \overline{k_{M,N} : KMN \to M} \\ \frac{L : M \to M'}{LN : MN \to M'N} & \overline{R : N \to N'} & \overline{MR : MN \to MN'} \end{array} $$

The action of $\mathcal{T}_{CL}$ on morphisms is by applying the given graph morphism to vertices $(x)$ and edges $(e)$. This functor is a monad whose multiplication (a.k.a. substitution) merely removes the top layer of $((\cdot)-)$s. It is inductively defined by

$$ \begin{array}{lclcl} \mu_{G,\star}(m) & = & m & \mu_{G,[1]}(r) & = & r \\ \mu_{G,\star}(K) & = & K & \mu_{G,[1]}(k_{M,N}) & = & k_{\mu_{G,\star}(M),\mu_{G,\star}(N)} \\ \mu_{G,\star}(S) & = & S & \mu_{G,[1]}(s_{M,N,P}) & = & s_{\mu_{G,\star}(M),\mu_{G,\star}(N),\mu_{G,\star}(P)} \\ \mu_{G,\star}(MN) & = & \mu_{G,\star}(M) \mu_{G,\star}(N) & \mu_{G,[1]}(LN) & = & \mu_{G,[1]}(L) \mu_{G,\star}(N) \\ & & & \mu_{G,[1]}(MR) & = & \mu_{G,\star}(M) \mu_{G,[1]}(R). \end{array} $$

**Example 3.17.** Let $M = (M_1) (M_2)$, with $M_1, M_2 \in \mathcal{T}_{CL}(0)(\star)$. Then, $\mu_{0,\star}(M) = M_1 M_2$. Similarly, for $k_{P,Q} \in \mathcal{T}_{CL}(0)(K P Q, P)$, we have $\mu_{0,[1]}((k_{P,Q}) M) = k_{P,Q} (M_1 M_2)$.

The free algebra $\mathcal{T}_{CL}(0)$ is a proof-relevant variant of combinatory logic.

### 3.2.2 Example with Labels: CCS.
As a second example, useful for illustrating labels, let us consider CCS, recalling the base category $C_{CCS}$ from §3.1.1.

**Definition 3.18.** Let $\mathcal{T}_{CCS}$ denote the functor on $\overline{C_{CCS}}$ such that

* $\mathcal{T}_{CCS}(G)(\star)$ is the set of CCS terms (simplified for expository purposes) with variables in $G(\star)$, i.e., generated by the grammar $P, Q ::= (x) | 0 | a.P | \bar{a}.P | (P|Q) | va.P$, with $x$ ranging over $G(\star)$, not considered equivalent up to renaming of bound names in $va.P$ ($\alpha$-equivalence is not necessary for CCS; by contrast, it is necessary for $\pi$-calculus, which forces us to use a more complex base category);

* for all $\alpha \neq \star$, $\mathcal{T}_{CCS}(G)(\alpha)$ is the set of transition proofs $P \xrightarrow{\alpha} Q$, much as in Boudol and Castellani [1988], inductively generated by the following rules.

$$ \begin{array}{ccc} \frac{e \in G(\alpha)}{(e) : (e \cdot s) \xrightarrow{\alpha} (e \cdot t)} & \overline{out_p^a : \bar{a}.P \xrightarrow{\bar{a}} P} & \overline{in_p^a : a.P \xrightarrow{a} P} \\ \frac{L : P \xrightarrow{\alpha} P'}{(L|Q) : (P|Q) \xrightarrow{\alpha} (P'|Q)} & \frac{L : P \xrightarrow{\bar{a}} P' \quad R : Q \xrightarrow{a} Q' \quad (\text{sym. } R \triangleleft L)}{L \triangleright R : (P|Q) \xrightarrow{\tau} (P'|Q')} & \frac{}{} \end{array} $$
Again substitution equips $\mathcal{T}_{CCS}$ with monad structure, and the free algebra $\mathcal{T}_{CCS}(0)$ is a proof-relevant variant of CCS.

**3.2.3 Abstract Congruence.** In the previous sections, we have seen two example monads on transition categories, which have the labelled transition systems for combinatorial logic and CCS as their free algebras. Let us now review what it means to be a congruence, and then give an abstract definition in the setting of algebras for a monad on a transition category.

Standardly, given a structural operational semantics specification $X$, we say that a relation $R$ is a congruence when for all multi-hole contexts $C$ and pairs $(x_1, y_1), \dots, (x_n, y_n)$ of related processes, $C[x_1, \dots, x_n]$ and $C[y_1, \dots, y_n]$ are again related. In the abstract setting, given any monad $\mathcal{T}$ on a transition category $\mathcal{A}$, we may mimick this definition, and even slightly generalise it by considering two different $\mathcal{T}$-algebras:

**Definition 3.19.** Given a monad $\mathcal{T}$ on a transition category $\mathcal{A}$, $\mathcal{T}$-algebras $a: \mathcal{T}(X) \to X$ and $b: \mathcal{T}(Y) \to Y$, and a relation $R \hookrightarrow X \times Y$, we say that $R$ is a *congruence* when the map $\mathcal{T}(R) \to \mathcal{T}(X \times Y) \xrightarrow{\langle \mathcal{T}(\pi)_R, \mathcal{T}(\pi') \rangle} \mathcal{T}(X) \times \mathcal{T}(Y) \xrightarrow{a \times b} X \times Y$ factors through $R \hookrightarrow X \times Y$.

**PROPOSITION 3.20.** When $R \hookrightarrow X \times Y$ is a congruence, $R$ is a $\mathcal{T}$-algebra and $R \hookrightarrow X \times Y$ is a morphism of $\mathcal{T}$-algebras.

**Remark 3.21.** What does factorisation through $R$ have to do with being a congruence? Intuitively, an element in $\mathcal{T}(R)$ has the form $C[(x_1, y_1), \dots, (x_n, y_n)]$, with $(x_i, y_i) \in R$ for all $i$. It is mapped by $\langle \mathcal{T}(\pi), \mathcal{T}(\pi') \rangle$ to the pair $(C[x_1, \dots, x_n], C[y_1, \dots, y_n]) \in \mathcal{T}(X) \times \mathcal{T}(Y)$, and $a \times b$ evaluates this back to $X \times Y$. Thus, the composite factoring through $R$ precisely means that $a(C[x_1, \dots, x_n])$ and $b(C[y_1, \dots, y_n])$ are related, i.e., $R$ is a congruence.

# 4 CONGRUENCE OF BISIMILARITY

In the previous sections, we have explained in which sense monads on transition categories model structural operational semantics specifications, and defined congruence in this setting. We now turn to proving congruence of bisimilarity, by filling in the details missing from the overview. We consider compositionality in §4.1, familiality in §4.2, and $T_s$-familiality in §4.3. Relying on the theory of weak factorisation systems, we are then able to prove congruence of bisimilarity.

## 4.1 Compositionality

In the overview, our proof sketch for congruence of bisimilarity started by assuming that the structure map $a: \mathcal{T}(X) \to X$ of the considered algebra was a functional bisimulation. Concretely, for any square as below, there exists a lifting $k$ making both triangles commute.

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

Thinking of $v$ as a process with variables in $X$, i.e., a context applied to some processes in $X$, of $a \circ v$ as its evaluation in $X$, and of $r$ as a transition from $a \circ v$, this says that $r$ may be decomposed as the evaluation $a \circ k$ of some transition proof $k$ with variables in $X$ and domain $k \circ s = v$. This leads us to:

**Definition 4.1.** A $\mathcal{T}$-algebra $a: \mathcal{T}(X) \to X$ is compositional iff $a \in T_s^2$.

**Notation 4.2.** We often denote algebras by their carriers, e.g., $X$ is compositional.
**Example 4.3.** It might be instructive to exhibit a simple example of a non-compositional algebra. Consider the monad $\mathcal{T}$ on **Gph** whose terms are freely generated by a constant $c$ and two unary operations $f$ and $g$, and whose transitions are freely generated by the axiom below left.

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

Clearly, the transition above right cannot be matched by $f[g(c)]$ because no rule has a conclusion starting from $f$ alone. The free $\mathcal{T}$-algebra $\mathcal{T}(0)$ is thus not compositional, i.e., the monad multiplication $\mu$ is not in $\mathcal{T}_s^2$.

**PROPOSITION 4.4.** The free $\mathcal{T}_{CL}$-algebra $\mathcal{T}_{CL}(0)$ is compositional, i.e., $\mu_0 \in \mathcal{T}_s^2$.

**PROOF SKETCH.** (More detail in [Hirschowitz 2018].) Any $M \in \mathcal{T}_{CL}^2(0)$ is a process with variables in $\mathcal{T}_{CL}(0)$, i.e., it has the shape $C[M_1, \dots, M_n]$. We need to be able to decompose any transition $R: \mu_{0,\star}(M) \to N$ into $E[e_1, \dots, e_n]$ such that $\mu_{0,[1]}(E[e_1, \dots, e_n]) = R$. We proceed by induction on C. E.g., if $C = C_1 C_2$ and $R = L P$, then there exists $i \in n$ such that $L \cdot s = \mu_{0,\star}(C_1[M_1, \dots, M_{i-1}])$ and $P = \mu_{0,\star}(C_2[M_{i'}, \dots, M_{n'}])$. Then, by induction hypothesis, we find $E'[e'_1, \dots, e'_{i-1}]$ such that $\mu_{0,[1]}(E'[e'_1, \dots, e'_{i-1}]) = L$, so we can pick $E = E' C_2$. $\square$

**PROPOSITION 4.5.** The $\mathcal{T}_{CCS}$-algebra $\mathcal{T}_{CCS}(0)$ is compositional.

**PROOF.** Similar to $\mathcal{T}_{CL}$, using the fact that, because we do not mod out by $\alpha$-equivalence, each $\alpha$-operator is considered as a unary operator. $\square$

## 4.2 Familiality

Let us now turn to proving that $\mathcal{T}(f) \in \mathcal{T}_s^2$, starting with familiality. Here is the long-awaited definition of genericness:

**Definition 4.6.** Given any functor $\mathcal{F}: \mathcal{A} \to \mathcal{X}$, a morphism $\xi: X \to \mathcal{F}(A)$ is **$\mathcal{F}$-generic**, or **generic** for short, when for all commuting squares of the form

$$ \begin{tikzcd} X \arrow[r, "\chi"] & \mathcal{F}(B) \arrow[d, "\xi"] \\ \mathcal{F}(A) \arrow[r, "\mathcal{F}(f)"', "\mathcal{F}(g)"'] & \mathcal{F}(C) \arrow[d] \end{tikzcd} \qquad (5) $$

there exists a unique $h$ such that $\mathcal{F}(h) \circ \xi = \chi$ and $g \circ h = f$.

**Example 4.7.** Let $\mathcal{F}$ denote the free monoid monad on sets, which associates to any set $X$ the set $\sum_n X^n$ of sequences of elements of $X$. The generic-free factorisation associated to any sequence $l = (x_1, \dots, x_n)$, viewed as a morphism $1 \to \mathcal{F}(X)$, is

$$ 1 \xrightarrow{(1, \dots, n)} \mathcal{F}(n) \xrightarrow{\mathcal{F}[x_i]_{i \in n}} \mathcal{F}(X), $$

where we recall that $n$ denotes $\{1, \dots, n\}$. Intuitively, the generic part retains only the ‘shape’ of $l$, or otherwise said the linear term from which $l$ may be obtained by substitution.

**Example 4.8.** In the same setting, a non-generic morphism is the sequence $(1, 1)$, viewed as a morphism $1 \to \mathcal{T}(1)$. Indeed, the square
<figure><img src="image_10.png" /></figure>

commutes, with diagonal the sequence (1, 1), but no renaming will send (1, 1) to (1, 2). This example shows the tight connection between genericity and linearity.

**Definition 4.9.** A functor $\mathcal{F}: \mathcal{A} \to \mathcal{X}$ is *familial* when any morphism $X \to \mathcal{F}(A)$ factors as the composite of some generic morphism followed by a *free* one, i.e., one of the form $\mathcal{F}(f)$. A monad $(\mathcal{F}, \eta, \mu)$ is *familial* when the underlying endofunctor is, and furthermore $\eta$ and $\mu$ are *cartesian* natural transformations, i.e., all their naturality squares are pullbacks.

**Remark 4.10.** By the pullback lemma, when the domain category has a terminal object, a natural transformation $\alpha: F \to G$ is cartesian iff its naturality squares of the form below are pullbacks.

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

It should now be clear that the mediating arrow $l$ in (4) follows from genericity of C.

**Example 4.11.** On **Set**, if the considered functor $\mathcal{T}$ is finitary, then arities $A$ of generic operations $C: 1 \to \mathcal{T}(A)$ may be proved to be finite, so we may simply choose them to be the ordinal corresponding to the number $n_C$ of holes in $C$. Familial functors thus coincide with standard polynomial functors [Kock 2011], as we have $\mathcal{T}(X) \cong \sum_C X^{n_C}$.

There is a slight generalisation of the formula of Example 4.11 to presheaf categories, which will be useful for showing that the monads $\mathcal{T}_{CL}$ and $\mathcal{T}_{CCS}$ of §3.2.1 and §3.2.2 are familial:

**LEMMA 4.12 ([WEBER 2007, REMARK 2.12]).** An endofunctor $\mathcal{T}$ on any presheaf category $\widehat{\mathbb{C}}$ is familial iff there is a functor $E: \mathrm{el}(\mathcal{T}(1)) \to \widehat{\mathbb{C}}$ and a natural isomorphism (in $X$ and $c$):

$$ \mathcal{T}(X)(c) \cong \sum_{x \in \mathcal{T}(1)(c)} \widehat{\mathbb{C}}(E(c, x), X). \qquad (6) $$

**PROOF SKETCH.** In presheaf categories, familiality is equivalent to pointwise familiality, i.e., existence of a generic-free factorisation for all morphisms of the form $y_c \to \mathcal{T}(X)$. Any functor of the form (6) is clearly pointwise familial: any map $(x, \varphi): y_c \to \mathcal{T}(X)$, with $\varphi: E(c, x) \to X$, factors as $y_c \xrightarrow{(x,id)} \mathcal{T}(E(c, x)) \xrightarrow{\mathcal{T}(\varphi)} \mathcal{T}(X)$. Conversely, if $\mathcal{T}$ is pointwise familial, define $E(c, x)$ for any $x: y_c \to \mathcal{T}(1)$ to be given by (any global choice of) generic-free factorisation of $x$: $y_c \to \mathcal{T}(E(c, x)) \to \mathcal{T}(1)$. $\square$

**PROPOSITION 4.13.** The monad $\mathcal{T}_{CL}$ is familial.

**PROOF SKETCH.** (More detail in [Hirschowitz 2018].) By Lemma 4.12, it suffices to exhibit a functor $E: \mathrm{el}(\mathcal{T}_{CL}(1)) \to \mathbf{Gph}$, such that $\mathcal{T}_{CL}(Z)(c) \cong \sum_{x \in \mathcal{T}_{CL}(1)(c)} [E(c, x), Z]$, naturally in $c$ and $Z$. Now, $\mathcal{T}_{CL}(1)(\star)$ consists of terms on a unique free variable, say $\top$, and we define $E$ to map any such term $C$ to the discrete graph with vertices in the ordinal $n_C$, where $n_C$ is the number of occurrences of $\top$ in $C$. Similarly, $\mathcal{T}_{CL}(1)[1]$ consists of transition proofs on just one transition axiom, say $\Pi: \top \to \top$. On such proofs, we define $E$ by induction:
$$E(|\Pi|) = \mathbf{y}_{[1]}, \quad E(k_{M,N}) = E(M) + E(N), \quad E(LN) = E(L) + E(N),...$$

E is then defined on $s \upharpoonright R$ and $t \upharpoonright R$ (recall §1.5), by straightforward induction. □

**PROPOSITION 4.14.** *T<sub>CS</sub>* is *familial*.

**PROOF.** Similar, using the fact that we do not mod out by $\alpha$-equivalence. □

## 4.3 Congruence of Bisimilarity And T<sub>s</sub>-Familiality

Let us now get to $T_s$-familiality. In the overview, we obtained by familiality of $\mathcal{T}$ the mediating morphism $l$, which we argued should intuitively be a coproduct of source maps. This allowed us to find a lifting: we found one for each source map individually, and then took the cotupling. In the general case, however, there is a priori no guarantee that the mediating morphism will have such a nice form. Now, the only thing we need in order to conclude is that the mediating morphism be in $\mathcal{V}(T_s^2)$, so it is tempting to take this as an additional hypothesis. But the question is then whether this will be expressive enough to cover our examples. E.g., will $\mathcal{V}(T_s^2)$ always contain coproducts of maps in $T_s$ and isomorphisms? This is where basic results from weak factorisation systems [Hovey 1999; Riehl 2014] come to the rescue.

**4.3.1 Weak Factorisation Systems and $\mathcal{V}(T_s^2)$**. Indeed, the point is that the classes of maps $\mathcal{V}(T_s^2)$ and $T_s^2$ will form a cofibrantly generated weak factorisation system. Let us start with the most general notion:

**Definition 4.15.** A weak factorisation system on a category $\mathcal{A}$ consists of two classes of maps $\mathcal{L}$ and $\mathcal{R}$ such that $\mathcal{L}^2 = \mathcal{R}$, $\mathcal{L} = \mathcal{V}\mathcal{R}$, and every map $f: A \to B$ factors as $A \xrightarrow{l} C \xrightarrow{r} B$ with $l \in \mathcal{L}$ and $r \in \mathcal{R}$.

Cofibrantly generated weak factorisation systems are those generated from a set of maps by lifting (this is the so-called *small object argument*). We introduce them in Proposition 4.19 below, which requires us to first define *transfinite composition*, *small objects*, and *relative cell complexes*:

**Definition 4.16.** For any ordinal $\lambda$, a $\lambda$-sequence is a cocontinuous functor from $\lambda$ viewed as a category, to $\mathcal{A}$. A transfinite composite of any $\lambda$-sequence $X: \lambda \to \mathcal{A}$ is the component $\rho_0: \lambda(0) \to \text{colim}_{\beta<\lambda} X(\beta)$ of any colimiting cocone $\rho$.

**Definition 4.17.** Let $\mathcal{J}$ denote any class of morphisms in a cocomplete category $\mathcal{A}$, and let $\kappa$ denote any cardinal. An object $A \in \mathcal{A}$ is $\kappa$-small relative to $\mathcal{J}$ iff, for all $\kappa$-filtered [Hovey 1999, Definition 2.1.12] ordinals $\lambda$ and $\lambda$-sequences $X: \lambda \to \mathcal{A}$ such that $X(\beta) \to X(\beta+1)$ is in $\mathcal{J}$ for all $\beta+1 < \lambda$, the canonical map $\text{colim}_{\beta<\lambda} \mathcal{A}(A, X(\beta)) \to \mathcal{A}(A, \text{colim}_{\beta<\lambda} X(\beta))$ is bijective. We say that $A$ is *small relative to* $\mathcal{J}$ iff it is $\kappa$-small relative to $\mathcal{J}$ for some $\kappa$.

**Definition 4.18.** For any class $\mathcal{J}$ of maps in a cocomplete category $\mathcal{A}$, let $\mathcal{J}$-cell denote the class of transfinite composites of pushouts of maps in $\mathcal{J}$, which we call *relative $\mathcal{J}$-cell complexes*.

**PROPOSITION 4.19 ([HOVEY 1999, THEOREM 2.1.14]).** For any set $\mathcal{J}$ of maps in a cocomplete category, if the domains of maps in $\mathcal{J}$ are small relative to $\mathcal{J}$-cell, then $\mathcal{V}(\mathcal{J}^2)$ and $\mathcal{J}^2$ form a weak factorisation system. Any so obtained weak factorisation system is called cofibrantly generated.

This applies to our abstract setting:

**PROPOSITION 4.20.** In any transition category, process types are small relative to $T_s$-cell.

**PROOF.** Smallness of an object $A$ means precisely that its covariant hom-functor preserves certain transfinite compositions, which holds for process types by tininess. □
We thus have by Proposition 4.19:

**COROLLARY 4.21.** In any transition category, $\mathcal{A}(\mathbf{T}_s^{\mathcal{A}})$ and $\mathbf{T}_s^{\mathcal{A}}$ form a weak factorisation system.

Cofibrantly generated weak factorisation systems enjoy an explicit characterisation of $\mathcal{L}$:

**Definition 4.22.** A retract of $f: X \to Y$ is any map $g: A \to B$ for which there exists a retraction $f \to g$ in the arrow category $\mathcal{A} \twoheadrightarrow$, i.e., morphisms $g \xrightarrow{s} f \xrightarrow{r} g$ such that $r \circ s = \text{id}_g$.

**PROPOSITION 4.23 ([HOVEY 1999, COROLLARY 2.1.15]).** In the setting of Proposition 4.19, the left class $\mathcal{A}(\mathcal{J}^{\mathcal{A}})$ consists precisely of retracts of relative $\mathcal{J}$-cell complexes.

We thus have:

**COROLLARY 4.24.** In any transition category, the classes of maps $(\mathcal{A}(\mathbf{T}_s^{\mathcal{A}}), \mathbf{T}_s^{\mathcal{A}})$ form a weak factorisation system whose left class consists precisely of retracts of relative $\mathbf{T}_s$-cell complexes. In particular, $\mathcal{A}(\mathbf{T}_s^{\mathcal{A}})$ contains coproducts of maps in $\mathbf{T}_s$ and of isomorphisms.

**4.3.2 Congruence of Bisimilarity.** Being assured that $\mathcal{A}(\mathbf{T}_s^{\mathcal{A}})$ is large enough for our purposes, let us now return to congruence of bisimilarity.

**Definition 4.25.** A monad $(\mathcal{T}, \eta, \mu)$ on a transition category $\mathcal{A}$ is $\mathbf{T}_s$-familial when it is familial and furthermore for any commuting diagram

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

where $s \in \mathbf{T}_s$ and $C$ and $D$ are generic, we have $s' \in \mathcal{A}(\mathbf{T}_s^{\mathcal{A}})$.

**Remark 4.26.** By Lemma 4.12, when $\mathcal{A}$ is a presheaf category and $P$ and $L$ are representable, this is equivalent to requiring that all maps of the form $s' \cong E(s \upharpoonright x)$ (for some $x \in \mathcal{T}(1)(L)$) are in $\mathcal{A}(\mathbf{T}_s^{\mathcal{A}})$. Indeed, above, take for $x$ the composite $L \xrightarrow{D} \mathcal{T}(R) \xrightarrow{\mathcal{T}(\iota)} \mathcal{T}(1)$: we then have $R \cong E(L, x)$, $A \cong E(P, x \cdot s)$, and $s' \cong E(s \upharpoonright x)$.

**THEOREM 4.27.** For any $\mathbf{T}_s$-familial monad $\mathcal{T}$ on a transition category, if $f: R \to X$ is a functional bisimulation, so is $\mathcal{T}(R) \xrightarrow{\mathcal{T}(f)} \mathcal{T}(X)$.

**PROOF.** We need to construct a lifting for any commuting square as the exterior of

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

We use familiality of $\mathcal{T}$ to factor $p$ as $\mathcal{T}(g) \circ C$ and $r$ as $\mathcal{T}(h) \circ D$ with $C$ and $D$ generic. Genericity of $C$ then yields $s': A \to B$ as shown, which is in $\mathcal{A}(\mathbf{T}_s^{\mathcal{A}})$ by $\mathbf{T}_s$-familiality, so we obtain a lifting $k: B \to R$, and $\mathcal{T}(k) \circ D$ is a lifting for the whole diagram. $\square$
We may now prove that bisimilarity is a congruence, based on the following well-known stability properties of factorisation systems.

**LEMMA 4.28** ([RIEHL 2014, LEMMA 11.1.4]). For any weak factorisation system $(\mathcal{L}, \mathcal{R})$, $\mathcal{L}$ (resp. $\mathcal{R}$) contains all isomorphisms and is closed under composition, retracts, coproducts (resp. products) of arrows, and pushouts (resp. pullbacks). $\mathcal{L}$ is furthermore closed under transfinite composition.

**COROLLARY 4.29.** For any bisimulation $R \to X \times Y$ between compositional algebras for a $T_s$-familial monad $\mathcal{T}$, the induced map $\mathcal{T}(R) \to X \times Y$ is a bisimulation.

**PROOF.** By compositionality, Theorem 4.27, and Lemma 4.28. □

**COROLLARY 4.30.** Between any two compositional algebras for a $T_s$-familial monad $\mathcal{T}$, bisimilarity is a congruence.

In most examples, the considered algebra is the free one $\mathcal{T}(0)$. This is thus covered by:

**COROLLARY 4.31.** Consider any $T_s$-familial monad $\mathcal{T}$ on some transition category $\mathcal{A}$ such that $\mu_1: \mathcal{T}^2(1) \to \mathcal{T}(1)$ is a functional bisimulation. Then for all $X$, if $f: R \to \mathcal{T}(X)$ is a functional bisimulation, so is $\mathcal{T}(R) \xrightarrow{\mathcal{T}(f)} \mathcal{T}^2(X) \xrightarrow{\mu_X} \mathcal{T}(X)$, and hence bisimilarity in $\mathcal{T}(X)$ is a congruence.

**PROOF.** Because $\mathcal{T}$ is familial, all naturality squares for $\mu$ are pullbacks, so $\mu_X$ is a functional bisimulation by Lemma 4.28. We conclude by Corollary 4.30. □

**Example 4.32.** Corollary 4.31 applies to $\mathcal{T}_{CL}(0)$, $\mathcal{T}_{CCS}(0)$, and $\mathcal{T}_{\pi}^{+}(0)$ (see §6.3 below). Indeed, $\mathcal{T}_{CL}$ and $\mathcal{T}_{CCS}$ are both $T_s$-familial (for different $T_s$), because any $s'$ obtained as in Definition 4.25 is a coproduct (in the arrow category) of isomorphisms and maps in $T_s$, hence in $\mathcal{T}(\mathcal{T}_s)$ by Lemma 4.28. Similarly, $T_s$-familiality of $\mathcal{T}_{\pi}^{+}$ is Proposition 6.16 below.

However, Corollary 4.31 does not apply to either of the other two variants of the $\pi$-calculus that we consider in §6. Indeed, for $\mathcal{T}_{\pi}(0)$ (§6.1), $\mu_1$ is not a functional bisimulation (this is the standard fact that bisimilarity is not a congruence), and in §6.2 the $\pi$-calculus is considered as an algebra for a certain submonad $\mathcal{T}_{\pi}^{-}$ of $\mathcal{T}_{\pi}$, not of the relevant form $\mathcal{T}_{\pi}^{-}(X)$, so we need to resort to the theorem rather than the corollary.

# 5 BISIMULATION UP TO CONTEXT

In this section, we consider an alternative notion of bisimulation in transition categories, pre-bisimulation, which we relate to bisimulation by showing that under a mild additional hypothesis any pre-bisimulation embeds into some bisimulation. We then define a notion of pre-bisimulation up to context, which in examples corresponds to bisimulation up to context. Finally, we prove that pre-bisimulation up to context is sound, in the sense that any pre-bisimulation up to context embeds into some pre-bisimulation (and hence into some bisimulation).

## 5.1 Progression and Pre-Bisimulation

In Definition 3.12, we defined functional bisimulation through a lifting property, which is flexible enough to, e.g., exclude some transitions from the considered labelled transition systems $X$ and $Y$. We will now define a slightly different notion which is in fact closer to the ordinary definition of bisimulation. A standard way to define bisimulation and bisimulation up to context is through the notion of progression [Sangiorgi and Rutten 2011, Definition 6.2.1]: a relation $R$ progresses to $R'$ when for all $(x, y) \in R$ and transitions $x \xrightarrow{\alpha} x'$, there exists $y \xrightarrow{\alpha} y'$ such that $(x', y') \in R'$ (and symmetrically). So in particular, $R$ is a bisimulation iff it progresses to itself. This may be defined in the abstract setting, as follows.
**Definition 5.1.** Consider maps $i: R \to X \times Y$ and $j: R' \to X \times Y$ in any transition category. We say that $R$ progresses to $R'$, notation $R \rightsquigarrow R'$, iff for all transition types $P \xrightarrow{s} L \xleftarrow{t} Q$, processes $c: P \to R$, and transitions $r: L \to X$ making the solid part below left commute, there exist $u$ and $d$ as shown making the whole commute, and symmetrically for $Y$.

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

A relation $R$ is a *pre-bisimulation* iff $R \unlhd R'$.

Let us mention an equivalent presentation of progression, which uses lifting analogously to bisimulation, but in the category of cospans:

**Definition 5.2.** Let $\mathcal{A}^\vee$ have cospans in $\mathcal{A}$ as objects, and as morphisms $(a, b) \to (c, d)$ all commuting diagrams as on the right of (7).

**PROPOSITION 5.3.** Given $R \to X \times Y$ and $R' \to X \times Y$, $R$ progresses to $R'$ iff every commuting diagram of the following form admits a dashed lifting as shown, and symmetrically for $Y$.

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

## 5.2 From Pre-Bisimulation to Bisimulation

Let us now relate pre-bisimulation to bisimulation. Intuitively, the value of $R$ over transitions is irrelevant in the definition of pre-bisimulation. But, thinking of $R$ as a relation over processes, one would expect that by completing it with all transitions that exist in $X \times Y$ between pairs of related processes we would get a bisimulation. This completion operation may be performed generically by a weak factorisation system, up to an additional stratification hypothesis. Let us first define the weak factorisation system in question, then introduce the relevant hypothesis, and finally relate pre-bisimulation to bisimulation (Proposition 5.8).

**PROPOSITION 5.4.** In any transition category $\mathcal{A}$, the set $\mathcal{J} = [[s, t]: P + Q \to L \mid (s, t) \in \mathbf{T}]$ generates a weak factorisation system, say $(\mathcal{L}, \mathcal{R})$.

**PROOF.** By Proposition 4.19 and tininess of process types. $\square$

**Definition 5.5.** A transition category $\mathcal{A}$ is two-level iff $\mathcal{J} \subseteq \mathbf{P}^2$, viewing each $P' \in \mathbf{P}$ as the unique map $0 \to P'$.
Explicitly, $\mathcal{A}$ is two-level when any map $f: P' \to L$ with $P' \in \mathbf{P}$ lifts through any $[s, t]$ with codomain $L$, i.e., there exists $k$ making the following triangle commute.

$$ P' \underset{f}{\overset{k}{\dashrightarrow}} L \xrightarrow{P+Q} [s,t] \qquad (9) $$

**Remark 5.6.** All our example transition categories are two-level. Indeed, the involved base categories feature a notion of dimension, given by the only non-trivial functors to 2, the two-element ordinal viewed as a category. E.g., the functor $\mathbb{C}_{\mathrm{CCS}} \to 2$ maps $\star$ to 0 and all labels to 1. Dimension extends to presheaves by decreeing that a presheaf has dimension 0 when it is empty over all objects of dimension 1, and dimension 1 otherwise. The point is that in examples, all morphisms $[s, t]: P+Q \to L$ are in fact bijective over objects of dimension 0, which directly ensures two-levelness.

**LEMMA 5.7.** In any two-level transition category, we have $\mathcal{L} \subseteq \mathbf{P}^2$.

**PROOF.** By Proposition 4.23, it suffices to show that $\mathbf{P}^2$ contains $\mathcal{J}$ and is stable under pushout, transfinite composition, and retracts. First of all, $\mathcal{J} \subseteq \mathbf{P}^2$ holds by hypothesis. Stability under retracts is direct, and stability under pushout and transfinite composition follows from tininess of process types (by transfinite induction in the latter case). $\square$

**PROPOSITION 5.8.** For any pre-bisimulation $i: R \to X \times Y$ in a two-level transition category, the factor $\bar{i}$ of the $(\mathcal{L}, \mathcal{R})$-factorisation $R \xrightarrow{l} \bar{R} \xrightarrow{\bar{i}} X \times Y$ of $i$ is a bisimulation.

Intuitively, $\bar{R}$ coincides with $R$ on states, but adds in all the transitions between pairs of related vertices that exist in $X \times Y$.

**PROOF.** Consider any commuting square as below left. By Lemma 5.7, we find a lifting, say $p': P \to R$ of $p$ through $l: R \to \bar{R}$. Because $R$ is a pre-bisimulation, we get $r'$ and $q'$ making the diagram below center commute. We may thus factor the original square as below right, and hence get the desired (dashed) lifting by $\bar{i} \in \mathcal{R}$.

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

## 5.3 Pre-bisimulation up to Context

After defining pre-bisimulations in the previous section, and showing that they embed into bisimulations by factorisation, we now proceed in this section to defining pre-bisimulations up to context,
and showing that they embed into pre-bisimulations, hence into bisimulations, under suitable hypotheses.

Let us consider any familial monad $\mathcal{T}$ on a transition category $\mathcal{A}$, and $\mathcal{T}$-algebras $a: \mathcal{T}(X) \to X$ and $b: \mathcal{T}(Y) \to Y$.

**Definition 5.9.** A map $i: R \to X \times Y$ is a pre-bisimulation up to $\mathcal{T}$ iff $R \rightsquigarrow \mathcal{T}(R)$, where $\mathcal{T}(R)$ is equipped with the map $\mathcal{T}(R) \xrightarrow{\mathcal{T}(i)} \mathcal{T}(X \times Y) \xrightarrow{\langle \mathcal{T}(\pi), \mathcal{T}(\pi') \rangle} \mathcal{T}(X) \times \mathcal{T}(Y) \xrightarrow{a \times b} X \times Y$.

Before proving soundness of pre-bisimulation up to $\mathcal{T}$, we need to refine $T_s$-familiality. Indeed, in order to find the desired lifting in the proof of Theorem 4.27, we needed to assume that the image by $E$ of any $s \in T_s$ was in $\mathcal{A}^2(T_s^2)$. For pre-bisimulations, we will proceed analogously, but in the cospan category.

**PROPOSITION 5.10.** The cospan category $\mathcal{A}^\vee$ is again a transition category with transition types, say $T^\vee$, given by

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

**PROPOSITION 5.11.** Any familial monad $\mathcal{T}$ on $\mathcal{A}$ lifts to a familial monad $\mathcal{T}^\vee$ on the cospan category $\mathcal{A}^\vee$, whose generics are given by componentwise generics.

This leads us to define:

**Definition 5.12.** A familial monad $\mathcal{T}$ on a transition category $\mathcal{A}$ is $T_s^\vee$-familial iff $\mathcal{T}^\vee$ is (as a monad on $\mathcal{A}^\vee$).

**THEOREM 5.13.** For any $T_s^\vee$-familial monad $\mathcal{T}$, compositional $\mathcal{T}$-algebras $a: \mathcal{T}(X) \to X$ and $b: \mathcal{T}(Y) \to Y$, and pre-bisimulation $i: R \to X \times Y$ up to $\mathcal{T}$, the following map is a pre-bisimulation:

$$ \mathcal{T}(R) \xrightarrow{\mathcal{T}(i)} \mathcal{T}(X \times Y) \xrightarrow{\langle \mathcal{T}(\pi), \mathcal{T}(\pi') \rangle} \mathcal{T}(X) \times \mathcal{T}(Y) \xrightarrow{a \times b} X \times Y. \quad (10) $$

**PROOF.** Let $i'$ denote the map (10), and define $a', b', i'_X$, and $i'_Y$ by composition as in

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

The cube on the left of Figure 1 commutes (notably by the monad algebra laws), which means that it forms a square as on the right in $\mathcal{A}^\vee$, whose top arrow is by hypothesis the image by $\mathcal{T}^\vee$ of a map in $(T_s^\vee)^2$.

**Notation 5.14.** Open arrow heads denote arrows of the form $\mathcal{T}^\vee(-)$, and commutation of a diagram of such arrows means that the underlying arrows, without $\mathcal{T}$, agree.

By symmetry, it suffices to prove that the bottom map $(i'_X, \pi, i'_X)$ is in $(T_s^\vee)^2$. For this, consider any commuting square as the perimeter of
<figure><img src="image_19.png" /><figcaption>Fig. 1. Cube for the proof of Theorem 5.13</figcaption></figure>

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

Because $(id_{\mathcal{T}(R)}, \langle a', b' \rangle, \mu_R)$ has identity first component and $(id_p, !_p)$ has identity top leg, $u$ factors through the former, say as $u'$. But by compositionality of $X$, we have $(a, a, a) \in (\mathcal{T}_S^\vee)^2$, so by lifting we find a $v'$ as shown making both parts of the diagram commute. Now, by familiality of $\mathcal{T}^\vee$, we find generic-free factorisations of $u'$ and $v'$, say with generics $C$ and $E$. Next, by genericity of $C$ we find a lifting $\mathcal{T}^\vee(h)$ as shown, with $h \in \mathcal{A}^2((\mathcal{T}_S^\vee)^2)$ by $\mathcal{T}_S^\vee$-familiality. We thus find a dashed lifting as shown, which at last yields a lifting for the whole diagram. $\square$

**COROLLARY 5.15.** For any $\mathcal{T}_S^\vee$-familial monad $\mathcal{T}$ and compositional $\mathcal{T}$-algebras $a: \mathcal{T}(X) \to X$ and $b: \mathcal{T}(Y) \to Y$, any pre-bisimulation up to $\mathcal{T}$ embeds into some bisimulation.

**PROOF.** By Theorem 5.13 and Proposition 5.8. $\square$

**Example 5.16.** In CCS, the cospans morphisms involved in $\mathcal{T}_S^\vee$-familiality are coproducts (in $(\mathcal{A}^\vee)\twoheadrightarrow$) of maps in $\mathcal{T}_S^\vee$ and isomorphisms, so the corollary applies and bisimulation up to context is sound.

# 6 THREE SHADES OF $\pi$-CALCULUS

Let us now consider a more significant example than combinatory logic and CCS: the $\pi$-calculus. Unlike in CCS, we have to mod out by $\alpha$-equivalence, because channel names may be input, hence substituted deep in process terms, which may force renaming. We essentially follow the presentation of Sangiorgi and Walker [2001, §1.3], using a simplified variant for expository purposes.

In §6.1, we make a first attempt at covering the $\pi$-calculus using our approach. We manage to design a familial monad, $\mathcal{T}_\pi$, over a certain presheaf category $\hat{\mathcal{B}}$, which faithfully encodes the desired labelled transition system. However, as bisimilarity is known not to be a congruence in $\pi$,
something is bound to fail. And indeed, we show that the initial $\mathcal{T}_\pi$-algebra $\mathcal{T}_\pi(0)$ of processes is not compositional. We rectify this in a standard way in §6.2, by defining a familial submonad, $\mathcal{T}_\pi^-$, such that the $\mathcal{T}_\pi$-algebra $\mathcal{T}_\pi(0)$ is compositional, thus recovering the known facts that (1) standard bisimilarity is a congruence for all operators but input, and (2) bisimulation up to non-input context is sound. We finally consider in §6.3 a different, though still standard, way of remedying the non-congruence problem. This consists in restricting attention to relations, called *wide open* [Fiore and Staton 2006; Sangiorgi and Walker 2001; Staton 2008], that are stable under channel renaming. We do this by working over a different base category $\mathcal{F}$, and adapting the definition of $\mathcal{T}_\pi$, yielding a new familial monad $\mathcal{T}_\pi^+$. We recover the known results that wide-open bisimilarity is a congruence and that wide-open bisimulation up to context is sound.

## 6.1 Basic Approach

In this section, we illustrate our approach by examining the failure of congruence for standard bisimilarity in $\pi$. We analyse the problem, which allows us to consider two different solutions in the next two sections.

Naively adapting what we did with CCS to the $\pi$-calculus, we could try considering a similar base category with CCS labels replaced with $\pi$-calculus labels, $\tau, o_{a,b}, l_{a,b}$, etc. However, this setting cannot accomodate the input axiom: $a(c).P \stackrel{l_{a,b}}{\rightleftharpoons} P[c \mapsto b]$. Indeed, this requires a definition of renaming, for which a standard, inductive definition stumbles upon the base case: it does not make any sense to replace $c$ with $b$ in $\langle x \rangle$. We thus consider a different base category.

**Definition 6.1.** Recalling $\mathcal{N}$ from Example 3.1, let $\mathcal{B}$ denote the subcategory of $\mathbf{Set}^{\mathcal{N}}$ with finite subsets of $\mathcal{N}$ as objects and bijections as morphisms, augmented with

* objects $\tau_\gamma, o_{\gamma,a,b}, o_{\gamma,a,c}^v, l_{\gamma,a,b}$, and $l_{\gamma,a,c}^v$ for all $\gamma \in \mathcal{P}_f(\mathcal{N})$, $a,b \in \gamma$, and $c \notin \gamma$,

* morphisms, arranged by transition types (denoting by $\gamma$, $c$ the (disjoint) union $\gamma' \uplus \{c\}$ – here but not, e.g., in $o_{\gamma,a,b}$: input and output labels have three arguments, a $\gamma$ and two names; we rely on context to disambiguate):

$$ \gamma \stackrel{s}{\rightarrow} \tau_\gamma, \stackrel{t}{\leftarrow} \gamma \quad \gamma \stackrel{s}{\rightarrow} o_{\gamma,a,b}, \stackrel{t}{\leftarrow} \gamma' \quad \gamma \stackrel{s}{\rightarrow} l_{\gamma,a,b}, \stackrel{t}{\leftarrow} \gamma' \quad \gamma \stackrel{s}{\rightarrow} o_{\gamma,a,c}^v, \stackrel{t}{\leftarrow} \gamma', c \quad \gamma \stackrel{s}{\rightarrow} l_{\gamma,a,c}^v, \stackrel{t}{\leftarrow} \gamma', c, $$

* plus, for all transition types $\gamma \stackrel{s}{\rightarrow} \alpha \stackrel{t}{\leftarrow} \gamma, \delta$ and bijections $h: \gamma \rightarrow \gamma'$ and $k: \delta \rightarrow \delta'$ such that $\gamma' \cap \delta' = \emptyset$, a morphism $(h,k): (h,k) \cdot \alpha \rightarrow \alpha$, where

$$ (h,k) \cdot \tau_{\gamma} = \tau_{\gamma'} \quad \text{and} \quad (h,k) \cdot \alpha_{\gamma,a,b} = \alpha_{\gamma',h(a),(h+k)(b)} \quad \text{for } \alpha \in \{o, \iota, o^v, l^v\}, $$

satisfying the obvious equations:

$$ \begin{array}{ccc} \begin{array}{c} \gamma \\ \uparrow \\ h \end{array} & \stackrel{s}{\rightarrow} & \alpha \leftarrow \begin{array}{c} t \\ \uparrow \\ (h,k) \end{array} \quad \gamma', \delta \\ \begin{array}{c} \gamma' \\ \uparrow \\ s \end{array} & \stackrel{X(f)}{\rightarrow} & (h,k) \cdot \alpha \leftarrow \begin{array}{c} t \\ \uparrow \\ h+k \end{array} \quad \gamma', \delta'. \end{array} \qquad (11) $$

**Notation 6.2.** For general presheaves $X$, we denote the action $X(c') \stackrel{X(f)}{\rightarrow} X(c)$ of any $f: c \rightarrow c'$ in the base by $x \mapsto x \cdot f$. However, for $f: \gamma \rightarrow \gamma'$ in sets, although $f$ acts contravariantly as a map $\gamma' \rightarrow \gamma$ in $\mathcal{B}$, it acts covariantly as a set-map, so we often write $f \cdot x$ instead. We use the same convention for arbitrary (potentially non-bijective) maps below.

**PROPOSITION 6.3.** The category $\widehat{\mathcal{B}}$ forms a transition category, with transition types $T^\pi$ as above.

Let us now define our monad on $\widehat{\mathcal{B}}$, in three stages. We first define $\mathcal{T}_\pi(X)$ on process types. We then observe that not only bijections act on $\mathcal{T}_\pi(X)$, but also arbitrary maps. The presheaf $\mathcal{T}_\pi(X)$
that we defined on process types and bijections thus extends to a functor on the category of finite subsets of $\mathcal{N}$ and all maps. We finally use this to define $\mathcal{T}_\pi(X)$ on transitions.

For any $X \in \tilde{\mathbb{B}}$, let $\mathcal{T}_\pi(X)(\gamma)$ denote the set of all $\alpha$-equivalence classes of $\pi$-calculus terms of the form $\gamma \vdash P$, as defined in the top part of Figure 2. Let us then define renaming, the action

$$ \frac{x \in X(\gamma) \qquad f \in \mathbf{Set}(\gamma, \gamma')}{\gamma' \vdash_X (|x|)(f)} \qquad \frac{\gamma \vdash_X P \qquad \gamma \vdash_X Q}{\gamma \vdash_X P|Q} \qquad \overline{\gamma \vdash_X 0} \qquad \frac{\gamma, a \vdash_X P}{\gamma \vdash_X va.P} $$

$$ \begin{gathered} e \in X(\alpha) \qquad \gamma \xrightarrow{s} \alpha \xleftarrow{t} \gamma, \delta \qquad h: \gamma \Rightarrow \gamma' \qquad k: \delta \Rightarrow \delta' \qquad \gamma' \cap \delta' = \emptyset \\ \langle\langle e \rangle\rangle(h, k) : \gamma' \vdash_X (|e \cdot s|)(h) \xrightarrow{(h,k) \cdot \alpha} \gamma', \delta' \vdash_X (|e \cdot t|)(h+k) \end{gathered} $$

$$ \frac{\gamma, b \vdash_X P \qquad a, c \in \gamma}{in_{b,P}^{a,c} : \gamma \vdash_X a(b).P \xrightarrow{\iota_{\gamma,a,c}} \gamma \vdash_X [b \mapsto c] \cdot P} \qquad \frac{\gamma \vdash_X P \qquad a, b \in \gamma}{out_{\gamma \vdash_X P}^{a,b} : \gamma \vdash_X \bar{a}\langle b \rangle.P \xrightarrow{\iota_{\gamma,a,b}} \gamma \vdash_X P} $$

$$ \frac{R : \gamma \vdash_X P \xrightarrow{\iota_{\gamma,a,b}} \gamma \vdash_X P' \qquad S : \gamma \vdash_X Q \xrightarrow{\iota_{\gamma,a,b}} \gamma \vdash_X Q'}{R \triangleright S : \gamma \vdash_X (P|Q) \xrightarrow{\tau_\gamma} \gamma \vdash_X (P'|Q')} + \text{symmetric rule } \triangleleft $$

$$ \frac{\gamma, b \vdash_X P \qquad a \in \gamma}{in_P^{a,vb} : \gamma \vdash_X a(b).P \xrightarrow{\iota_{\gamma,a,b}^v} \gamma, b \vdash_X P} \qquad \frac{R : \gamma, b \vdash_X P \xrightarrow{\iota_{(\gamma,b),a,b}} \gamma, b \vdash_X Q \qquad a \neq b}{\nabla b.R : \gamma \vdash_X vb.P \xrightarrow{\iota_{\gamma,a,b}^v} \gamma, b \vdash_X Q} $$

$$ \frac{R : \gamma \vdash_X P \xrightarrow{\iota_{\gamma,a,b}^v} \gamma, b \vdash_X P' \qquad S : \gamma \vdash_X Q \xrightarrow{\iota_{\gamma,a,b}^v} \gamma, b \vdash_X Q'}{R \triangleright^{vb} S : \gamma \vdash_X P|Q \xrightarrow{\tau_\gamma} \gamma \vdash_X vb.(P'|Q')} + \text{symmetric rule } \triangleleft^{vb} $$

$$ \frac{R : \gamma, b \vdash_X P \xrightarrow{\alpha} \gamma, b, \delta \vdash_X Q \qquad b \notin fv(\alpha)}{vb.R : \gamma \vdash_X vb.P \xrightarrow{vb.\alpha} \gamma, \delta \vdash_X vb.Q} $$ $$ \frac{L : \gamma \vdash_X P \xrightarrow{\alpha} \gamma, \delta \vdash_X P' \qquad \gamma \vdash_X Q}{L|Q : \gamma \vdash_X P|Q \xrightarrow{\alpha} \gamma, \delta \vdash_X P'|Q} + \text{symmetric rule } Q|L $$

<caption>Fig. 2. Syntax and labelled transition system for $\pi$</caption>

$\mathcal{T}_\pi(\gamma') \to \mathcal{T}_\pi(\gamma'')$ of any set-map $f: \gamma \to \gamma'$, denoted by $P \mapsto f \cdot P$, by straightforward induction; notably, for the base case, if $g: \gamma'' \to \gamma$, we set $f \cdot (|x|)(g) = (|x|)(f \circ g)$ (see full definition in [Hirschowitz 2018]).
Finally, let us define $\mathcal{T}_\pi(X)$ on transitions. For all $\gamma \stackrel{s}{\to} \alpha \stackrel{t}{\leftarrow} \gamma'$, $\mathcal{T}_\pi(X)(\alpha)$ denotes the set of $\alpha$-equivalence classes of transitions $P \xrightarrow{\alpha} Q$ with constants in $X$, for $P \in \mathcal{T}_\pi(X)(\gamma')$ and $Q \in \mathcal{T}_\pi(X)(\gamma')$, as defined in the bottom part of Figure 2, where

* the only binding operations are $in_{b,P}^{a,c}$, $vb.R$, and $R \triangleright^v S$ - binding $b$;

* a peculiarity is that in $\langle x \rangle(f)$, the status of names in $\gamma$ is analogous to that of 'binding' names in contexts, e.g., as $b$ in $a(b)$.□; in particular they are neither free, nor bound, nor $\alpha$-convertible;

* $[b \mapsto c]$ stands for the map $(\gamma', b) \to \gamma$ mapping $b$ to $c$ and the rest of $\gamma$ to itself;

* weakening (i.e., renaming along an injective map) is used implicitly in $L|Q$ and $Q|L$;

* for $vb.R$, we define

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
fv(o_{\gamma,a,b}) = fv(\iota_{\gamma,a,b}) = fv(o_{\gamma,a,b}^{\nu}) = fv(\iota_{\gamma,a,b}^{\nu}) = \{a,b\} & \text{and} & fv(\tau_{\gamma}) = \emptyset \\
\text{and} & vc.\tau_{\gamma,c} = \tau_{\gamma} & vc.\alpha_{(\gamma,c),a,b} = \alpha_{\gamma,a,b}, \text{ for } \alpha \in \{o, \iota, o^{\nu}, \iota^{\nu}\},
\end{array}
$$

where $vc.\alpha$ is defined iff $c \notin fv(\alpha)$.

This almost defines an assignment $ob(\mathbb{B}) \to ob(\mathbb{B})$: it remains to define the action of maps in $\mathbb{B}$ on $\mathcal{T}_\pi(X)$ and show that it is functorial. For maps of the form $\gamma \to \gamma'$, we merely use renaming; for $s$ and $t$, we use the sources and targets specified in transitions. For $(h, k): (h, k) \to \alpha$, we define $(h, k) \cdot R$ by induction on $R$, e.g.,

$$ 
\begin{align}
(h, k) \cdot (\langle\!\langle e \rangle\!\rangle(h', k')) &= \langle\!\langle e \rangle\!\rangle(h \circ h', k \circ k') \nonumber \\
(h, id_{\emptyset}) \cdot in_{b,P}^{a,c} &= in_{a,\gamma'}.((h+(b \mapsto a, \gamma')) \cdot P) \tag{12} \\
(h, id_{\emptyset}) \cdot (R \triangleright^v S) &= ((h, (b \mapsto a, \gamma')) \cdot R) \triangleright^{v a, \gamma'} ((h, (b \mapsto a, \gamma')) \cdot S), \nonumber
\end{align}
$$

where $(b \mapsto c)$ is the unique map $\{b\} \to \{c\}$, and $a_\gamma$ denotes some globally chosen name not in $\gamma$.

Finally, we prove that this is functorial, again by induction. This defines an assignment $ob(\mathbb{B}) \to ob(\mathbb{B})$, which easily extends to a functor $\mathcal{T}_\pi: \mathbb{B} \to \mathbb{B}$: the action of a morphism $F: X \to Y$ in $\mathbb{B}$ is obtained by renaming $x$, resp. $e$, according to $F$ in $\langle x \rangle(f)$, resp. $\langle\!\langle e \rangle\!\rangle(h, k)$.

**Remark 6.4 (Replication).** The $\pi$-calculus standardly features additional operations like guarded sum and replication. Guarded sum may be incorporated readily, but, depending on presentation,

replication may be less easy. E.g., the compact transition rule $\frac{P!P \xrightarrow{\alpha} Q}{!P \xrightarrow{\alpha} Q}$ does not obviously yield

a familial monad. However, the rules of Sangiorgi and Walker [2001, §1.3], a variant of which is reproduced below (without the $\gamma$'s for readability), do yield a familial monad directly.

$$ 
\frac{
  \begin{array}{r@{\quad}l}
  P & \xrightarrow{\alpha} P' \\
  \multicolumn{2}{c}{\big) \quad P' \overline{\hspace{2.5cm}} \quad P} \\
  \multicolumn{3}{c}{\alpha \quad P' \overline{\hspace{2.5cm}} \quad P'}
  \end{array}
}{
  \begin{array}{r@{\quad}l}
  P & \xrightarrow{\alpha} P' \vert!P \\
  \multicolumn{2}{c}{\big) \quad P' \overline{\hspace{2.5cm}} \quad P} \\
  \multicolumn{3}{c}{\alpha \quad P' \overline{\hspace{2.5cm}} \quad P' \vert!P}
  \end{array}
}
$$

**PROPOSITION 6.5.** $\mathcal{T}_\pi$ forms a $\mathbf{T}_s^\pi$-familial monad.

**PROOF SKETCH.** (More detail in [Hirschowitz 2018].) To see that $\mathcal{T}_\pi$ is a familial functor, by Lemma 4.12, it is enough to exhibit a functor $E: el(\mathcal{T}_\pi(1)) \to \mathbb{B}$ such that

$$ \mathcal{T}_\pi(X)(c) \cong \sum_{R \in \mathcal{T}_\pi(1)(c)} [E(c, R), X], $$
naturally in X and $c \in \mathbb{B}$. Elements of $\mathcal{T}_\pi(1)(\gamma)$ are processes of type $\gamma'$, over exactly one constant process, say $\tau_{\gamma'}$ of each type $\gamma'$. Elements of $\mathcal{T}_\pi(1)(\alpha)$ are transitions with exactly one constant transition of each type $\gamma \xrightarrow{s} \beta \leftarrow^t \gamma'$, say $\tau_\beta$, with source $\tau_\beta \cdot s = \tau_\gamma$ and target $\tau_\beta \cdot t = \tau_{\gamma'}$.

On objects, we construct $E$ by induction on the depth of the considered proof (globally for all objects $c \in \mathbb{B}$), as in Figure 3, relying on some global choice of binary coproducts and fresh name $a_\gamma$, for all $\gamma \in \mathcal{P}_f(\mathcal{N})$, as in the definition of renaming. The choice of $a_\gamma$ is in fact completely irrelevant, because for all maps $h : \gamma \to \gamma'$, $k : \delta \to \delta'$ in sets, processes $\gamma \vdash P$, and transitions $R : (\gamma \vdash P) \stackrel{\alpha}{\to} (\gamma, \delta \vdash Q)$, we have by induction:

$$E(h \cdot P) = E(P) \quad \text{and} \quad E((h, k) \cdot R) = E(R) \quad (\text{yes, equality!}). \quad (13)$$

Typically, if $f : \gamma \to \gamma'$, we have by definition $E(f \cdot (\tau_\gamma)(id)) = E((\tau_\gamma)(f)) = y_\gamma$: $f$ is not taken into account.

<table><caption>Fig. 3. Definition of $E$ on objects</caption><thead><tr><th colspan="2">Processes</th><th colspan="2">Transitions</th></tr></thead><tbody><tr><td>$E((\tau_\gamma)(f)) =$</td><td>$y_\gamma$</td><td>$E(\langle\langle \tau_\alpha \rangle\rangle(h, k)) =$</td><td>$\overline{y_\alpha}$</td></tr><tr><td>$E(P|Q) =$</td><td>$E(P) + E(Q)$</td><td>$E(in_{a_\gamma, P}^{a,c}) =$</td><td>$E(P) \quad E(R \triangleright^{va_\gamma} S) =$</td></tr><tr><td>$E(0) =$</td><td>$0$</td><td>$E(\overline{oui_P^{a,c}}) =$</td><td>$E(\overline{va_\gamma, R}) =$</td></tr><tr><td>$E(\overline{va_\gamma, P}) =$</td><td>$E(P)$</td><td>$E(R \triangleright S) =$</td><td>$E(R) + E(S) \quad E(\overline{L} | Q) =$</td></tr><tr><td>$E(\overline{a \langle\rangle P}) =$</td><td>$E(P)$</td><td>$E(in_P^{a,\nu b}) =$</td><td>$E(P|R) =$</td></tr><tr><td>$E(a_\gamma, P) =$</td><td>$E(P)$</td><td></td><td></td></tr></tbody></table>

Let us now define $E$ on morphisms:

* For any $f : \gamma \to \gamma'$ in sets and $P \in \mathcal{T}_\pi(1)(\gamma)$, we have $f \uparrow P : (\gamma', f \cdot P) \to (\gamma, P)$ in $el(\mathcal{T}_\pi(1))$ and define $E(f \uparrow P) : E(\gamma', f \cdot P) \to E(\gamma, P)$ to be just the identity (which makes sense by (13)).

* Similarly, for all $(h, k) : (h, k) \cdot \alpha \to \alpha$, let $E((h, k) \uparrow R) = id_{E(R)}$.

* Finally, for all $\gamma \xrightarrow{s} \alpha \leftarrow^t \gamma$, $\delta$ and $R \in \mathcal{T}_\pi(1)(\alpha)$, we define $E(s \uparrow R)$ and $E(t \uparrow R)$ straightforwardly by induction, thanks to (13). An example key case is $E(R \triangleright^{va_\gamma} S)$, for which we define $E(s \uparrow R \triangleright^{va_\gamma} S)$ and $E(t \uparrow R \triangleright^{va_\gamma} S)$ to be

$$E(P) + E(Q) \stackrel{E(s \uparrow R) + E(s \uparrow S)}{\longrightarrow} E(R) + E(S) \stackrel{E(t \uparrow R) + E(t \uparrow S)}{\longrightarrow} E(P') + E(Q').$$

Clearly, by induction, each $E(s \uparrow R)$ lies in $\mathbb{B}(\langle\langle T_s^\pi \rangle\rangle^\mathbb{B})$, so that $\mathcal{T}_\pi$ is $T_s^\pi$-familial by Remark 4.26. The unit is given by variables, and multiplication is essentially substitution, which is straightforwardly defined by induction. Key cases are:

$$\mu_{X,\alpha}(\langle\langle r \rangle\rangle(h, k)) = (h, k) \cdot r \qquad \mu_{X,\tau_\gamma}(R \triangleright^{\nu b} S) = \mu_{X,\alpha,\nu}(R) \triangleright^{\nu b} \mu_{X,\gamma,\alpha,b}(S).$$

Unit and multiplication are natural and satisfy the monad laws. Finally, cartesianness of $\eta$ and $\mu$ may be checked pointwise (i.e., relative to representable presheaves), and follows by induction. $\square$

As announced and expected, because bisimilarity is not a congruence in $\pi$, something must fail:

**PROPOSITION 6.6.** *The free $\mathcal{T}_\pi$-algebra, $\mathcal{T}_\pi(0)$, with action given by $\mu_0$, is not compositional.*

**PROOF.** The problem comes from renaming, as embedded in constant terms $(\overline{x})(f)$. Indeed, consider $p = (\overline{a}\langle\rangle a).0|b(c).0$ (for $a \neq b$), a process involved in a standard counterexample to bisimilarity being a congruence [Sangiorgi and Walker 2001]. Letting $f : \{a, b\} \to \{a\}$ denote the unique such
map, $(|p|)(f) \in (\mathcal{T}_\pi)^2(0)\{a\}$ is mapped by $\mu_{0,|a|}$ to $p' = (\bar{a}\langle a\rangle.0|a(c).0)$. The latter process has a $\tau$-transition to $0|0$, which the former cannot match. $\square$

**Remark 6.7.** The root of the problem here is $in_{b,p}^{a,c}$, which forces the syntax for processes to feature renaming, even if only at the level of constants $(\lvert x \rvert)(f)$. To emphasise that this does make renaming a proper syntactic operation, it may help to realise that $\mathcal{T}_\pi$ could be presented using an explicit renaming operation $P[f]$ together with equations describing how it propagates down towards the leaves, e.g., $(P|Q)[f] = P[f]|Q[f]$, to finally integrate with constants: $(\lvert x \rvert)(g)[f] = (\lvert x \rvert)(f \circ g)$.

## 6.2 Non-Input Congruence

A first, standard way around non-congruence of bisimilarity is to elude the problematic case, and prove that bisimilarity is a congruence for all operators but input. Our framework can cover this by viewing $\pi$-calculus as a non-free algebra for a smaller monad $\mathcal{T}_\pi^-$. □

**Definition 6.8.** Let $\mathcal{T}_\pi^-$ denote the sub-functor of $\mathcal{T}_\pi$ obtained by removing $a(b)P$ from the syntax of Figure 2, replacing the rule for $(\lvert x \rvert)(f)$ by

$$ \frac{x \in X(\gamma) \quad f \in \mathbf{Inj}(\gamma, \gamma')}{\gamma' \vdash_X (\lvert x \rvert)(f)}, $$

where $\mathbf{Inj}(\gamma, \gamma')$ denotes the set of injective maps $\gamma \hookrightarrow \gamma'$, and removing $in_{b,p}^{a,c}$ and $in_P^{a,vb}$ from the labelled transition system of Figure 2.

**Remark 6.9.** We need to retain injective renaming for $L|Q$ and $P|R$ to make sense.

We clearly obtain:

**PROPOSITION 6.10.** $\mathcal{T}_\pi^-$ is a $\mathbf{T}_s^\pi$-familial monad.

But this time, instead of considering $\mathcal{T}_\pi^-(0)$, which does not even satisfy the input rule, we observe that $\mathcal{T}_\pi^-(0)$ forms a $\mathcal{T}_\pi^-$-algebra (because it satisfies all $\pi$-calculus rules, hence in particular those of $\mathcal{T}_\pi^-$). We thus obtain:

**PROPOSITION 6.11.** The $\mathcal{T}_\pi^-$-algebra $\mathcal{T}_\pi^-(0)$ is compositional.

This gives an alternative proof of [Sangiorgi and Walker 2001, Theorem 2.2.8(1)], which says that bisimilarity is a non-input congruence [Sangiorgi and Walker 2001, Definition 2.1.23]. In our language:

**COROLLARY 6.12.** Bisimilarity for the $\mathcal{T}_\pi^-$-algebra $\mathcal{T}_\pi^-(0)$ is a congruence.

**PROOF.** By Corollary 4.30 and Propositions 6.10 and 6.11. $\square$

Similarly, $\mathcal{T}_\pi^-$ is $(\mathbf{T}_s^\pi)^\vee$-familial, so we recover Sangiorgi and Walker [2001, Lemma 2.3.21]:

**COROLLARY 6.13.** Bisimulation up to non-input context is sound.

## 6.3 Wide-Open Bisimilarity

Another standard solution to the failure of bisimilarity to be a congruence is to resort to wide-open bisimilarity. For this, following Staton [2008], we need to modify our base category $\mathbb{B}$ to include non-bijective maps $\gamma \to \gamma'$.

**Definition 6.14.** Let $\mathbb{F}$ be defined just as $\mathbb{B}$ (Definition 6.1), but including all morphisms from $\mathbf{Set}^{\mathbb{op}}$ (between relevant objects), instead of just bijections.
Please note that while we include non-bijective morphisms $f: \gamma \to \gamma'$, we do not (need to) do so for transition objects. The presheaf category $\mathbb{F}$ forms a transition category with the same transition types as $\mathbb{B}$, which we denote by $\mathbf{T}^+$.

Let us now adapt our monad on $\mathbb{B}$ to $\mathbb{F}$.

**PROPOSITION 6.15.** *Replacing the rules for $(x)(f)$ and $\langle\langle e\rangle\rangle(h, k)$ in Figure 2 by*

$$ \frac{x \in X(\gamma)}{\gamma \vdash_X (|x|)} \qquad \frac{e \in X(\alpha)}{\gamma \vdash_X \langle\langle e\rangle\rangle'} $$

and changing the base cases for renaming to $f \cdot (|x|) = (|f \cdot x|)$ and $(h, k) \cdot \langle\langle e\rangle\rangle = \langle\langle (h, k) \cdot e\rangle\rangle$ yields a functor $\mathcal{T}_\pi^+ : \mathbb{F} \to \mathbb{F}$.

It is not entirely trivial that this again forms a familial monad.

**PROPOSITION 6.16.** *$\mathcal{T}_\pi^+$ is a $\mathbf{T}_s^+$-familial monad.*

**PROOF SKETCH.** (More detail in [Hirschowitz 2018].) Most of the definitions are adapted from $\mathbb{B}$ to $\mathbb{F}$, modulo the following subtlety. On objects, fresh names $a_\gamma$ are chosen globally for all $\gamma$ as in the proof of Proposition 6.5, and only the base cases change to $E(|x|) = \mathbf{y}_\gamma$ (for $x \in X(\gamma)$) and $E\langle\langle e\rangle\rangle = \mathbf{y}_\alpha$ (for $e \in X(\alpha)$). However, over $\mathbb{B}$, we had $E(f \cdot P) = E(P)$, which considerably eased the definition of $E$ on morphisms. But because of the new treatment of renaming, this no longer holds over $\mathbb{F}$. E.g., consider $P = (|T_{[a]}|)$. We have $E(P) = \mathbf{y}_{[a]}$, but $E((a \mapsto b) \cdot P) = \mathbf{y}_{[b]}$ (where, we recall from (12), $(a \mapsto b)$ denotes the unique map $\{a\} \to \{b\}$), so we only get $E(P) \cong E((a \mapsto b) \cdot P)$. The treatment of morphisms thus needs adjustment: for $h: \gamma \to \gamma'$ and $k: \delta \to \delta'$ as in (13), we get inductively-defined, functorial assignments

$$ E(h \upharpoonright P): E(h \cdot P) \to E(P) \quad \text{and} \quad E((h, k) \upharpoonright R): E((h, k) \cdot R) \to E(R). $$

Finally, the definitions of $E(s \upharpoonright R)$ and $E(t \upharpoonright R)$ also need adjustment for scope-changing constructors $in_P^{a,vb}$, $\nabla b.R$, $vb.R$, and $R \triangleright^{vb} S$. E.g., consider the morphism $t \vdash in_{b,P}^{a,c}$: $[b \mapsto c] \cdot P \to in_{b,P}^{a,c}$. We have by definition $E(in_{b,P}^{a,c}) = E((b \mapsto a_\gamma) \cdot P)$ so we define $E(t \vdash in_{b,P}^{a,c})$ to be

$$ E([b \mapsto c] \cdot P) \xrightarrow{E([a_\gamma \mapsto c] \upharpoonright (b \mapsto a_\gamma) \cdot P)} E((b \mapsto a_\gamma) \cdot P). $$

We then show by induction that this assignment on morphisms is functorial, which entails that $\mathcal{T}_\pi^+$ is familial. Finally, by definition, morphisms $s \upharpoonright R$ are mapped to coproducts of isomorphisms and maps in $\mathbf{T}_s^+$, up to isomorphism in the arrow category, hence $\mathcal{T}_\pi^+$ is indeed $\mathbf{T}_s^+$-familial. $\square$

The compositionality problem created by $x(|f|)$ having disappeared, we get:

**PROPOSITION 6.17.** *$\mathcal{T}_\pi^+(0)$ is a compositional algebra.*

Calling *wide-open* bisimilarity the largest bisimulation relation over $\mathcal{T}_\pi^+(0)$, we get:

**PROPOSITION 6.18.** *Wide-open bisimilarity is a congruence.*

**PROOF.** By Corollary 4.31 and Propositions 6.16 and 6.17. $\square$

Similarly, we recover Sangiorgi and Walker [2001, Corollary 2.3.25]:

**COROLLARY 6.19.** *Wide-open bisimulation up to context is sound.*

**Remark 6.20.** A different presentation of wide-open bisimilarity may be obtained by augmenting $\mathbb{B}$ with a transition type $\gamma, a \xrightarrow{s} \sigma_{\gamma,a,b} \xleftarrow{t} \gamma$ (for $b \in \gamma$), and adding the rule $P \xrightarrow{\sigma_{\gamma,a,b}} [a \mapsto b] \cdot P$.
*Remark 6.21.* Similarly, *open* bisimilarity [Sangiorgi and Walker 2001, Definition 4.6.2] may be obtained by considering yet another base category, where instead of finite sets of names and (bi-)jective) maps we would have as objects pairs $(\gamma, D)$ of a finite set $\gamma$ of names and a distinction $D$, i.e., an irreflexive relation on $\gamma$, with maps $(\gamma, D) \to (\gamma', D')$ all maps $f: \gamma \to \gamma'$ respecting $D$, i.e., if $(a, b) \in D$ then $f(a) \neq f(b)$.

# 7 CONCLUSION AND PERSPECTIVES

We presented a categorical framework for studying congruence of bisimilarity, based on familial monads and lifting properties. We then refined the framework to account for soundness of bisim- ulation up to context, using lifting in the cospan category. We finally showed that the framework flexibly accounts for most known results about congruence of bisimilarity and soundness of bisim- ulation up to context in the $\pi$-calculus. To our knowledge, this is the first categorical account of congruence of bisimilarity and soundness of bisimulation up to context in the presence of binding. We furthermore hope to have demonstrated that the approach is close to operational intuitions.

However, although the framework provides abstract, rather general proofs of non-trivial facts, it does not yet come with any format, i.e., means to construct instances from more basic data. An obvious next step is thus to look for such formats, which in our case means automatically constructing familial monads satisfying the relevant hypotheses. An intermediate step would be to show that relevant formats (e.g., Middelburg [2001]; Mousavi et al. [2005]; Sands [1997]) give rise to familial monads with compositional initial algebras. Another potential direction is to con- sider questions related to congruence of bisimilarity and soundness of bisimulation up to context, e.g., weak variants of these results, environmental bisimulation, or solutions of process equations. Finally, we could consider adapting *pointwise analytic* monads [Garner and Hirschowitz 2018] to transition categories, which could accomodate *structural congruence*, hence possibly provide a new language to study the derivation of labelled transition systems from reduction rules [Sewell 1998].

# ACKNOWLEDGMENTS

Thanks to Uli Fahrenberg, André Hirschowitz, Paul-André Melliès, David Sands, Sam Staton, and the reviewers for useful comments, and to Paweł Sobociński for bringing my attention to this question some 10 years ago. And eternal categorical thanks to Richard Garner.

# REFERENCES

C. Berger, P.-A. Melliès, and M. Weber. 2012. Monads with arities and their associated theories. *Journal of Pure and Applied Algebra* 216, 8 (2012), 2092–2048. https://doi.org/10.1016/j.jpaa.2012.02.039

Karen L. Bernstein. 1998. A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages. In *Proc. 13th Symposium on Logic in Computer Science* IEEE Computer Society, 153–164. https://doi.org/10.1109/LICS.1998.705652

Bard Bloom, Sorin Istrail, and Albert R. Meyer. 1995. Bisimulation Can't be Traced. *Journal of the ACM* 42, 1 (1995), 232–268. https://doi.org/10.1145/200836.200876

Roland N. Bol and Jan Friso Groote. 1996. The Meaning of Negative Premises in Transition System Specifications. *Journal of the ACM* 43, 5 (1996), 863–914. https://doi.org/10.1145/234752.234756

Filippo Bonchi, Daniela Petrişan, Damien Pous, and Jurriaan Rot. 2016. A general account of coinduction up-to. *Acta Informatica* (2016), 1–64. https://doi.org/10.1007/s00236-016-0271-4

Gérard Boudol and Ilaria Castellani. 1988. A non-interleaving semantics for CCS based on proved transitions. *Fundamenta Informaticae* XI (1988).

Aurelio Carboni and Peter Johnstone. 1995. Connected limits, familial representability and Artin glueing. *Mathematical Structures in Computer Science* 5, 4 (1995), 441–459. https://doi.org/10.1017/S0960129500001183

Gian Luca Cattani, John Power, and Glynn Winskel. 1998. A Categorical Axiomatics for Bisimulation, See [Sangiorgi and de Simone 1998], 581–596. https://doi.org/10.1007/BFb0055649

Yves Diers. 1978. Spectres et localisations relatifs à un foncteur. *Comptes rendus hebdomadaires des séances de l'Académie des sciences* 287, 15 (1978), 985–988.
Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. 2016. Bisimulations and unfolding in *P*-accessible categorical models. In Proc. 27th International Conference on Concurrency Theory (LIPIcs), Josée Desharnais and Radha Jagadeesan (Eds.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.25

Marcelo P. Fiore and Sam Staton. 2006. A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics. In Proc. 21st Symposium on Logic in Computer Science IEEE, 49-58. https://doi.org/10.1109/LICS.2006.7

Marcelo P. Fiore and Daniele Turi. 2001. Semantics of Name and Value Passing. In Proc. 16th Symposium on Logic in Computer Science IEEE, 93-104. https://doi.org/10.1109/LICS.2001.932486

Richard H. G. Garner and Tom Hirschowitz. 2018. Shapely monads and analytic functors. Journal of Logic and Computation 28, 1 (2018), 33-83. https://doi.org/10.1093/logcom/exx029

Tom Hirschowitz. 2018. Familial monads and structural operational semantics. (2018). https://hal.archives-ouvertes.fr/hal-01815328 Preprint.

Mark Hovey. 1999. Model Categories. Mathematical Surveys and Monographs, Volume 63, AMS (1999), Vol. 63. American Mathematical Society. https://doi.org/10.1090/surv/063

Peter T. Johnstone. 2002. Sketches of an Elephant: A Topos Theory Compendium - Volume 1. Oxford University Press.

André Joyal, Mogens Nielsen, and Glynn Winskel. 1993. Bisimulation and open maps. In Proc. 8th Symposium on Logic in Computer Science IEEE, 418-427. https://doi.org/10.1109/LICS.1993.287566

Bartek Klin. 2011. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science 412, 38 (2011), 5043-5069. https://doi.org/10.1016/j.tcs.2011.03.023

Joachim Kock. 2011. Polynomial functors and trees. International Mathematics Research Notices 2011, 3 (2011), 609-673. https://doi.org/10.1093/imrn/rnq068

F. W. Lawvere. 1963. *Functorial semantics of algebraic theories*. Ph.D. Dissertation. Columbia University.

Saunders Mac Lane. 1998. Categories for the Working Mathematician (2nd ed.). Number 5 in Graduate Texts in Mathematics. Springer.

Saunders Mac Lane and Ieke Moerdijk. 1992. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer.

C. A. Middelburg. 2001. Variable binding operators in transition system specifications. Journal of Logic and Algebraic Programming 47, 1 (2001), 15-45. https://doi.org/10.1016/S1567-8326(00)00003-5

Mohammad Reza Mousavi, Michel A. Reniers, and Jan Friso Groote. 2007. SOS Formats and Meta-Theory: 20 Years After. Theoretical Computer Science 373, 3 (2007), 238-272. https://doi.org/10.1016/j.tcs.2006.12.019

Mohammad Reza Mousavi, Murdoch Gabbay, and Michel A. Reniers. 2005. SOS for Higher Order Processes. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings (Lecture Notes in Computer Science), Martín Abadi and Luca de Alfaro (Eds.), Vol. 3653. Springer, 308-322. https://doi.org/10.1007/11539452_25

Gordon D. Plotkin. 1981. *A Structural Approach to Operational Semantics*. DAIMI Report FN-19. Computer Science Department, Aarhus University.

Damien Pous and Davide Sangiorgi. 2011. Enhancements of the bisimulation proof method, Chapter 6. In Sangiorgi and Rutten [Sangiorgi and Rutten 2011].

Emily Riehl. 2014. *Categorical Homotopy Theory*. Number 24 in New Mathematical Monographs. Cambridge University Press.

David Sands. 1997. From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages. In Proc. 24th International Symposium on Principles of Programming Languages, Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM Press, 428-441. https://doi.org/10.1145/263699.263760

Davide Sangiorgi. 1994. The Lazy Lambda Calculus in a Concurrency Scenario. Information and Computation 111, 1 (1994), 120-153. https://doi.org/10.1006/inco.1994.1042

Davide Sangiorgi and Robert de Simone (Eds.). 1998. Proc. 9th International Conference on Concurrency Theory. LNCS, Vol. 1466. Springer.

Davide Sangiorgi and Jan Rutten (Eds.). 2011. Advanced Topics in Bisimulation and Coinduction. Number 52 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.

Davide Sangiorgi and David Walker. 2001. *The π-calculus – A Theory of Mobile Processes*. Cambridge University Press.

Peter Sewell. 1998. From Rewrite Rules to Bisimulation Congruences, See [Sangiorgi and de Simone 1998], 269-284. https://doi.org/10.1007/BFb0055628

Sam Staton. 2008. General Structural Operational Semantics through Categorical Logic. In Proc. 23rd Symposium on Logic in Computer Science 166-177. https://doi.org/10.1109/LICS.2008.43

Daniele Turi and Gordon D. Plotkin. 1997. Towards a Mathematical Operational Semantics. In Proc. 12th Symposium on Logic in Computer Science 280-291. https://doi.org/10.1109/LICS.1997.614955

Mark Weber. 2007. Familial 2-functors and parametric right adjoints. Theory and Applications of Categories 18, 22 (2007), 665-732.