Ambroise Lafont

© T Hirschowitz

A CATEGORICAL FRAMEWORK FOR CONGRUENCE OF APPLICATIVE BISIMILARITY IN HIGHER-ORDER LANGUAGES

Keywords: Programming languages, categorical semantics, operational semantics, Howe's method

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct proof that it is a congruence, and generalised the result to all languages complying with a suitable format. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name, call-by-value, and call-by-name non-deterministic -calculus, and more generally all languages complying with a variant of Howe's format.

1. Introduction 1.1. Motivation. This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about programming languages. This search arguably goes back at least to Turi and Plotkin [START_REF] Turi | Towards a mathematical operational semantics[END_REF], who coined the name "Mathematical Operational Semantics", and proved a general congruence theorem for bisimilarity. This approach has been deeply investigated, notably for quantitative languages [START_REF] Bartels | On Generalised Coinduction and Probabilistic Specification Formats[END_REF]. However, as of today, attempts to apply it to higher-order (e.g., functional) languages have failed.

In previous work [START_REF] Hirschowitz | Familial monads and structural operational semantics[END_REF][START_REF] Hirschowitz | Cellular Monads from Positive GSOS Specifications[END_REF], the first author has proposed an alternative approach to the problem, dropping the coalgebraic notion of bisimulation used by Turi and Plotkin in favour of a notion based on factorisation systems, similar to Joyal et al.'s [START_REF] Joyal | Bisimulation and open maps[END_REF]. Furthermore, congruence of bisimilarity is notably obtained by assuming that syntax induces a familial monad [Die78, [START_REF] Carboni | Connected limits, familial representability and Artin glueing[END_REF][START_REF] Weber | Familial 2-functors and parametric right adjoints[END_REF].

However, the new approach has only been applied to simple, first-order languages like the -calculus [START_REF] Milner | A calculus of mobile processes, I/II[END_REF][START_REF] Sangiorgi | The -calculus -A Theory of Mobile Processes[END_REF], and Positive GSOS specifications [START_REF] Bloom | Bisimulation can't be traced[END_REF]. In this paper, we extend it to functional languages, notably covering the paradigmatic case of applicative bisimilarity [START_REF] Abramsky | The lazy lambda calculus[END_REF] in call-by-name and call-by-value -calculus, as well as in a simple, nondeterministic -calculus [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF][START_REF] Douglas | Proving congruence of bisimulation in functional programming languages[END_REF]§7]. We even show that our framework subsumes the general, syntactic format proposed by Howe [How96, Lemma 6.1]. We thus obtain for the first time a generic, categorical congruence result for applicative bisimilarity in functional languages.

1.2. Overview. A bit more precisely:

• We propose a simple notion of signature for programming languages.

• Each signature has a category of models, including an initial one, intuitively its operational semantics. • An abstract analogue of applicative bisimilarity, called substitution-closed bisimilarity, may be defined in any model, and in particular in the initial one. • Under suitable hypotheses, we show that substitution-closed bisimilarity is a congruence in the initial model. Categorically, this unfolds as follows. (i) We define an abstract notion of (labelled) transition systems, as objects of a category C, in such a way that • there is a forgetful functor C → C 0 , intuitively returning the (potentially structured) set of states of a transition system; • bisimulation and bisimilarity may be defined for any transition system. (ii) Adopting Fiore, Plotkin, and Turi's seminal framework [START_REF] Fiore | Abstract syntax and variable binding[END_REF][START_REF] Fiore | Second-order and dependently-sorted abstract syntax[END_REF], we then assume that C 0 is monoidal, and define models of the syntax to be monoid algebras for a given pointed strong endofunctor Σ 0 on C 0 . Monoid algebras, a.k.a. Σ 0 -monoids, are Σ 0 -algebras equipped with compatible monoid structure, which models capture-avoiding substitution. The category Σ 0 -Mon of Σ 0 -monoids has an initial object Z 0 , whose carrier is the free Σ 0algebra on the monoidal unit , as we prove in Coq [START_REF] Lafont | Initial Sigma-monoids for skew monoidal categories in UniMath[END_REF]. In all examples, Z 0 is precisely the syntax.

(iii) This category Σ 0 -Mon induces by pullback a category Σ 0 -Trans of transition systems whose states are equipped with Σ 0 -monoid structure. We call these transition monoid algebras, or transition Σ 0 -monoids, or even simply transition monoids when Σ 0 is the identity. The relevant notions of bisimulation and bisimilarity for such objects are defined as in (i), but for substitution-closed relations. (iv) We then define models of the dynamics to be certain algebras, called vertical, for an endofunctor on Σ 0 -Trans. There is an initial vertical algebra Z, which in examples is the syntactic transition system. (Furthermore, standard applicative bisimilarity coincides with substitution-closed bisimilarity.) (v) Finally, following an abstract analogue of Howe's method, we show that, under suitable hypotheses, substitution-closed bisimilarity on Z is a congruence. One crucial hypothesis is cellularity, in a sense closely related to [START_REF] Richard | Shapely monads and analytic functors[END_REF].

1.3. Related work. Plotkin and Turi's bialgebraic semantics [START_REF] Turi | Towards a mathematical operational semantics[END_REF] and its few variants [START_REF] Corradini | Compositional SOS and beyond: a coalgebraic view of open systems[END_REF][START_REF] Staton | General structural operational semantics through categorical logic[END_REF] prove abstract congruence theorems for bisimilarity. However, they do not cover higher-order languages like the -calculus, let alone applicative bisimilarity. This was one of the main motivations for our work. Among more recent work, quite some inspiration was drawn from Ahrens et al. [START_REF] Ahrens | Reduction monads and their signatures[END_REF][START_REF] Hirschowitz | Modules over monads and operational semantics[END_REF], notably in the use of vertical algebras. However, a difference is that we do not insist that transitions be stable under substitution. In a different direction, Dal Lago et al. [START_REF] Dal Lago | Effectful applicative bisimilarity: Monads, relators, and Howe's method[END_REF] prove a general congruence theorem for applicative bisimilarity, for a -calculus with algebraic effects. As briefly discussed in the conclusion, our framework does not yet account for such results. However, it places the generality in a different direction: namely, it is not tied to any particular language (like the -calculus in [START_REF] Dal Lago | Effectful applicative bisimilarity: Monads, relators, and Howe's method[END_REF]). It would of course be useful to find a common generalisation.

Links with other relevant work by, e.g., Bodin et al. [START_REF] Bodin | Skeletal semantics and their interpretations[END_REF], though desirable, remain unclear, perhaps because of the very different methods used.

Furthermore, the cellularity used here is close to but different from the T ∨ -familiality of [START_REF] Hirschowitz | Familial monads and structural operational semantics[END_REF]. It would be instructive to better understand potential links between the two. Finally, let us mention recent work which, just like ours, strives to establish abstract versions of standard constructions and theorems in programming language theory like type soundness [START_REF] Arkor | Algebraic models of simple type theories: A polynomial approach[END_REF] or gluing [START_REF] Fiore | Semantic analysis of normalisation by evaluation for typed lambda calculus[END_REF][START_REF] Fiore | Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure[END_REF][START_REF] Fiore | Relative full completeness for bicategorical cartesian closed structure[END_REF].

1.4. Relation to conference version. This paper is a bit more than a journal version of our previous work [START_REF] Borthelle | A cellular Howe theorem[END_REF]. Here is a brief summary of changes.

(a) In [START_REF] Borthelle | A cellular Howe theorem[END_REF], we work with a non-trivial generalisation of monoid algebras to skew monoidal categories [START_REF] Szlachányi | Skew-monoidal categories and bialgebroids[END_REF] and structurally strong functors. Here, by giving a better type to Σ 1 , the endofunctor for specifying the dynamics, we manage to work with standard monoid algebras. This has the additional advantages of • avoiding a slightly ad hoc compositionality assumption of [START_REF] Borthelle | A cellular Howe theorem[END_REF], and • relaxing the requirement that the tensor product should be familial. (b) In [START_REF] Borthelle | A cellular Howe theorem[END_REF], because Howe's closure operates only at the level of states, we work mostly with prebisimulations, in the sense of [START_REF] Hirschowitz | Familial monads and structural operational semantics[END_REF]§5.1]. This notion is designed to detect when the state part of a relation underlies a bisimulation, regardless of what it does on transitions. However, it feels more ad hoc than the standard definition of bisimulation by lifting [START_REF] Joyal | Bisimulation and open maps[END_REF]. In this paper, we extend Howe's closure to transitions, thus avoiding prebisimulations entirely. (c) In [START_REF] Borthelle | A cellular Howe theorem[END_REF], we rely on directed unions of relations, which leads to quite a few, rather painful proofs by induction. Here, we use higher-level methods to construct Howe's closure, essentially through categorification and algebraicisation. Namely:

(1) We define bisimilarity as the final object not in some partially-ordered set of relations as usual, but in some category of spans (see also [START_REF] Basold | Monoidal company for accessible functors[END_REF]). (2) Furthermore, we define Howe's closure directly as a free monoid algebra for a suitable pointed strong endofunctor on spans. (3) More generally, we systematically rely on universal properties, which simplifies a significant number of proofs. (d) We put less emphasis on cellularity, viewing it only as a sufficient condition for a perhaps more natural hypothesis, which already appeared in a slightly different form in [START_REF] Staton | General structural operational semantics through categorical logic[END_REF], namely the fact that Σ 1 preserves functional bisimulations. (e) We obtain a congruence theorem of similar scope (Theorem 6.15), and cover three new, detailed applications ( §8): call-by-value, big-step -calculus (which was covered but too naively in [START_REF] Borthelle | A cellular Howe theorem[END_REF], as we explain), a call-by-name -calculus with unary, erratic choice from [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF]§7], and a general format proposed by Howe [How96, Lemma 6.1]. (f ) We fill a gap in the proof of [BHL20, Lemma 5.13], by requiring the endofunctor Σ 0 for specifying the dynamics to preserve sifted colimits (see Remark 5.13).

1.5. Plan. In §2, we start by briefly recalling call-by-name -calculus and applicative bisimilarity. We then explain how to view the latter as substitution-closed bisimilarity, and sketch Howe's method. In §3, we then give a brief overview of the new framework by example, including a recap on monoid algebras and a statement of the main theorem (in the considered case). We then dive into the technical core of the paper by presenting our framework for transition systems and bisimilarity ( §4), operational semantics ( §5), and then substitutionclosed bisimilarity and the main result (Theorem 6.15), together with a high-level proof sketch ( §6). In §7, we reformulate the main hypothesis of Theorem 6.15 using cellularity, which allows us to use well-known results from weak factorisation systems as sufficient conditions. We then apply our results to examples in §8. The full proof of Theorem 6.15 is given in §9. Finally, we conclude and give some perspectives on future work in §10.

1.6. Notation and preliminaries. In this subsection, we fix some basic notation, and review some preliminaries. 1.6.1. Basic notation. We often conflate natural numbers ∈ N with the corresponding sets {1, . . . , }. For all sets and objects of a given category, we denote by • the -fold coproduct of with itself, i.e., ∈ . Let Gph denote the category of (directed, multi) graphs, Cat the category of small categories, and CAT the category of locally small categories.

1.6.2. Comma categories and lax limits. Given functors : A → C and : B → C, the comma category / has • as objects all triples ( , , ), where ∈ A, ∈ B, and : ( ) → ( ), and • as morphisms ( , , ) → ( ′ , ′ , ′ ) all pairs of morphisms : → ′ and : → ′ making the following square commute.

( ) ( ′ ) ( ) ( ′ ) ( ) ( ) ′
We have the following well-known fact:

Proposition 1.1. If A and B have, and preserves colimits of any given shape, then the projection functor / → A × B creates them. Symmetrically, if A and B have, and preserves limits of any given shape, then the projection functor / → A × B creates them.

The comma category / is well-known [START_REF] Kelly | Elementary observations on 2-categorical limits[END_REF][START_REF] Weber | Yoneda structures from 2-toposes[END_REF] to be the universal category equipped with projections to A and B and a natural transformation as in the following diagram.

/ B A C

Kelly [START_REF] Kelly | Elementary observations on 2-categorical limits[END_REF] explains that the comma category is a kind of lax limit of and . When is an identity, we call the comma category a lax limit of . 1.6.3. Presheaves. Let C denote the category of (contravariant) presheaves on C, and y : C → C the Yoneda embedding, mapping to C(-, ). Given a presheaf ∈ C, an element ∈ ( ), and a morphism -→ ′ , we sometimes denote ( ) ( ) by • . Given two categories C 1 and C 2 , we denote by [C 1 , C 2 ] the functor category between them. 1.6.4. Spans and relations. In a category C with binary products, we interchangeably use spans ← → and their pairings → × , sometimes also calling the latter spans. Spans from to are the objects of a category Span (C) ( , ), which is isomorphic to the slice category C/ × in the presence of binary products. When C has pullbacks, these categories are the hom-categories of a bicategory [START_REF] Bénabou | Introduction to bicategories[END_REF] Span (C), in which composition of morphisms is given by pullback. A relation from to is merely a span whose pairing → × is monic. 1.6.5. Images. Let us now recall a few elements about images.

Definition 1.2. An image of a morphism : → is a factorisation -→ with a monomorphism, which is initial in the sense that for any factorisation ′ -→ ′ ′ there is a (unique by monicness) morphism :

→ ′ making both triangles commute in the following diagram. ′ ′ ′ Definition 1.3. A strong epimorphism is a morphism with the strong left lifting property w.r.t. all monomorphisms, i.e., a morphism : → such that for all (solid) commuting squares with monic there exists a unique lifting making both triangles commute.

The terminology is justified by the following result.

Lemma 1.4. In a category with equalisers, any strong epimorphism is an epimorphism.

Proof. Let us assume that : → is a strong epi and = , with , : → . Then, let : ′ → denote the equaliser of and . Because equalises and , it factors as ℎ, for some unique ℎ : → ′ . But now is monic, so by lifting there is a unique making both triangles commute in the following diagram.

′ ℎ

We thus have

= • id = • • = • • = • id = .
The morphism is thus epi, as claimed.

Corollary 1.5. Factoring a morphism as a strong epi followed by a mono yields an image.

Proof. Initiality is directly given by the lifting property.

Proposition 1.6. In any locally finitely presentable category, images always exist, and may be computed as (strong epi, mono)-factorisations.

Proof. This is (part of) [AR94, Proposition 1.61].

Let us finally observe:

Proposition 1.7. In locally presentable category, unions of subobjects exist, and may be computed by taking the cotupling of all considered subobjects, and then their (strong epi, mono)-factorisation.

Proof. Straightforward. 1.6.6. Initial algebras. Any finitary endofunctor on any cocomplete category admits by [Rei77, Theorem 2.1] an initial algebra, which we denote by Z . Although this is detailed below, we prefer to avoid confusion and warn the reader that we also use Z for the initial -monoid, for any pointed strong endofunctor on any nice monoidal category (which is incidentally the initial ( + )-algebra). Throughout the paper, when not explicitly attached to any , Z is shorthand for Z Σ1 (see, e.g., Proposition 3.21 or Theorem 5.18). 1.6.7. Weak factorisation systems. Finally, let us fix some notation about weak factorisation systems. In any category , we say that a morphism : → has the (weak) left lifting property w.r.t. : → when for all commuting squares , there is a lifting as shown that makes both triangles commute. Equivalently, we say that has the right lifting property w.r.t. , and write ⋔ . Given a fixed set J of morphisms, the set of morphisms such that ⋔ for all ∈ J is denoted by J ⋔ . Similarly, the set of morphisms such that ⋔ for all ∈ J is denoted by ⋔ J. In particular, if ∈ ⋔ (J ⋔ ) and ∈ J ⋔ , then ⋔ . If is locally presentable [START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF], then ( ⋔ (J ⋔ ), J ⋔ ) forms a weak factorisation system, in the sense that additionally any morphism : → factors as -→ -→ with ∈ ⋔ (J ⋔ ) and ∈ J ⋔ (see [Hov99, Theorem 2.1.14]). Morphisms in J ⋔ are generically called fibrations, while morphisms in ⋔ (J ⋔ ) are called cofibrations.

Let us conclude with the following easy, yet helpful result.

Lemma 1.8. For any locally finitely presentable category and set J of maps therein, if the domains and codomains of maps in J are finitely presentable, then fibrations are closed under filtered colimits in the arrow category.

Proof. Let us consider any given filtered diagram ( : → ) ∈D of fibrations, and a colimit : → in the arrow category, say C → . We must show that ⋔ for all ∈ J. Let us thus consider any given commuting square with ∈ J. Colimits in the arrow category are pointwise, so = colim and = colim . Thus, by finite presentability of and , and by filteredness of the diagram D → C, and factor through some 0 and 1 , respectively. By filteredness of the diagram again, w.l.o.g., we may take 0 = 1 , such that ( , ) : → factors through 0 . But because 0 is a fibration, we find a lifting as in 0 0 , ′ ′ 0 which provides the desired lifting for the original square.

A brief review of Howe's method

2.1. Applicative bisimilarity. Let us consider the standard, big-step presentation of callby-name -calculus:

. ⇓ .

1 ⇓ . ′ 1 ′ 1 [ ↦ → 2 ] ⇓ 3 1 2 ⇓ 3
Standardly, the evaluation relation ⇓ is considered between closed terms only.

Applicative bisimilarity is an important notion of program equivalence in this language. Indeed, it is coinductive, so one may prove that any two given programs are applicative bisimilar merely by exhibiting an applicative bisimulation. Furthermore, it is sound and complete w.r.t. (i.e., it coincides with) standard contextual equivalence.

Let us briefly recall the definition. Applicative bisimilarity is standardly introduced in two stages, which we now recall.

[ ↦ → ] ′ 2 [ ↦ → ].
An applicative bisimulation is an applicative simulation whose converse, say † , is also an applicative simulation.

Applicative bisimulations are closed under unions, and so there is a largest applicative bisimulation, called applicative bisimilarity and denoted by ∼.

Then comes the second stage: The result we wish to abstract over is the following (see [START_REF] Pitts | Howe's method for higher-order languages, chapter 5[END_REF] for a historical account).

Theorem 2.5. The open extension ∼ ⊗ of applicative bisimilarity is a congruence: it is an equivalence relation, and furthermore it is context-closed, i.e.,

• 1 ∼ ⊗ 2 entails . 1 ∼ ⊗ . 2 for all ; • 1 ∼ ⊗ 2 and ′ 1 ∼ ⊗ ′ 2 entail 1 ′ 1 ∼ ⊗ 2 ′ 2 .
Proving that ∼ ⊗ is an equivalence relation is in fact straightforward. In the following, we focus on the context-closedness property.

2.2. Howe's method. Howe's method for proving Theorem 2.5 consists in considering a suitable relation ∼ • , closed under substitution and context, and containing ∼ ⊗ by construction. He then shows that this relation ∼ • is an applicative bisimulation. By maximality of ∼ ⊗ , we thus also have ∼ • ⊆ ∼ ⊗ hence both relations coincide and ∼ ⊗ is context-closed as desired. However, as explained in [BHL20, §5.1], the presence of a substitution in the premises of a transition rule seems to require ∼ • to be closed under heterogeneous substitution, in the sense that, e.g., if

1 ∼ • ′ 1 and 2 ∼ • ′ 2 (for open terms), then 1 [ ↦ → 2 ] ∼ • ′ 1 [ ↦ → ′ 2 ].
The problem is that building this into the definition of ∼ • leads to difficulties in the proof that it is an applicative bisimulation. Howe's workaround consists in requiring ∼ • to be closed under sequential composition with ∼ ⊗ from the outset. Coupling this right action with context closedness, he thus defines ∼ • as the smallest context-closed relation satisfying the rules

∼ • ∼ • ′ ′ ∼ ⊗ ′′ ∼ • ′′ •
By construction, ∼ • is reflexive and context-closed. By induction, it also substitution-closed. Furthermore, by reflexivity and the second rule, it also contains ∼ ⊗ , and finally the second rule clearly entails ∼ • ; ∼ ⊗ ⊆ ∼ • , where ";" denotes relational (or sequential) composition. It takes an induction to prove stability under heterogeneous substitution, but to give a feel for it, in the basic case where 1 ∼ ⊗ ′ 1 , we have

1 [ ↦ → 2 ] ∼ • 1 [ ↦ → ′ 2 ] ∼ ⊗ ′ 1 [ ↦ → ′ 2 ] by context closedness of ∼ • and substitution closedness of ∼ ⊗ , so we conclude by ∼ • ; ∼ ⊗ ⊆ ∼ • .
The initial plan was to show that ∼ • is an applicative bisimulation and deduce that it coincides with ∼ ⊗ . It can in fact be slightly optimised by first showing that ∼ • is an applicative simulation, and then that its transitive closure (∼ • ) + is symmetric. The relation (∼ • ) + is also an applicative simulation, hence by symmetry an applicative bisimulation. This entails the last inclusion in the chain ∼ ⊗ ⊆ ∼ • ⊆ (∼ • ) + ⊆ ∼ ⊗ , showing that all relations coincide. Finally, because ∼ • is context-closed, so is ∼ ⊗ , as desired.

2.3. Non-standard presentation. The above, standard evaluation rules for call-by-name -calculus are not directly compatible with our framework. We thus adopt a slightly different presentation, where the evaluation relation relates closed terms to terms with just one potential free variable. The problem and its solution should become clear in §8.4, where we investigate Howe's general format [How96, Lemma 6.1]. There, we show that any language complying with Howe's format may be covered by our framework, up to suitable encoding. The present, non-standard presentation is a slight variant of this encoding, optimised for -calculus. The new transition rules are as follows.

.

⇓ 1 ⇓ ′ 1 ′ 1 [ 2 ] ⇓ 3 1 2 ⇓ 3 Here ′ 1 [ 2 ]
denotes substitution of the unique potential free variable in ′ 1 by 2 . We will see below that, with this transition system, the essentially standard notion of bisimulation coupled with the substitution-closedness requirement yields applicative bisimilarity.

Overview by example

In this section, we describe one particular instance of our framework, which models call-byname -calculus.

3.1. Syntax. Let us first define the syntax of -calculus, following [START_REF] Fiore | Abstract syntax and variable binding[END_REF], as an initial1 object in a suitable category of models. Very roughly, a model of -calculus syntax should be something equipped with operations modelling abstraction and application, but also with substitution. Furthermore, certain natural compatibility axioms should be satisfied, e.g.,

( 1 2 ) [ ] = 1 [ ] 2 [ ].
(3.1) A natural setting for specifying such operations is the functor category

C 0 := [F, Set],
where F ↩→ Set denotes the full subcategory spanning all sets of the form (i.e., {1, . . . , }, recalling notation from §1). For any ∈ [F, Set] and ∈ F, we think of ( ) as a set of 'terms' with potential free variables, e.g., in {1, . . . , } or, if the reader prefers, { 1 , . . . , }. The action of on morphisms → ′ is thought of as variable renaming. Returning to operations, being equipped with abstraction is the same as being a Σ 0 -algebra, where

Σ 0 : C 0 → C 0 is defined by Σ 0 ( ) ( ) = ( +1
). An algebra structure on any thus consists of a family of maps ( + 1) → ( ), natural in . Similarly, for specifying both application and abstraction, we consider

Σ Λ ( ) ( ) = ( + 1) + ( ) 2 .
(3.2)

Let us now consider substitution. The idea here is to equip C 0 with monoidal structure (⊗, ), such that • elements of ( ⊗ ) ( ) are like explicit substitutions ( ), where ∈ ( ) and : → ( ) for some , considered equivalent up to some standard equations2 ; • elements of ( ) := {1, . . . , } are merely variables. Being equipped with substitution (and variables) is thus the same as being a monoid for this tensor product:

• the multiplication : ⊗ → maps any formal, explicit substitution ( ) to an actual substitution [ ], and • the unit : → injects variables into terms. Finally, how do we enforce equations such as (3.1)? This goes in two stages:

• we first collect the way substitution is supposed to commute with each operation, by providing a pointed strength, i.e., a natural transformation with components , : Σ Λ ( ) ⊗ → Σ Λ ( ⊗ ), where ∈ C 0 and ∈ /C 0 , satisfying some equations [Fio08, §I.1.2];

• we then use the pointed strength to enforce all equations in one go, by requiring models to have compatible Σ Λ -algebra and substitution structure, in a suitable sense. Let us first explain the notion of pointed strength.

Application: For modelling Equation (3.1) for application, we would in particular define , to map any ( 2 ( 1 , 2 ))( ) to 2 ( 1 ( ), 2 ( )), for all 1 , 2 ∈ ( ) and : → ( ). (The coproduct injection 2 here acts as a formal application, recalling Σ Λ ( ) ( ) = ( + 1) + ( ) 2 .) Abstraction: For abstraction, let us start by first stating the corresponding equation. We will then define the pointed strength accordingly. Supposing that is equipped with a point : → , we define ↑ : + 1 → ( + 1) by copairing

-→ ( ) ( 1 )
-----→ ( + 1) and 1 = (1)

( ) 1 ----→ (1) ( 2 )
-----→ ( + 1). The equation is then

( ) [ ] = ( [ ↑ ]). (3.3)
Accordingly, we define the pointed strength to map any 1 ( )( ), where ∈ ( + 1) and : → ( ), to 1 ( ( ↑ )). Let us now go through the second stage of how we impose the desired equations: a model of syntax will be a monoid equipped with Σ Λ -algebra structure : Σ Λ ( ) → , such that the following diagram commutes.

Σ Λ ( ) ⊗ Σ Λ ( ⊗ ) Σ Λ ( ) ⊗ , ⊗ Σ Λ ( ) (3.4)
Indeed, suppose given, e.g., 1 ( )( ) ∈ Σ Λ ( ) ⊗ , by applying the left then bottom morphisms we obtain ( ) [ ], while applying the top then right morphisms we obtain ( [ ↑ ]), as desired.

All in all, we have:

Definition 3.1. For any finitary, pointed strong endofunctor Σ 0 , a monoid algebra for Σ 0 , or a Σ 0 -monoid, is a Σ 0 -algebra ( , : Σ 0 ( ) → ), equipped with monoid structure ( : ⊗ → , : → ), such that (3.4) commutes. A Σ 0 -monoid morphism is a morphism in C 0 which is both a monoid morphism and a Σ 0 -algebra morphism.

Let Σ 0 -Mon denote the category of Σ 0 -monoids and morphisms between them.

Let us conclude by (slightly informally) stating the result exhibiting standard syntax as the initial model [FPT99, FS17, BHL20]. See Proposition 5.4 below for a general and rigorous statement. Proposition 3.2. For any finitary, pointed strong endofunctor Σ 0 , under mild hypotheses, the forgetful functor Σ 0 -Mon → C 0 is monadic, and the free Σ 0 -algebra over (equivalently the initial ( + Σ 0 )-algebra) is an initial Σ 0 -monoid.

Example 3.3. In the case of -calculus, the initial Σ Λ -monoid is thus the least fixed point Z 0 := .( + Σ Λ ( )), which is isomorphic to the standard, low-level construction of syntax.

From this, one may deduce a characterisation of not only the initial Σ Λ -monoid, but all free Σ Λ -monoids, or in other words an explicit formula for the left adjoint to the forgetful functor. Namely: Proposition 3.4. For any finitary, pointed strong endofunctor Σ 0 , under the same hypotheses as in Proposition 3.2, the free Σ 0 -monoid, say ℒ 0 ( ), over any ∈ C 0 is .( + Σ 0 ( ) + ⊗ ).

Syntactically, when Σ 0 = Σ Λ , letting ⊢ mean that ∈ ℒ 0 ( ) ( ), ℒ 0 ( ) is inductively generated by the following rules [Ham04, §3.1],

⊢ ( ∈ ) ⊢ 1 . . . ⊢ ⊢ ( 1 , . . . , ) ( ∈ ( )) ⊢ 1 ⊢ 2 ⊢ 1 2 + 1 ⊢ ⊢ ( ) modulo the equivalence ( • )( 1 , . . . , ) ∼ ( (1) , . . . , ( ) ),
for all : → , ∈ ( ), and ⊢ 1 , . . . , , or perhaps more synthetically

( • )( ) ∼ ( • ),
where : → ℒ 0 ( ) ( ) denotes the cotupling of 1 , . . . , viewed as maps 1 → ℒ 0 ( ) ( ).

The first rule is the standard rule for variables, while the second one is for "constants", i.e., elements of . It corresponds to the term ⊗ in the above fixed-point formula. When = 0, we sometimes shorten the notation from () to . The last two rules are the standard rules for application and abstraction, and they correspond to the term Σ 0 ( ) in the formula. The Σ Λ -monoid structure is syntactically straightforward; notably substitution satisfies ( 1 , . . . , )[ ] = ( 1 [ ], . . . , [ ]).

3.2.

Transition systems and bisimilarity. The appropriate notion of transition system for -calculus is as follows.

Definition 3.5. A transition system consists of

• a state object 0 ∈ C 0 = [F, Set],
• a set 1 of transitions, and • maps 0 (0) ← --1 --→ 0 (1) giving the source and target of transitions (cf. §2.3). Transition systems form a category C, whose morphisms → consist of compatible morphisms 0 : 0 → 0 and 1 : 1 → 1 , in the sense that both of the following squares commute.

1 1 0 (0) 0 (0) 1 0 1 1 0 (1) 0 (1) 1 0
Notation 3.6. We write : ⇓ for ∈ 1 such that ( ) = and ( ) = .

Example 3.7. The syntactic transition system has Z 0 ∈ C 0 from Example 3.3 as state object, and as transitions all derivations following the transition rules. We will come back to this case in Proposition 3.21.

Our next goal is to introduce bisimulation, for which it is convenient to characterise C as a presheaf category. This characterisation may be established by abstract means, but let us describe it concretely first. It is clear from the definition that transitions systems are glorified graphs. And they form a presheaf category for essentially the same reason as graphs do. Here is the base category:

More concretely:

• There is exactly one morphism 0 → in F for all , which is an identity when = 0, so for all ≠ 0 we have a morphism ⇓, : ⇓ → making the following triangle commute.

⇓ 0 ⇓ ⇓,

!

• There are exactly morphisms 1 → in F for all ∉ {0, 1} (and no morphisms 1 → 0), so for all such and ∈ we have a morphism ⇓, , : ⇓ → making the following triangle commute. Notation 3.10. We often implicitly convert from transition systems to covariant presheaves, and conversely.

Proof sketch. This will be proved below by abstract means, but for intuition let us sketch the correspondence. Given a transition system , : 1 → 0 (0) × 0 (1), we construct a presheaf ′ by setting

• ′ ( ) = 0 ( ) for all ∈ F, • ′ (⇓) = 1 ,
• with the action of ⇓ , ⇓ ∈ F given by and , • inducing the action of all ⇓, and ⇓, , by composition. Conversely, for any presheaf , we construct a transition system ′ defined as follows:

• the state object ′ 0 ∈ [F, Set] is given by restriction of ; • the set ′ 1 of transitions is (⇓); • and ′ and ′ are ( ⇓ ) and ( ⇓ ), respectively.

The correspondence yields basic, graph-like examples of transition systems.

Example 3.11. (a) The representable presheaf y 0 associated to 0 ∈ F has a single closed state 0 and its renamings (i.e., (y 0 ) 0 ( ) = 1 for all and for transitions (y 0 ) 1 = ∅). (b) The representable presheaf y ⇓ consists of a closed state 0 , a state 1 with one free variable, their renamings, and a transition : 0 ⇓ 1 . (c) Let y ⇓ : y 0 → y ⇓ denote the morphism mapping 0 to 0 .

Using these basic examples, we may define bisimulation and bisimilarity by lifting following [JNW93]:

Definition 3.12. A morphism → in C is a functional bisimulation when it has the right lifting property w.r.t. the source map y ⇓ : y 0 → y 1 . A span ← → is a simulation when its left leg → is a functional bisimulation, and a bisimulation when both legs are. Remark 3.13. In this case, the Yoneda lemma says that C(y 0 , ) 0 (0) and C(y ⇓ , ) 1 . The right lifting property for a morphism : → thus says that given any ∈ 1 whose source • ⇓ is ( ) for some ∈ 0 (0), there exists ′ ∈ 1 such that ( ′ ) = and ′ • ⇓ = , which matches the usual definition of functional bisimulation. The following diagram might help readability. Example 3.16. Bisimilarity on the syntactic transition system merely amounts to simultaneous convergence, because evaluation returns an open term, which does not have any further transition. In this case, a more relevant behavioural equivalence is substitutionclosed bisimilarity, which we will define below.

3.3. Operational semantics. Just as we have defined the syntax as an initial Σ 0 -monoid (Example 3.3), let us now define the dynamics by initiality, again starting by finding the right notion of model. First of all, models will be found among transition systems whose underlying presheaf 0 ∈ [F, Set] is a Σ 0 -monoid. Let us give these a name. Definition 3.17. A transition Σ 0 -monoid is a transition system , together with Σ 0 -monoid structure on its vertices (a.k.a. states) object 0 . When Σ 0 = id, we call transition Σ 0monoids simply transition monoids. (Any transition Σ 0 -monoid is thus in particular a transition monoid.)

Let Σ 0 -Trans denote the category of transition Σ 0 -monoids, with as morphisms all transition system morphisms which induce Σ 0 -monoid morphisms on vertices objects.

The idea is to model the transition rules as an endofunctor on transition Σ 0 -monoids, leaving the underlying Σ 0 -monoid untouched, i.e., a functor making the triangle

Σ 0 -Trans Σ 0 -Trans Σ 0 -Mon Σ 1
commute, where denotes the forgetful functor (i.e., ( ) = 0 ). For call-by-name -calculus, the functor Σ 1 : Σ 0 -Trans → Σ 0 -Trans modelling the nonstandard rules at the end of §2 is defined as follows.

• On states, commutation of the above triangle imposes Σ 1 ( )

0 = 0 . • On transitions, let Σ 1 ( ) 1 = 0 (1) + ( ),
where ( ) denotes the set of valid premises for the second rule in §2.3, i.e., triples

( 1 , 2 , 2 ) such that -1 , 2 ∈ 1 are transitions, -2 ∈ 0 (0) is a state, and -2 • ⇓ = ( 1 • ⇓ ) [ 2 ],
i.e., the source 2 • ⇓ of 2 is obtained by substituting 2 for the unique free variable in the target of 1 . In other words:

1 1 ⇓ ′ 1 2 ′ 1 [ 2 ] ⇓ 3 1 2 ⇓ 3 •
Let us notice that substitution here follows from the monoid structure of .

• We then define the source and target maps:

for the first term 0 (1), * the source of any 1 ( ) is 1 ( ), where : 0 ( + 1) → 0 ( ) follows from the Σ 0 -algebra structure of 0 ; * the target is itself; -for the second term ( ), * the source of any 2 ( 1 , 2 , 2 ) is ( 1 • ⇓ ) 2 , i.e., the application of the source of 1 to 2 (again using the Σ 0 -algebra structure of 0 ); * the target is 2 • ⇓ . Accordingly, our notion of model is the following. Definition 3.18. A vertical Σ 1 -algebra is a transition Σ 0 -monoid equipped with a morphism : Σ 1 ( ) → such that ( ) = id 0 , or equivalently a map ( ) 1 making the following triangle commute.

Σ 1 ( ) 1 1 0 (0) × 0 (1) ( ) 1 Σ 1 ( ) , Σ 1 ( ) ,
In the case of call-by-name -calculus, it should be clear that such a vertical algebra is indeed a model of the rules.

However, in order to ensure that the rules are syntax-directed, we want to distinguish, for each rule, the head operator of the source of the conclusion (abstraction for the first rule; application for the second one). Instead of demanding that (Σ 1 ) have the form Σ 1 ( ) 1 → 0 (0) × 0 (1), we thus rather require something of the form Σ 1 ( ) 1 → Σ 0 ( 0 ) (0) × 0 (1): Definition 3.19 (Dynamic signatures and vertical algebras).

• A dynamic signature Σ 1 consists of -a finitary functor Σ 1 : Σ 0 -Trans → Set, and -a natural transformation (Σ 1 ) : Σ 1 ( ) → Σ 0 ( 0 ) (0) × 0 (1).
• The endofunctor Σ1 induced by a dynamic signature maps any to the composite

Σ 1 ( ) (Σ 1 ) -----→ Σ 0 ( 0 ) (0) × 0 (1) 0 ,0 × 0 (1) ----------→ 0 (0) × 0 (1)
, where 0 : Σ 0 ( 0 ) → 0 denotes the Σ 0 -algebra structure of 0 .

• A vertical algebra of a dynamic signature is a vertical algebra of the induced endofunctor, in the sense of Definition 3.18.

Concretely, a vertical algebra is a dashed map making the following diagram commute.

Σ 1 ( ) 1 Σ 0 ( 0 ) (0) × 0 (1) 0 (0) × 0 (1) (Σ 1 ) 0 ,0 × 0 (1)
, Example 3.20. For call-by-name -calculus, we only need to modify the source components of the above definition of Σ 1 , replacing actual operations by formal ones, like so:

• the source of any 1 ( ) ∈ 0 (1) + ( ) is 1 ( ) ∈ Σ 0 ( 0 ) (0) = 0 (1) + 0 (0) 2 ; • the source of any 2 ( 1 , 2 , 2 ) is 2 (( 1 • ⇓ ), 2 ) ∈ Σ 0 ( 0 ) (0).
This successfully captures the syntactic transition system:

Proposition 3.21. The initial Σ1 -algebra Z Σ1 , or Z for short, is an initial vertical algebra, and is isomorphic to the transition system of Example 3.7.

Substitution-closed bisimilarity.

There is an obvious notion of bisimulation for transition Σ 0 -monoids:

Definition 3.22. A morphism is Σ 0 -Trans is a functional bisimulation iff its underlying morphism in C is.
However, as foreshadowed by Example 3.16, the relevant notion in this case combines bisimulation with substitution-closedness, in the following sense. Definition 3.23. For any monoid in C 0 , an -module is an object equipped with algebra structure ⊗ → for the monad -⊗ . A module morphism is an algebra morphism.

Example 3.24. The monoid is itself an -module by multiplication, and -modules are closed under limits in C 0 , so in particular 2 is an -module, with action given by the

composite 2 ⊗ 1 ⊗ , 2 ⊗ -------------→ ( ⊗ ) 2 2 ---→ 2 .
Definition 3.25. For any transition monoid , a span of the form → 2 in C is substitution-closed iff 0 may be equipped with 0 -module structure making the morphism 0 → 2 0 into an 0 -module morphism. Example 3.26. To see what this definition has to do with substitution-closedness, let us observe that if is a relation in [F, Set], an element of ( ⊗ ) ( ) is an explicit substitution ( ) with ∈ ( ) for some , and : → ( ). Now, substitution-closedness amounts to a morphism : ⊗ → commuting with projections, so if is a relation, then is merely a pair ′ , and the morphism ensures that [ ] ′ [ ].

Proposition 3.27. For any transition Σ 0 -monoid , there is a terminal substitution-closed bisimulation ∼ ⊗ , called substitution-closed bisimilarity.

Proof. See Proposition 6.10 for a proof in the general case.

Remark 3.28. One may prove that substitution-closed bisimilarity is a relation.

Proposition 3.29. Substitution-closed bisimilarity ∼ ⊗ Z on the syntactic transition system Z coincides with applicative bisimilarity.

Proof. Let us denote the open extension of applicative bisimilarity by ∼ ⊗

std , and recall that applicative bisimilarity is denoted by ∼. Using Lemma 2.4, ∼ ⊗ std is straightforwardly a substitution-closed bisimulation, so we have ∼ ⊗ std ⊆ ∼ ⊗ Z . But conversely any substitutionclosed bisimulation relation (hence ∼ ⊗ Z ) is in particular a substitution-closed relation contained in ∼ on closed terms. It is thus globally contained in ∼ ⊗ std by Lemma 2.4. Finally, our main result instantiates to the following.

Theorem 3.30. Substitution-closed bisimilarity is context-closed. More precisely, it is a transition Σ 0 -monoid, and ∼ ⊗ Z → Z 2 is a transition Σ 0 -monoid morphism. In particular, there exists a span morphism

Σ 0 ((∼ ⊗ Z ) 0 ) → (∼ ⊗ Z ) 0 .

Transition systems and bisimilarity

In this section, we start to abstract over the situation of §3, by introducing a general framework for transition systems and bisimilarity. In §4.1, we first introduce the ambient setting for this, pre-Howe contexts, and construct a category of transition systems, for any pre-Howe context. Then, in §4.2, we show that transition systems form a presheaf category.

We then exploit this in §4.3 to define bisimulation and bisimilarity.

4.1. Pre-Howe contexts and transition systems.

Definition 4.1. A pre-Howe context3 consists of • a small category C 0 of state types,

• a small category C 1 of transition types, and • two source and target functors s, t :

C 1 → C 0 .
Precomposition by s and t yields functors Δ s , Δ t :

C 0 → C 1 mapping any ∈ C 0 to • s and • t, respectively. Let Δ denote the pointwise product Δ s × Δ t .
Intuitively, objects of C 0 may be thought of as typings (typically sequents 1 , . . . , ⊢ , or merely natural numbers, as in §3), and objects of C 1 as transition types. The source and target functors associate to every transition type the corresponding typings. We now use these functors to define transition systems. Definition 4.2. Given any pre-Howe context, a transition system consists of

• a state presheaf 0 ∈ C 0 , • a transition presheaf 1 ∈ C 1 , and • two source and target natural transformations 0 • s ← 1 → 0 • t, or equivalently a natural transformation 1 → Δ( 0 ).
Proposition 4.3. In any pre-Howe context, transition systems are precisely the objects of the lax limit category

C 1 /Δ of the functor C 0 Δ -→ C 1 in CAT, or equivalently the comma category id C 1 /Δ.
Proof. An object of the lax limit is by construction a triple ( 1 , 0 , ), where : Proposition 4.5. The projection functor -0 : C → C 0 has a left adjoint mapping any object 0 to ∅ → 0 s × 0 t, where ∅ denotes the initial presheaf on C 1 . For any 0 , we call this object the discrete transition system on 0 .

1 → Δ( 0 ) = 0 s × 0 t.

Proof. Straightforward.

Example 4.6. We can get C → C 0 to be the forgetful functor Gph → Set by taking and• s, t : 1 → 1 to be the unique such functor, i.e., the identity. A transition system thus consists of sets and together with a map → 2 , i.e., a graph.

• C 0 = 1, so that C 0 = 1 Set, • C 1 = 1, so that C = Set,
Example 4.7. A proof-relevant variant of standard labelled transition systems (over any set A of labels) may be obtained as follows. We take

• C 0 = 1 again, • C 1 = A viewed
as a discrete category, and • s, t : C 1 → C 0 the unique such functor. Thus, a transition system consists of a set 0 and sets for all ∈ A, together with maps → 2 0 returning the source and target of each -labelled edge. More generally, given any graph L, taking s, t : C 1 → C 0 to be the source and target maps L 1 → L 0 viewed as functors between discrete categories, we obtain for C → C 0 a functor equivalent to Gph/L → Set/L 0 .

Example 4.8. Let C 0 = F op and C 1 = 1, with s and t picking respectively 0 and 1. In particular, C 1 Set. Then, Δ( 0 ) = 0 (0) × 0 (1) and we recover the category C of §3.2, and its forgetful functor to

C 0 = [F, Set].

4.2.

Transition systems as presheaves. Before introducing bisimulation, let us establish an alternative characterisation of the category C of transition systems.

Proposition 4.9. The lax limit category C 1 /Δ of transition systems is isomorphic to a presheaf category C s,t .

Proof. Let C s,t denote the lax colimit in Cat of the parallel pair s, t. By definition, it is the universal category with functors and natural transformations as in

C 1 C 0 C s,t . s t 1 0
It thus consists of the coproduct C 1 + C 0 , augmented with arrows : s( ) → and : t( ) → for all ∈ C 1 , naturally in . Presheaves on C s,t coincide with C 1 /Δ because the presheaf construction turns lax colimits into lax limits. Notation 4.10. We often omit the isomorphism C 1 /Δ C s,t , considering it as an implicit coercion. E.g., for any ∈ C 0 , y may be used to denote the transition system with 1 = ∅ and 0 = y . Similarly, y may be used to denote the 'minimal' transition system with one transition over , say , i.e., 1 = y , 0 = y s( ) + y t( ) , and the map 1 → 0 s × 0 t uniquely determined by the element

( 1 (id s( ) ), 2 (id t( ) )) ∈ 0 (s( )) × 0 (t( )).
Finally, y : y s( ) → y and y : y t( ) → y denote the Yoneda embedding of the canonical morphisms and from the proof of Proposition 4.9.

By Yoneda, we thus have:

Corollary 4.11. For all , we have C(y , ) 1 ( ) and C(y , ) 0 ( ).

Notation 4.12. In the case of call-by-name -calculus, we call ⇓ the unique object coming from C 1 = 1.

Remark 4.13. Presheaves on C s,t intuitively have two dimensions, 0 and 1; the projection functor forgets dimension 1, while the left adjoint (Proposition 4.5) adds an empty dimension 1, thus lifting its 0-dimensional argument to a 1-dimensional object.

This dimensional intuition leads to the following useful observation on the forgetful functor.

Proposition 4.14. The forgetful functor C → C 0 preserves all limits and colimits, as well as image (in the sense of strong epi, mono) factorisations.

Proof. The forgetful functor C → C 0 is equivalent to the restriction functor C s,t → C 0 , which is both a left and right adjoint, hence preserves all limits and colimits. Finally, image factorisations are computed pointwise in presheaf categories (see, e.g., [ Here is a characterisation of fibrations which will be important. Let us recall that a weak pullback satisfies the same universal property as a pullback, albeit without uniqueness. Proposition 4.17. A morphism :

→ is a functional bisimulation iff the following diagram is a pointwise weak pullback.

1 1 0 s 0 s 1 0 s
Remark 4.18. Being a pointwise weak pullback means that all squares 1 ( ) 1 ( )

0 (s( )) 0 (s( )) ( 1 ) ( ) ( ) ( 0 ) s( )
should be weak pullbacks, for ∈ ob(C 1 ). This is weaker than being a weak pullback.

Proof of Proposition 4.17. By Yoneda, a lifting problem in C as below left is the same as a cone in C 1 as below right, and a lifting is the same as a mediating morphism to 1 . We now define general bisimulations, based on functional bisimulations. Usually, one considers bisimulation relations. Here, we generalise this a bit and consider arbitrary spans: Definition 4.19. A simulation is a span ← → whose left leg is a fibration. A bisimulation is a span of fibrations (equivalently, a simulation whose converse span is also a simulation).

A simulation (resp. bisimulation) relation is a relation which is a simulation (resp. bisimulation).

Remark 4.20. Of course, the relevant notion in our applications is substitution-closed bisimulation, to which we will come below.

Lemma 4.21. Simulation relations and bisimulation relations are stable under unions.

Proof. By symmetry, it is enough to deal with the case of simulation relations. Consider any family ( ↩→ × ) ∈ of simulation relations. By Proposition 1.7, their union is the image of their cotupling. But because the domain y s( ) of y is representable for all ∈ C 1 , any lifting problem y → lifts to a lifting problem y → , which in turn lifts to a lifting problem y → 0 , for some 0 ∈ . We then find a lifting for the latter because 0 is a simulation by hypothesis, which yields a lifting for the original. Proposition 4.22. For all , ∈ C, the full subcategory Bisim( , ) of spans between and which are bisimulations admits a terminal object ∼ , , called bisimilarity.

Proof. As a presheaf category by Proposition 4.9, C is well-powered, so we may consider the union ∼ , of all bisimulation relations, which is again a bisimulation by Lemma 4.21. Finally, ∼ , is terminal, because any bisimulation factors through its image ( ), which is again a bisimulation; as a bisimulation relation, ( ) thus embeds into ∼ , , hence we obtain a morphism ։ ( ) ↩→ ∼ , , which is unique by monicity of ∼ , ↩→ × .

Howe contexts for operational semantics

Operational semantics is a combination of syntax and transition systems, in the sense that it is about transition systems whose states form a model of a certain syntax. Our framework for operational semantics thus combines the frameworks of Fiore et al. [START_REF] Fiore | Abstract syntax and variable binding[END_REF] for syntax with variable binding, and of §4 for transition systems.

In §5.1, we introduce the ambient setting for our framework, Howe contexts, which are pre-Howe contexts equipped with structure modelling substitution. Furthermore, for any Howe context and pointed strong endofunctor Σ 0 on C 0 , we introduce the category Σ 0 -Trans of transition Σ 0 -monoids, which are transition systems whose states form a Σ 0 -monoid. We prove that the forgetful functor Σ 0 -Trans → C is monadic.

In §5.2, we then introduce dynamic signatures over Σ 0 , which specify the dynamics of a transition system. The (dependent) pair (Σ 0 , Σ 1 ) then forms what we call an operational semantics signature. We then define the models of any such signature, called vertical Σ 1algebras. They form a category Σ 1 -alg v , and we prove that the forgetful functor Σ 1 -alg v → Σ 0 -Trans is monadic. We also prove that a suitably constrained construction of the initial Σ 1 -algebra is in fact vertical, yielding an initial vertical Σ 1 -algebra. Finally, we prove that, although both components are monadic, the composite functor Σ 1 -alg v → Σ 0 -Trans → C is not. 5.1. Transition monoid algebras. In this section, we introduce Howe contexts, and introduce transition Σ 0 -monoids, for any suitable endofunctor Σ 0 . Definition 5.1. A Howe context consists of a pre-Howe context s, t : C 1 → C 0 , together with a monoidal structure on C 0 , such that the tensor preserves all colimits on the left and filtered colimits on the right. Notation 5.2. As for pre-Howe contexts, we let

C := C 1 /Δ.
Let us assume that some syntax has been specified by a finitary, pointed strong endofunctor Σ 0 on C 0 . We then define transition Σ 0 -monoids just as in §3.

Definition 5.3. The category Σ 0 -Trans of transition Σ 0 -monoids is the following pullback in CAT.

Σ 0 -Trans Σ 0 -Mon C C 0 (-) 0 0
When Σ 0 is the constantly empty endofunctor, we speak of transition monoids: they consist of objects equipped with monoid structure on 0 .

We are now interested in computing initial Σ 0 -monoids. For this, we abstract over the concrete Proposition 3.2, as follows, replacing [F, Set] with any suitable category 0 .

Proposition 5.4 [FPT99, FS17, BHL20]. For any finitary, pointed strong endofunctor Σ 0 on a monoidal, cocomplete category 0 such that the tensor preserves all colimits on the left and filtered colimits on the right, the forgetful functor 0 : Σ 0 -Mon → 0 is monadic, and the free Σ 0 -algebra over (equivalently the initial ( + Σ 0 )-algebra) is an initial Σ 0 -monoid.

Proof. This has been proved in Coq [START_REF] Borthelle | A cellular Howe theorem[END_REF].

Notation 5.5. We denote the initial Σ 0 -monoid by Z Σ 0 , or Z 0 for short.

Using this, we obtain the following.

Proposition 5.6. The adjunction between C and C 0 (Proposition 4.5) lifts to an adjunction

Σ 0 -Mon ⊥ Σ 0 -Trans ℳ with • (ℳ( 0 )) = 0 and
• the left adjoint ℳ maps any Σ 0 -monoid to the discrete transition system on , equipped with the original Σ 0 -monoid structure on . (In particular, we have

ℳ( 0 ) 1 = ∅.)
Proof. This directly follows from the next lemma.

Lemma 5.7. Let us consider any pullback

A C B D
in CAT such that is monadic, say with left adjoint : D → C, and has a left adjoint with identity unit = id : → . Then, admits a left adjoint with identity unit, such that the canonical natural transformation → is an identity.

Proof. First of all by the triangle identities ,

( )
we have ( ) = id and = id (5.1) for all and .

Similarly, we have = id D (5.2) not only on objects but also on morphisms, since by naturality of we have for any : → ′ :

= • = ′ • = .
Let us furthermore assume w.l.o.g. that the pullback is constructed in the standard way, using compatible pairs.

We then define ( ) = ( ( ), ), which is legitimate since ( ) = ( ) by hypothesis. To prove the universal property, assume given ( ′ , ′ ) such that ( ′ ) = ( ′ ), and a morphism :

→ ( ′ , ′ ) = ′ in C. Then, letting ( ) : ( ) → ′ denote the transpose of ( ) ( ) ----→ ( ′ ) = ( ′ )
, we have by (5.1) and (5.2)

( ( )) = ( ′ • ) = = , so (
( ), ) : ( , ) → ( ′ , ′ ) in the pullback A. Furthermore, the desired triangle

( , ) ( ′ , ′ ) = C' ( ( ), )=
commutes as desired, trivially. Finally, any ( , ℎ) : ( , ) → ( ′ , ′ ) making it commute must satisfy ℎ = and = ℎ = . But : = → ′ is the transpose of , so must conversely be the transpose of = , and hence ( , ℎ) = ( ( ), ), proving the desired uniqueness property.

It remains to prove that the canonical natural transformation

= = -----→
is an identity. But by construction = ( , ) = , and = id by (5.1), hence the result.

Remark 5.8. The names, ℳ and , stand for "monter" and "descendre", "go up" and "go down" in French.

Proposition 5.9. The forgetful functor : Σ 0 -Trans → C is finitary and monadic.

Proof. This follows from the fact that transition Σ 0 -monoids are the algebras of an equational system over C in the sense of Fiore and Hur, to which [FH09, Theorem 6.1] applies.

Notation 5.10. We denote by ℒ the left adjoint to . 5.2. Operational semantics signatures. Similarly, we define abstract dynamic signatures, which abstract over those of Definition 3.19: Definition 5.11. Given a Howe context s, t : C 1 → C 0 and a pointed strong

Σ 0 : C 0 → C 0 , a dynamic signature Σ 1 = (Σ 1 , Σ 1 ) over Σ 0 consists of a finitary functor Σ 1 : Σ 0 -Trans → C 1 , together with a natural transformation Σ 1 with components Σ 1 ( ) → Σ 0 ( 0 )s × 0 t.
Let us pack up the static and dynamic notions of signature.

Definition 5.12. An operational semantics signature (Σ 0 , Σ 1 ) on a given Howe context s, t : C 1 → C 0 consists of a pointed strong endofunctor Σ 0 preserving sifted colimits, together with a dynamic signature Σ 1 over it.

Remark 5.13. Preservation of sifted colimits [START_REF] Adámek | What are sifted colimits? Theory and Applications of Categories[END_REF] is stronger than finitarity for Σ 0 . We need it for Lemma 9.51 below. In a presheaf category like C 0 , if Σ 0 preserves pullbacks (for example, by familiality), it is equivalent to being finitary and preserving all epis, as seen from the proof of [ARV10b, Theorem 18.1]. In [START_REF] Borthelle | A cellular Howe theorem[END_REF], we mistakenly only require Σ 0 to be finitary, which yields a gap in the proof of [BHL20, Lemma 5.13].

Example 5.14. The endofunctor Σ 0 ( ) ( ) = ( + 1) + ( ) 2 on [F, Set] preserves sifted colimits. This easily follows from the fact that sifted colimits are the ones commuting with products in sets.

Let us now introduce the models of a dynamic signature. We start by fixing, for the rest of this section, an operational semantics signature (Σ 0 , Σ 1 ) on a Howe context s, t : C 1 → C 0 .

Definition 5.15. Let Σ1 : Σ 0 -Trans → Σ 0 -Trans map any transition Σ 0 -monoid to the composite

Σ 1 ( ) (Σ 1 ) -----→ Σ 0 ( 0 )s × 0 t 0 s× 0 t --------→ 0 s × 0 t,
where 0 denotes the Σ 0 -algebra structure of 0 .

Proposition 5.16. The endofunctor Σ1 is finitary and makes the following triangle commute.

Σ 0 -Trans Σ 0 -Trans

Σ 0 -Mon Σ1 Proof.
Commutativity of the triangle holds by construction, and finitarity follows from finitarity of Σ 1 .

Definition 5.17. A Σ1 -algebra structure Σ1 ( ) → on an object ∈ Σ 0 -Trans is vertical when its image under the forgetful functor Σ 0 -Trans → Σ 0 -Mon is the identity. Let Σ 1 -alg v denote the full subcategory of Σ1 -alg spanned by all vertical algebras.

Theorem 5.18. The forgetful functor Σ 1 -alg v → Σ 0 -Trans is monadic, and furthermore the initial Σ1 -algebra Z Σ1 , or Z for short, may be chosen to be vertical, hence is also initial in Σ 1 -alg v .

Proof. For the first statement, vertical algebras may be specified as an equational system, in the sense of [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF], so the result follows by [FH09, Theorem 6.1]. For the second statement, Z is the colimit of the initial chain

Z 0 ! - → Σ1 (Z 0 ) Σ1 (!)
----→ . . .

Σ -1 1 (!) ------→ Σ 1 (Z 0 ) → . . .
(where Z 0 is shorthand for ℳ(Z 0 ), for readability, which is initial in Σ 0 -Trans, by Proposition 5.6). The image of this chain in Σ 0 -Mon is the everywhere-identity chain on Z 0 .

By construction, we have:

Proposition 5.19. We have (Z) = Z 0 .

Let us readily annihilate any hope that vertical Σ 1 -algebras are monadic over C.

Lemma 5.20. Consider the operational semantics signature of -calculus with Σ 0 from (3.2) and Σ 1 from Example 3.20. Then, the composite forgetful functor Σ 1 -alg v → Σ 0 -Trans → C is not monadic.

Proof. Let us draw inspiration from the classical example of a non-monadic composite of monadic functors [BW05, p. 107], namely the composite Cat → RGph → Set, where RGph denotes the category of reflexive graphs, and the forgetful functor to sets returns the set of arrows. One may show that both functors are monadic, but that their composite is not. By Beck's monadicity theorem [Mac98, Theorem VI.7.1], it suffices to find a parallel pair ⇒ in Cat whose image in sets admits an absolute coequaliser, and show that this coequaliser is not created by the composite forgetful functor. The idea is to take to consist of two arrows 1 -→ 2 3 -→ 4, and = 1 + to have an additional object, say 0. We then define , : → to be the identity on , and respectively map 0 to 2 and 3. The coequalisers in Cat (top) and Set (bottom) look as follows, abbreviating each id to just for readability.

0 1 2 3 4 1 2 3 4 1 {2, 3} 4
0 1 2 3 4 1 2 3 4 1 {2, 3} 4 • /
One easily proves that the one in sets is split, hence absolute. Because of the composite arrow • that the coequaliser in Cat must have but the one in sets does not, the coequaliser is not created by the forgetful functor, thus contradicting monadicity.

For proving the lemma, we rely on the -rule to mimick composition in constructing the following parallel pair ⇒ in Σ 1 -alg v .

• is the vertical Σ 1 -algebra defined as the -calculus extended with two constants and , unary operations and , and an axiom ⇓ ( ); • is the vertical Σ 1 -algebra extending with a constant ; • the Σ 1 -algebra morphisms , : → respectively map to and ( ). ( )) ] has a unique representative, namely ( . ( )) , whose evaluation in gets stuck at ( ). However, the coequaliser in Σ 1 -alg v does have such a reduction by applying the -rule:

[ . ( )] ⇓ [ ( )] [ ( )] = [ ] ⇓ [ ( )] [( . ( )) ] ⇓ [ ( )] •
Thus, the coequaliser is not created by the forgetful functor.

Finally, this coequaliser is split (hence absolute): the morphism : → mapping to ( ) has a section : → , which maps ( ) to , and the coequaliser arrow : → has a section : → mapping ( ) to . It is straightforward to check that this indeed defines a split coequaliser, i.e., that • = • .

Remark 5.21. A crucial point is that may (and does) map and to themselves (the latter being necessary to preserve the target of ( . ( )) ⇓ ( )), and ( ) to ≠ ( ). Indeed, lives in C, as opposed to Σ 0 -Trans, hence need not preserve substitution. All that is required is naturality. But ( ), being closed, cannot be the target of any transition, and by induction cannot be the source of any transition either, hence the result.

Also, let us stress that in , ( . ( )) does not evaluate, since ( ) itself does not. Similarly, in , which is not saturated by the evaluation rules, we do have the premises ( . ( )) ⇓ ( ) and ( ) = ⇓ ( ), but not the conclusion ( . ( )) ⇓ ( ).

Substitution-closed bisimilarity

We have now introduced our notion of syntactic transition system, given by Σ 0 -transition monoids in a Howe context, and explained how to generate such systems from operational semantics signatures. In this section, we incorporate substitution into the notions of bisimulation and bisimilarity introduced in §4.3, which yields substitution-closed bisimilarity. We then state our main theorem, for which we include a high-level proof sketch.

In order to introduce substitution-closed bisimilarity, we first lift the notion of bisimulation to Σ 0 -monoids, generalising §3.4: Definition 6.1. A morphism in Σ 0 -Trans is a functional bisimulation iff its underlying morphism in C is. A span is a simulation iff its left leg is a functional bisimulation, and a bisimulation iff both of its legs are functional bisimulations.

Let us readily prove the following characterisation by lifting, recalling from Notation 5.10 that ℒ : C → Σ 0 -Trans is left adjoint to the forgetful functor. As seen in Example 3.16, we now want to go beyond bisimilarity, and introduce abstract versions of substitution-closed bisimulation and bisimilarity. For this, let us give the general definition of modules over a monoid. Definition 6.3. For any monoid in a monoidal category , let -Mod denote the category of algebras for the monad -⊗ .

An -module thus consists of an object equipped with an action ⊗ → of satisfying straightforward coherence conditions. Example 6.4.

itself is an -module, with action given by multiplication.

Before going into substitution-closed bisimulation, let us record the following useful properties of modules in a Howe context. Proposition 6.5. In any Howe context, for all monoids in C 0 ,

• the forgetful functor -Mod → C 0 creates all limits and colimits, and furthermore • the category -Mod is regular and the forgetful functor -Mod → C 0 creates image factorisations.

Proof. For creation of limits and colimits:

• As algebras for the monad -⊗ , -modules are closed under limits.

• They are also closed under all types of colimits preserved by -⊗ , i.e., all of them by definition of Howe contexts. Thus, -Mod is complete and cocomplete, hence regularity reduces to showing that the pullback of any regular epi is again a regular epi. So let us consider any pullback square in -Mod, with a regular epi, and show that must also be a regular epi. By creation, hence preservation, of limits and colimits, the given pullback square is also a pullback in C 0 and is a regular epi there too. So by regularity of the presheaf category C 0 , is a regular epi in C 0 . Equivalently, it is a coequaliser of its kernel pair. But by creation of limits the kernel pair uniquely lifts to a kernel pair in -Mod, and by creation of colimits is a coequaliser there too. This shows that -Mod is regular. Finally, given , ∈ -Mod, let us consider any image factorisation in C 0 of a morphism : → in -Mod, i.e., is a regular epi and is a mono in C 0 . In this situation, is the coequaliser of its kernel pair in C 0 , but, as we just saw, this kernel pair lifts to a kernel pair in -Mod, whose coequaliser is created by the forgetful functor, hence is a coequaliser, hence a regular epi in -Mod. Finally, also coequalises the kernel pair, hence the existence of a unique mediating morphism → in -Mod, which must be by faithfulness of the forgetful functor -Mod → C 0 . Thus, is also a morphism in -Mod. Finally, its monicity follows again by faithfulness of the forgetful functor.

Let us now introduce substitution-closed spans, first in an arbitrary monoidal category, and then in a Howe context. This then leads us to substitution-closed bisimulation. Definition 6.6. In a monoidal category with binary products, given a monoid and -modules and , a substitution-closed span is a span : → × equipped withmodule structure : ⊗ → on , such that : → × is an -module morphism.

The last condition is equivalent to commutation of the following diagram.

⊗ ( × ) ⊗ ( ⊗ ) × ( ⊗ ) × ⊗ 1 ⊗ , 2 ⊗ ×
Definition 6.7. Consider any Howe context s, t : C 1 → C 0 and transition monoid ∈ C. Let , ∈ C be equipped with 0 -module structure on 0 and 0 . A substitution-closed span is a span → × equipped with substitution-closed structure on 0 → 0 × 0 . Definition 6.8. For any Howe context s, t : C 1 → C 0 and transition monoid ∈ C, a substitution-closed simulation (resp. bisimulation) is a substitution-closed span → 2 (viewing 0 itself as an 0 -module by Example 6.4) which is a simulation (resp. bisimulation). Let Bisim ⊗ ( ) denote the full subcategory of C/ 2 spanned by substitution-closed bisimulations.

Let us now prove the existence of substitution-closed bisimilarity. Lemma 6.9. Substitution-closed simulation and bisimulation relations are stable under unions.

Proof. By Lemma 4.21, the union of a family of substitution-closed simulation (resp. bisimulation) relations is again a simulation (resp. bisimulation) relation. But by Proposition 6.5, the union in C is again substitution-closed, which concludes the proof. Proposition 6.10. For any Howe context s, t : C 1 → C 0 and monoid ∈ C, the category Bisim ⊗ ( ) of substitution-closed bisimulations over admits a terminal object ∼ ⊗ , called substitution-closed bisimilarity.

Proof. Straightforward generalisation of the proof of Proposition 4.22 using the lemma. Notation 6.11. When = Z, we abbreviate ∼ ⊗ Z to just ∼ ⊗ . We now want to state the abstract version of our main theorem, but we need an additional hypothesis, which we now introduce. The idea is essentially that Σ 1 should preserve functional bisimulations, which does not quite make sense, because the codomain of Σ 1 is C 1 , where no notion of functional bisimulation has been defined yet. Recalling Proposition 4.17, we work around this as follows. Definition 6.12. A dynamic signature Σ 1 = (Σ 1 , Σ 1 ) preserves functional bisimulations iff for any functional bisimulation : → in Σ 0 -Trans, the following square is a pointwise weak pullback.

Σ 1 ( ) Σ 1 ( ) Σ 0 ( 0 )s Σ 0 ( 0 )s Σ 1 ( ) 1 •(Σ 1 ) Σ 0 ( 0 )s 1 •(Σ 1 ) (6.1)
Remark 6.13. It may not be obvious that the dynamic signature for call-by-namecalculus preserves functional bisimulations. We will come back to this in §7 by showing that it satisfies a sufficient condition, cellularity.

Remark 6.14. It may seem linguistically inappropriate to say that Σ 1 preserves functional bisimulations, since Σ 1 is not merely a functor, and we have not even defined fibrations in the codomain category C 1 anyway. We will justify the terminology in Proposition 7.8, but for now let us move on directly to the main result.

Theorem 6.15. If Σ 1 preserves functional bisimulations, then substitution-closed bisimilarity is context-closed. More precisely, ∼ ⊗ is a transition Σ 0 -monoid, and ∼ ⊗ → Z 2 is a transition Σ 0 -monoid morphism.

Proof sketch (see §9 for the full proof ). The proof takes inspiration from Howe's original method.

1. We first define the Howe closure 0 of substitution-closed bisimilarity ∼ ⊗ 0 on states as the initial Σ 0 -monoid for the pointed strong endofunctor Σ 0 on C 0 /Z 2 defined by Σ 0 ( ) = Σ 0 ( )+( ; ∼ ⊗ 0 ). We then show that, by construction, 0 is a Σ 0 -monoid and both projections are Σ 0 -monoid morphisms.

2. We then define the transition Howe closure of (the full) substitution-closed bisimilarity ∼ ⊗ , as an initial algebra for an endofunctor Σ 1 on a suitable category C Z . Very roughly, C Z is the category of spans → Z 2 whose projection is precisely 0 → Z 2 0 , and Σ 1 ( ) = Σ1 ( ) + ( ; ∼ ⊗ ). We show: Lemma 6.16. There exists a span morphism i : ∼ ⊗ → .

Next comes the key lemma:

Lemma 6.17. If Σ 1 preserves functional bisimulations, then the transition Howe closure is a substitution-closed simulation.

Remark 6.18. Since 0 is a Σ 0 -monoid by construction, is easily seen to be substitutionclosed, so the lemma really is about it being a simulation.

The key lemma is proved by characterising as an initial algebra for a different endofunctor on a different category, whose initial chain involves iterated applications of Σ 1 (preserving simulations by hypothesis) to 1 : ℳ( 0 ) → ℳ(Z 0 ), which is trivially a simulation.

4.

In the standard proof method, the next step is to prove that the transitive closure of 0 is symmetric. But in our case 0 is a general span, not a relation. In order to avoid some coherence issues, we introduce a suitable notion of relational transitive closure for general spans, denoted by -+ , which is equipped with a canonical map i + : → + for each span . We then show: Lemma 6.19. The relational transitive closure 0 + of the Howe closure 0 on states is symmetric.

As substitution-closed simulations are closed under transitive closure, we obtain Corollary 6.20. + is a substitution-closed simulation which is symmetric on states.

We then use the following lemma (proved in §9.7). Lemma 6.21. For any substitution-closed simulation such that 0 is symmetric, there exists a substitution-closed bisimulation ′ and a span morphism i ′ : → ′ .

By terminality of ∼ ⊗ , we thus get a unique morphism ! +′ : + ′ → ∼ ⊗ over Z 2 .

From the chain

∼ ⊗ i --→ i + --→ + i ′ -→ + ′ ! +′ ---→ ∼ ⊗
we get by terminality that ∼ ⊗ is a retract of a transition Σ 0 -monoid, namely . The result then readily follows from monadicity of transition Σ 0 -monoids (Proposition 5.9) and the following result, taking = , = ∼ ⊗ , and = Z 2 . Lemma 6.22. Consider a monad : → on any category , -algebras and , and morphisms in such that the composite is a -algebra morphism, is a split epi, and is monic. Then there is a unique -algebra structure on such that and both are -algebra morphisms.

Proof. Let : → denote any section of . The desired structure is given by

( ) ( ) ----→ ( ) → ,
where the middle morphism is the given -algebra structure on , and the rest follows by monicity of .

Preservation of functional bisimulations, and cellularity

Let us now consider the main hypothesis of Theorem 6.15, preservation of functional bisimulations. In §7.1, we rephrase the condition in a way that makes more sense linguistically, i.e., by an actual preservation condition. We then work towards a characterisation in terms of cellularity. In §7.2, we first briefly recall familial functors [Die78, CJ95, Web07a], and show that the operational semantics signature for call-by-name -calculus gives rise to two familial functors, in a suitable sense. In §7.3, we restrict attention to the case where both components of the dynamic signature give rise to familial functors in this sense, and show that preservation of functional bisimulations is then equivalent to a cellularity condition [GH18, BHL20], which itself comes with a useful sufficient condition.

7.1. An alternative characterisation. Let us first give an alternative definition of dynamic signatures.

Definition 7.1. Let C 1 /Δ s denote the following lax limit category.

C 1 /Δ s C 0 C 1 2 1 Δ s
Concretely, an object consists of presheaves 1 and 0 , together with a morphism 1 → 0 s. Just as C, C 1 /Δ s is in fact a presheaf category:

Proposition 7.2. The category C 1 /Δ s is isomorphic to the presheaf category over the lax colimit C s of the functor s : C 1 → C 0 , as in

C 1 C 0 C s . s 1 0
Proof. Similar to Proposition 4.9.

Remark 7.3. Concretely, C s is the coproduct of C 0 and C 1 , augmented with morphisms : s( ) → for all ∈ C 1 , naturally in .

Notation 7.4. In the case of call-by-name -calculus, as in C (Notation 4.12), we call ⇓ the unique object coming from C 1 = 1.

Definition 7.5. For any operational semantics signature (Σ 0 , Σ 1 ), let Σ s 1 : Σ 0 -Trans → C 1 /Δ s map any 1 → 0 s × 0 t to the first leg Σ 1 ( ) → Σ 0 ( 0 )s of (Σ 1 ) .

Proposition 7.6. For any operational semantics signature (Σ 0 , Σ 1 ), the functor Σ s 1 : Σ 0 -Trans → C 1 /Δ s is finitary, and makes the following diagram commute,

Σ 0 -Trans C 1 /Δ s Σ 0 -Mon C 0 C 0 Σ s 1 0 Σ 0 2 (7.1)
where 2 , as in Definition 7.1, maps any object 1 → 0 s to 0 .

Proof. Finitarity holds because it does pointwise, by assumption. The diagram commutes by construction.

In C s (or, through the isomorphism of Proposition 7.2, in C 1 /Δ s ), we may define functional bisimulations by analogy with Definition 4.15.

Definition 7.7. A morphism : → in C s is a functional bisimulation, or a fibration, iff it enjoys the (weak) right lifting property w.r.t. y : y s( ) → y , for all ∈ C 1 .

Proposition 7.8 (Price for our linguistic mischief). A dynamic signature preserves functional bisimulations (Definition 6.12) iff the induced functor Σ s 1 : Σ 0 -Trans → C 1 /Δ s does. Proof. The functor Σ s 1 maps any functional bisimulation : → to the square (6.1), and just as in Proposition 4.17 a morphism in C s is a functional bisimulation iff the corresponding square in C 1 is a pointwise weak pullback. 7.2. Familiality. In the previous sections, we have seen that functional bisimulations may be defined by lifting both in Σ 0 -Trans and C 1 /Δ s . We now want to exploit this to obtain a characterisation of preservation of functional bisimulations, which will then lead us to useful sufficient conditions.

For this, let us briefly recall familial functors, and show that the functors Σ 0 and Σ s 1 : Σ 0 -Trans → C 1 /Δ s induced by the dynamic signature for call-by-name -calculus are familial.

Familial functors are a generalisation of polynomial functors on sets, i.e., functors of the form ( ) = ∈ , where is a set of 'operations', and ∈ N is the 'arity' of any ∈ . We want to generalise this to presheaf categories.

Example 7.9. Consider for example the 'free category' monad on Gph. Analysing and abstracting over the definition of , we will arrive at the notion of familial functor. Let us first recall that graphs are presheaves over the category

[0] [1].
does not change the vertex set, and an edge of ( ) is merely a path in . Indexing this by the length of the path, we obtain

( ) [0] Gph(y [0] , ) and
( ) [1] Gph([ ],
), where [ ] denotes the filiform graph • → • . . . → • with edges (which is consistent with [0] and [1] through the Yoneda embedding). Furthermore, the source of a path [ ] → is obtained as the composite

[0] --→ [ ] → ,
where the first morphism selects the first vertex of the path. Similarly the target is obtained by precomposition with the morphism, say , selecting the last vertex.

From these observations, let us now explain how the whole of may be derived from • the graph (1), which generalises the set of operations, and • a functor el( (1)) → Gph, morally describing the arity of each operation, where we recall from MacLane and Moerdijk [MM92]:

Definition 7.10. The category of elements el( ) of a presheaf over any category C has pairs ( , ) with ∈ ( ) as objects, and a morphism ↾ ′ : ( , ) → ( ′ , ′ ) for all : → ′ such that ( ) ( ′ ) = .

The graph (1) has a single vertex, and as many paths as we can derive from a single endo-edge on this vertex: N, because there is one for each length. The category of elements of (1) thus looks like the following,

([1], 0) ([1], 1) ... ([1], ) ... ([0], ★) ↾0 ↾0 ↾1 ↾1 ↾ ↾
and the assignments

([0], ★) ↦ → [0] ([1], ) ↦ → [ ]
extend to a functor : el( (1)) → Gph by mapping each source or target map

([0], ★) → ([1], ) to the corresponding map [0] → [ ].
This functor may be visualised as

[0] [1] ... [ ] ... [0]. 0 0 1 1
The promised expression of in terms of (1) and is:

( ) ( ) ∈ (1) ( )
Gph( ( , ), ).

Definition 7.11. A functor : → C to some presheaf category is familial iff we have a natural isomorphism

( ) ( ) ∈ ( ) ( ( , ), ),
for some presheaf ∈ C and functor : el( ) → . The presheaf is called the presheaf of operations, or the spectrum [Die78] of , while is called the arity, or exponent functor.

Remark 7.12. This definition is a bit elliptic, so let us make functoriality more explicit.

• Functoriality in is by post-composition.

• For functoriality in , for any : → in C and ∈ ( ), letting ′ = • , we get a morphism ↾ : ( , ′ ) → ( , ) in el( ), hence a morphism ( ↾ ) : ( , ′ ) → ( , ).

Precomposition by this morphisms yields a map ( ( , ), ) → ( ( , ′ ), ).

Postcomposing with the obvious coproduct injections, and cotupling, we get the desired map

∈ ( ) ( ( , ), ) → ′ ∈ ( ) ( ( , ′ ), ).
Remark 7.13. If has a terminal object, we always have (1).

Example 7.14. Let us show that the endofunctor Σ 0 : C 0 → C 0 from §3.1 for -calculus is familial, where we recall that C 0 = F op . Indeed, we then have

Σ 0 ( ) ( ) = ( + 1) + ( ) 2 C 0 (y +1 , ) + C 0 (2 • y , )
Thus, we choose:

( ) = {abs, app} ( , abs) = y +1 ( , app) = 2 • y .
These definitions can be straightforwardly upgraded to functors ∈ C 0 and : el( ) → C 0 , and we get the desired isomorphism.

Example 7.15. Let us now show that the functor Σ s 1 : Σ 0 -Trans → C 1 /Δ s for call-by-name -calculus is familial. By definition, it maps any to the set-map 0 (1)+ ( ) → Σ 0 ( 0 ) (0) defined in Example 3.20. Let us transfer this across the isomorphism C 1 /Δ s C s (recalling Remark 7.3), and show that Σ s 1 may be expressed as in Definition 7.11, first for ∈ F and then for =⇓.

For = ∈ F, we almost may proceed as for Σ 0 , except that the domain category has changed (from C 0 to Σ 0 -Trans). But recalling that ℒ : C → Σ 0 -Trans denotes the left adjoint to the forgetful functor , we have

Σ s 1 ( ) ( ) = Σ 0 (( ( )) 0 ) ( ) C(y +1 , ( )) + C(2 • y , ( )) Σ 0 -Trans(ℒ(y +1 ), ) + Σ 0 -Trans(ℒ(2 • y ), ),
so we may (partially) define

( ) = {abs, app} ( , abs) = ℒ(y +1 ) ( , app) = ℒ(2 • y ). (7.2)
Now, for =⇓, remembering from Notation 7.4 that we call ⇓ ∈ C s the unique object of C s coming from C 1 = 1, on transitions, we have:

Σ s 1 ( ) (⇓) = 0 (1) + ( ) C(y 1 , ( )) + ( ) Σ 0 -Trans(ℒ(y 1 ), ) + ( ).
We thus need to find such that ( ) Σ 0 -Trans( , ), and then we would complete equations (7.2) with:

(⇓) = { -val, -red} (⇓, -val) = ℒ(y 1 ) (⇓, -red) = .
Definition 7.16. The morphism ¯ : ℒ(y 0 ) → ℒ(y 1 + y 0 ) is defined as follows.

• We start from 1 ( 0 ) ∈ (ℒ(y 1 + y 0 )) (0), where we recall from the rules below Proposition 3.4 that the presheaf (ℒ(y 1 + y 0 )) (0) has as states -terms over a closed constant 0 , and a unary constant 1 . • We then let ¯ denote the mate of the morphism y 0 → (ℒ(y 1 + y 0 )) corresponding to 1 ( 0 ) by the Yoneda lemma. Let now denote the following pushout,

ℒ(y 0 ) ℒ(y 1 + y 0 ) ℒ(y ⇓ + y 0 ) ℒ(y ⇓ ) ¯ ℒ (y ⇓ ) ℒ (y ⇓ +y 0 ) 1 2
which exists because by Proposition 5.9 Σ 0 -Trans is the category of algebras for a finitary monad on a presheaf category, hence a locally finitely presentable category by [AR94, Remark in §2.78], hence cocomplete.

Let us now show that ( ) Σ 0 -Trans( , ) for any : as Σ 0 -Trans(-, ) turns colimits into limits, we have the pullback

[ , ] [ℒ(y ⇓ ), ] [ℒ(y ⇓ + y 0 ), ] [ℒ(y 1 + y 0 ), ] [ℒ(y 0 ), ], [ ¯ , ] [ℒ (y ⇓ ), ] [ℒ (y ⇓ +y 0 ), ]
where ¯ is as in Definition 7.16, and we abbreviate Σ 0 -Trans(-1 , -2 ) to [-1 , -2 ] for readability. By Yoneda, this reduces to

[ , ] (⇓) (⇓) × (0) (1) × (0) (0), ( ⇓ )× (0) ( ⇓ ) ( , )↦ → [ ]
which shows that we have ( ) [ , ] as desired. We have thus defined the actions of the functors ∈ C s and : el( ) → Σ 0 -Trans on objects. On morphisms, the only non-obvious point is the image of ⇓ ↾ -val and ⇓ ↾ -red. The former morphism is mapped to the identity on (0, abs) = ℒ(y 1 ) = (⇓, -val). The latter is mapped to the composite

ℒ(2 • y 0 ) ℒ (y ⇓ +y 0 ) --------→ ℒ(y ⇓ + y 0 ) 2 --→ . (7.3)
This achieves the desired isomorphism Σ s 1 ( ) ( ) ∈ ( ) Σ 0 -Trans( ( , ), ).

7.3. Cellularity. We now want to exploit familiality to obtain an alternative characterisation of preservation of functional bisimulations. The starting point is the observation that when a functor : → C is familial, say as ( ) ( ) = ∈ ( ) ( ( , ), ), then any morphism of the form : y → ( ), corresponding by Yoneda and familiality to some pair ( , ) with : ( , ) → , factors as

y ( ,id ( , ) ) ---------→ ( ( , )) ( ) ----→ ( ).
Furthermore, the first component ( , id ( , ) ) is easily seen to be generic, in the following sense.

Definition 7.17. Given any functor :

→ ℬ, a morphism : → ( ) is -generic (or generic for short) whenever for all , , and making the square below (solid) commute,

( ) ( ) ( ) ( ) ( ) ( )
there is a unique lifting (dashed) such that ( ) • = and • = .

In fact, we have the following important alternative characterisation of familial functors to presheaf categories. Proof. This is [GH18, Proposition 3.8], using the remark just before it.

Remark 7.19. The factorisation is essentially unique.

The characterisation of familiality in terms of generic morphisms allows us to characterise familial functors which preserve fibrations, as cellular functors, which we now introduce.

Definition 7.20. A category with generating cofibrations is a category equipped with a set J of morphisms.

For any such ( , J), as in §1.6, we call fibrations all morphisms in J ⋔ , and cofibrations all morphisms in ⋔ (J ⋔ ).

Example 7.21. In Σ 0 -Trans, with generating cofibrations consisting of all morphisms ℒ(y ), fibrations are precisely functional bisimulations, by Proposition 6.2.

Example 7.22. In C s , with generating cofibrations consisting of all morphisms y , fibrations are precisely functional bisimulations, by Definition 7.7. Definition 7.23. For any categories with generating cofibrations ( , J) and ( C, K), such that C is small and has a terminal object, a familial functor : → C is cellular iff for all commuting squares

( ) ( ) ( ) (7.4)
with ∈ K and and generic, is a cofibration (i.e., ∈ ⋔ (J ⋔ )).

Before exploiting cellularity as promised, let us briefly pause to give an equivalent characterisation of cellularity in suitably nice cases. By construction, for any and as in the definition, if y is a generating cofibration (i.e., is in K), then the diagram y y

( ( , • )) ( ( , )) y • ( ( , ↾ ))
is of the form (7.4) by construction. We thus have by definition:

Proposition 7.26. Let us consider any cellular : → C between categories with generating cofibrations ( , J) and ( C, K) such that C is small and has a terminal object. Then, for any representable morphism y : y → y in K, the -arity of any operation ∈ (1) ( ) is a cofibration. When all domains and codomains of generating cofibrations ∈ K are representable, say as y : y → y , then all generic morphisms : → ( ), with a codomain of some generating cofibration, are isomorphic to some y → ( ( , )), for some operation ∈

(1) ( ), and the morphism must then be isomorphic to ( , ↾ ) : ( , • ) → ( , ). We thus get a partial converse to Proposition 7.26: Proposition 7.27. For any categories with generating cofibrations ( , J) and ( C, K), such that C is small, has a terminal object, and all domains and codomains of generating cofibrations ∈ K are representable, a familial functor :

→ C is cellular iff the boundary arities of all operations are cofibrations.

Returning to the general case, let us now prove a first characterisation of preservation of fibrations in terms of cellularity.

Lemma 7.28. For any categories with generating cofibrations ( , J) and ( C, K) such that C is small and has a terminal object, a familial functor : → C preserves fibrations iff it is cellular.

Proof. Let us first prove the 'if' direction. We must show that for any : → in J ⋔ , ( ) is in K ⋔ , i.e., that any commuting square

( ) ( ) ( ) (7.5)
with ∈ K and ∈ J ⋔ admits a lifting. But taking generic factorisations of both horizontal morphisms and using genericness, any such square factors as the solid part of

( ) ( ) ( ) ( ). ( ) ( ) ( ) ( ) ( )
By cellularity, we have ∈ ⋔ (J ⋔ ). We thus find a lifting as shown, which makes ( ) • into a lifting for the original square.

Conversely, let us assume that preserves fibrations, and consider any square of the form (7.4) with ∈ K. We need to show ∈ ⋔ (J ⋔ ). But for any commuting square as below left

( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )
with ∈ J ⋔ , by pasting this square with our generic square (7.4), we obtain the solid part above right. Finally, because preserves fibrations, we find a lifting as shown, which by genericness of (and then ) yields the desired lifting .

Corollary 7.29. For any categories with generating cofibrations ( , J) and ( C, K), such that C is small, has a terminal object, and all domains and codomains of generating cofibrations ∈ K are representable, a familial functor :

→ C preserves fibrations iff the boundary arities of all operations are cofibrations.

Proof. By Proposition 7.27 and Lemma 7.28.

Here is the announced characterisation of preservation of functional bisimulations, which follows directly from Lemma 7.28 and Corollary 7.29.

Corollary 7.30. In any Howe context, for any operational semantics signature (Σ 0 , Σ 1 ), let Σ s 1 : Σ 0 -Trans → C s be familial with exponent : el(Σ s 1 (1)) → Σ 0 -Trans. Then the following are equivalent:

(i) Σ s 1 preserves functional bisimulations; (ii) Σ s 1 is cellular; (iii) the boundary arities of all operations are cofibrations, i.e., for all ∈ C 1 and ∈ Σ s 1 (1) ( ), the morphism

( ↾ ) : (s( ), • ) → ( , ) is a cofibration.
This characterisation of preservation of functional bisimulations in terms of cofibrations is easier to prove in practice, since cofibrations in turn admit the following well-known characterisation.

Definition 7.31. Consider any set J of maps in a given category.

• A basic relative J-cell complex is any morphism obtained by pushing out some morphism from J along any morphism, as in .

∈J

• A relative J-cell complex is a (potentially transfinite) composite of basic relative J-cell complexes.

Proposition 7.32 [Hov99, Lemma 2.1.10]. For any set J of maps in a locally presentable category, all relative J-cell complexes are cofibrations in the generated weak factorisation system ( ⋔ (J ⋔ ), J ⋔ ).

Applications

In this section, we apply our results to show that substitution-closed bisimilarity is a congruence in concrete examples.

8.1. Call-by-name. We have already specified the syntax ( §3.1) and transitions ( §3.3) of call-by-name -calculus. We have also seen (Example 7.15) that the induced functor Σ s 1 : Σ 0 -Trans → C 1 /Δ s is familial. By Theorem 6.15, Corollary 7.30, and Proposition 7.32, congruence of substitution-closed bisimilarity will follow if we prove that the boundary arities ( ⇓ ↾ ) corresponding to both transition rules are relative cell complexes.

The boundary arity ( ⇓ ↾ -val) is an identity, hence trivially a relative cell complex. For the -rule, it is not entirely trivial that the boundary arity ( ⇓ ↾ -red) of the second transition rule, defined as the composite (7.3), is a cofibration. But, as (essentially) noted in [BHL20, Example 5.21], it is a relative cell complex by construction, as both components are pushouts of ℒ(y ⇓ ), as should be clear from the following diagram, where again ¯ is as in Definition 7.16.

ℒ(y 0 )

ℒ(y ⇓ )

ℒ(y 0 + y 0 ) ℒ(y ⇓ + y 0 ) ℒ (y ⇓ +y 0 ) ℒ (y ⇓ +y 0 )• ¯ ℒ (y ⇓ )
8.2. Call-by-value. Let us now treat the call-by-value variant of untyped -calculus, essentially as in [START_REF] Ong | The concurrent lambda calculus I: A general precongruence theorem for applicative bisimulation[END_REF][START_REF] Pitts | Howe's method for higher-order languages, chapter 5[END_REF]. In this setting, it is important to distinguish substitution by values and by terms. Indeed, letting denote the identity . , the terms = . and ′ = .(( . ) ) are contextually equivalent, since during evaluation in any context, the bound variable will only be replaced with a value. However, if one defines applicative bisimulation naively, i.e., requiring it to be closed under arbitrary substitution, then and ′ are not bisimilar, as is not bisimilar to ( . ) Ω -which diverges. We thus want to restrict to value substitution -which our treatment in [START_REF] Borthelle | A cellular Howe theorem[END_REF] overlooks! Here is one way of doing this. The idea is to have two sorts, one for values and the other for general terms. We thus would like C 0 to be equivalent to the category [Set 2 , Set 2 ] of finitary endofunctors on Set 2 . But

[Set 2 , Set 2 ] ≃ [2 • Set 2 , Set] ≃ [2 • F 2 , Set],
so we take C 0 to be the opposite of 2 • F 2 . By the equivalence, composition of finitary endofunctors equips C 0 with monoidal structure, and we denote the two sorts by p and v, respectively for "programs" and "values". In the presheaf point of view, we denote by ( , ) p and ( , ) v , respectively, objects in the first and second term of 2 × F 2 = F 2 + F 2 , so that ( , ) ( ) in the finitary endofunctor world corresponds to ( , ) in the presheaf world, for ∈ {v, p}. We think of ( , ) v (resp. ( , ) p ) as a set of values (resp. programs) with potential free program variables, and potential free value variables.

Since abstraction should bind a value variable, the syntax

, ::= | ::= | .
is thus specified by

Σ 0 ( ) ( , ) (p) = ( , ) (p) 2 + ( , ) (v) and Σ 0 ( ) ( , ) (v) = ( , + 1) (p).
A model of the syntax should thus in particular feature operations abs , :

( , + 1) (p) → ( , ) (v) app , : ( , ) (p) 2 → ( , ) (p) val , : ( , ) (v) → ( , ) (p),
where the last operation requires that values should embed into programs. Notation 8.1. We implicitly view any ∈ [2 • F 2 , Set] as (some fixed, global choice of) the corresponding functor Set 2 → Set 2 . In particular, we write ( ), for any ∈ Set 2 . Accordingly, we view pairs ( , ) as objects of Set 2 . E.g., in this sense, ( , +1) is isomorphic to ( , ) + y v , where y v denotes the Yoneda embedding of v along 2 → F 2 ↩→ Set 2 . So the arity for abstraction in fact yields an operation

( + y v ) (p) → ( ) (v).
Denoting composition of finitary endofunctors by ⊗, we define a pointed strength for Σ 0 as follows. For any ∈ C 0 , ∈ / C 0 , and ∈ F 2 : • at p, we have

(Σ 0 ( ) ⊗ ) ( ) (p) = ( ( )) (p) 2 + ( ( )) (v) = Σ 0 ( ⊗ ) ( ) (p),
so we take , , ,p to be the identity;

• at v, we have (Σ 0 ( ) ⊗ ) ( ) (v) = ( ( ) + y v ) (p)
and Σ 0 ( ⊗ ) ( ) (v) = ( ( + y v )) (p), so we define , , ,p by applying (-) (p) to the copairing of ( ) → ( + y v ) and y v → ( + y v ) → ( + y v ).

We then specify transitions, which we first recall:

1 . ⇓ 1 ⇓ ′ 1 2 ⇓ ′ 2 ′ 1 [ 1 . ′ 2 ] ⇓ 3 1 2 ⇓ 3 • Remark 8.2.
Here, we adopt the same convention as in the categorical picture, where terms are implicitly considered as indexed over sets, say { 1 , . . . , }, of potential free variables. Furthermore, the evaluation relation again relates closed terms to terms over one potential free variable 1 .

In order to specify such transitions, we take C 1 = 1, as in the call-by-name case, with s and t mapping the unique object to (0, 0) p and (0, 1) p , respectively: transitions will relate a closed program to a program with one value variable (morally the body of the obtained abstraction). For any ∈ C = C 1 /Δ Set/Δ, We take Σ 1 ( ) to be the coproduct

Σ 1 ( ) = 0 (0, 1) + ( ),
where ( ) denotes the set of valid premises for the second rule, i.e., triples

( 1 , 2 , 3 ) ∈ 1 such that 3 • ⇓ = ( 1 • ⇓ ) [ ( 2 • ⇓ )].

Familiality of the induced functor Σ s

1 : Σ 0 -Trans → C 1 /Δ s follows similarly to the callby-name case, from the fact that ( ) is isomorphic to [ , ], where denotes the following pushout.

ℒ(y 0 ) ℒ(y ⇓ ) ℒ(y ⇓ + y ⇓ ) ℒ (y ⇓ )
Here, corresponds by adjunction and Yoneda to the closed term

( 1 • ⇓ ) [ ( 2 • ⇓ )] ∈ (ℒ(y ⇓ + y ⇓ )) (0),
where 1 and 2 denote the two transition constants generating y ⇓ + y ⇓ . By Theorem 6.15, Corollary 7.30, and Proposition 7.32, congruence of substitutionclosed bisimilarity will follow if we can prove that boundary arities ( ↾ ) of both transition rules are relative cell complexes. This is again trivial for the first rule, while for the second one we obtain the following morphism, which is a relative cell complex by construction.

ℒ(y 0 ) ℒ(y ⇓ ) ℒ(y 0 + y 0 ) ℒ(y ⇓ + y ⇓ ) ℒ (y ⇓ +y ⇓ ) ℒ (y ⇓ )
8.3. Erratic non-determinism. In this section, we consider the non-deterministiccalculus investigated in [San94, §7]. Its syntax is that of pure -calculus, augmented with a unary operation ⊎, and its reduction rules [San94, on pages 125 and 142] are

⊎ ⇒ ⊎ ⇒ Ω ( . ) ⇒ [ ] 1 ⇒ 3 1 2 ⇒ 3 2 ⇒ 1 ⇒ 2 2 ⇒ 3 1 ⇒ 3 ,
where Ω denotes any diverging term. Let us start by giving a big-step presentation of this language. We consider a labelled transition relation, i.e., we have two transition relations ⇓ (between a closed term and a term with one free variable, as before) and ⇓ (between closed terms), inductively generated by the following rules.

⊎ ⇓ ⊎ ⇓ Ω . ⇓ 1 ⇓ 3 3 [ 2 ] ⇓ 4 1 2 ⇓ 4 1 ⇓ 3 3 [ 2 ] ⇓ 4 1 2 ⇓ 4 1 ⇓ 3 1 2 ⇓ 3 2 ⇓ 1 ⇓ 2 2 ⇓ 3 1 ⇓ 3 1 ⇓ 2 2 ⇓ 3 1 ⇓ 3 •
We have:

Proposition 8.3. A relation is an applicative bisimulation in Sangiorgi's sense, say a Sangiorgi bisimulation, iff its open extension is a substitution-closed bisimulation with the new rules.

Proof. This is an easy corollary of the following lemma.

Lemma 8.4. For all closed 1 and 2 , and 3 with one potential free variable, we have

• 1 ⇒ 2 iff 1 ⇓ 2 , and • 1 ⇒ ( 3 ) iff 1 ⇓ 3 .
Proof.

• All reduction rules also occur as some new rule for ⇓ , except the -rule, which is easily derivable. We thus have ⇒ ⊆ ⇓ . • Similarly, if 1 ⇒ ( 3 ), then by the previous point 1 ⇓ ( 3 ), hence by the last rule

1 ⇓ 3 .
• Finally, let us prove both converse statements in one go by induction on the transition proof.

-The first two axioms also are axioms in the original rules, hence easy.

-For the third axiom, we are given ( ) ⇓ , hence clearly ( ) ⇒ ( ) as desired.

-For the first rule, 1 = 4 5 , and we know by induction hypothesis that 4 ⇒ ( 6 ) and 6 [ 5 ] ⇒ ( 3 ). We thus get 4 5 ⇒ ( 6 ) 5 ⇒ 6 [ 5 ] ⇒ ( 3 ), hence the desired result. -The second rule is similar, except that we get a chain 4 5 ⇒ ( 6

) 5 ⇒ 6 [ 5 ] ⇒ 2 .
-The next three rules also occur as original rules, hence are easily dealt with by induction hypothesis. -For the last rule, we have by induction hypothesis 1 ⇒ 4 and 4 ⇒ ( 3 ), hence 1 ⇒ ( 3 ), as desired. The syntax is easily modelled by taking Σ 0 ( ) ( ) = ( + 1) + ( ) 2 + ( ), and the new rules are easily seen to fit into a Σ 1 such that Σ s 1 preserves functional bisimulations by Corollary 7.30 and Proposition 7.32. Finally, substitution-closed bisimilarity in the initial model coincides with Sangiorgi's applicative bisimilarity, so we again deduce congruence of applicative bisimilarity by Theorem 6.15. 8.4. Howe's format. In this section, we show that, up to suitable encoding, our framework covers languages complying with a format proposed by Howe [How96, Lemma 6.1] -or rather a slight variant thereof (see Remark 8.27 below). We first introduce the format, and then explain how to embed it into our framework. The format illustrates in which sense cellularity is in particular an acyclicity condition. Furthermore, it would be easy, but much more verbose, to extend the format to a simply-typed setting; we refrain from doing so in this already quite long paper. 8.4.1. Recalling Howe's format. Regarding syntax, Howe's framework is parameterised by the choice between call-by-name and call-by-value. His signatures are then much like standard binding signatures [START_REF] Plotkin | An illative theory of relations[END_REF]. We model this in a setting similar to the call-by-value setting of §8.2, except that this time we build into the base category the fact that values embed into terms. Specifically, we work with the monoidal category

[Set 2 , Set 2 ] ≃ [2 × F 2 , Set],
where 2 denotes the walking arrow category v -→ p. We think of an object of the base category 2 × F 2 , which is a pair ( , : → ) with ∈ {v, p}, as the index of terms of sort , with value variables and program variables, each ( ) being thought as the program counterpart of ∈ .

Let us first explain how the syntactic part of Howe's format may be understood in terms of pointed strong endofunctors. Howe's notion of syntactic signature encodes a choice between call-by-value and call-by-name, through the choice of a distinguished sort, v or p. Notation 8.5.

• Given , ∈ F and ∈ {v, p}, we denote any object ( , ( -→ )) of 2 × F 2 by ( -→ ) , and the particular morphism ( , id) : ( -→ ) v → ( -→ ) p by .

• Given , ∈ F, we denote the object ( 1 --→ + ) of F 2 by ( , ). Otherwise said, we treat the corresponding embedding F 2 ↩→ F 2 as an implicit coercion.

• Accordingly, for any , ∈ F and ∈ {v, p}, we denote ( 1 --→ + ) by ( , ) .

• Given : 2 × F 2 → Set and ∈ {v, p}, we denote by : F 2 → Set the functor mapping ( -→ ) to ( -→ ) .

Remark 8.6. Through the equivalence [Set 2 , Set 2 ] ≃ [2 × F 2 , Set], composition of endofunctors becomes a monoidal product defined by

( ⊗ ) ( -→ ) = Lan ( ) ( ( -→ ) v --→ ( -→ ) p ),
where : F 2 → Set 2 is the canonical embedding. The unit is defined by

( v -→ p ) = .
for any object ( v -→ p ) . Intuitively, merely returns the set of variables of each sort. Terminology 8.8. For any operation ∈ p (resp. v ), the sequence ( p ,1 , . . . , p , p ) (resp. (0, . . . , 0, - ,1 , . . . , - , -), with + leading 0s) is called the (binding) arity of . Typically, -abstraction and pairing are value operations. The numbers + and -respectively count • active arguments which should be evaluated before reaching a value, as both arguments of the pairing operation, and • passive arguments which are not evaluated until the operation is destroyed, as the argument of a -abstraction. Active arguments are not allowed to bind any variable, hence the absence of a family + in signatures.

Despite their name, value operations may or may not return values, depending on the status of their arguments: a pair 1 , 2 is only a value when both 1 and 2 are. In order to generate the right syntax in our strongly-sorted setting, we need to introduce two with obvious action on morphisms, so that

el( ) = p • (F 2 ) op + v • (2 × F 2 ) op ,
• and as exponent the functor : el( ) → [2 × F 2 , Set] defined as the cotupling

[[ p ] ∈ p , [ v ] ∈ v ].
Proof. By mere calculation, using the Yoneda lemma.

Corollary 8.14. We have, for all ∈ [2 × F 2 , Set] and

( -→ ) ∈ F 2 , Σ 0 ( ) (( -→ ) p ) ∈ p [ p ( -→ ), ] + ∈ v [ v ( -→ ) p , ] and
Σ 0 ( ) ( -→ ) v ∈ v [ v ( -→ ) v , ].
We now describe the syntax generated by . Let 0 be the monad induced by the monadic forgetful functor

Σ 0 -Mon → [2×F 2 , Set].
In order to define the format, we need to unfold 0 ( ), for a coproduct of representable presheaves of the form y ( v , p ) . For a single such presheaf, by Proposition 3.4,

0 (y ( v , p ) ) = .( + Σ 0 ( ) + y ( v , p ) ⊗ ).
Unfolding the definition of tensor product (Remark 8.6), noticing that the hom-set [ , ′ ] • is empty iff = p and ′ = v, and • is otherwise a singleton, we obtain the following result.

Proposition 8.15. We have, for all v , p , , ∈ N, , ′ ∈ {v, p}, : 2 × F 2 → Set, and : → :

(y ( v , p ) ⊗ ) ( -→ ) ′ [ , ′ ] × p ( -→ ) p × v ( -→ ) v ∅ if = p and ′ = v p ( -→ ) p × v ( -→ ) v otherwise.
Remark 8.16. Intuitively, this will entail that 0 (y ( v , p ) ) extends the syntax generated by Σ 0 with a new operation taking p programs and v values as arguments, and returning a program or a value, depending on . As usual, if the output is a value, by action of , there is a corresponding program operation.

We now describe 0 ( ), for any coproduct of representable presheaves of the form y ( v , p ) . Let us first introduce some notations. Definition 8.17. A family of operation arities is a family = ( , , ) ∈ of triples ( , , ) ∈ N 2 × {v, p}. Notation 8.18. We think of any such triple = ( , , ) as an operation : v × p → , hence denote any such family by ( : v × p → ) ∈ . We in fact extend this notation by • writing v × p × , to denote either v + × p , when = v, or v × p + , when = p, • omittingif = 0 in the above product, e.g., v → denotes v × p 0 → , and finally Remark 8.20. Program operations ∈ p only have one list of arguments. Furthermore, they always return programs, so there is no need to annotate them. By contrast, value operations ′ ∈ v have two lists of arguments (active and passive arguments, see Terminology 8.8), and may return values or programs, depending on the status of their active arguments. Thus, e.g., any unannotated operation application ( 1 , . . . , ) must be a program operation application, while any annontated operation application ( 1 , . . . , ; 1 , . . . , ) must be a value operation application.

The action on morphisms is straightforward: for renaming, we rename (value and program) variables accordingly; for , we replace each v (resp. v ) with p (resp. p ). For morphisms → , we proceed similarly.

Terminology 8.21. We think of elements from as metavariables, while terms of the form or are mere variables.

Notation 8.22.

• Following [START_REF] Hamana | Free Σ-monoids: A higher-order syntax with metavariables[END_REF], for any ( : v × p → ) ∈ , we abbreviate ( v 1 , . . . , v ; 1 , . . . , ) to just when ( , ) is clear from context.

• For value operations , we sometimes omit the subscript in (. . .), when the expected sort is clear from context. • Similarly, we sometimes omit the exponent in variables .

• In metavariable application ( 1 , . . . , ′ ; 1 , . . . , ′ ), as well as in value operation application ( 1 , . . . , ; 1 , . . . , ), when one sequence is empty we omit it altogether, writing, e.g., ( 1 , . . . , ′ ) or ( 1 , . . . , ). When both lists are empty we simply write , resp. . Thus, e.g., may denote a nullary metavariable, or a non-nullary metavariable with identity substitution.

Let us now introduce Howe's notion of signature for evaluation rules, restricting attention to signatures satisfying the syntactic condition of [START_REF] Douglas | Proving congruence of bisimulation in functional programming languages[END_REF]Lemma 6 • a composable sequence of premises 0 An applicative bisimulation is an applicative simulation whose converse relation also is one.

1 ⇓ 1 ----→ 1 → . . . → -1 ⇓ ----
Applicative bisimulations are closed under union, and we let ∼ , , or ∼ for short, denote the largest one.

Finally, the open extension • of a relation is the largest substitution-closed relation contained in on closed programs and values.

Remark 8.30. By definition, being a subobject of the injection 0 (∅) (0, 0) v ↩→ 0 (∅) (0, 0) p in Set 2 , any applicative simulation is such that for any related values v ′ , and ′ should also be related as programs, i.e., • p • ′ . 8.4.2. Congruence by encoding in our framework. We now want to prove using Theorem 6.15 that ∼ • is a congruence. For this, we could try to naively model evaluation rules as a dynamic signature Σ 1 over Σ 0 . However, substitution-closed bisimilarity in the obtained system would not coincide with applicative bisimilarity in Howe's sense. Furthermore, the induced functor Σ s 1 : Σ 0 -Trans → C s would not be cellular. Indeed, consider for instance the usual, call-by-name rule for application. In Howe's format, it gives the following:

1 ⇓ ( 3 ) 3 ( 2 ) ⇓ 4 1 2 ⇓ 4
, where all are metavariables.

Notation 8.31. For any ∈ N, we use the abbreviation := ((0, 0) + ) -because we will mainly need tuples ( p , v ) with only ≠ 0 from now on.

Letting denote the exponent of the induced Σ s 1 , and denote the element corresponding to this rule in the spectrum, the boundary arity ( ⇓ ↾ ) : (s(⇓), • ⇓ ) → (⇓, ) is the bottom composite in the following diagram,

ℒ(y 0 p ) ℒ(y ⇓ ) ℒ(y 0 v + y 0 p ) ℒ(y 1 p + y 0 p ) ℒ(y 0 p + y 0 p ) ℒ(y ⇓ + y 0 p ) (⇓, ) ℒ (y ⇓ +y 0p ) ( 1 )+id ℒ (y 0p ) ℒ (y ⇓ +y 0p ) ℒ (y ⇓ )
¯ where • ¯ is analogous to Definition 7.16;

• we implicitly use transposition, the Yoneda lemma, and canonical isomorphisms ℒ( ) + ℒ( ) ℒ( + ). This bottom composite is not a relative cellular complex, because ( 1 ) : ℒ(y 0 v ) → ℒ(y 1 p ) is not of the form ℒ(y ⇓ ).

So we have two problems: substitution-closed bisimilarity is not as desired, and Σ s 1 is not cellular. The solution to both problems is to rectify this last point. Namely, we construct a new signature from the evaluation rules, in such a way that we may observe each argument of a value. For this, we first need to generalise the notions of premise, rule, and signature, as well as the evaluation relation induced by a signature, which in turn requires us to introduce the Howe context induced by a Howe dynamic signature over a Howe binding signature.

We fix a Howe binding signature and a Howe dynamic signature over it for the rest of this section. Definition 8.32. We define the Howe context induced by ( , ), as follows.

• For state types, we take C 0 = (2 × F 2 ) op , with the monoidal structure on Ĉ0 = [2×F 2 , Set] specified in Remark 8.6.

• For transition types, we take

C 1 = {⇓} ⊎ ∈ v , ∈ + {⇓ + , } ⊎ ∈ v , ∈ - {⇓ - , }.
• We define source and target as follows

s : C 1 → C 0 ⇓ ↦ → 0 p ⇓ + , ↦ → 0 v ⇓ - , ↦ → 0 v t : C 1 → C 0 ⇓ ↦ → 0 v ⇓ + , ↦ → 0 v ( ∈ v , ∈ + ) ⇓ - , ↦ → ( - , ) p ( ∈ v , ∈ -)
We now introduce the new notions of premise, rule, and dynamic signature, which we deem rigid to avoid confusion with the original. Definition 8.33. A rigid premise consists of a family of operation arities , called the source type, a transition type ∈ C 1 and a source term 0, 0 ⊢ : s( ). The target type of a rigid premise ( , , ) is the family := + ( : → ), where t( ) = , and its target is the fresh metavariable : → ∈ .

We denote such a premise by ---→ . We will not need the rest of the structure. All we need to know is that cells compose horizontally and vertically just as in a weak double category. We will use the double bicategories 2Sp ( C 0 ) and 2Sp ( C 1 ).

Notation 9.21. We use the following notational conventions.

• We denote cells 2Sp ( C 0 ) such as (9.1) above by

′′ ′′ . ′ ′′ ′ ′
• Furthermore, cells in C 1 of the form below left will be denoted as below right.

0 s 0 s 0 s 1 1 1 ′ 0 t ′ 0 t ′ 0 t 0 0 ′ 0 ′ 0 0 1 ′ 0 1 1 (9.2)
Explicitly, spans of the form 0 s ← 1 → ′ 0 t are denoted by 0 1 ′ 0 , while spans of the form 0 ← 0 → 0 are still denoted by 0 0 0 , but silently coerced by Δ s or Δ t depending on context.

• For both types of cells, we collapse identity borders, as usual.

• When a span is trivial on one side, we use standard arrows for its borders, and a double arrow for its middle arrow, all in the relevant direction. E.g., the diagram below left may be depicted as below right.

′ ′ ′ ′ ′ ′
Cells of the form (9.2) live in 2Sp ( C 1 ), hence may be composed horizontally. Relevant examples of vertical composition will be obtained by embedding cells of the form (9.1) along Δ s (resp. Δ t ), and vertically composing with cells of the form (9.2) in 2Sp ( C 1 ). This yields a top (resp. bottom) action of 2Sp ( C 0 ), which we both denote by mere pasting. Lemma 9.22. Given a composable pasting diagram made of cells of both types, any two parsings agree up to isomorphism. 9.4. Howe closure on transitions. Let us now define the Howe closure on transitions. First, we delineate an ambient category C Z . The idea is that objects of this category should be transition systems → Z 2 over Z 2 whose image under the projection C/Z 2 → C 0 /Z 2 0 is precisely 0 → Z 2 0 . Thus, an object of C Z consists of an object 1 ∈ C 1 , equipped with a dashed cone to the outer part of the diagram below.

Z 0 s 0 s Z 0 s Z 1 1 Z 1 Z 0 t 0 t Z 0 t (9.3)
Equivalently, they are morphisms over the limit, so that we may define C Z as a slice category by merely stating the following.

Definition 9.28. Let denote the limit of the outer part of (9.3).

Definition 9.29. C Z is the category of cones over the outer part of (9.3), or equivalently, it is the slice category C 1 / . Furthermore, we denote by Z : C Z → C/Z 2 the forgetful functor.

Proposition 9.30. The initial object in C Z is the span Z ← 0 → Z, i.e., the one with 1 = 0. Definition 9.31. Let Σ 1 : C Z → C Z map any object Z ← → Z to the coproduct of the following two pastings.

Z 0 Z 0 Σ 0 (Z 0 ) Σ 0 (Z 0 ) Z 0 Z 0 0 Σ 0 ( 0 ) Σ 1 (Z) 0 Σ 1 (Z) Σ 1 ( ) Z 1 Z 1 Z 0 Z 0 Z 0 Z 0 Z 0 Z 0 0 Z 1 0 Z 1 ∼ ⊗ 0 ∼ ⊗ 0 Z 1 1 ∼ ⊗ 1 0 0 (9.4) Proposition 9.32. The functor Σ 1 : C Z → C Z is finitary. Proof. The forgetful functor C Z C 1 / → C 1 creates colimits, so it suffices to show that the composite C Z Σ 1 --→ C Z → C 1 is finitary.
This functor maps any to Σ 1 ( ) + 1 ; ∼ 1 ⊗ , hence is finitary because Σ 1 is and -; ∼ ⊗ 1 is cocontinuous. The last result legitimates the following definition. Definition 9.33. Let Z denote the initial Σ 1 -algebra. We call := Z ( Z ) ∈ C/Z 2 the Howe closure of substitution-closed bisimilarity.

We readily can prove the following. Lemma 6.16. There exists a span morphism i : ∼ ⊗ → . Proof. By construction, the underlying object of is in particular a Σ1 -algebra, so by initiality we obtain a unique span morphism Z → -in other words is reflexive. Furthermore, again by construction, is an algebra for the endofunctor -; ∼ ⊗ on C/Z 2 . We thus may form the composite ∼ ⊗ Z; ∼ ⊗ → ; ∼ ⊗ → . 9.5. Alternative characterisations of the Howe closure. In this section, we exhibit a few alternative characterisations of the Howe closure on transitions. The definition in the previous section is convenient for proving that the transitive closure is symmetric, while our final alternative characterisation will enable a conceptual proof of the simulation property.

First of all, we have:

Lemma 9.34. The object Z ∈ C Z is (isomorphic to) the initial algebra of the endofunctor Σ 1,pack : C Z → C Z mapping any Z ← → Z to the following pasting.

Z 0 Z 0 Z 0 Z 0 Σ 0 (Z 0 ) Σ 0 (Z 0 ) Z 0 Z 0 Z 0 Z 0 0 ∼ ⊗ * 0 Z 1 Σ 0 ( 0 ) Σ 1 (Z) 0 Σ 1 (Z) ∼ ⊗ * 0 Z 1 Σ 1 ( ) ∼ ⊗ * 1 Z 1 0 0 (9.5)
For the proof, we need an intermediate result, Corollary 9.36 below, which relies on the following lemma. where : ( * ( )) → * ( ) denotes the canonical -algebra structure on * ( ), and similarly for . Furthermore, the right-hand square above, viewed as a morphism → * exhibits * as a free -algebra on .

Proof. Let us first observe that lifts to a functor : -alg → -alg, which maps → to --→ → . This in particular equips ( * ( )) with -algebra structure. Let us thus define * , by universal property of * ( ), to be the unique -algebra morphism * ( ) → ( * ( )) whose restriction to is ( ) • . This ensures in particular that the required diagram commutes.

Let us finally show that * is an initial -algebra. For this, we observe thatalgebra structure on : → ( ) means morphisms and making the following diagram commute.

( )

( ( )) ( ( )) ( ) ( ) ( )
Thus, -algebra structure ( , ) on is exactly the same as -algebra structure on , -algebra structure on , and an -algebra morphism → ( ). This shows that -alg is isomorphic to the comma category -alg/ . But for any morphism, say (ℎ, ) from to any ′ : ′ → ( ′ ) in -alg/ , by universal property of * ( ) and * ( ), we get maps h and ˜ , respectively in -alg and -alg, making both triangles commute in the following diagram. * ( )

′ ( * ( )) ( ) ( ′ ) ℎ ( ) ′ * h ( ˜ )
By functoriality of and uniqueness in the universal property of * ( ), the left-hand square also commutes, so ( h, ˜ ) is a morphism in -alg/ , as desired. Finally, uniqueness follows again by universal property of * ( ) and * ( ).

Z 0 Z 0 Z 0 Z 0 0 Z 1 0 Z 1 1 = Z 0 Z 0 Z 0 Z 0 Z 0 Z 0 0 Z 1 0 Z 1 ∼ ⊗ 0 ∼ ⊗ 0 Z 1 1 ∼ ⊗ 1 0 0
Now, by the packing lemma, it is enough to show that

★ Z 0 Z 0 Z 0 Z 0 0 Z 1 0 Z 1 1 = Z 0 Z 0 Z 0 Z 0 Z 0 Z 0 0 Z 1 0 Z 1 ∼ ⊗ * 0 ∼ ⊗ * 0 Z 1 1 ∼ ⊗ * 1 0 0
To this end, we are going to organise C Z as a comma category on which acts, so as to apply Corollary 9.36. Let denote the category of objects 1 equipped with a span Z 1 ← 1 → Z 1 and ℬ denote the product category ℬ s × ℬ t , where ℬ is the category of objects 1 equipped with a span Z 0 ← 1 → Z 0 .

Let : → ℬ denote the functor mapping Z 1 ← 1 → Z 1 to (Z 0 s ← 1 → Z 0 s, Z 0 t ← Theorem 1.66], since its domain is a locally presentable category. Let : 1 → ℬ be the functor selecting the pair (Z 0 s ← 0 s → Z 0 s, Z 0 t ← 0 t → Z 0 t). Now, it is straightforward to check that C Z is isomorphic to the comma category / .

Next, we reconstruct as acting on / through this isomorphism in order to fit the setting of Corollary 9.36. Let

• : → denote the functor mapping → so that corresponds to our endofunctor through the isomorphism C Z / . Since ★ (Z 1 ← 1 → Z 1 ) = (Z 1 ← 1 ; ∼ ⊗ * 1 → Z 1 ), the only thing to check is that the proposed definition for ★ ( 1 ) indeed defines a -algebra, and that 1 → ★ ( 1 ) induces a morphism 1 → ★ ( 1 ), which is straightforward.

Z 1 ← 1 → Z 1 to Z 1 ← 1 ← 1 ; ∼ ⊗ 1 →∼ ⊗ 1 → Z 1 ; • : ℬ → ℬ
Let us now turn to our final characterisation of , which relies on the following category, which is a relaxation of C Z , in which the left-hand object in (9.3) is only forced to coincide with Z on C 0 . Definition 9.37. Let C lax denote the category whose objects consist of objects 1 and 1 in C 1 , equipped with dashed arrows making the following diagram commute. Proposition 9.41. The initial object in C lax is the span Z 0 ← 0 → Z, i.e., the one with

1 = 1 = 0.
Let us now introduce the endofunctor of which our characterisation of will be an initia algebra. Definition 9.42. Let Σ 1,lax : C lax → C lax map any object ← → Z to the following pasting. Proof. In order to apply Corollary 9.36, we organise C lax as a comma category /C , decomposing its left and middle/right parts, with : C → C defined as follows:

Z 0 Z 0 Z 0 Z 0 Σ 0 (Z 0 ) Σ 0 (Z 0 ) Z 0 Z 0 Z 0 Z 0 0 ∼ ⊗ * 0 Z 1 Σ 0 ( 0 ) Σ 1 ( ) 0 Σ 1 (Z) ∼ ⊗ * 0 Z 1 Σ 1 ( ) ∼ ⊗ * 1 Σ1 (
• C = C 1 /Δ(Z 0 ); • C is the comma category C 1 C 1 /Δ( 0 ) C 1 /Δ(Z 0 ); C 1 /Δ( 2 )
Z concretely, objects consist of a presheaf 1 ∈ C 1 , together with dashed maps making the following diagram commute;

0 s Z 0 s 1 Z 1 0 t Z 0 t 2 s 2 t
(9.9)

• is the composite

C ---→ C 1 /Δ( 0 ) C 1 Δ( 1 )
-------→ C 1 /Δ(Z 0 ); concretely, maps any object (9.9) to the following diagram.

Z 0 s 0 s 1 Z 0 t 0 t 1 s 1 t
We note that is cocontinuous since colimits are computed pointwise in C and C , and thus has a right adjoint , since its domain is locally presentable, by [AR94, Theorem 1.66]. Furthermore, C Z is isomorphic to the comma category /Z6 . We then define functors Σ 1, and ( Σ1 ) |Z 0 and a natural transformation ℎ as in • ( Σ1 ) |Z 0 is Σ1 restricted to the fibre of C 1 /Δ → C 0 over Z 0 , as in the left part of (9.8);

• Σ 1, acts as the right part of (9.8);

• ℎ connects both parts using the left projection. Now, we apply Corollary 9.36 twice with = Σ 1, , = ( Σ1 ) |Z 0 and = ℎ:

(1) for = , the identity endofunctor, the identity natural transformation, and = id ∅ : (∅) → ∅, the induced endofunctor is precisely Σ 1,lax , and Corollary 9.36 yields a morphism, say * , making the diagram below commute; so by (i), (ii), and Proposition 1.1, the projection functor

, ! : C → C 1 /Δ( 0 ) × 1 C 1 /Δ( 0 )
to the product preserves colimits. (iv) In the commuting square

C 1 /Δ(Z 0 ) C 1 /Δ C 1 × 1 C 1 × C 0 , 1 ,! C 1 ×Δ(Z 0 )
1 , 0 both vertical functors (which are the canonical projection functors) create colimits. Furthermore, the bottom functor preserves them, because • colimits are pointwise in a product of cocomplete categories, and • any functor from the terminal category is cocontinuous. Thus, the top functor is cocontinuous, as desired. (v) Same, with the square

C 1 /Δ( 0 ) C 1 /Δ C 1 × 1 C 1 × C 0 . C 1 ×Δ( 0 )
(vi) The functor : C lax → C 2 is induced by universal properties of lax limits as in

C C 1 /Δ( 0 ) C 1 /Δ C lax C C 2 C C 1 /Δ(Z 0 ) C 1 /Δ, C 1 /Δ( 1 )
where C is defined as the lax limit of C 1 /Δ( 1 ), and , which is induced by universal property of C 1 /Δ, has as component at any : → Δ( 0 ) the morphism

Δ( 0 ) Δ(Z 0 ) Δ( 1 ) Δ( 1 )•
in C 1 /Δ. For each lax limit, the given functor is cocontinuous, so the projection functor to the product creates colimits. We thus get a diagram

C lax C C 2 C × C C 1 /Δ( 0 ) × C 1 /Δ(Z 0 ) ( C 1 /Δ) 2
×id in which all vertical functors create colimits, and both bottom functors are cocontinuous by the previous points. Thus, the top functor is cocontinuous as desired.

Finally, it remains to prove: Lemma 6.21. For any substitution-closed simulation such that 0 is symmetric, there exists a substitution-closed bisimulation ′ and a span morphism i ′ : → ′ .

Proof. First, consider the relation induced by by the image factorisation ։ ↩→ Z×Z. is still a substitution-closed simulation and 0 is symmetric. Now, we define ′ as follows:

• ′ 0 = 0 • ′
1 is the limit of the following diagram:

Z 0 s ′ 0 s Z 0 s Z 1 ′ 1 Z 1 Z 0 t ′ 0 t Z 0 t.
More concretely, an element of ′ 1 ( 1 ) is a pair of transitions at 1 with related sources and targets. The morphism → ′ is obtained by the composite → → ′ , where the last morphism exploits the definition of ′ 1 as a limit. It is straightforward to check that ′ is a substitution-closed simulation. Moreover, it is symmetric (even at the level of transitions), so it is a bisimulation.

Conclusion

We have introduced the notion of Howe context, in which we have defined transition monoids, an abstract notion of labelled transition system whose states feature some sort of substitution. For them, we have introduced an abstract variant of applicative bisimilarity called substitution-closed bisimilarity.

Furthermore, we have introduced operational semantics signatures as a device for specifying syntax with variable binding and operational semantics. We have finally shown that if the dynamic part of an operational semantics signature preserves functional bisimulations, then substitution-closed bisimilarity on the generated transition monoid is a congruence. This all follows the pattern of our previous work [START_REF] Borthelle | A cellular Howe theorem[END_REF], but simplifying the framework and relaxing some hypotheses, as explained in the introduction.

We hope these simplifications pave the way for more abstract results in the same vein. To start with, we would like to generalise our approach. Indeed, it fails to directly account for some important applications of Howe's method, notably to PCF [START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF], algebraic effects [START_REF] Dal Lago | Effectful applicative bisimilarity: Monads, relators, and Howe's method[END_REF], and higher-order process calculi [START_REF] Lenglet | Howe's method for contextual semantics[END_REF]. Furthermore, methods similar to Howe's have been used for purposes other than congruence of applicative bisimilarity [Pit11, LG19, GLN08]: it might be useful to design abstract versions of such results using our methods.

Definition 3. 8 .⇓

 8 Let F[⇓] denote the category obtained by augmenting F with an object ⇓, together with morphisms 0 and their formal composites with non-identity morphisms from F.

  Proposition 3.9. Transition systems are isomorphic to covariant presheaves on F[⇓].

  14. Let Bisim( , ) denote the category of bisimulations, with span morphisms between them.Proposition 3.15. Bisim( , ) has a terminal object, called bisimilarity and denoted by ∼ , .

Notation 4. 4 .

 4 In any pre-Howe context, we let C := C 1 /Δ, and denote the projections by 1 : C → C 1 and 0 : C → C 0 , respectively.

(

  On the left and s( ) are viewed as objects of C s,t , hence should technically by written 1 ( ) and 0 (s( )), respectively.)

  The coequaliser of these two morphisms computed in the presheaf category C is a quotient of by the equation = ( ). It thus has as reductions [ ] ⇓ [ ] between equivalence classes, for all reductions ′ ⇓ ′ between representatives ′ ∈ [ ] and ′ ∈ [ ]. E.g., it has a reduction [ ( )] ⇓ [ ( )], since ∈ [ ( )] and ⇓ ( ). However, lacks a reduction [( . ( )) ] ⇓ [ ( )]. Indeed, [( .

  Proposition 6.2. A morphism in Σ 0 -Trans is a functional bisimulation iff it has the right lifting property w.r.t. ℒ(y ) : ℒ(y s( ) ) → ℒ(y ), for all ∈ C 1 .Proof. By adjunction.

Theorem 7. 18 .

 18 For any functor : → C such that has a terminal object, is familial iff all morphisms : → ( ) factor as -

Definition 7. 24 .

 24 Let us consider any familial functor : → C, say as ( ) ( ) = ∈ ( ) ( ( , ), ), such that C is small and has a terminal object. Then, for any operation ∈ (1) ( ) and morphism : → in C, the -arity of , or its boundary arity when is clear from context, is the morphism ( , ↾ ) : ( , • ) → ( , ) in . Notation 7.25. Let denote the generic morphism y → ( ( , )) induced by any operation ∈ (1) ( ).

  Howe distinguishes value operations 4 from program operations: Definition 8.7. A Howe binding signature consists of • a binding sort ∈ {v, p}, • a set p of program operations, equipped with a map p : p → N and a family p ∈ ∈ p N p , and • a set v of value operations, equipped with two maps + : v → N and -: v → N, and a family -∈ ∈ v N -.

Definition 8. 23 .

 23 Given any families and of operation arities, a premise → consists of a source program 0, 0 ⊢ : p and a target value 0, 0 ⊢ : v, where and take one of the following two forms:• either = + ( : v), extending with one closed value metavariable, in which case = , • or = + ( : v) ∈ {1,..., + } + ( : -, → p) ∈ {1,..., -} for some value operation ∈ v , in which case the target is v ( 1 , . . . , + ; 1 , . . . , -).Notation 8.24. We write any premise ( , ) : → as ⇓ ---→ .Definition 8.25. A rule consists of • a head program operation ,

  Definition 8.34. A rigid rule consists of • cells, called double spans, are precisely commuting diagrams of the following form.

  Lemma 9.35. Consider any diagram ℬ ℬ ⇓ of functors and natural transformations, such that and are finitary, and and ℬ are cocomplete. Let be the induced endofunctor on the comma category / , mapping -→ to ---→ --→ . Then, given an object : → ( ) of / , there is a unique morphism * : ★ → ★ such that the following diagram commutes,

  and natural transformations such that has a right adjoint, and are cocomplete, and and are finitary. Furthermore, let be the induced endofunctor on the comma category / , mapping-→ to ( --→ ---→ --→ ).Then, given an object : → of / , there is a unique morphism * : ★ → ★ making the following diagram commute. right-hand square above exhibits * as a free -algebra on .Proof. This follows from Lemma 9.35 with = , = , as where is the right adjoint of , by considering the mate ′ :→ of : → , defined as ----→ ----→ ----→, (where and denote the unit and the counit of the adjunction ⊣ ) and composing it with to get a natural transformation → .Proof of Lemma 9.34. Let us denote by the endofunctor on C Z mapping an object Z ← → Z to the the right pasting of Diagram 9.4:

1

  Remark 9.38. Using the notation of §9.3, an object of C lax is a cell of the form Such an object may also be viewed as a span of the form ← → Z in C, which projects down toZ 0 ← 0 → Z 0 in C 0 .Let us briefly relate C lax to other useful categories.Definition 9.39. Let 2 denote the free category on the graph 0 → 1, and C 2 /Z denote the comma categoryC 2 /Z 1 C 2 C,dom Z whose objects are spans of the form ← → Z. Definition 9.40. We define a commuting diagram • Z and lax are the obvious forgetful functors, • ℐ and are the obvious embeddings, and • and are defined by composition with the domain functor dom.

(

  Σ 1, ((Σ 1, ) * (∅))) ((Σ 1, ) * (∅)) (∅) ( Σ1 ) |Z 0 ( ((Σ 1, ) * (∅))) ( Σ1 ) |Z 0 (( C selecting Z 0 s ← Z 1 → Z 0 t,induced by the -algebra structure on it, and = ! Z : (∅) = ∅ → Z, the induced endofunctor is precisely Σ 1,pack , and Corollary 9.36 yields a unique morphism, say * , making the diagram below commute.(Σ 1, ((Σ 1, ) * (∅))) ((Σ 1, ) * (∅)) (∅) ( Σ1 ) |Z 0 ( ((Σ 1, ) * (∅))) ( Σ1 ) |Z 0 (Z)Both right-hand squares are trivial, and both left-hand hand squares are in fact the same, so that * = * . Finally, in terms of /C , the statement claims that the -algebra structure of * decomposes as( Σ1 ) |Z 0 (( Σ1 ) * |Z 0 (∅)) ( Σ1 ) |Z 0 ( ((Σ 1, ) * (∅))) (Σ 1, ((Σ 1, ) * (∅))) ( Σ1 ) * |Z 0 (∅) (Σ 1, ((Σ 1, ) * (∅))) ( Σ1 ) * |Z 0 (∅) ((Σ 1, ) * (∅)), (Σ1) |Z 0 ( * ) ℎ (Σ 1, ) * (∅) ( Σ1 ) |Z 0 ( * ) * ( Σ1 ) |Z 0 ∅ (

  Definition 2.2. The open extension of a relation on closed terms is the relation ⊗ on potentially open terms such that The open extension of any relation is the greatest substitution-closed relation contained in on closed terms. Proof. Let us first show that ⊗ is substitution-closed. For any 1 ⊗ 2 and , we want to show 1 [ ] ⊗ 2 [ ]. For this, we in turn need to show that for all closing substitutions , we have 1 [ ] [ ] Furthermore, [ ] is closing. So, because we have 1 ⊗ 2 , by definition of open extension, we get 1 [ ] [ ] 2 [ ] [ ] as desired. Let us now show that ⊗ is the greatest substitution-closed relation contained in on closed terms. For this, consider any substitution-closed ′ contained in on closed terms: for all

		⊗ ′ iff for all closed substitutions	covering all
	involved free variables we have [ ]	′ [ ].
	Let us readily notice the following alternative characterisation of open extension.
	Definition 2.3. A relation on open terms is substitution-closed iff for all	′ and
	(potentially open) substitutions , we have [ ]	′ [ ].
	Lemma 2.4.

2 [ ] [ ]. But [ ] [ ] = [ [ ]], where by definition and [ ] ( ) = ( ) [ ]. ′ ′ , by substitution-closedness, we have [ ] ′ ′ [ ] for all closing . So because ′ is contained in on closed terms, we further have [ ] ′ [ ]. This proves ⊗ ′ , and thus ′ ⊆ ⊗ as desired.

  AR94, §0]), hence are preserved by restriction functors. 4.3. Bisimulation and bisimilarity. Morphisms in C are a generalisation of graph morphisms, which are a proof-relevant version of functional simulations. The analogue of functional bisimulations is as follows. Definition 4.15. A morphism : → in C s,t is a functional bisimulation, or a fibration, iff it enjoys the (weak) right lifting property w.r.t. y : y s( ) → y , for all ∈ C 1 . Remark 4.16. This definition is strongly inspired by Joyal et al.'s [JNW93].

  .1]. Evaluation is a binary relation between closed programs and closed values. By default, all value operations are considered as coming equipped with their canonical evaluation rule ( 1 , . . . , + ; 1 , . . . , -) ⇓ v ( 1 , . . . , + ; 1 , . . . , -) . Howe's signatures thus only need to specify evaluation of program operations. We now successively introduce notions of premises, rules, and signatures. We start by fixing a global choice of finite coproducts in both [2 • N 2 , Set] (families of operation arities) [2 • F 2 , Set] (presheaves).

	1 ⇓ 1	. . .	+ ⇓ +	(8.1)

p

  ∈ {1,..., p } , and • a tail metavariable ( : v) in . A Howe dynamic signature over a Howe binding signature is a family of rules. We restrict to rules with a finite number of premises 5 .• We have a slightly different treatment of value vs. program variables and metavariables.Definition 8.28. For any Howe binding signature , and Howe dynamic signature over it, the evaluation, denoted by ⇓ , , or ⇓ for short, is the binary relation between programs and values, obtained inductively by instantiating the given rules together with the canonical rules (8.1). For any Howe binding signature , and Howe dynamic signature over it, an applicative simulation is a binary relation in Set 2 over the injection 0 (∅) (0, 0) v ↩→ 0 (∅) (0, 0) p , such that for any closed programs and ′ such that p ′ , and any transition ⇓ v ( 1 , . . . , + ; 1 , . . . , -), there exist ′

	-→ Remark 8.27. There are some discrepancies w.r.t. Howe's original format [How96, Lemma , where 0 = ( : Notation 8.26. Such a rule is denoted by 1 ⇓ 1 . . . ⇓ ( 1 , . . . , p ) ⇓ . The families of operation arities 0 , . . . , are left implicit. 6.1]. extension. • Let us now recall Howe's general definition of applicative bisimulation, and its open Definition 8.29. 1 , . . . , ′ + , ′ -and a transition 1 , . . . , ′ ′ ⇓ v ( ′ 1 , . . . , ′ + ; ′ -), such that v ′ for all ∈ + , and [ ] p ′ [ ], for 1 , . . . , ′ all ∈ -and closing substitutions .

p , → p)

  denote the functor s × t , where :ℬ → ℬ maps Z 0 ← 1 → Z 0 to Z 0 ← 1 ; ∼ ⊗

	•	→ Z 0 ; : 1 → 1 denote the identity endofunctor. 0
	Now we apply Corollary 9.36 with suitable	:	→	and	:

  Remark 9.43. The difference with Σ 1,pack is that, being different from Z in general, we cannot use any Σ1 -algebra structure on the left.Proposition 9.44. The functor Σ 1,lax : C lax → C lax is finitary.Proof. Just as Proposition 9.32.Let us now work towards our final characterisation of .Furthermore, let: Σ 1,pack -alg → Σ 1,lax -alg denote the induced lifting of ℐ , as in Lemma 9.46. The Σ 1,lax -algebra ( Z ) is initial. In other words, letting lax denote any initial Σ 1,lax -algebra, we have (

	Σ 1,pack -alg		Σ 1,lax -alg
	C Z		C lax ,
			0
	) 1			(9.8)
			0
	Definition 9.45. Let denote the natural transformation
	C Z	ℐ	C lax
	Σ 1,pack		Σ 1,lax
	C Z	ℐ	C lax
	Σ1 (Z)	Σ1 ( ); ∼ ⊗ *	Z
	Z	Σ1 ( ); ∼ ⊗ *	Z

whose component at any Z ← → Z in C Z is the following morphism in C lax .

ℐ

where both vertical arrows denote forgetful functors. Z ) lax .

This pattern is advocated by the approach of initial algebra semantics[START_REF] Goguen | An initial algebra approach to the specification, correctness and implementation of abstract data types[END_REF], where initiality provides a recursion principle.

In[START_REF] Borthelle | A cellular Howe theorem[END_REF], we instead considered a skew-monoidal variant where the tensor product does not enforce any standard equation.

The Howe contexts of[START_REF] Borthelle | A cellular Howe theorem[END_REF] may be defined similarly. The difference is that for them, s and t are not necessarily functorial, but 1 ↦ → (s( 1 ), t( 1 )) defines a functor C 1 → C 0 ×C 0 , where C 0 ×C 0 denotes the category whose objects are pairs of elements of C 0 , and where a morphism ( 1 , 2 ) → ( 1 , 2 ) consists of some indices , ∈ {1, 2}, together with a pair of morphisms 1 → and 2 → .

Value operations correspond to canonical operators in[START_REF] Douglas | Proving congruence of bisimulation in functional programming languages[END_REF].

We expect that our setting can be extended to account for rules with an infinite number of premises by replacing the finitarity condition on Σ 1 with a weaker accessibility requirement.

→ Z 0 t), by postcomposing with the relevant morphisms. As the forgetful functor from a category of spans creates colimits, is cocontinuous and thus has a right adjoint by[START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF]

Note that this decomposition as a comma category differs from the one in the proof of Lemma 9.34.

incarnations of each value operation, one for constructing values, the other for constructing programs. Any Howe binding signature generates a pointed strong endofunctor, as follows. We first define an auxiliary operation for adding bound variables in the right componentas prescribed by the binding sort . Notation 8.9. For any ( -→ ) ∈ F 2 , ∈ F, and ∈ {v, p} let ( -→ ) + denote

Definition 8.10. Given any Howe binding signature , the generated endofunctor Σ 0 on [2 × F 2 , Set] is defined by

Set] and , ∈ F, with obvious action on morphisms.

We now want to express Σ 0 as a familial functor. For this, we start by defining Remark 8.12. The arity functors are contravariant because the Yoneda embedding is, for covariant presheaves.

By construction:

Proposition 8.13. The endofunctor Σ 0 is familial, with • as spectrum the functor

• writing : for : v 0 × p 0 → . We furthermore denote the disjoint union of families of operation arities and by + . Given a family = ( : v × p → ) of operation arities, we also denote by the coproduct of representable presheaves y ( , ) : 2 × F 2 → Set.

Remark 8.19. By Notation 8.9, for , , ∈ F, ( , ) + denotes ( + , ) if = v, and ( , + ) otherwise.

We now give an inductive description of 0 ( ) on objects of the form ( , ) (Notation 8.9). Letting , ⊢ : mean that ∈ 0 ( ) ( , ) , for a family of operation arities, the free Σ 0 -monoid over is inductively generated on objects of the form ( , ) by the following rules.

( 1 , . . . , + ; 1 , . . . , -) :

• a head program operation ,

• a composable sequence of rigid premises 0

, where 0 = ( : p , → p) ∈ {1,..., p } , and • a tail metavariable ( : v) in .

A rigid dynamic signature over a Howe binding signature is a family of rigid rules.

Definition 8.35. The labelled transition system induced by any the rigid dynamic signature ′ is defined by instantiating the given rigid rules, together with the canonical rules (8.1), and the following new rules.

v ( 1 , . . . ,

We may now define the rigid signature induced by ( , ).

Definition 8.36. Let the rigid dynamic signature ( , ) induced by ( , ) be obtained as follows. For each rule in , ( , ) has a rule for the same program operation, whose premises are obtained by replacing each original premise

----------------------→ with any linearisation (in the straightforward, suitable sense) of the following tree.

Let us show that the rigid signature ( , ) is adequate.

Proposition 8.37. The open extension of applicative bisimilarity in the sense of ( , ) coincides with substitution-closed bisimilarity in the labelled transition system generated by ( , ).

Proof. Let ∼ ′ denote substitution-closed bisimilarity in the sense of ( , ). First of all, ∼ • is a substitution-closed bisimulation; indeed, ⇓ is the same relation in both systems -by a straightforward induction -and by definition of applicative bisimulation, for any v ( 1 , . . . , + , 1 , . . . , -) ∼ v ( ′ 1 , . . . , ′ + , ′ 1 , . . . , ′ -), we have ∼ ′ and ∼ • ′ , for all and , which ensures that the new transitions ⇓ + , and ⇓ - , are matched. Thus, we have

Conversely, the new transitions ensure that ∼ ′ is an applicative bisimulation, hence is contained in ∼ on closed terms. But it is substitution-closed, so we get ∼ ′ ⊆ ∼ • , as desired.

Finally, we show that the rigid signature ( , ) straightforwardly gives rise to a dynamic signature Σ , 1 , such that the initial vertical Σ , 1 -algebra is isomorphic to the generated labelled transition system, and furthermore that the induced functor (Σ , 1 ) s is cellular, hence that by Proposition 8.37, Corollary 7.30, and Theorem 6.15, ∼ • is a congruence. Notation 8.38. We tend to abbreviate Σ , 1 to Σ 1 , for readability.

Let us present the dynamic signature Σ , 1 , which will consist of various components: one dynamic signature Σ 1, for each value operation ∈ v , describing both kinds of canonical rules (8.1) and (8.2), plus one dynamic signature Σ 1, for each other rule.

• For each value operation ∈ v , we define

( 1 , . . . , + , 1 , . . . , -) ↦ → ( v ( 1 , . . . , + , 1 , . . . , -), ). • For each rigid premise = ( ---→ ), we define the cospan induced by to be

where the left-hand morphism ℓ is defined by the pushout

and the right-hand morphism

is obtained by copairing ℓ and the bottom composite in (8.3). • For each rigid rule

where for all ∈ , ℒ( -1 ) -→ ← -ℒ( ) denotes the cospan induced by the th premise, with Σ 1, ( )

∈ - ′ , and again with the morphism Σ 1, ( ) → Σ 0 ( )s × t mapping any compatible tuple ( 1 , . . . , ) ∈ Σ 1, ( ) (⇓) to ( ( ), ), where ∈ ∈ p (( p , ) p ) corresponds by Yoneda and adjunction to the morphism

and ∈ (0 ) corresponds to

, with morphism to Σ 0 (-)s× (-)t given by cotupling. By construction, we have: Proposition 8.39. The transition Σ 0 -monoid generated by the dynamic signature Σ , 1 is isomorphic to the rigid transition system ( , ).

Furthermore, we observe:

Lemma 8.40. The induced functor (Σ , 1 ) s is cellular.

Proof. The functor is familial by construction. By Corollary 7.30(iii) and Proposition 7.32, it suffices to show that for any rule whose conclusion is a transition of type , the boundary arity ( ↾ ) : (s( ), • ) → ( , ) is a relative cell complex. The arity of each canonical rule (8.1) is clearly a coproduct of generating cofibrations. The arities of canonical rules (8.2) are identities, hence trivially relative cell complexes. For any other rule , by (8.4) the arity is the left-hand leg of cospan obtained by composing all -1 → ← , which is thus by construction a composite of pushouts of generating cofibrations, hence a relative cell complex.

We at last obtain: Theorem 8.41. For any Howe binding signature and dynamic signature , the open extension of applicative bisimilarity on the generated transition system is a congruence.

Proof. The open extension of applicative bisimilarity for ( , ) coincides with substitutionclosed bisimilarity for ( , ) by Proposition 8.37, which further coincides with substitutionclosed for the transition system generated by Σ , 1 by Proposition 8.39. Finally, the latter is a congruence by Lemmas 7.28 and 8.40, and Theorem 6.15.

Congruence of substitution-closed bisimilarity

In this section, we elaborate on the proof sketch of Theorem 6.15 given in §6. The overall structure remains the same, and the final part of the proof sketch is complete, so we mainly elaborate on items (1)-(4). 9.1. Preliminaries on spans. In this section, we fix a locally finitely presentable category , recall some known tools about spans, and develop a few new ones, including categorified notions of reflexivity, transitivity, symmetry, and transitive closure. As announced in §1.6, we freely switch from spans ← → to their pairings → × in / × . Furthermore, Definition 9.1. Given any spans

------→ × , their span, or sequential, composition, denoted by ; → × , is the (or, rather, some global choice of) following span obtained by pullback.

;

Finally, it is symmetric if there is a morphism † → , where (-) † denotes the functor swapping projections, i.e., mapping any

For potentially non-reflexive spans, we will use the following reflexive transitive closure.

Definition 9.3. The reflexive transitive closure * of any span → 2 is the coproduct ∈N ; , or for short ∈N when the context is clear, where ; denotes iterated span composition of with itself, inductively defined by ;0 = and ; +1 = ; ; . At some point, we will also use a more "relational" notion of transitive closure, which we now introduce. Remark 9.6. Unions of relations exist by Proposition 1.7, as we have assumed the ambient category to be locally finitely presentable.

We immediately observe the following.

Lemma 9.7. For all ∈ N, spans → 2 and → 2 , and families ( → 2 ) ∈ of relations spans, we have

Proof. Let := 2 , 1 : 2 → 2 .

• For (1), by definition each side of the isomorphism corresponds to one side of the exterior of the following commuting pentagon. † 2

But, being an isomorphism, both sides are strong epi-mono factorisations of the morphism 2 , 1 : → 2 , hence are isomorphic. • The first point of (2) is clear. For the second one, we proceed by induction. The base case is trivial, and assuming ( † ) ;

( ; ) † , we have ( † ) ; +1 ( † ) ; ; † ( ; ) † ; † ( ; ; ) † ( ; +1 ) † , hence the result. • For (3) we have

( ∈ ) † by (1), so it suffices to show ∈ † ( ∈ ) † . But, letting : → 2 denote each projection, the former is (shorthand for) the morphism [ • ] :

→ 2 , and the latter is • [ ] , which are in fact equal.

Corollary 9.8. For all spans → 2 , we have †+ + † .

Proof. We have †+ = >0 ( † ) ; ( >0 ; ) † + † , by the lemma.

The following lemma will later be used to exploit preservation of sifted colimits by Σ 0 .

Lemma 9.9. If is a reflexive span on , then + is the (filtered) colimit of the chain → ; → ; ; ; → ; ; → . . .

Proof. Consider a colimiting cone for the given diagram, say to ∈ . Because the forgetful functor / 2 → creates colimits, it is in fact a colimiting cocone in / 2 . Now, the diagram consists of monic morphisms, hence by [AR94, Proposition 1.62(i)], so does the colimiting cocone. Furthermore, by [AR94, Proposition 1.62(ii)], the mediating morphism → 2 is again monic. The cocone thus lifts to the category Rel( ) of (binary) relations over . Because the forgetful functor Rel( ) → / 2 is fully faithful, the cocone remains colimiting in Rel( ). Finally, Rel( ) is a preorder category, so the colimit of the considered, directed diagram is equally a colimit of the underlying discrete diagram, which is + by definition.

The next result will be useful to show that the relational transitive closure of the Howe closure of substitution-closed bisimilarity is symmetric on states.

Lemma 9.10. For any reflexive span → 2 , + is symmetric if there exists a span morphism → + † .

Proof. Given a morphism : → + † , we consider the composite

where the first morphism is obtained from , and the second one is obtained from morphisms ( + ) ; → + . 9.2. Howe closure on states. We fix an operational semantics signature (Σ 0 , Σ 1 ) on a Howe context s, t : C 1 → C 0 , and recall • from Notation 5.5 that Z 0 denotes the initial Σ 0 -monoid, • from Theorem 5.18 that Z denotes the initial vertical Σ1 -algebra (hence in particular that (Z) = Z 0 ), and • from Notation 6.11 that ∼ ⊗ denotes substitution-closed bisimilarity on Z (hence in particular that (∼ ⊗ ) = ∼ ⊗ 0 is its state part). Definition 9.11. Let Σ 0 :

This functor Σ 0 is clearly inspired from the standard Howe closure. We now want to prove that it is pointed strong, which requires us to equip C 0 /Z 2 0 with monoidal structure. But Z 2 0 is a monoid, and it is well-known [Web04, §2] that any slice of a monoidal category over any monoid is again monoidal. The tensor of → and → is simply ⊗ → ⊗ → , and the unit is → . We may thus state the following result.

Proposition 9.12. The functor Σ 0 is pointed strong.

For proving this, we first need the following. Lemma 9.13. For any monoid in any monoidal category with finite limits, there is a natural transformation with components , , : ( ; ) ⊗ → ⊗ ; ⊗ in / 2 . Proof. Let : ⊗ → denote multiplication. By tensoring the defining pullback of ; with we obtain the back face below.

By universal property of pullback, we then get the dashed arrow making all faces commute, which gives our candidate , , . Naturality follows by universal property of pullback.

Proof of Proposition 9.12. Because the tensor preserves all colimits on the left, pointed strong endofunctors are closed under coproducts, so it suffices to show that both terms of the sum are pointed strong. The first one inherits the pointed strength of Σ 0 , while the pointed strength of -; ∼ ⊗ 0 follows from Lemma 9.13 and substitution-closedness of ∼ ⊗ 0 , like so:

Presheaf categories being well-known to be closed under the slice construction, we have the following.

Lemma 9.14. The category C 0 /Z 2 0 is a presheaf category. This allows us to deduce the following.

Proposition 9.15. The endofunctor Σ 0 is finitary.

Proof. By commutation of filtered colimits with finite limits in presheaf categories. By Proposition 9.12, Lemma 9.14, and Proposition 9.15, the following is legitimate. Definition 9.16. Let 0 = Z Σ 0 denote the initial Σ 0 -monoid. We denote by 1 , 2 : 0 → Z 0 the left and right projections. By Proposition 5.4, we also get the following for free.

Proposition 9.17. The object 0 → Z 2 0 is an initial algebra for the endofunctor C 0 /Z 2 0 → C 0 /Z 2 0 mapping any → Z 2 0 to + Σ 0 ( ) → Z 2 0 . Proposition 9.18. The underlying object 0 is a Σ 0 -monoid.

Proof. Directly follows from the Σ 0 -monoid structure.

Next, we exhibit an alternative characterisation of 0 , which relies on the following result. Proposition 9.20. The object 0 → Z 2 0 is an initial algebra for the endofunctor

We observe that preserves coproducts (because pullback along the first projection ∼ ⊗ 0 → Z 0 , as a left adjoint, preserves colimits), so that ★ ( ) ( ). By commutation of coproducts with ; -, we thus have

Thus, by Lemma 9.19, we get ★ ( ( )) ( + Σ 0 ( )); ∼ ⊗ * 0 ( ; ∼ ⊗ * 0 ) + (Σ 0 ( ); ∼ ⊗ * 0 ), as desired. 9.3. Double categorical notation. Our next goal is to define the Howe closure on transitions. For this, we appeal to Morton's double bicategories [START_REF] Morton | Double bicategories and double cospans[END_REF]. They are a refinement of double categories, in which both the horizontal and vertical categories are bicategories. We rely in particular on his Theorem 4.1.3, which (when dualised) states that for any category with pullbacks, there is a double bicategory 2Sp ( ): • objects are objects of , • both the vertical and horizontal bicategories are Span ( ), Proof. By interchange of limits.

Let us end this subsection by generalising simulations to 2Sp ( C 1 ). By Proposition 4.17, the span denoted by a cell (9.2, right) in 2Sp ( C 1 ) is a simulation iff the top left square in the corresponding diagram (9.2, left) is a pointwise weak pullback. Abstracting over this: Definition 9.23. A cell in any double bicategory of the form 2Sp ( C) is a simulation iff its top left square is a pointwise weak pullback.

Proposition 9.24. Simulations are closed under horizontal and vertical composition in any double bicategory of the form 2Sp ( C).

In order to prove this, we need the following weak analogues of the pullback lemma.

Notation 9.25. We denote weak pullbacks (in any category) by dashed corners.

Lemma 9.26. In any category (resp. presheaf category), (i) for any commuting diagram , if both squares are weak pullbacks (resp. pointwise weak pullbacks), then so is the outer rectangle; and (ii) for any commuting diagram , if the right-hand square is a pullback and the outer rectangle is a weak pullback (resp. pointwise weak pullback), then the left-hand square is a weak pullback (resp. pointwise weak pullback).

Proof. Similar to the proof of the standard pullback lemma.

Proof of Proposition 9.24. Straightforward, using Lemma 9.26.

For vertical composition with cells from 2Sp ( C 0 ), as in Notation 9.21, we will also need the following. Proposition 9.27. Precomposition with s and t yields maps 2Sp ( C 0 ) → 2Sp ( C 1 ) between cell sets, which preserve borders and simulations.

Proof. Both precomposition functors straightforwardly preserve pointwise weak pullbacks. which in terms of spans yields exactly the desired form.

Corollary 9.47. We have

9.6. Simulation property. Our next goal is to prove the following.

Lemma 6.17. If Σ 1 preserves functional bisimulations, then the transition Howe closure is a substitution-closed simulation.

The rest of this subsection is devoted to the proof. For substitution-closedness, ∼ ⊗ 0 is reflexive and by Lemma 6.16 we have a span morphism ∼ ⊗ 0 → 0 , so we may form the composite 0 ⊗ Z → 0 ⊗ ∼ ⊗ 0 → 0 ⊗ 0 → 0 , where the last morphism is the monoid multiplication of 0 , as established in Proposition 9.18.

For the simulation property, we will use the characterisation of as Z Σ 1,lax . For this, we need to lift the notion of simulation from C to C lax . Recalling the functor : C lax → C 2 from Definition 9.40, which maps each span ← → Z in C lax to its left-hand leg ← , we have:

Definition 9.48. An object ← → Z of C lax is a simulation iff its image by , i.e., ← , is a functional bisimulation.

Next, we want to show that the computation of as an initial chain in C lax is preserved by . We intend to use this to apply Lemma 1.8, which will reduce our goal to proving that each object of the chain is a functional bisimulation.

Lemma 9.49. All of the following functors are cocontinuous:

(i) any functor from the terminal category;

(ii) both functors C 1 /Δ( ) : C 1 /Δ( 0 ) → C 1 /Δ(Z 0 ), for = 1, 2, which map any span

(iii) the projection functor : C → C 1 /Δ( 0 ), mapping any object (9.9) to (the pairing of ) its left-hand border 0 s ← 1 → 0 t;

Proof.

(i) Trivial.

(ii) As post-composition functors, these have right adjoints.

(iii) C is by definition the comma category Our next step, in order to apply Lemma 1.8, is to prove that each object of the initial chain for Z is a simulation in C lax . This will follow from the next result.

Lemma 9.50. If Σ 1 preserves functional bisimulations and ∈ C lax is a simulation, then so is Σ 1,lax ( ).

Proof. The pasting (9.8) is isomorphic to the following.

By Propositions 9.24 and 9.27, it suffices to show that all non-identity cells in (9.10) are simulations if is. Let us run through them, left-to-right, top-to-bottom:

similarly, by Proposition 9.20, 0 is the initial algebra for the endofunctor ↦ → ( ;

are pullbacks. The right-hand one is mapped by Δ s (which, as a right adjoint, preserves pullbacks) precisely to the top left square of the top cell. • The first little cell Σ 1 ( ) is a simulation by hypothesis.

• The middle little cell is trivially a simulation.

• The third little cell ∼ ⊗ * 1 is a simulation because simulations are closed under transitive closure.

• Finally, the bottom cell is trivially a simulation.

Finally:

Proof of Lemma 6.17. Let us start by observing that, because the domains and codomains of all are representable, hence finitely presentable, functional bisimulations are closed under filtered colimits in C 2 , by Lemma 1.8. Now, the first projection Z 0 ← 0 is trivially a functional bisimulation, since there are no transitions in Z 0 , so by Proposition 9.41 the initial object ∅ C lax of C lax is a simulation in the sense of Definition 9.48. Hence, by induction, using Lemma 9.50, so are all objects of the initial chain of Σ 1,lax . Thus, by Definition 9.48, maps this initial chain to a chain of functional bisimulations in C 2 and so By Lemma 9.10, Lemma 6.19 will follow if we construct a span morphism 0 → + † 0 . As 0 is an initial algebra for + Σ 0 (Proposition 9.17), it suffices to prove the following lemma.

Lemma 9.51. The span + † 0 has an algebra structure for ( + Σ 0 ). This relies on the following lemmas, used in particular with = Σ 0 . The first one is well known: Lemma 9.52. Given an endofunctor on some category , the forgetful functor -alg → creates limits, and all colimits that preserves.

Lemma 9.53. Given an endofunctor on a regular category , if preserves reflexive coequalisers, then the forgetful functor from the category of -algebras creates image factorisations.

Proof. Suppose given an algebra morphism -→ . The image factorisation is obtained as the (reflexive) coequaliser of the kernel pair × ⇒ . The diagram of this reflexive coequaliser lifts to -alg, hence so does the coequaliser, by the previous lemma.

Proof of Lemma 9.51. We need to find algebra structures on + † 0 for , Σ 0 , and -; ∼ ⊗ 0 . For , we have the morphism → Z 0 → † 0 → + † 0 . For Σ 0 , note that by Lemmas 9.9 and Corollary 9.8, + † 0 is the colimit of the chain

. . As it is filtered and thus sifted, and Σ 0 preserves sifted colimits by hypothesis, by Lemma 9.52, it is enough to show that each † 0 ; . . . ; † 0 has a structure of Σ 0 -algebra (morphisms in the above chain are then automatically algebra morphisms because the involved spans are relations). But, Σ 0 also preserves reflexive coequalisers (which are sifted colimits), so, by Lemma 9.53, the forgetful functor from Σ 0 -algebras creates image factorisations. It is thus enough to equip † 0 ; . . . ; † 0 with Σ 0 -algebra structure, which is straightforward because 0 is already an algebra and algebras are stable under pullbacks (Lemma 9.52).

It remains to find a suitable morphism + † 0 ; ∼ ⊗ 0 → + † 0 , or equivalently, by applying - † , a morphism ∼ ⊗ † 0 ; + 0 → + 0 . But by symmetry of ∼ ⊗ 0 , we have the composite ∼ ⊗ † 0 ; + 0 → ∼ ⊗ 0 ; + 0 → 0 ; + 0 → + 0 .