Tom Hirschowitz

A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on

Keywords: syntax, variable binding, substitution, category theory

We introduce a category-theoretic abstraction of a syntax with auxiliary functions, called an admissible monad morphism. Relying on an abstract form of structural recursion, we then design generic tools to construct admissible monad morphisms from basic data. These tools automate ubiquitous standard patterns like (1) defining auxiliary functions in successive, potentially dependent layers, and (2) proving properties of auxiliary functions by induction on syntax. We cover significant examples from the literature, including the standard lambda-calculus with capture-avoiding substitution, a lambda-calculus with binding evaluation contexts, the lambda-mu-calculus with named substitution, and the differential lambda-calculus.

INTRODUCTION

Motivation. The literature offers several initial-algebra semantics frameworks for generating and reasoning about syntax with variable binding (e.g., [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF][START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF][START_REF] Gabbay | A New Approach to Abstract Syntax Involving Binders[END_REF][START_REF] Hofmann | Semantical Analysis of Higher-Order Abstract Syntax[END_REF]). Still, even state-of-the-art frameworks lack some expressiveness to suit the working operational semanticist's needs. One typical limitation, which is the topic of active research [START_REF] Coraglia | Context, judgement[END_REF][START_REF] Gratzer | Syntactic categories for dependent type theories: sketching and adequacy[END_REF], concerns some complex typing features like dependent types.

In this paper, we are concerned with a different limitation: although existing frameworks do explain capture-avoiding substitution satisfactorily, they largely ignore the numerous similar auxiliary operations on syntax, like context application (e.g., in ML [Pierce 2004, Chapter 10]), named substitution in the -calculus [START_REF] Parigot | -calculus: an algorithmic interpretation of classical natural deduction[END_REF]] (a.k.a. named application [START_REF] Vaux | calcul différentiel et logique classique : interactions calculatoires[END_REF]]), partial differentiation in the differential -calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF], and so on.

One way of dealing with such auxiliary operations is to build them into the syntax, and view their defining equations as an equational theory, by which to quotient the initial model (see, e.g., [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF][START_REF] Gratzer | Syntactic categories for dependent type theories: sketching and adequacy[END_REF]). The problem with this approach is that it lacks the basic, inductive construction of the initial model. Or in other words, it misses the fact that auxiliary operations are... auxiliary, i.e., that they are admissible (= encodable) in the initial model.

Contributions.

In this paper, we propose a categorical foundation for such admissible operations, called admissible monad morphisms, together with a general framework for constructing them and reasoning about them. In particular, the framework offers tools to (a) define successive layers of auxiliary operations, each layer potentially depending on previous ones (as, e.g., in the differential -calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF]), (b) automatically derive benign equations, i.e., equations involving auxiliary operations that are satisfied by the syntax (such as, e.g., associativity of substitution

[ ] [ ] = [ [ ]]).
Remark 1. The framework does not yet allow the user to automatically prove that auxiliary operations are compatible with severe equations, i.e., equations not involving auxiliary operations (as, again, in the differential -calculus), whose initial model thus may be a proper quotient of the syntax.

We illustrate the expressiveness of the framework by reconstructing (1) Fiore et al. 's [1999] approach as a special case, and (2) a few concrete examples from the literature, notably a -calculus with explicit substitution [START_REF] Accattoli | A Fresh Look at the lambda-Calculus (Invited Talk)[END_REF]] (which involves variable capture by evaluation contexts) and the differential -calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF] (without quotienting by structural equations). We also demonstrate that our framework is not tied to any particular setting for modelling variable binding, by reconstructing pure -calculus with capture-avoiding substitution in De Bruijn representation ( §4.6).

The framework consists of the following components.

1. First, we offer a fundamental, very easy construction of admissible monad morphisms from suitable monad distributive laws in the sense of [START_REF] Beck | Distributive laws[END_REF]. A monad distributive law is a natural transformation → , where we think of as the monad of basic operations, hence call it the basic monad, and of as the one of auxiliary operations, hence call it the auxiliary monad. We show that, whenever preserves the initial object, any monad distributive law induces an admissible monad morphism → to the composite monad. 2. Then, we design a toolbox for constructing such distributive laws from more basic data:

(i) We first introduce a simple notion of signature for distributive laws. A signature consists of an endofunctor Σ, equipped with an abstract analogue of a structurally recursive definition, called a simple structural law. From such a signature, we generate a distributive law of the desired form, whose basic monad is the free monad Σ * on Σ. We also establish a simple characterisation of augmented algebras, i.e., Σ-algebras featuring the specified auxiliary operations in a compatible way. Simple structural laws are expressive enough to equip (potentially binding) syntax with captureavoiding substitution, but not to tackle Features (a) and (b) above. (ii) We then introduce a second notion of signature, which is an incremental form of the first. A signature consists of a distributive law : → whose basic monad is free on some endofunctor Σ, equipped with a so-called incremental structural law over it. The idea is that we have already specified a few auxiliary operations over , bundled as the monad , and an incremental structural law is like a structurally recursive definition by pattern-matching on basic operations, whose body may use all auxiliary operations. From this, we construct a new distributive law with the same basic monad, but whose auxiliary monad contains new operations. We again present a simple explicit description of augmented algebras. Incremental structural laws are expressive enough to equip syntax with incremental layers of auxiliary operations, hence implement Feature (a) above.

(iii) We finally address the benign equations feature (b). For this, we again start from a distributive law with a free basic monad, and introduce structural equational systems, which, roughly, consist of:

• (an abstract form of) equations on terms, potentially using auxiliary operations, and • data that ensures that the equations will be satisfied by the syntax. From this, we construct a distributive law with the same basic monad.

Plan. We start in §2 by introducing admissible monad morphisms and showing how they may be derived from suitable monad distributive laws. We then study simple structural laws in §3, incremental structural laws in §4, and benign equations in §5, giving applications along the way. Finally, we conclude and give some perspectives in §6.

Related work. Our framework abstracts over the idea of a definition by structural recursion, to categories other than sets. The abstraction emphasises the idea that the syntax equipped with auxiliary functions is initial in a category of augmented algebras. Our framework is directly inspired by (and abstracts over) Fiore et al. 's [Fiore et al. 1999;[START_REF] Fiore | Second-Order and Dependently-Sorted Abstract Syntax[END_REF]. A notable difference is that Fiore et al. rely on a technical notion called pointed strong endofunctors, which intuitively amounts to assuming that the argument of the endofunctor already has part of the desired structure -in this case, variables. The corresponding instance of our abstract framework avoids this astute trick by taking the free structure. Technically, this is visible in the presence of ⊗ ( ) in the codomain of our simple structural law in §3.5. Indeed, taking ( ) instead of merely is what allows us to use ↑ in the definition.

Our work is related to the idea of traversals [START_REF] Allais | A type and scope safe universe of syntaxes with binding: their semantics and proofs[END_REF]]. The latter are however limited to categories of families of sets indexed by some fixed set of types, and tailored for capture-avoiding substitution.

Notation and prerequisites. We often conflate natural numbers with the corresponding finite ordinals, or some choice of equipotent set, hopefully made clear by the context.

We assume basic knowledge of category theory [START_REF] Mac | Categories for the Working Mathematician[END_REF] and locally finitely presentable categories [START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF] (although the latter may be ignored on a superficial reading). By default, our categories are locally small, although we occasionally repeat it for emphasis. We let CAT denote the category of (locally small) categories.

We generally denote initial objects by ∅, relying on context to infer the corresponding category. For any category C and object ∈ C, we denote by C/ the slice category over .

On any category C with binary coproducts, for any object ∈ C, we denote the corresponding option functor by , i.e., ( ) = + , for some choice of coproducts.

For any endofunctor , we denote its category of algebras byalg. For any monad , we denote its category of monad algebras by -Alg; it is then a full subcategory ofalg. We denote the coproduct of two monads and ′ by ⊕ ′ , to distinguish it from the coproduct + ′ of underlying endofunctors.

Any finitary endofunctor on a locally finitely presentable category C generates a free monad, that we denote by * . In particular, the initial algebra is denoted by * ∅. As is well-known, this may often be computed as a directed colimit which we denote by . ( ). We furthermore denote the unit → * by . Please also note that * -Alg is isomorphic toalg: the isomorphism maps an algebra * → to → * → . We write Δ for the diagonal functor C → C × C mapping an object of a category C to ( , ). We use the letters Γ and Θ to denote bifunctors C × C → C. We sometimes write Γ instead of ΓΔ. E.g., we talk about Γ-algebras instead of ΓΔ-algebras, and denote (ΓΔ) * by Γ * . We furthermore sometimes denote Γ( , ) by Γ . If is a functor to C, the bifunctor mapping ( , ) to Γ( , ) is denoted by Γ . Moreover, for denoting the components of a natural transformation : → , we freely switch between and , and we denote horizontal composition in CAT by mere juxtaposition. E.g.,. given any : → in the domain category, we also write , or , for either composite

• ( ) = ( ) • .
The middle dot • is overloaded: it may have the followin three meanings, depending on context:

• for any presheaf : C op → Set, morphism : → in C, and element ∈ ( ), we define • := ( ) ( ); • for any set and object of any category with enough coproducts, we denote by • the -fold coproduct

∈

; and finally, • the middle dot is used in the syntax of differential -calculus. Definition 1.1. A monad morphism → between monads and on a given category C is a natural transformation : → commuting with multiplication and unit, i.e., making the following diagrams commute.

id C

We let Mnd(C) denote the category of monads in C and monad morphisms between them, and Mnd (C) denote its full subcategory spanned by finitary monads.

ADMISSIBLE MONAD MORPHISMS AND DISTRIBUTIVE LAWS

In this section, we introduce admissible monad morphisms, and show how to construct them from monad distributive laws.

Admissible monad morphisms

Definition 2.1. Let C have an initial object. A morphism : → of monads on C is admissible iff its component ∅ : ∅ → ∅ at the initial object is an isomorphism.

Remark 2. Intuitively, thinking of and as algebraic structures, or families of operations, (∅) and (∅) are the initial algebras, i.e., morally the syntaxes of both languages. The monad morphism translates each operation from to some (derived) operation from . Admissibility then amounts to the translation being an isomorphism.

We will give the paradigmatic example of admissible morphism just below, but before that, let us mention a different point of view on admissible morphisms. Definition 2.2 ( [Mac Lane 1998, §VI.3]). We call monadic (over C) any functor isomorphic in CAT/C to some forgetful functor -Alg → C, and let Monadic/C denote the full subcategory of CAT/C spanned by monadic functors.

Given a category C, the assignment mapping any monad on C to the forgetful functor : -Alg → C extends to a functor sem : Mnd(C) op → Monadic/C, and we have:

L 2.3.
The functor sem is an equivalence of categories.

P

. The functor sem is essentially surjective by definition of monadic functors. It is also full and faithful by [Barr 1970, Proposition 5.3].

P

2.4. Given a category C with initial object, monads and on C, and a monad morphism : → , the following are equivalent: [Mac Lane 1998, §V.1], which in this case means that the initial -algebra ∅ possesses a unique -algebra structure : ∅ → ∅ making the triangle

(i) is admissible; (ii) sem( ) : -Alg → -Alg preserves the initial object; (iii) sem( ) : -Alg → -Alg creates the initial object in the sense of
∅ ∅ ∅ ∅ ∅
commute, which furthermore makes it initial in -Alg.

P

. See §A.

Example 2.5. Our motivating example is in fact a class of examples. For any finitary, pointed strong endofunctor Σ on any nice monoidal category (C, ⊗, , , , ) (the impatient reader may consult Definitions 5.14 and 5.16 below for details, but these are not yet needed), [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF] introduce a category Σ -Mon of Σ-monoids, which are objects ∈ C with both Σ-algebra structure Σ → and monoid structure → ← ⊗ , satisfying a standard coherence condition (Definition 5.15 below).

They then show that the initial ( + Σ)-algebra, or equivalently the free Σ-algebra on , admits a unique Σ-monoid structure, which makes it initial in Σ -Mon. Furthermore, both forgetful functors from ( +Σ)alg and Σ -Mon to C are monadic, and there is an obvious forgetful functor Σ -Mon → ( + Σ)alg.

Thus, denoting by ( +Σ) * and Σ ⊛ the corresponding monads, their result may be read as proving that the induced monad morphism ( + Σ) * → Σ ⊛ is admissible.

From distributive laws

Let us now show how to construct admissible monad morphisms from distributive laws. We first recall from [START_REF] Beck | Distributive laws[END_REF]] that (i) a monad distributive law of over is a natural transformation :

→ , commuting with unit and multiplication of both monads and , and that (ii) any such distributive law equips the composite functor with monad structure, which in particular makes the natural transformation : → into a monad morphism. The idea is to start from a distributive law with a suitable constraint on , namely that (∅) ∅. Intuitively, may have many operations, but no constants to feed them with. We name such monads accordingly: Definition 2.6. A monad on a category with an initial object ∅ is constant-free iff its unit at ∅, ∅ : ∅ → (∅), is an isomorphism. P 2.7. For any distributive law : → with constant-free, the monad morphism : → is admissible.

P . Immediate.

This result might seem purely academic, but in fact all of our applications arise in this way. The technical core of the paper thus consists in designing tools to construct such distributive laws over constant-free monads.

SIMPLE STRUCTURAL LAWS

In this section, we introduce our first construction of distributive laws with constant-free auxiliary monad, from what we call simple structural laws. Let us start by working on a simple (perhaps surprising) example, and abstract over it in the following subsection.

On a simple example

We consider the unary (Peano) natural numbers, viewed as the initial algebra of the endofunctor Σ on sets defined by Σ( ) = 1 + . We use standard syntax, i.e., 0 for the constant and for successor. Let us now consider the category, say Σalg add , of Σ-algebras equipped with a binary operation, denoted by ( , ) ↦ → + , satisfying the following equations.

( ) + = ( + ) 0 + =
We call such an operation an addition. P 3.1. The initial algebra Σ * (∅) is equipped with a unique addition, which makes it initial in the category of Σ-algebras with addition.

P

. An easy induction.

Furthermore, the forgetful functor add : Σalg add → Set is monadic, and the corresponding monad, say add maps any set of variables to terms generated from 0 and all ∈ by and +, modulo the above equations. Now, for each set , there is an obvious inclusion ↩→ add . This family of inclusions induces a monad morphism → add , and it is admissible by Propositions 3.1 and 2.4.

Let us now describe the monad add and its relation to more carefully, which will lead us to distributive laws.

Orienting equations, terms generated by 0, , and + from a given set of variables, quotiented by the equations, have a normal form in which the first argument of an addition is either a variable, or a further addition. Otherwise said, normal forms with variables in are generated by the following grammar:

:

:= 0 | ( ) | ::= | + . (1)
Clearly, if no variable is available, only the first two cases can occur in a term , which together correspond precisely to the syntax generated by . We thus recover the fact that ∅ → add ∅ is an isomorphism.

Let us replay this reasoning, at a slightly more abstract level. The starting point is to refine the arity of the auxiliary function (addition), here the endofunctor ↦ → 2 , into a bifunctor

Γ : Set 2 → Set ( , ) ↦ → × .
Intuitively, this allows us to distinguish the "decreasing" occurrence of the argument. By mimicking the recursive definition of addition on ∅, we then define the following natural transformation , :

Γ(Σ( ), ) → (Γ( , ) + ) (0, ) ↦ → ( 2 ( )) ( ( ), ) ↦ → ( ( 1 ( , ))), (2)
where we write elements of Σ( ) as terms of depth 1 in ( ), for any set . (We will use a slightly more general codomain in the abstract case.) Elements of the domain are thought of as patterns in the first argument, and the natural transformation maps them to "definition bodies", which are basic terms generated from the auxiliary arguments in , and potentially a "recursive call" in Γ( , ) -hence with "strictly smaller" main argument.

We furthermore define a monad := Γ * , which, we recall from §1, denotes (Γ Δ) * . Concretely, ( ) := .( + × ( )) corresponds to the syntactic category above: terms consist of additions in normal form, i.e., additions whose first argument may be a variable or some further addition, inductively, and whose second argument is an arbitrary expression. We thus have add

• . Finally, we construct a distributive law → , by induction from the natural transformation (2), which repeatedly applies oriented equations until some normal form is reached. We will be done if we prove (∅) ∅, for then

add (∅) (∅) (∅),
as desired. But (∅) ∅ follows from the next lemma with Θ = Γ . L 3.2. For any category C and functor Θ : C 2 → C, if Θ is cocontinuous in its first argument and finitary in its second argument, then the initial object possesses a unique ΘΔ-algebra structure, which furthermore makes it initial in ΘΔalg.

P

. By cocontinuity, Θ ∅ ∅ is initial, hence there is a unique morphism Θ ∅ ∅ → ∅. The rest follows easily.

It may not be entirely obvious that Γ is cocontinuous in its first argument, but × is isomorphic to the coproduct ∈ , which is cocontinuous by interchange of colimits. Most of our examples below follow the same pattern.

The abstract case

In this subsection, we introduce the general notion of simple structural law, and construct, from any such law, a monad distributive law with constant-free auxiliary monad. Definition 3.3. A simple structural law on a given locally finitely presentable category C consists of

• a basic finitary endofunctor Σ : C → C,

• an auxiliary functor Γ : C 2 → C which is cocontinuous in its first argument and finitary in its second argument, and • a natural transformation , : Γ (Σ( )) → (Γ ( ) ( ) + + ), where := Σ * denotes the free monad generated by Σ.

Remark 3. Comparing with the example (2) of the previous section, we have added a new base case , and replaced with the more general ( ) in the recursive call.

Let us now state the construction result, relying on the following lemma.

L 3.4. For any finitary bifunctor : C 2 → C which is cocontinuous in its first argument, * is constant-free.

P

. More generally, if an endofunctor preserves the initial object ∅, then ∅ equipped with the isomorphism (∅) → ∅ is easily seen to be the initial -algebra, hence is isomorphic to * ∅.

Furthermore, being constant-free by Lemma 3.4, the monad morphism → is admissible.

P

. This is a special case of Theorem 4.10 below, instantiating with the identity monad.

Remark 4. By the usual characterisation of free algebras for finitary endofunctors [START_REF] Reiterman | A left adjoint construction related to free triples[END_REF]], we have ( ) = .( + Γ ( )).

Augmented algebras

As a bonus, we may characterise algebras for the generated monad , which we call augmented algebras.

Definition 3.6.

• An algebra for a simple structural law = (Σ, Γ, ) on C consists of an object ∈ C, equipped with -Σ-algebra structure a : Σ( ) → and -ΓΔ-algebra structure b : Γ ( ) → , making the following diagram commute,

Γ (Σ( )) (Γ ( ) + + ) (Γ ( ) + + ) Γ ( ) , Γ (a)
(Γ ā ( )+ + ) [b, , ] b ā
where ā : ( ) → is freely induced by a. • A morphism → of algebras for = (Σ, Γ, ) is a morphism between underlying objects which is both a morphism of Σ-and ΓΔ-algebras. • Letalg denote the category of algebras for , or -algebras. P 3.7. Let = (Σ, Γ, ) be any simple structural law on C, and let = Γ * . Then we have alg -Alg over C, where we recall from the basic notations of §1 that capital Alg denotes monad algebras.

P

. This is a special case of Theorem 4.13 below, instantiating with the identity monad.

Application: evaluation contexts

Let us present a first application of Theorem 3.5, to generate a simple language with context application. The language is generated by the following grammar

, ::= | | . ::= |
and context application is defined inductively by

[ ] = ( ) [ ] = [ ] .
We now define a simple structural law, whose basic monad is the term monad, including contexts, and whose associated auxiliary monad will account for context application.

• Following [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF], at least in spirit, we first choose as ambient category the category [Set, Set 2 ] of finitary functors Set → Set 2 , or equivalently [F, Set 2 ], where F denotes the category of finite ordinals and all maps between them.

We call p and c the two elements of 2, respectively for "program" and "context".

For any object ∈ [F, Set 2 ] and ∈ F, ( ) is a pair of sets, which we denote by ( ( ) p , ( ) c ). We think of -( ) p as a set of programs with free variables, and of -( ) c as a set of contexts with free variables. • The basic endofunctor is defined by:

Σ( ) ( ) p = + ( ) 2 p + ( + 1) p ( , ::= | | . ) Σ( ) ( ) c = 1 + ( ) c × ( ) p ( ::= | ).
• The auxiliary bifunctor is

Γ( , ) ( ) p = ( ) c × ( ) p Γ( , ) ( ) c = ∅.
• For our simple structural law, which is trivial by construction at c, we take at p:

Σ( ) ( ) c × ( ) p → (Γ( , ( )) + + ) ( ) p ( , ) ↦ → ( 3 ( )) ( , ) ↦ → ( 1 ( , ( ))) ( 2 ( )).

Application: capture-avoiding substitution

In this section, we present a third application of Theorem 3.5, to pure -calculus with captureavoiding substitution. This will be subsumed by §5.5, but we find it instructive to unfold the development on a concrete example.

• We take as ambient category the category [Set, Set] of finitary endofunctors of sets, or equivalently

[F, Set]. • The basic endofunctor on [F, Set] is defined by Σ( ) ( ) = + ( ) 2 + ( + 1) ( , ::= | | ).
• The auxiliary bifunctor is [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF]]'s substitution tensor product

( ⊗ ) ( ) = ∫ ( ) × ( ) , or, expressed in [Set, Set] , ( ⊗ ) ( ) = ( ( )).
• For our simple structural law, we take (sometimes omitting for readability)

∫ Σ( ) ( ) × ( ) → ( ⊗ ( )) + + ) ( ) ( , ) ↦ → 3 ( ( )) ( , ) ↦ → 1 ( , • ) 1 ( , • ) ( , ) ↦ → ( 1 ( , ↑ )),
where ↑ : + 1 → ( ) ( + 1) denotes the copairing of the following two maps.

-→ ( )

( 1 ) -----→ ( +1) , +1 ----→ ( ) ( +1) 1 2 --→ +1 1 --→ Σ( ) ( +1) ↩→ ( ) ( +1)
Remark 5. In the final case, we crucially rely on the recursive call being in Γ( , ), rather than just Γ( , ). In [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF], this is done by taking "pointed", in the sense of being equipped with a natural transformation → ( ).

Remark 6. We obtain the expected syntax and substitution, but not yet the following standard equations,

[ ] [ ′ ] = [ [ ′ ]] [id] =
where id : → ( ) ( ) picks the variables. We will complete the picture in §5.

Application: binding contexts

For a slightly more involved example, we consider in this subsection the sharing -calculus [Accattoli 2019, §4.1] (but see also [START_REF] Hirschowitz | Compilation of extended recursion in call-by-value functional languages[END_REF][START_REF] Sewell | Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction[END_REF]). Following Accattoli, the syntax is given by

, ::= | | . | ↦ → ::= | ↦ → .
Context application is then defined inductively by

[ ] = ( ↦ → ) [ ] = [ ] ↦ → .
Remark 7. Context application may give rise to variable capture. E.g., ( ↦ → ) [ ] = ↦ → .

In order to model this, we extend the setting of the previous section as follows. In §3.4, for any functor : F → Set 2 , we thought of ( ) p and ( ) c as sets of programs, resp. contexts with free variables. We now need to refine this point of view, and index contexts over the number of capturing variables, i.e., variables bound above the context hole . Instead of functors F → Set 2 , we thus consider functors F → Set 1+N . Of course, we have N 1 + N, but we write 1 + N to emphasise the fact that 1 (★), the unique element of the left-hand summand, models terms, while each 2 ( ) models contexts with capturing variables. Notation 1. We abbreviate 1 (★) to p and 2 ( ) to c , so that, e.g., ( ) c is thought of as a set of contexts with free variables and capturing variables.

Accordingly, we specify the syntax by the endofunctor

Σ( ) ( ) p = + ( ) 2 p + ( + 1) p + ( + 1) p × ( ) p Σ( ) ( ) c +1 = ( + 1) c × ( ) p Σ( ) ( ) c 0 = 1.
Remark 8. On the second line, the expression ( + 1) c × ( ) p reflects the fact that in the above grammar, in ↦ → , may use the bound variable , hence the use of + 1, and has one less capturing variable than ↦ → , hence the passing from + 1 to . Otherwise said, is free in , but capturing in ↦ → .

The generated monad = Σ * may be presented syntactically by the following rules

∈ ( ) p ⊢ : p ∈ ⊢ : p ⊢ : p ⊢ : p ⊢ : p + 1 ⊢ : p ⊢ ( ) : p + 1 ⊢ : p ⊢ : p ⊢ : p ∈ ( ) c ; ⊢ : c ; 0 ⊢ : c + 1; ⊢ : c ⊢ : p ; + 1 ⊢ : c , with ( ) p = { | ⊢ : p} and ( ) c = { | ; ⊢ : c}.
One then straightforwardly defines the functorial action in : for any renaming : → ′ , one replaces all with ( ) , for ∈ .

Let us now model context application by a simple structural law:

• the arity functor is defined by

Γ( , ) ( ) c = ∅ Γ( , ) ( ) p =
∈N ( ) c × ( + ) p , reflecting the fact that in a context application [ ], has as free variables the disjoint union of the free and capturing variables of ;

• the simple structural law is defined componentwise by

Σ( ) ( ) c × ( + ) p → (Γ( , ( )) + + ) ( ) p ( , ) ↦ → 3 ( ) (if = 0) ( , ) ↦ → 1 ( , ) 2 ( ) (if = ′ + 1),
for all , ∈ N (omitting again for readability).

Remark 9. The reason may be applied to both and is that both contexts have the same number of free or capturing variables (( + 1) + ′ and + ( ′ + 1), respectively).

Application: named substitution

Let us now consider a last illustration of simple structural laws: named substitution in -calculus [START_REF] Parigot | -calculus: an algorithmic interpretation of classical natural deduction[END_REF][START_REF] Vaux | calcul différentiel et logique classique : interactions calculatoires[END_REF]. Its usual form is as follows. The syntax of -calculus is:

, , ::= | | . | . , ::= [ ] .
There are two syntactic categories: programs, ranged over by , , , . . ., and continuations, ranged over by , . Accordingly, there are two kinds of variables: program variables, ranged over by , , , . . ., and continuation variables, ranged over by , , . . .

Remark 10. In this subsection, always denote the syntactic operation, as opposed to any monad multiplication, or least fixed-point operator.

Intuitively, named substitution ( ) (notation from [Vaux 2007, Definition 6.5]) takes as argument any term (program or continuation) with a distinguished continuation variable , together with a program , and replaces all subterms of the form [ ] with [ ] ( ) in . This may be defined recursively by:

( ) = ( . ) = .(( ) ) ( ∉ ) ( ) = (( ) ) (( ) ) ( . ) = .(( ) ) ( ∉ , ) ( [ ] ) = [ ] ((( ) ) ) (if = ) [ ] (( ) ) (otherwise).
In order to model this categorically, since we have two syntactic categories, each with its own set of variables, we work with finitary functors Set 2 → Set 2 , or equivalently the category [F 2 , Set 2 ]. We write p and c for the elements of 2 (respectively standing for "program" and "continuation"). Thus, for any ∈ [F 2 , Set 2 ], we think of • ( , ) p as a set of programs with free program variables and continuation variables, and of • ( , ) c as a set of continuations with free program variables and continuation variables.

The basic syntax is specified by the endofunctor Σ defined by

Σ( ) ( , ) p = + ( , ) 2 p + ( + 1, ) p + ( , + 1) c Σ( ) ( , ) c = × ( , ) p .
For specifying named substitution, we take as auxiliary bifunctor

Γ( ) ( , ) p = ( , ) p × × ( , ) p Γ( ) ( , ) c = ( , ) c × × ( , ) p .
Notation 2. Slightly generalising previous notation, we denote by the th program variable, for ∈ , and by the th continuation variable, for ∈ .

Using this notation, we model named substitution by the following simple structural law (omitting again for readability):

, , , ,p : Σ( ) ( , ) p × × ( , ) p → (Γ( , ) + + ) ( , ) p ( , , ) ↦ → 2 ( ) ( ( ), , ) ↦ → ( 1 ( , , p , • )) ( , , ) ↦ → 1 ( , , ) 1 ( , , ) ( ( ), , ) ↦ → ( 1 ( , , c , • )) , , , ,c : Σ( ) ( , ) c × × ( , ) p → (Γ( , ) + + ) ( , ) c , i.e., , , , ,c : × ( , ) p × × ( , ) p → (Γ( , ) + + ) ( , ) c ( [ ] , , ) ↦ → [ ] ( 1 ( , , ) 3 ( )) ( [ ′ ] , , ) ↦ → [ ′ ] 1 ( , , ) (for ′ ≠ ),
where

• p , := ( 1 , ) : ( , ) ↩→ ( + 1, ); • c , := ( , 1 ) : ( , ) ↩→ ( , + 1
); and • • denotes the action of a morphism : ( , ) → ( ′ , ′ ) in F 2 on an element of some ( , ) , for some : F 2 → Set 2 and ∈ {p, c}.

INCREMENTAL STRUCTURAL LAWS

In this section, we introduce the incremental variant of structural laws. In §4.1, we sketch the idea on a simple example. In §4.2, we introduce incremental structural laws in full generality, and prove that they induce admissible morphisms (Theorem 4.2). In §4.3, we characterise the composite monad induced by an incremental structural law, as objects equipped with suitably compatible algebra structures. Then, in §4.4, we explain how to combine several, independent incremental structural laws. Finally, we cover applications: partial differentiation in the differential -calculus ( §4.5), and De Bruijn's presentation of capture-avoiding substitution in the -calculus ( §4.6).

On a simple example

Recalling the distributive law, say : → constructed in §3.1 from the simple structural law (2), we now want to extend the language with a second binary operation, multiplication, satisfying

( ) × = ( × ) + 0 × = 0.
Furthermore, the full quotiented term language yields a monad add,mul , and a monad morphism → add,mul . As in §3.1, orienting equations, we obtain normal forms, which are generated for any argument by the grammar

::= 0 | ( ) | ::= | + | × .
Of course, by the same reasoning as for mere addition, the initial -algebra is initial in the category of models of the whole language (i.e., -algebras with addition and multiplication, satisfying all four equations), hence the monad morphism → add,mul is admissible. Categorically, because the new equation uses addition, we cannot define a second, independent structural extension of . However, the recursive definition of multiplication yields a natural transformation

Θ(Σ( ), ) → (Θ( , ) + ), (4)
where Θ( , ) := × . Furthermore, inspecting the above grammar for normal forms, we find add,mul

• (Γ + Θ ) * : from the top level, we have a first layer of basic operations, until we meet a binary operation; the first argument of the latter may then only consist of binary operations until it reaches a variable ∈ , while the second argument is arbitrary. Equivalently, letting ′ = Θ * , we have

(Γ + Θ ) * Γ * ⊕ Θ * ⊕ ′ , hence add,mul • ( ⊕ ′ ).
By induction, i.e., applying (4) repeatedly, we define a distributive law

( ⊕ ′ ) • → • ( ⊕ ′ ).
Of course Θ is cocontinuous in its first argument, which easily entails that ⊕ ′ is constant-free, and so → add,mul

• ( ⊕ ′ ) is admissible. where ′ = Γ * , making the following diagram commute.

Γ Σ (Γ + + ) (Γ + ) Γ ( ′ + ) Γ (( ⊕ ′ ) ( ⊕ ′ ) + ) ′ ( ⊕ ′ ) ( ⊕ ′ ) ( ⊕ ′ ) ( ⊕ ′ ) , Γ Σ, Γ / ⊕ ′ Γ , 2 1 [ ⊕ ′ , ⊕ ′ ] ( 2 1 + ) (Γ +[ , ]) ( Γ , + ) (5)
Furthermore, ⊕ ′ is constant-free, hence the monad morphism

→ ( ⊕ ′ )
is admissible.

The next subsection is devoted to sketching the proof, and may be safely ignored.

4.2.2 Proof sketch. Our first step will consist in defining an intermediate notion called incremental lifting, fitting in the following process: incremental structural law → incremental lifting → distributive law → admissible morphism.

To explain the idea, let us start by recalling from [START_REF] Beck | Distributive laws[END_REF] that distributive laws are equivalent to monad liftings. Given any monads and on a category C, a -lifting of is a lifting of along the forgetful functor -Alg → C. [1969, §1]). For any monads , : C → C, monad distributive laws → are in one-to-one correspondence with -liftings of .

We now introduce incremental liftings.

Definition 4.6. Let , , and ′ be monads on C, and : → be a monad distributive law. An incremental lifting of to ′ -Alg along is a functorial assignment, to each pair of a -algebra structure and a ′ -algebra structure on , of a ′ -algebra structure on , such that for each such , the multiplication → and unit → are ′ -algebra morphisms.

This rather technical definition in fact unfolds rather simply, as we now explain. We first recall the following, well-known characterisation of ( ⊕ ′ )-algebras. L 4.7. Let and ′ be monads on a complete (locally small) category C such that the monad coproduct ⊕ ′ exists. Then, the category of ( ⊕ ′ )-algebras consists of objects of C equipped with algebra structures for both and ′ . Otherwise said, the following square is a pullback.

( ⊕ ′ ) -Alg -Alg ′ -Alg C P . See §B.
Remark 11. In passing, this result yields an easy proof that ⊕ ′ is constant-free.

This directly entails the following equivalent presentation of incremental liftings.

C 4.8. Incremental liftings of to ′ -Alg along on a complete category C such that the coproduct ⊕ ′ exists are in one-to-one correspondence with liftings along the projection ( ⊕ ′ ) -Alg → -Alg of the monad on -Alg, say , itself obtained by lifting , as in

( ⊕ ′ ) -Alg ( ⊕ ′ ) -Alg -Alg -Alg C C.
, ′

In such a situation, , ′ is furthermore a ( ⊕ ′ )-lifting of .

It is now easy to see that incremental liftings give rise to distributive laws. C 4.9. Let , , and ′ be monads on a complete category C such that the monad coproduct ⊕ ′ exists, and let : → be any monad distributive law. Then, any incremental lifting of to ′ -Alg along gives rise to a distributive law ′ : ( ⊕ ′ ) → ( ⊕ ′ ).

Furthermore, if and ′ are constant-free, so is ⊕ ′ , hence the induced monad morphism → ( ⊕ ′ ) is admissible.

P

. By Corollary 4.8 and Lemma 4.5. Constant-freeness of ⊕ ′ follows by Lemma 4.7.

Remark 12. With the same hypotheses, it is straightforward to deduce that → ( ⊕ ′ ) is admissible, since → and → → ( ⊕ ′ ) both are.

We thus mostly reduce Theorem 4.2 to the following. Remark 13. This result does not directly entail (5), which will follow from the construction of the incremental lifting.

P , §C

. We first define from a natural transformation

• , : Γ ( ( )) → (Γ ( ) + + ), notably using the fact that Γ , being a cocontinuous endofunctor on a locally finitely presentable category, admits a right adjoint.

We then want to construct a lifting of to some functor ( ⊕ ′ ) -Alg → ′ -Alg. But we have

Γ Γ -----→ Γ • , ---→ (Γ ( ) + + ) (b⊲c) ------→ b --→ ,
where (b ⊲ c) : Γ + + → is defined as follows.

Definition 4.11. For any -algebra b : → equipped with Γ Δ-algebra structure c : Γ → , let b ⊲ c denote the following composite.

Γ ( ) + + Γ b +[ , ] ---------→ Γ + [c, ]
----→ .

We then show that and are algebra morphisms, as desired.

Augmented algebras

Let us now present the announced characterisation of the category of algebras of the composite monad ( ⊕ ′ ) induced by an incremental structural law, which we call augmented algebras.

Γ(Σ , ) (Γ( , ) + + ) Γ( , ) (Γ( , ) + ) Γ( , ) ( ) , Γ ( Σ, , ) (Γ ( ,a• b)+[ , ]) Γ (a, ) [c, ] c a• b (d2)
• A ( , )-algebra morphism is a morphism between underlying objects which is an -, -, and ΓΔ-algebra morphism. • We let ( , ) -Alg denote the category of ( , )-algebras and morphisms between them. → , with = Σ * . Letting ′ = Γ * as before, there is an isomorphism ( ⊕ ′ ) -Alg ( , ) -Alg of categories over the base category C.

More precisely, for any • ( ⊕ ′ )-algebra , the canonical morphisms from , , and Γ( , ) into (( ⊕ ′ ) ( )) equip with ( , )-algebra structure. This assignment extends to a functor ( ⊕ ′ ) -Alg → ( , ) -Alg over C, which is an isomorphism of categories.

Independent extensions

Let us end the theoretical part of this section by briefly showing how to combine independent incremental structural laws. where = (Γ ) * and ⊕ is constant-free. We thus get an admissible morphism → ( ⊕ ).

P

. Taking Γ ( ) = Γ ( ) and observing that = Γ * , we obtain the desired result directly by applying Theorem 4.2 to the cotupling of all

Γ (Σ( )) , ---→ (Γ ( ) ( ) + + ) ( ( ) , ( ) + + ) -----------------→ (Γ ( ) ( ) + + )

Application: differential -calculus

In this section, we sketch an imperfect treatment of differential -calculus, to illustrate incremental structural laws.

D(D • ) • ≡ D(D • ) • + + ≡ + + (6)
Structural operations are then defined as follows:

1. First of all, operations are extended to multiterms by induction, as in Figure 1.A. The first two A. Extended operations

0 + = ( + ) + = + ( + ) 0 = 0 ( + ) = ( ) + .0 = 0 .( + ) = . + . D( ) • 0 = 0 D( ) • ( + ) = D( ) • + D( ) • D(0) • = 0 D( + ) • = D( ) • + D( ) • .
B. Capture-avoiding substitution

[ ↦ → ] = [ ↦ → ] = + 0 (when ≠ ) ( . ) [ ↦ → ] = .( [ ↦ → ]) ( fresh for and ) ( ) [ ↦ → ] = [ ↦ → ] [ ↦ → ] (D • ) [ ↦ → ] = D [ ↦ → ] • [ ↦ → ] 0[ ↦ → ] = 0 ( + ) [ ↦ → ] = [ ↦ → ] + [ ↦ → ].
C. Partial differentiation

• = • = 0 (when ≠ ) ( ) • = • + D • • . • = .
• ( fresh for and )

D • • = D( • ) • + D • ( • ) 0 • = 0 ( + ) • = • + • .
Fig. 1. Auxiliary functions for differential -calculus lines extend + to take a multiterm as its first argument. The next two extend similarly. The next two extend -abstraction. Matters then get slightly subtle: D-• -is first extended to take a multiterm as its second argument, and then the obtained extension is further extended to take a multiterm as its first argument. 2. Then, relying on this, capture-avoiding substitution of a variable by a multiterm in a simple or multiterm is defined by induction in Figure 1.B, the result being a multiterm. 3. Finally, partial differentiation is also defined inductively, relying on extended operations, in Figure 1.C.

Using incremental structural laws.

Let us now model this syntax and auxiliary operations using incremental structural laws, but ignoring equations for this paper.

We have two syntactic categories, simple terms and multiterms, but only one sort for variables, to be replaced with multiterms. As in §3.4, we model this by working with the category [Set, Set 2 ] of finitary functors : Set → Set 2 , or equivalently functors F → Set 2 . For a change, this time, we emphasise the presentation as functors Set → Set 2 . Furthermore, we write s and m for the elements of 2, and think of ( ) s as a set of simple terms with free variables in , and of ( ) m as a set of multiterms with free variables in . We sometimes write such functors as pairs ( s , m ) of set-functors.

The basic endofunctor is then defined as follows.

Σ( ) ( ) s = + ( ) s × ( ) m + ( + 1) s + ( ) 2 s , ::= | | ( ) | D • Σ( ) ( ) m = 1 + ( ) s × ( ) m ::= 0 | + Notation 3. Writing y s = (1, ∅
) and y m = (∅, 1) (viewing Set 2 as the category of presheaves over the discrete category {s, m}), we equivalently have Remark 14. The operation in the fourth layer is defined by induction on the second argument, so the main (inductive) argument for Γ lapp 0 goes to the right of the product.

For the last layer in Figure 1.A, we define an incremental structural law over 4 , with arity

Γ lapp ( , ) ( ) = ( ( ) m × ( ) m ) • y m .
Again the equations of the last layer may be read as defining this incremental law. By Theorem 4.2, we get a distributive law 5 : 5 → 5 , where 5 = 4 ⊕ lapp , with lapp = (Γ lapp ) * .

We now define capture-avoiding substitution. The arity is reminiscent of substitution monoidal structures, so we write it as a tensor product. Because the result of a substitution is a multiterm, we readily put ( ⊗ ) ( ) s = ∅. Then, we define

( ⊗ ) ( ) m = ( ( ) m ) s + ( ( ) m ) m ,
reflecting the fact that we substitute multiterms for variables in both simple and multiterms.

The two layers of Figure 1.B may be read as defining the two components of the desired incremental structural law Σ( ) ⊗ → 5 ( ⊗ 5 + + ), which yields by Theorem 4.2 a distributive law 6 : 6 → 6 , where 6 = 5 ⊕ subst , with subst = (-⊗ -) * . Finally, we define partial differentiation. The arity is again empty at s, with

Γ diff ( , ) ( ) m = ( + 1) s × ( ) m + ( + 1) m × ( ) m .
The additional variable in the first argument models the distinguished variable along which we differentiate. Again the equations may be read as defining an incremental structural law and we get a distributive law 7 : 7 → 7 , where 7 = 6 ⊕ diff , with diff = (Γ diff ) * .

One could be content with this, prove the desired commutation lemmas [Vaux 2007, §6.1.4], and then show that everything is compatible with Equations ( 6), all by hand. But of course, it would be better to derive both results automatically. In the next section, we will explain how to derive commutation lemmas (though on a simpler example), leaving compatibility with equations for further work.

4.6 Application: capture-avoiding substitution, De Bruijn style Most applications of the paper take place in the setting of so-called presheaf models, i.e., mild generalisations of the category of finitary functors Set → Set [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF]. Our framework, however, applies just as well in other settings. To illustrate this, in this subsection, we transpose the example of capture-avoiding substitution to the De Bruijn-style setting of [Hirschowitz et al. 2022b].

To summarise the idea: just as the presheaf-based approach equipes the nested datatypes representation [START_REF] Bird | De Bruijn notation as a nested datatype[END_REF] with initial algebra semantics, the setting of [Hirschowitz et al. 2022b] does the same for De Bruijn representation [START_REF] De Bruijn | Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem[END_REF]. In the presheaf-based approach, terms are indexed by sets of potential free variables, and by convention the bound variable is always the greatest one, typically +1 for : ( + 1) → ( ). Indexing is thus made necessary by the binding convention. In De Bruijn representation, the binding convention is the opposite: the bound variable is always 0. This makes indexing unnecessary, but some operations become less intuitive (to many, at least [START_REF] Berghofer | A Head-to-Head Comparison of de Bruijn Indices and Names[END_REF]).

In order to specify capture-avoiding substitution in the De Bruijn setting, we will need several layers. Indeed, the presheaf-based approach features not only indexing, but also built-in renaming, which is not the case in the De Bruijn setting. We thus need to define a first layer for renaming, and then a second one for substitution.

We take Set as ambient category, and the basic syntax is specified by the endofunctor

Σ( ) = N + 2 + .
For the first layer, letting = Σ * again, the auxiliary bifunctor is

Γ( , ) = × N N ,
and renaming is specified by the following simple structural law (omitting for readability):

, : Σ( ) × N N → ( × N N + + ) ( , ) ↦ → ( ) ( ( ), ) ↦ → ( 1 ( , 1 + )) ( , ) ↦ → 1 ( , ) 1 ( , ) where 1 + : N → N is defined by (1 + ) (0) = 0 (1 + ) (1 + ) = 1 + ( ).
Letting = Γ * , we get a distributive law :

→ by Theorem 3.5.

Notation 4. We denote by [ ] the renaming operation of .

We then specify substitution by taking as auxiliary bifunctor Θ( , ) = × N , with incremental structural law defined by

Σ( ) × N → ( × ( ) N + + ) ( , ) ↦ → 3 ( ( )) ( ( ), ) ↦ → ( 1 ( , ⇑ )) ( , ) ↦ → 1 ( , ) 1 ( , )
, where ⇑ : N → is defined by

⇑ : N → 0 ↦ → 0 + 1 ↦ → ( ) [↑],
letting ↑: N → N denote the successor map.

BENIGN EQUATIONS

In this section, we examine what we call "benign equations", i.e., equations that are automatically satisfied by the initial model. The initial model is thus initial in a potentially smaller category. We start in §5.1 by presenting a simple example to motivate this investigation. In §5.2, along with recalling [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF] equational systems and some basic facts about them, we then introduce a mathematical definition of a system of benign equations, called a benign equational system. In §5.3, we present a notion of signature for benign equational systems, called structural equational systems, which we apply in §5.4 to prove associativity of capture-avoiding substitution.

On a simple example

In the case of addition, as defined by structural recursion in §3.1, an example of benign equation is associativity:

( + ) + = + ( + ).

(7) This is typically proven by induction on the first variable . We explain how to derive this result from the results of §3.1 and §4, which leads to structural equational systems.

We start by briefly sketching the idea. By the construction of §4, we define a new, auxiliary ternary operation op( , , ) by the structurally recursive equations

op(0, , ) = + (8) op( ( ), , ) = (op( , , )). (9)
By Theorem 4.2, the syntax, ∅, admits a unique such operation. But on the other hand, one easily proves that taking op( , , ) = + ( + ) or op( , , ) = ( + ) + yields two such operations. Indeed, we have

( ) + ( + ) = ( + ( + )) 0 + ( + ) = + and ( ( ) + ) + = ( + ) + = (( + ) + ) (0 + ) + = +
by the defining equations of addition. By uniqueness, both definitions of op must thus coincide, which proves (7). More formally, we start from the distributive law : → of §3.1. We introduce a bifunctor Ψ : Set 2 → Set mapping ( , ) to × × , for the arity of the ternary operation. Again, corresponds to the decreasing argument in the recursive definition of op, while accounts for other arguments. As in §4, the recursive definition is modelled by an incremental structural law

, : Ψ(Σ , ) → (Ψ( , ) + + ) (0, 1 , 2 ) ↦ → 3 ( 1 ) + 3 ( 2 ) ( ( ), 1 , 2 ) ↦ → ( 1 ( , 1 , 2 )).
Equation ( 7) induces a pair , : Ψ( , ) → of natural transformations, respectively mapping any triple ( , , ) ∈ 3 to ( + ) + and +( + ), and we want to show that the algebra structure ∅ :

∅ → ∅ ( ∅) of the initial -algebra coequalises ∅ and ∅ , as in

Ψ( ∅, ∅) ∅ ∅. ∅ ∅ ∅
By Theorem 4.13, models of the incremental structural law are -algebras equipped with an additional ternary operation making the diagram (d2) commute (with := and Γ := Ψ), and furthermore, by Theorem 4.10, ∅ is an initial model. By initiality, we thus merely need to show that both induced composites Ψ( ∅, ∅) → ∅ make (d2) commute.

In the next subsections, we propose an abstract version of this idea, with a simple sufficient condition for it to work.

Equations

In this subsection, loosely following [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF]Hirschowitz et al. 2022a], we introduce an abstract notion of equational system, and define what it means for such an equational system to be benign. Definition 5.1. Given a finitary monad on a locally finitely presentable category C, an equational system consists of a finitary monad on C, together with two monad morphisms → .

Example 5.2. Taking C = Set, we model associativity of a binary operation by taking and to be the free monads on the endofunctors Σ( ) = 2 and Θ( ) = 3 on sets, respectively. The monad morphisms , : → are induced by universal property of = Θ * from the natural transformations 0 , 0 : Θ → defined by

0 ( 1 , 2 , 3 ) = 1 + ( 2 + 3 ) 0 ( 1 , 2 , 3 ) = ( 1 + 2 ) + 3 .
Definition 5.3. The quotient ★ of a finitary monad by an equational system = ( , , ) is the coequaliser

★ of , in Mnd (C).
Remark 15. The coequaliser exists because the category of finitary monads on a locally finitely presentable category is itself locally finitely presentable [START_REF] Lack | On the monadicity of finitary monads[END_REF]], hence in particular cocomplete.

Remark 16. The coequaliser is also a coequaliser in the category Mnd(C) of (not necessarily finitary) monads on C, since colimits are preserved by the embedding Mnd (C) → Mnd(C) by Blackwell [1976, Proposition 5.6]. Definition 5.4. An equational system is benign when the universal coequalising morphism → ★ is admissible.

Although coequalisers of finitary monads may not be intuitive to all readers, the monad ★ admits the following nice characterisation by its algebras.

Definition 5.5. Given a finitary monad and an equational system = ( , , ) on it, a -algebra :

→ satisfies iff coequalises and , i.e., • = • . Such -algebras are called -algebras, and we denote byalg the full subcategory of -Alg spanned by them.

Remark 17. Equivalently,alg is the equaliser in CAT of the induced functors -Alg → -Alg, which a priori might differ from the equaliser in Monadic /C, the full subcategory of Monadic/C spanned by finitary monadic functors. They in fact coincide, by the following Proposition. P 5.6. For any finitary monad on a locally finitely presentable category C and equational system = ( , , ) on it, we have an isomorphismalg ★ -Alg over C. Otherwise said, the forgetful functoralg → C is finitary and monadic, and the associated monad is isomorphic to ★ .

P

. By Remark 16, ★ is a coequaliser of and , as monad morphisms. By Kelly [1980, Proposition 26.3], its category of algebras is thus computed as the equaliser in CAT/C of the functors -Alg → -Alg Θalg, as claimed.

We may derive from this the following useful characterisation of benign equational systems. P 5.7. An equational system is benign iff the initial -algebra satisfies it, i.e., ∅ • ∅ = ∅ • ∅ . P . If the initial algebra satisfies an equational system , then it is a fortiori initial inalg, hence in ★ -Alg by Proposition 5.6. The forgetful functor ★ -Alg → -Alg thus preserves the initial object, and we conclude by Proposition 2.4.

Conversely, if an equational system is benign, then, by Proposition 2.4, the initial -algebra admits a unique ★ -algebra structure : ★ ∅ → ∅ making the following diagram commute

∅ ★ ∅ ∅, ∅ ∅
and makes ∅ into an initial ★ -algebra. But ∅ coequalises ∅ and ∅ , hence so does ∅ , as desired.

Let us conclude this subsection with the following observation on combining equations.

Definition 5.8. For any family ( ) ∈ of equational systems on a given finitary monad on a locally finitely presentable category C, with = ( , , ) for all ∈ , let denote the equational system defined by the cotuplings

[ ] ∈ : ∈ →
and [ ] ∈ : ∈ → . P 5.9. For any family ( ) ∈ of equational systems on a given finitary monad on a locally finitely presentable category C, is benign iff each is.

P

. By Proposition 5.7 and universal property of coproduct.

Structural equational systems

In this subsection, we introduce a notion of signature for benign equational systems. We fix a free monad = Σ * on a locally finitely presentable category C, with Σ (hence ) finitary.

Definition 5.10.

• A structural interpretation of an incremental structural law

, : Θ(Σ , ) → (Θ( , ) + + )
over some given distributive law :

→ is a natural transformation : Θ( , ) → making the coherence diagram of Figure 2 commute. Θ(Σ , ) (Θ( , ) + + ) Θ( , ) (Θ( , ) + ) ( + ) ( ) Θ( Σ, , ) , (Θ( , )+[ , ]) ( + ) [ , ]

Fig. 2. Coherence diagram for structural interpretations

• A structural equational system over a distributive law : → consists of an incremental structural law (Θ, ) over , together with a pair of structural interpretations , : ΘΔ → of .

We now associate an equational system to any structural equational system, and prove that it is benign.

Θ Θ -----→ Θ ---→ ---→ ---→ .
For any structural equational system = ( , , ) over , the equational system ˜ induced by is the pair ˜ , ˜ : Θ * → .

Notation 5. We often conflate and the associated equational system ˜ . In particular, recalling Definition 5.5 and Proposition 5.6, we speak of -algebras, which form a categoryalg ★ -Alg.

T 5.12. Consider any monad distributive law : → in a locally finitely presentable category C such that is constant-free. Then for any structural equational system over , the quotient morphism → ˜ ★ is admissible.

P ( §E ). Let , : Θ(Σ , ) → (Θ( , ) + + )
denote the given incremental structural law, and and denote the two structural interpretations. We first prove that each any structural interpretation induces ΘΔ-algebra structure on any -algebra , given by Θ( , ) --→ → , and furthermore that this ΘΔ-algebra structure satisfies (d2), hence by Theorem 4.13 makes into an ( ⊕ ′ )-algebra.

The given structural interpretations and thus induce two extensions of the -algebra structure of ∅ ∅ to ( ⊕ ′ )-algebra structure. But by Theorem 4.2 and Proposition 2.4, ∅ has a unique compatible ΘΔ-algebra structure making it into a ( ⊕ ′ )-algebra structure, so both algebra structures derived from and must agree with the canonical one. In particular the diagram

Θ( ∅, ∅) ∅ ∅ ∅ ∅
commutes, hence ∅ satisfies the induced equational system, and is thus initial in ( ⊕ ′ ) -Alg.

Let us conclude this subsection with the following direct consequence of Theorem 5.12 and Proposition 5.9. C 5.13. Consider any monad distributive law : → in a locally finitely presentable category C such that is constant-free. Then for any family ( ) ∈ of structural equational systems over , the quotient morphism → ( ˜ ) ★ is admissible.

Application: associativity of substitution

In this section, we continue the development of §3.5. There, we specified the syntax of purecalculus by an endofunctor Σ on [Set, Set] , and substitution by a simple structural law , : Γ(Σ , ) → (Γ ( ) + + ), where Γ( , ) = ⊗ , thus generating an admissible morphism →

, where = Σ * and = Γ * . We now want to show that the ΓΔ-algebra structure of the syntactic model ∅, a.k.a. captureavoiding substitution, is associative. Again, this will be subsumed by §5.5.

We define a structural equational system with the following components:

• the arity functor is Θ( , ) = ( ⊗ ) ⊗ ;

• the incremental structural law is defined by

′ , ( , , ) = ( ) [ ] ′ , ( , , ) = ( , , ) ( , , ) ′ , ( ( ), , ) = ( , ↑ , ↑ ),
where

-: → ( ) ( ), -: → ( ) ( ), --1 [-2 ]
denotes the formal (= explicit) substitution operation of , and we omit coproduct injections and for readability;

• the structural interpretations are defined by

( , , ) = [ ] [ ] and ( , , ) = [ [ ]],
where by definition [ ] ( ) := ( ) [ ] (writing for the th element of to emphasise that it is thought of as a variable). Checking the coherence condition of Figure 2 essentially amounts to checking each case of the usual induction, separately. The most interesting case is that of abstraction, with the right-hand side :

• maps any triple ( ( ), , ) to ( , ↑ , ↑ ), which the right-hand composite then maps to

( [ ↑ [ ↑ ]]), while • the left-hand composite maps the triple to ( [ [ ] ↑ ]). We thus need to prove ↑ [ ↑ ] = [ ] ↑ :
• on +1 , we directly have [ ] ↑ ( +1 ) = +1 , and, slightly less directly,

↑ [ ↑ ] ( +1 ) = ↑ ( +1 ) [ ↑ ] = +1 [ ↑ ] = +1 ; • on for ∈ , we have [ ] ↑ ( ) = • ( ( ) [ ]) = ( ) [ ( ) • ]
, where : ↩→ + 1 denotes the inclusion, while

↑ [ ↑ ] ( ) = ↑ ( ) [ ↑ ] = ( • ( )) [ ↑ ] = ( ) [ ↑ • ].
But the following square commutes by definition of ↑ , hence the result.

+

( ) ( + 1) ( ) ↑ 1
Theorem 5.12 then tells us that the usual substitution lemma is satisfied in the syntax (∅).

Embedding presheaf-based models

In this section, we show how the general framework of pointed strong endofunctors [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF][START_REF] Fiore | Second-Order and Dependently-Sorted Abstract Syntax[END_REF]] embeds into ours. More precisely, for any pointed strong endofunctor Σ on a monoidal, locally finitely presentable category (C, ⊗, , , , ) satisfying standard additional axioms (see Definition 5.16 below):

• We define a simple structural law, whose initial algebra ∅ = ( + Σ) * ∅ is the desired syntax, and whose category of algebras is a relaxed variant of Fiore et al. 's; • We then define two structural equational systems 1 and 2 , whose joint algebras in the sense of Corollary 5.13 are precisely those of Fiore et al. 's. We thus recover the admissible morphism

→ → ( ˜ 1 + ˜ 2 ) ★ Σ ⊛ of Example 2.5.
Remark 18. The motivation for this subsection is one of connecting to other people's work. In applications, it will probably be easier to directly define the desired structural laws and equational systems.

We start by recalling the notion of pointed strong endofunctor, and its associated category of models.

Definition 5.14. A pointed strength on an endofunctor Σ : C → C on a monoidal category (C, ⊗, , , , ) is a family of morphisms ,( , ) : Σ( ) ⊗ → Σ( ⊗ ), natural in ∈ C and ( , : → ) ∈ /C, the coslice category below , making the following diagrams commute,

Σ( ) Σ( ) ⊗ Σ( ⊗ ) Σ ( ) Σ( ) ,( ,id) (Σ( ) ⊗ ) ⊗ Σ( ⊗ ) ⊗ Σ(( ⊗ ) ⊗ ) Σ( ) ⊗ ( ⊗ ) Σ( ⊗ ( ⊗ )) ,( , ) ⊗ Σ ( ), , ⊗ ,( , )
Σ( , , )

,( ⊗ , ⊗ )

where : → and : → are the given points, and ⊗ denotes the composite

-1 --→ ⊗ ⊗ -----→ ⊗ .
Definition 5.15. For any pointed strong endofunctor Σ on C, a Σ-monoid is an object equipped with Σ-algebra and monoid structure, say : Σ( ) → , : ⊗ → , and : → , such that the following pentagon commutes.

Σ( ) ⊗ Σ( ⊗ ) Σ( ) ⊗ , ( , ) ⊗ Σ( ) (10)
A morphism of Σ-monoids is a morphism in C which is a morphism both of Σ-algebras and of monoids. We let Σ -Mon denote the category of Σ-monoids and morphisms between them.

Let us now show how any pointed strong endofunctor Σ gives rise to a simple structural law, and how the coherence laws of Σ-monoids may be enforced by benign equations.

Following [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF][START_REF] Fiore | Second-Order and Dependently-Sorted Abstract Syntax[END_REF], we assume that our category C is leftist, in the following sense.

Definition 5.16. A monoidal category (C, ⊗, , , , ) is leftist iff ⊗ is cocontinuous in its first argument, and finitary in its second argument.

Definition 5.17. The simple structural law associated to any pointed strong endofunctor (Σ, ) is defined as follows.

• We take as basic functor Σ + ( ) = + Σ( ), and • as auxiliary bifunctor Γ( , ) = ⊗ .

• We then take as simple structural law , the composite

Σ + ( ) ⊗ ⊗ + Σ( ) ⊗ + Σ( ⊗ ) Σ + ( ) ⊗ ( ⊗ + + ), ; Σ + ( ) ⊗ ∼ + ,( , ) [ 3 , ( 1 )• Σ + , ⊗ • 2 ]
where = (Σ + ) * and denotes the composite → Σ + → .

By Theorem 3.5, the initial Σ + -algebra has a unique model structure, which makes it initial, and furthermore, by Theorem 4.13, models are Σ-algebras : Σ → , equipped with morphisms : → and : ⊗ → making the pentagon

Σ + ( ) ⊗ ( ⊗ + + ) ( ⊗ + + ) ⊗ [ , ] ⊗ , ( ⊗ [ , ]+ + ) [ , , ] [ , ] (11)
commute, where [ , ] is induced by universal property of ( ). P 5.18. Commutation of (11) is equivalent to joint commutation of the pentagon (10) and the diagram below.

⊗ ⊗ ⊗ (12)
P . The domain of ( 11) is a coproduct, and we claim that the restriction to each term yields one of the given diagrams. For the first term, we get the following diagram.

⊗ ⊗ ( ⊗ + + ) ( ⊗ + + ) ⊗ ⊗ ( ⊗ [ , ]+ + ) [ , , ] [ , ] ⊗ 3
For the second term, we verify that both pentagons are equivalent by chasing the following diagram.

Σ( ) ⊗ Σ( ) ⊗ ( ) Σ( ⊗ ) Σ + ( ⊗ ) ( ⊗ + + ) Σ( ) ⊗ Σ( ⊗ ) Σ + ( ⊗ ) ( ⊗ + + ) ⊗ Σ( ) Σ + ( ) ⊗ ( ⊗ [ , ]+ + ) [ , , ] [ , ] Σ( ) ⊗ ,( , ) 2 Σ + , 1 Σ( ⊗ [ , ]) Σ + , 1 2 Σ( ) ⊗ [ , ] ,( , ) Σ( ) 2 Σ + , Σ + ( )
However, and are not yet required to satisfy the remaining monoid equations. In order to enforce them, relying on Corollary 5.13, we introduce two structural equational systems, one for each equation. First, we introduce some notation.

Definition 5.19. For any object , we define : ⊗ → to be the composite

⊗ ⊗ ----→ ⊗ = Γ Γ Δ,
-----→ .

Definition 5.20. For our first structural equational system 1 , we take • as auxiliary bifunctor Θ 1 ( , ) = ( ⊗ ) ⊗ ;

• as incremental structural law, say 1 , we take the left-hand composite of Figure 3;

Σ + ⊗ ⊗ Σ + ⊗ ⊗ ⊗ + Σ ⊗ ⊗ ⊗ + Σ ⊗ ⊗ + Σ ⊗ ⊗ + Σ( ⊗ ) + Σ( ⊗ ) ⊗ Σ + ( ⊗ ) + Σ( ⊗ ⊗ ) ( ⊗ ) + Σ + ( ⊗ ⊗ ) ( ⊗ ) + ( ⊗ ⊗ ) ( ⊗ + + ) ( ⊗ ⊗ + + ) ⊗ + ⊗ ⊗ + ,( , ) ⊗ + ⊗ , ( , ) [ 3 , 1 ]
+ ,( , )

Σ + ⊗ 1 + Σ + ( ⊗ ⊗ ) + 2
Fig. 3. Two incremental structural laws

• as first structural interpretation, say 1 , at any , we take

⊗ ⊗ ⊗ -----→ ⊗ ---→ ----→ ;
• as second structural interpretation, say 1 , at any , we take

⊗ ⊗ , , -----→ ⊗ ( ⊗ ) ⊗ -----→ ⊗ ---→ ----→ .
Definition 5.21. For our second structural equational system 2 , we take • as auxiliary bifunctor Θ 2 ( , ) = ⊗ ;

• as simple structural law, say 2 , we take the right-hand composite of Figure 3;

• as first structural interpretation, say 2 , at any , we take

⊗ ⊗ -----→ ⊗ ---→ --→ ;
• as second structural interpretation, say 2 , at any , we simply take ⊗ --→ ---→ .

T 5.22. For any locally finitely presentable, leftist monoidal category (C, ⊗, , , , ) and pointed strong endofunctor Σ, the above data 1 and 2 indeed form structural equational systems, and ( 1 + 2 )-algebras form a category isomorphic to Σ -Mon over C.

Furthermore, there are unique morphisms

: 0 ⊗ 0 → 0 : → 0
rendering the pentagon (10) and triangle [START_REF] Hirschowitz | Modules over Monads and Operational Semantics[END_REF] commutative.

Finally, these morphisms, together with 0 , satisfy the remaining Σ-monoid axioms, and make the initial Σ + -algebra 0 into an initial Σ-monoid.

P

. We start by reducing to proving the first claim, by observing that

• the second claim has already been stated, right before Proposition 5.18, and,

• assuming the first claim, the last one follows directly by Corollary 5.13.

The first claim is proved in §F.

CONCLUSION AND PERSPECTIVES

We have introduced admissible monad morphisms as a foundation for syntax with auxiliary functions. We have then shown how to generate admissible morphisms from monad distributive laws, and defined simple structural laws and incremental structural laws as basic notions of signatures to generate such monad distributive laws, hence admissible morphisms. We have also defined structural equational systems as a basic format for ensuring that the generated auxiliary functions satisfy some (hopefully useful) properties. We have used these tools to cover significant examples of auxiliary functions, from addition and multiplication of natural numbers to binding evaluation contexts, capture-avoiding substitution, and partial differentiation. We have finally shown that the standard framework of [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF] is subsumed by ours. An important question, already raised in the introduction, remains open: can we devise some further tools to ensure that the auxiliary functions generated by our signatures are compatible with severe equations, i.e., equations on the basic syntax?

Finally, our framework is designed to account for auxiliary functions defined on top of an existing syntax. It would be useful to extend it to settings where the syntax and functions are mutually dependent, as in induction-recursion [START_REF] Dybjer | Indexed Induction-Recursion[END_REF].

A PROOF OF PROPOSITION 2.4 First, : → is an -algebra morphism between and sem( ) ( ). Since ∅ is an initial -algebra, sem( ) ( ∅) is initial if and only if ∅ is an isomorphism. This argument shows (i) ⇔ (ii). Morever, since ∅ is an initial -algebra, creation implies preservation, so (iii) ⇒ (ii).

Finally, let us show that preservation implies creation, (ii) ⇒ (iii). Let -→ be an initial algebra. We show that there is a unique -algebra structure on that is mapped to by sem( ), and moreover that it is initial as a -algebra. Since, by hypothesis, sem( ) preserves the initial object, sem( ) ( ∅) is also initial, and thus is isomorphic to ∅, as -algebras. Now, sem( ) is an isofibration: through this isomorphism, inherits a -algebra structure which is mapped to → by sem( ), and this isomorphism lifts to the category of -algebras. Since this -algebra → is isomorphic to ∅, it is initial. It remains to show uniqueness. Consider an alternative -algebra structure on , that is also mapped to → by sem( ). By initiality of as aalgebra, there is a morphism → between these two -algebras. It is enough to show that its image by sem( ) is the identity morphism, which follows from initiality of as a -algebra.

B COLIMITS OF MONADS AND THEIR ALGEBRAS

In this section, we state a few useful results on colimits of monads, and on limits of the corresponding monadic functors, which notably entail Lemma 4.7.

Definition B.1. For any functor : A → Mnd(C), let -Alg denote a (choice of) limit of the induced diagram

A op → Mnd(C) op ≃ Monadic/C ↩→ CAT/C.
Thus, an -algebra is an object ∈ C, equipped with compatible -algebra structures, for all ∈ A. The next proposition, due to Kelly, relates this with the colimit of , when the latter exists. For any functor : B.2 ([K 1980, P 26.3]). For any functor : A → Mnd(C) with colimit , if C is complete (and locally small), then the functor : -Alg → -Alg is an isomorphism.

A → Mnd(C), if ∈ Mnd(C)
Remark 19. Kelly explicitly requires C to be locally small, which is implicit here by the convention fixed in §1.

This immediately entails Lemma 4.7. Notation 6. When applied to, say, Γ for some endofunctor , the notation Γ • is ambiguous, as it could denote (Γ • ) or (Γ ) • . The issue is even worse for, e.g., Γ • . In order to resolve the ambiguity, we write

Γ • | for (Γ ) • , i.e., Γ • | := Γ( , ) + + .
We now want to show that any incremental structural law The plan is to successively define families

• ℎ • , : Γ • | (Σ( )) → (Γ • | ( )), • ℎ • , : Γ • Σ → Γ • | , • ℎ • , : Σ → Γ × Γ • , • ℎ • , : → Γ × Γ • , • ℎ • , : Γ • → Γ •
(involving new functors defined along the way), from which we then define ℎ • and prove that it satisfies the properties stated in Lemma C.37 below. We then use this to construct the desired incremental lifting.

C.1 The family ℎ • Let us start with ℎ • , which requires the following preliminary definition.

Definition C.4. Consider any pointed endofunctor . We let ↑ denote the natural transformation defined at any , ∈ C by the composite

+ + -----→ + [ 1 , 2 ]
---------→ ( + ).

Remark 21. In particular, for any and with pointed, we have

↑ Γ + , : Γ • | → Γ • | . L C.5.
For any bifunctor : C 2 → C, distributive law : → , and objects , ∈ C, the following diagram commutes.

• | • | • | • | • | • | ↑ ↑ • | ↑ • | ↑ P .
Unfolding the definition, we refine the claim as follows, ( + ) [ where all subdiagrams easily commute except the top right square and the bottom left polygon.

Both have coproducts as their domains, so we chase them termwise. The first term of the top right square is chased as follows.

( + ) ( + + ) ( + ) ( ( + ) + ) ( + ) + ( + + ) ( + ) + ( ( + ) + ) [ 1, 2 ] ( + ) + [ 1, 2 ] 1 1 1 1 ( + )
The second term of the top right square is chased as follows.

↑ Γ • Γ • Γ • Σ [ 1, 2 ] ℎ • , ↑ Γ • [ 1, 2 ] ℎ • , ↑ Γ • Γ • Σ Γ • ↑ Γ • Γ •
where

• both top rectangles, as well as the bottom left and bottom right rectangles, commute by naturality, and • the third rectangle commutes by naturality and Lemma C.14 below.

L

C.14. For any monad on a category with binary coproducts, for all objects and , the following diagram commutes.

↑ ↑ ↑

P

. This hold by diagram chasing, as follows.

+ + + + + ( + ) ( + ) ( + ) ( + ) + + [ 1, 2 ] + [ 1, 2 ] ( + ) [ 1, 2 ] + [ 1, 2 ] [ 1, 2 ] + + C.3 The family ℎ •
We now turn to defining our next family of morphisms, ℎ • . For this, we need to exploit the cocontinuity hypothesis in the first argument of Γ.

Because we have assumed C to be locally finitely presentable, each Γ has a right adjoint, which we denote by Γ . Furthermore, we have: L C.15. Each Γ • has as right adjoint the functor Γ × defined by Γ × ( ) = Γ ( ) × .

P

. We have

C(Γ • ( ), ) = C(Γ ( ) + , ) C(Γ ( ), ) × C( , ) C( , Γ ) × C( , ) C( , Γ ( ) × ) C( , Γ × ( )).
Furthermore, by [Mac Lane 1998, Theorem IV.7.3], we readily get: natural in all variables.

Here, naturality in means that, e.g., for all morphisms : → ′ and : ′ → , the transpose of

---→ ′ - → is ˜ - → ′ ---→
, where ˜ denotes the transpose of .

C

C.17. For all : → , : → , : → , and : → , letting ˜ and ˜ denote the transposed morphisms, the square below left commutes iff the one below right does.

˜ ˜

In particular, for all and : → , the following diagrams commute.

Notation 7. Let = Γ • : C 2 → C, = Γ × : C × C op → C, and
( ) = (hence : C 2 → C). We thus have for all that is left adjoint to , and that is a monad.

Furthermore, we observe the following: L C.26. For any ∈ C and ∈ alg, has a canonical Σ-algebra structure given by

Σ ℎ • , ------→ -------→ → .
This defines a functor alg → Σalg over , for all .

P

. Functoriality is straightforward.

Unfolding the definition, the family ℎ • , is in fact constructed in this way, with = , whose -algebra structure is given by . Let us prove that the functorial assignment of Lemma C.26 is in fact also functorial in , in the following sense.

(Corollary C.17)

Moreover, we have:

it suffices to equip with Σ-algebra structure and show that the bottom and right morphisms above, i.e., and , are Σ-algebra morphisms. For the Σ-algebra structure on , we apply Lemma C.26 with the following -algebra structure on :

-

-------→ ---→ . Σ Σ = ℎ • , Σ 2 Σ 2 Σ 2 2
+ ) ( ( + )+ ) [ 1, 2 ] ( + + ) [ 1, 2 ] ( ( + ) + ) ( ( + )+ ) ( + ) [ 1, 2 ] ( ( + )+ ) [ 1, 2 ] ( ( + )+ ) [ 1, 2 ] ( + ) [ 1, 2 ] ( + + ) ( +[ , ]) ( + + ) ( + + ) + + [ 1, 2 ] ( ( + )+ ) ( + + ) ( + ) ( ( + )+ ) [ 1, 2 ] (
Fig. 5. Proof of Lemma C.31

( + ) ( + ) ( + ) ( + ) ( ) ( + ) ( + ) ( + ) ( + ) ( + ) [ 1, 2 ] ( ; ) ( ; + ) [ 1, 2 ] ; ( ; + ) ↑ ; ( ↑ ) ↑ ; ( ↑ ) ( + ) ( ↑ ) [ 1, 2 ] [ 1, 2 ] ; ( ; ) ( ↑ )
Σ Σ ℎ • , ℎ • , ↑ ( ; ) ℎ • , Γ × ; Σ Γ × ; Γ × ; Γ • ; ↑ ( ; ) Γ × ; Γ × ; (Lemma C.21) (Corollary C.17)
We then consider the fourth law, for which we proceed similarly: it suffices to show that the bottom morphism and right-hand composite are Σ-algebra morphisms. We first prove that the bottom morphism is a Σ-algebra morphism by diagram chasing as in Figure 7. Finally, we show that the right-hand composite is a Σ-algebra morphism, by Lemma C.26: we verify that it applies by proving that the composite is a morphism of -algebras, as we show by diagram chasing in Figure 8, where the bottom left heptagon commutes by Lemma C.32 below.

L

C.32. For all objects and , the following diagram commutes.

↑ ↑ ↑ ( ↑) P .
The domain is a coproduct, so we proceed termwise, by diagram chasing. The first term is chased as follows.

( + ) ( + )

+ + + + ( + ) + ( + ) + ( ( + ) + ) ( ( + ) + ) ( + + ) ( + ) ( + ) ( + + ) + + ( + ) +[ , ] ( +[ , ]) + [ 1, 2 ] + + [ 1, 2 ]+ ( ( + )+ ) [ 1, 2 ] + [ 1, 2 ] +[ , ] ( + ) ( + ) + + ( + ) + ( + ) + ( ( + ) + ) ( ( + ) + ) ( + + ) ( + + ) + ( + ) ( +[ , ]) + [ 1, 2 ] [ 1, 2 ]+ ( ( + )+ ) [ 1, 2 ] [ 1, 2 ] +[ , ] 2 2 2 1 2 1 1 1 2 2 2
Finally, the third term is chased as follows.

+ + ( + ) + ( + ) + ( ( + ) + ) ( ( + ) + ) ( + + ) ( + + ) + ( + ) ( +[ , ]) + [ 1, 2 ] [ 1, 2 ]+ ( ( + )+ ) [ 1, 2 ] [ 1, 2 ] +[ , ]
ℎ • , Γ (Γ + + ) ( Γ • | + + ) ( (Γ + + ) + + ) ( (Γ + + ) + + ) ( (Γ + + ) + + ) (Γ + + + + ) (Γ + + ) Γ Γ • | (ℎ • , + + ) ( ↑ + + ) ( (Γ + + )+ + ) [ 1 , 2 , 3 ] [ 1 , 2 , 3 , 2 , 3 ] Γ ℎ • Γ Γ Γ • Γ • | (ℎ • , + + ) ( ↑ + + ) ( (Γ + + )+ + ) [ P .
The given composite readily equips with ( ⊕ ′ )-algebra structure by Lemma 4.7 and the isomorphism Γalg ′ -Alg. It remains to verify that the unit and multiplication are Γalgebra morphisms. The former follows easily by Lemma C.37, and the latter by Figure 11. There, the middle, unlabelled polygon is chased as follows,

[ 1, 2, 3 ] [ 1, 2 ] Γ • [ 1, 2 ] [ 1, 2 ] [ 1, 2 ] [ 1, 2 ] [ 1, 2 ]
where the middle, bottom polygon is the image by of a diagram whose domain is a coproduct, and whose commutativity may be checked termwise. E.g., the second term is chased as follows.

( + ) ( + ) ( + ) ( + ) [ 1, 2 ] [ 1, 2 ] [ 1, 2 ] [ 1, 2 ] [ 1, 2
] 2 2 1 1 2 1 2 1 [ 1, 2 ] 1 2 2 1
It remains to show: P C.39. The distributive law / : ( ⊕ ′ ) → ( ⊕ ′ ) satisfies (5), which we repeat here for convenience.

Γ Σ

(Γ + + )

(Γ + ) Γ ( ′ + ) Γ (( ⊕ ′ ) ( ⊕ ′ ) + ) ′ ( ⊕ ′ ) ( ⊕ ′ ) ( ⊕ ′ ) ( ⊕ ′ ) , Γ Σ, Γ / ⊕ ′ Γ , a Γ Γ Γ Γ• | Γ• | h , ( h , + + ) ( ↑ +2• ) ( Γ• | +2• ) [ 1, 2, 3 ] (Γ +2• ) (Γ a +2• ) ( h , +2• ) ( Γ• |a +2• ) (↑ ) Γ• | Γ• | (↑ ) ( Γ• | + + ) ( Γ• | + + ) ( (Γ + + )+2• ) ( ↑ +2• ) ( (Γ +2• )+2• ) [ 1, 2, 3 ]
( (Γ a + + )+2• )

( ↑ +2• ) ( (Γ +2• )+2• ) [ 1, 2, 3 ] (Γ +∇
A -algebra morphism → is a morphism between underlying objects which is both anand -algebra morphism.

We let -Alg denote the category of -algebras and morphisms between them. D.2 ([B 1969, §2]). Given any monad distributive law : → , and -algebra x :

L

→ , the derived -and -algebra structures

---→ x - → ---→ x - →
equip with -algebra structure. Furthermore, this underlies an isomorphism -Alg → -Alg of categories over C.

In our situation, applying this to the distributive law / : ( ⊕ ′ ) → ( ⊕ ′ ) from Theorem 4.10, we obtain:

C D.
3. An ( ⊕ ′ )-algebra is equivalently an -algebra a : → , equipped with ( ⊕ ′ )-algebra structure satisfying the pentagon (13) with = ⊕ ′ .

But we can say more, by Corollary B.3: L D.4. An ( ⊕ ′ )-algebra is equivalently an objet , equipped with morphisms a :

• a morphism c : Γ( , ) → satisfying (d2 ′ ); and furthermore the notions of morphisms agree.

For any c : Γ( , ) → satisfying (d2), we define č to be the following composite → which is both a -algebra morphism, an -algebra morphism, and a Γ-algebra morphism is a morphism between the corresponding Γ -algebras, and

Γ a Γ a Γ Γ a Γ a • , (b⊲č)
(Γa +[ , ]) ( Γ • a + ) [ 1, 2 ] ( Γ • b + ) [ 1, 2 ] ( Γ • a + ) [ Γ • , 2 ] (Γ • a + ) (Γ • +a) ( + ) [c

P

. By coherence of , this reduces to commutativity of both of the following diagrams. In Figure 20, the subdiagram marked ( / ⊗ ) commutes by chasing as follows.

Σ + ⊗ ⊗ ( ⊗ + + ) ⊗ ⊗ ⊗ ⊗ ⊗ ⊗ ⊗ ⊗ ⊗ ⊗ ⊗ ⊗ ⊗ Σ + , ⊗ ⊗ , ⊗ [ Γ Δ, , , ]) ⊗ ⊗ ⊗ Γ ⊗ Σ + , ⊗ ⊗ ⊗ ⊗ Γ , ⊗ ⊗ [ Γ Δ, , , ]) ⊗ ⊗ ⊗ ⊗ (3)
The subdiagram marked ( / ) has a coproduct as domain, so we check its commutation termwise in Figure 21.

The subdiagram (Γ; Γ) commutes as in Figure 22.

F.2 Coherence of 1

We now check coherence of 1 , in Figure 23.

F.3 Coherence of 2

We then check coherence of 2 in Figure 24, where, in the middle triangle which unfolds , , we use

• Σ + , • 1 instead of as a point. This is justified because these morphisms are in fact equal, as the diagram below shows.

Σ + Σ + ∅ Σ + ∅ 1 Σ + , 1 Σ + , 1 Σ + ! Σ + ! Σ + ,∅ ! !
The left-hand, question-marked subdiagram of Figure 24 only commutes when postcomposed with

• = • • , as follows.
The second term is chased as follows.

4. 2

 2 The abstract case 4.2.1 Main result. Let us now abstract over the previous section. Definition 4.1. An incremental structural law on a locally finitely presentable category C consists of • a distributive law : → with free basic monad = Σ * and constant-free auxiliary monad , together with • a functor Γ : C 2 → C which is cocontinuous in its first argument and finitary in its second argument, equipped with • a natural transformation Γ (Σ( )) → (Γ ( ) + + ).

  T 4.2. Any incremental structural law , : Γ (Σ( )) → (Γ ( ) ( ) + + ) over : → , with := Σ * , induces a distributive law / : ( ⊕ ′ ) → ( ⊕ ′ ),

  Definition 4.3. A lifting of a monad : C → C along a functor : E → C is a monad ′ : E → E such that the following square commutes E E C C ′ and, furthermore, preserves multiplication and unit, i.e., for all ∈ E, ( ′ ) = ( ) and ( ′ ) = ( ) .

  P 4.4. For all and , -liftings of are in one-to-one correspondence with endofunctors ′ : -Alg → -Alg, such that the following square commutes -Alg -Alg C C ′ and, for all ∈ -Alg, : → and : → are -algebra morphisms. P . Straightforward.

T 4. 10 .

 10 Any incremental structural law , : Γ (Σ( )) → (Γ ( ) ( ) + + ) over : → , with := Σ * , induces an incremental lifting of to ′ -Alg along , where ′ = Γ * .

Definition 4. 12 .

 12 Consider any incremental structural law, : Γ (Σ( )) → (Γ ( ) + + ) over :→ , with = Σ * .• A ( , )-algebra is an object equipped with morphismsa : → b : → c : Γ( , ) → ,the first two of which are monad algebra structures, making the following diagrams commute.

T 4. 13 .

 13 Consider any incremental structural law, : Γ (Σ( )) → (Γ ( ) + + ) over :

P 4. 14 .

 14 For any set , any -indexed family , : Γ (Σ( )) → (Γ ( ) ( ) + + ) of incremental structural laws over :→ , with ∈ and := Σ * , induce a distributive law

4. 5 . 1

 51 Standard definition. Let us first introduce the calculus in the usual, informal way. The syntax is: Simple terms ∋ , ::= | | . | D • Multiterms ∋ , ::= 0 | + , where simple and multiterms are considered equivalent modulo the following equations.

  Definition 5.11. For any structural interpretation : ΘΔ → of , : Θ(Σ , ) → (Θ( , ) + + ) over : → , let ˜ : Θ * → denote the monad morphism induced by universal property of Θ * from the composite

  is a colimit of , then the colimiting cocone induces a cone over the diagram A op → Mnd(C) op ≃ Monadic/C ↩→ CAT/C, hence a functor : -Alg → -Alg over C.

P

C B. 3 .

 3 Consider two monads and on a locally finitely presentable category C, and a monad distributive law : → . For any bifunctor Γ : C × C → C, letting ′ := Γ * , the following square is a pullback. ( ⊕ ′ ) -Alg -Alg Γalg C P . By Lemma 4.7 and the isomorphism ′ -Alg Γalg over C. Remark 20. Otherwise said, giving a ( ⊕ ′ )-algebra structure on is equivalent to giving a -algebra structure and a Γ -algebra structure. C PROOF OF THEOREM 4.10 Definition C.1. A bifunctor Γ : C 2 → C on a category C is bipointed if it comes equipped with natural transformations For any bifunctor Γ, let Γ • ( , ) := Γ( , ) + + . P C.3. For any bifunctor Γ, the bifunctor Γ • is bipointed. (It is in fact the free bipointed bifunctor over Γ.) P . Straightforward.

  lifting of to ′ -Alg along . For this, we extend ℎ to a natural transformation how it induces an incremental lifting. This route being slightly long-winded, let us point to the definition of ℎ • (Definition C.35) and the proof that it induces an icremental lifting (Proposition C.38).

P C. 16 .

 16 For all bifunctors : C 2 → C such that each has a right adjoint , the functors assemble into a bifunctor C × C op → C making the bijection C( ( ), ) C( , ( ))

L C. 27 .

 27 For any morphism : → and object ,

1 (Fig. 4 .

 14 Fig. 4. Diagram for proof of Lemma C.30, first statement

Fig. 6 .

 6 Fig. 6. Lemma C.30: bo om morphism li s to Σalg

  family ℎ • Transposing back, we obtain a family ℎ • , : Γ • → Γ • of morphisms. By extranaturality of ℎ • in , naturality in , and Corollary C.17, we get: L C.33. The family ℎ • is natural in both variables.

Γ

1 .

 1 Given any monad distributive law : → , a -algebra is an object ∈ C of the underlying category, equipped with -and -algebra structures, say a :

  any c : Γ( , ) → satisfying (d2 ′ ), we define ĉ to be It thus suffices to prove: (a) the assignments c ↦ → č and c ↦ → ˆ are mutually inverse, (b) for any c : Γ( , ) → satisfying (d2), č satisfies (d2 ′ ), and conversely (c) for any c : Γ( , ) → satisfying (d2 ′ ), ĉ satisfies (d2); (d) for any ( , )-algebras and , a morphism :

(Fig. 13 .

 13 Fig. 13. Main diagram for proving (d2 ′ ) for č

1 .

 1 Fig. 15. Chasing subsubdiagram (A')

  Fig. 19. Proof of Lemma D.8, second step

  Fig. 20. Coherence of 1

, : Γ (Σ( )) → (Γ ( ) ( ) + + ) (with again = Σ * ) induces a monad distributive law → , where := Γ * , making the following diagram commute.Γ Σ (Γ + + ) Γ Γ [ Γ , , , ],

′ -Alg Γalg, so we reduce to constructing a functor ( ⊕ ′ ) -Alg → Γ -Alg -still behaving like on underlying objects.For any -algebra b : → equipped with Γ Δ-algebra structure c : Γ → , we construct the desired Γ Δ-algebra structure on ( ) as

Σ( ) ( ) = ( + ( ) s × ( ) m + ( + 1) s + ( ) 2 s ) • y s + (1 + ( ) s × ( ) m ) • y m .Let us now define extended operations. We start by defining the first four layers of Figure1.A independently, using Proposition 4.14 (with = id). The relevant arities areΓ plus ( , ) ( ) = ( ( ) m × ( ) m ) • y m Γ app ( , ) ( ) = ( ( ) m × ( ) m ) • y m Γ abs ( , ) ( ) = ( + 1) m • y m Γ lapp 0 ( , ) ( ) = ( ( ) s × ( ) m ) • y m ,and the equations in the table may be read as defining the desired simple structural laws Γ (Σ( ), ) → (Γ ( , ( )) + + ),for ∈ {plus, app, abs, lapp 0 }. We get a distributive law 4 : 4 → 4 , where 4 = ( Γ ) * .

P. The first two laws hold by construction. For the third law, by universal property of coproduct, it suffices to verify it on each term of the coproductΓ • Σ = Γ Σ + Σ + .The result follows straightforwardly by diagram chasing in each case. The first term is chased as follows, using the coherence properties of monad distributive laws.Γ Σ Γ Σ Γ Σ Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Σ Γ • | Σ Γ • | Σ Γ • | Γ • | Γ • | Γ • |

|The second term is chased as follows.Σ Σ Σ Γ • | Σ Γ • | Σ Γ • | Σ Γ • | Γ • | Γ • |

;

; | ℎ • , Γ Σ Γ Σ Γ • Σ Γ • | Γ Σ ℎ , 1 ℎ • , Γ • Σ Γ • Σ Γ • Γ • Γ • Γ • ℎ • , ↑ Γ • Γ • ℎ • , Γ • Σ P .The first law holds by chasing the following diagram.Σ Γ • Σ Γ • | Σ Γ • | Γ • | Γ • | [ 1 , 2 ]

2For the second one, we proceed by diagram chasing, as follows.

| Σ Γ • | Σ Γ • | Σ Γ • | Σ Γ • | Σ Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | Γ • | [ 1, 2 ] ℎ • ,

; | Γ • | ↑ ↑ Γ • | (Lemma C.5) Γ • | ( ; ) Γ • ; | (Lemma C.7)Let us now consider the third claim. It follows by chasing the following diagram,Γ Σ Γ Σ Γ • Σ Γ Σ Γ • | Σ Γ • | Σ Γ • | Γ • | Γ • | Γ • | Γ Σ 1 [ 1 , 2 ] ℎ • , ↑ ℎ , Γ Σ Γ Σ 1 ℎ • , 1 Γ • | Σ Γ • | Γ • | (Lemma C.7)whose bottom right triangle commutes by chasing the following diagram.

| ( + ) (Γ + + )Finally, we prove the last claim by diagram chasing as follows,Γ • Σ Γ • Σ Γ • Σ Γ • Σ Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ •

LC.20. The family ℎ • is extranatural[START_REF] Kelly | Basic concepts of enriched category theory[END_REF]] in , i.e., for all and : → , the following square commutes.Σ Γ × Γ • Γ × Γ • Γ × Γ • ℎ • , ℎ • , Γ × Γ • Γ × Γ • P .By naturality of ℎ • and Corollary C.17.L C.21. The family ℎ • satisfies the following laws.Σ Γ × Γ • | Γ • | Σ, ℎ • , 2 Γ • | , Σ Γ × Γ • | Γ × Γ • Γ × Γ • | Γ × Γ • | Γ × Γ • | ℎ • , ℎ • , Γ × ↑ , Γ × ( ; )Γ • ; | Γ × Γ • Γ × Γ • Σ Γ × Γ • | Γ Γ • | Γ Γ • | ℎ , ℎ • , 1 Γ Γ • |

Σ Γ × Γ • Γ × Γ • Γ × Γ • Γ × Γ • ℎ • Γ × Γ • | , Γ × Γ • ℎ • Γ × Γ • | ,

LC.28. The family ℎ • , is extranatural in , i.e., the following square commutes for all and : → .Γ × Γ • Γ × Γ • Γ × Γ • ℎ • , ℎ • , Γ × Γ • Γ × Γ •

The bottom morphism then lifts to Σalg by Lemma C.27. Finally, the fact that the right-hand morphism is a Σ-algebra morphism will thus follow from being a -algebra morphism, which in turn follows by chasing the following diagram.L C.30. The family ℎ • satisfies the following laws.Γ × Γ • Γ • ℎ • , 2 Γ • | , Γ × Γ • | Γ × Γ • | Γ × Γ • | Γ × Γ • | Γ × Γ • | ℎ • , ℎ • , Γ × ↑ , Γ × ( ; )Γ • ; | Γ × Γ • | Γ × Γ • | Σ Γ × Γ • | Γ Γ • | Γ Γ • | ℎ , 1 Γ Γ • | ℎ • , Σ,

1 1 1 1 1 1 1 1The second term is chased as follows.

Σ Γ × Γ • | Σ Γ × Γ • | Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • Γ × Γ • | Γ × Γ • | Γ × ↑ Γ × Γ × ℎ • Γ × Γ • | , Γ × Γ • | Γ × ℎ • Γ × Γ • | , Γ × Γ • | Γ × Γ • | Γ × Γ • Σ Γ × Γ • | Γ × Γ • Γ × Γ • | ℎ • Γ × Γ • | , Γ × ↑ Γ × Γ • Γ × Γ • | Γ × Γ × ↑ Γ × Γ • | Γ × Γ × Γ × Γ • Γ × Γ • | Γ × Γ • Γ × Γ • Γ × Γ • |Fig. 7. Proof of Lemma C.34, fourth law, bo om morphism

Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ • Γ •

Γ • , ℎ • , Γ • | , Γ • Γ • Γ • Γ • | Γ • | Γ • | ℎ • , ↑ , Γ • Γ • ( ; )Γ • ; | ℎ • , Γ • Γ • Γ • Γ • | Γ • Γ • ℎ • 1 Γ • Γ • | Γ • | Γ • Γ • | Γ • ℎ • , ↑ Γ • | ℎ • , Γ • Γ • Γ • Γ • Γ • ℎ • , Γ • ℎ • , ℎ • , Γ • Γ Σ Γ

C.6 The family ℎ• Definition C.35. Let ℎ • , : Γ → Γ • | denote the composite Γ Γ ------→ Γ 1 --→ Γ • ℎ • , -----→ Γ • | . L C.36. The natural transformation ℎ • , : Γ • → Γ • |is natural in both variables.P. This follows straightforwardly from Lemma C.33.L C.37. The natural transformation ℎ • makes all diagrams below commute, for all , ∈ C.Γ Γ Γ • | Γ • | Γ • | Γ • | ℎ • , ↑ Γ • | Γ • |

, ℎ • ,

Γ Γ • | ℎ • , Γ Γ 1 Γ Σ Γ Γ • | ℎ • , Γ Σ, ℎ , P .The last diagram is direct by Lemma C.34. The third one follows by chasing as follows,Γ Γ Γ • Γ • | Γ • Γ Γ Γ • Γ • | Γ Γ Γ 1 ℎ • , Γ11 Γ • 1 using Lemma C.34. The first statement follows by chasing the next diagram.Γ Γ Γ Γ Γ Γ • Γ • Γ • Γ • | Γ • | Γ • | Γ • | ↑ Γ • | Γ • | Γ ℎ • , Γ 1 ℎ • , 1 Γ Γ

[b, ] ------→ a --→defines an incremental lifting of to ′ -Alg along .

| + ) (Γ + + + + ) Γ • (Γ + + )

,

,

] [ 1 , 2 , 3 , 2 , 3 ] Γ ℎ • , Γ 1 ℎ • , Γ 1 Γ • ( ℎ • , + ) Γ • (interchange) (Lemma C.34)Fig. 9. Proof of Lemma C.37

[ ⊕ ′ , ⊕ ′ ] (

1 + ) (Γ +[ , ]) ( Γ , + )We need the following intermediate result.L C.40. For any object , the following diagram commutes.

( h , +2• ) ( (Γ a +2• +2• )) ( [b, , ]+2• ) ( a+2• ) [ , , ]

(easy) (easy) (naturality of ; ) Fig. 11. Multiplication is an algebra morphism

→ , and let ′ = Γ * . Given any distributive law, algebras for the composite monad admit the following well-known characterisation.

→ b : → c : Γ( , ) → , the first two of which are monad algebra structures, satisfying the pentagon (13) with = , together with the following diagram, Γ Γ Γ

(e) conversely for any / -algebras and , a morphism : → which is both a -algebra morphism, an -algebra morphism, and a Γ -algebra morphism is a morphism between the corresponding Γ-algebras. Statements (d) and (e) follow easily by naturality of and the fact that the considered morphism is an algebra morphism.Statement (b) follows from commutation of the diagram in Figure13, and • , as in Definition C.35. Subdiagram (A) commutes by chasing as in Figure14. Subdiagram (A') commutes asΓ Γ Γ Γ Γ Γ Γ • | Γ (Γ + ) (Γ • | ) (Γ + ) (Γ + 2 • ) (Γ + ) ( ) Γ a Γ a

č shown in Figure 15. Subdiagram (B) commutes by Lemma D.7 below.Statement (c) follows from commutation of the diagram in Figure16, where

• ,• ,• , Γ ↑ Γ • | Γ • |

1, 2 ] Γ • | Γ • | (Γ b +[ , ]) (Γ b +[ , ]) (Γa+ )

• the top part commutes by Lemma C.37 and • the bottom right part commutes by Lemma D.6 below.Γ Σ Γ Γ Γ (Γ + + ) Γ (Γ + ) Γ (Γ + ) Γ Γ Σ, Γ Γ • ,

→ , precomposition with morphisms Γ a and Γ induces a bijection (natural in the algebra) between morphisms Γ → and morphisms Γ → making the following diagram commute.

we readily get the top right part of (d2 ′ ), hence the result. For the top right part of (14), the result follows by chasing the diagram below.69T. Hirschowitz and A. LafontΓ Γ Γ Γ Γ Γ Γ Γ Γ Γ Γ • | Γ a Γ a Γ Γ a Γ a Γ a Γ a Γ a Γ a

b : → c : Γ → , the following diagram commutes Γ Γ Γ • | Γ • Γ Γ Γ a • , [c, ] c a• b (Γ a• b +[ , ]) P .We start by reducing to Subdiagram (C) as below.Γ Γ Γ • Γ • | Γ

•(Γ ) Γ a• b + a• b (Γ a• b +[ , ]) [c, ] (C)Commutation of (C) is then equivalent to commutation of the transposed diagram below.

Σ Σ Γ × Γ • Σ Γ × Γ • Σ Γ × Γ × Γ • Γ × Γ • Γ × Γ • Γ × Γ • Γ × Γ × Γ • Σ Γ × Γ • Γ × Γ • Γ × Γ × Γ × Γ • Γ × Γ • Γ × Σ , • , Σ Γ × Γ • a• b Γ × Γ • (a• Σ, ) Γ × • , , Γ × Γ • , • Γ × Γ • , Σ Γ × [c, ] • Γ × , Γ × Γ • Γ × Γ × Γ • a• b Γ × [c, ] Γ × [c, , ] Γ × Γ • a• b Γ × [c, ] Γ × [ , ] Γ × (a• b) ,Σ a• Σ,Fig. 17. Diagram for Lemma D.7 lemma reduces (using interchange) to commutation of the following diagram,

| ↑ • , Fig. 18. Proof of Lemma D.8, first stepΓ Σ Γ • | Γ • | Γ • | Γ Σ Γ • | Γ • Γ Γ • , Γ • | ↑ [c, ]

We first check coherence of 1 in Figure20, which uses the following lemma. L F.1. For all objects , the following diagram commutes. 75 T. Hirschowitz and A. Lafont Γ Γ Γ Γ , Γ , Γ Γ P . By diagram chasing, as follows.

1, 2 ] (Γ + + ) [ Γ , , , ] Γ • , (Lemma C.40)

The first term of the bottom left polygon is chased as follows.

( + )

Finally, the second term of the bottom left polygon is chased as follows. Definition C.6. Let

be defined by cotupling the following three composites.

L C.7. For all ℎ, ℎ • satisfies the following coherence laws.

Σ( ) ( )

The third and final term is chased as follows.

Finally, for the fourth law, ℎ • , • 1 yields the first composite of Definition C.6. But precomposing the latter with Γ Σ , we obtain by naturality of ℎ the composite

which we now prove equal to ℎ , , i.e., that the last three morphisms compose to the identity.

The family ℎ • We now want to make the Σ in the domain of ℎ • into an . For this, as an intermediate step, we emphasise the less pointed variant of Γ defined as follows.

Definition C.8. A bifunctor Γ : C 2 → C is main-pointed iff it comes equipped with a natural transformation Γ , : → Γ( , ). Definition C.9. For any C with binary coproducts and bifunctor Γ :

By the last lemma, ℎ •

, equivalently has type

Definition C.12. Let ℎ • , denote the natural transformation with components

13. For all ℎ, ℎ • satisfies the following coherence laws.

Σ( ) ( )

Let us return to the construction of the next family.

Definition C.18. Let ℎ • , denote the transpose

L C.19. The family ℎ • is natural in , i.e., for all and : → , the following square commutes.

P

. By naturality and bijectivity of transposition.

Finally, the last diagram is precisely the transpose of the last diagram of Lemma C.13.

C.4 The family ℎ •

We now want to define the next family, ℎ • . For this, we start by observing the following: We have:

For all , the composite functor Γ × Γ • is a monad.

P

. We already know that is a monad. Furthermore, precomposing any monad by any option functor again yields a monad, by the following (folklore) lemma. We conclude by the adjunction Γ × ⊢ Γ • . Furthermore, the following result is folklore.

L

C.23. For all monads on a category with binary coproducts, and for all objects therein, the natural transformation ↑ : → defined at any by

forms a monad distributive law, thus equipping with monad structure.

We may now define ℎ • .

Definition C.24. For all , ∈ C, let ℎ • , :

Using the notation, we want to prove that the following square commutes.

We first observe that both morphisms have the same restriction to Σ , by definition of ℎ • and Lemma C.20. Thus, by

• universal property of as a free Σ-algebra over , and • the fact that for any morphism : 1 → 2 of monads, any : 1 → 2 is a 1 -algebra morphism, equipping 2 with the 1 -algebra structure given by

, is an -algebra morphism, or equivalently a Σ-algebra morphism,

The third law is direct by Lemma C.21. For the first two, we proceed similarly to the proof of Lemma C.28, by showing that all the needed morphisms are Σ-algebra morphisms. For the first diagram, the top and right-hand morphisms are free Σ-algebra morphisms, so we reduce to proving that 2 is a Σ-algebra morphism. This holds by commutativity of the diagram in The top triangle commutes by construction of

and the second component of is 2 : Γ ( ) × → . Let us now turn to the second diagram. We start by equipping the codomain with Σ-algebra structure, by applying Lemma C.26 with = and

, whose algebra structure is given by either of the following three equal composites.

L C.31. The above -algebra structures are indeed equal.

P

. The latter equivalence is clear. For the former, we proceed by diagram chasing as in Figure 5, where = .

Returning to the second law of Lemma C.30, the bottom row is the image by Γ × of a morphism that lifts to alg, by commutation of the diagram in Figure 6. It thus itself lifts to Σalg by Lemma C.26.

Finally, we prove that the right-hand composite is a Σ-algebra morphism by diagram chasing as follows. ( ) ( )

P

. By Lemma C.30, Corollary C.17, and the fact that ℎ • , is a monad morphism by contruction. E.g., the third law holds iff the transposed morphisms coincide. This gives the following diagram,

which is precisely commutation of ℎ • with unit. Similarly, the penultimate law holds iff the transposed morphisms coincide. This gives the following diagram,

For the second statement, we first reduce to the rightmost subdiagram in Figure 9, which further reduces as in Figure 10.

P . Up to some easy rewriting of the right-hand composite, this is proved in Figure 12.

. By diagram chasing, as follows.

Γ Σ (Γ + + )

• ,

D PROOF OF THEOREM 4.13

We fix a given incremental structural law : Γ (Σ( )) → (Γ ( ) + + ) over :

( / is a Γ -algebra morphism) (easy)

P

. The pentagon (13) with = ⊕ ′ equivalently states that the -algebra structure a :

→ is a morphism of ( ⊕ ′ )-algebras. But by Lemma 4.7 this is equivalent to being both a -and Γ Δ-algebra morphism. The former is taken care of by ( 13) with = , the latter by the given diagram.

It remains to show that, given an object equipped with -and -algebra structures a : → and b :

→ satisfying (d1), the following are equivalent: • a morphism c : Γ( , ) → satisfying (d2), and

P

. We show commutation of the diagram by precomposing both sides by the split epimorphism Γ a a, and observing that they both are equal to the left bottom composite in (d2 ′ ). For c,

Because • , is a monad morphism by construction, one easily proves that both sides have the same restriction along : → , so it suffices to prove that both sides are -algebra morphisms. By construction, a and • , are, so we focus on other morphisms. • We first recall Lemma C.26, which says that Γ × lifts to a functor -Alg → Σalg, by considering, for any -algebra e : → , the following Σ-algebra structure:

• For proving that the top right composite is a morphism of Σ-algebras, it thus suffices to prove that the underlying composite Γ • → is a morphism of -algebras. But this is in turn equivalent to being both a morphism of -and -algebras. This easy to see for , and the given composite is a morphism of -algebras as a composite of two free -algebra morphisms, and the -algebra structure → . • For the bottom left composite, we show that it is a Σ-algebra morphism by chasing the diagram in Figure 17, where the bottom right subdiagram commutes by Lemma D.8 below.

L D.8. For any ( , )-algebra with structure induced by

the following diagram commutes.

Since the domain is a coproduct, we proceed termwise. On Σ , the result is straightforward. On Γ Σ , we observe that the diagram in Figure 18 commutes for all , , so that the

The assignment of the previous lemma lifts to a section ¯ :

Let us now prove Theorem 5.12. Suppose given a structural equational system over a distributive law :

→ , i.e., an incremental structural law

and a pair of structural interpretations , : ΘΔ → . In this section, we show that the initial -algebra ∅ → ∅ coequalises ∅ and ∅ . To this end, we exploit admissibility of the monad morphism → ( ⊕ ′ ) (Remark 12) which entails that the -algebra structure on ∅ uniquely extends to an ( ⊕ ′ )-algebra structure. By Theorem 4.13, we obtain that there is a unique ΘΔ-algebra structure on ∅ satisfying (d2).

But by the corollary and both induce ΘΔ-algebra stucture on ∅ which satisfy (d2), namely the composites

We thus conclude by uniqueness.

F PROOFS OF §5.5

We need to check coherence (Figure 2) for all of 1 , 1 , 2 , and 2 .

Fig. 22. Subdiagram (Γ; Γ)

There, the top subdiagram with red arrows is the associativity axiom for pointed strengths. We then use naturality of three times easily, and a fourth time much less easily. The point is that we use naturality at the pair of morphisms

-----→ , which requires us to prove that the second morphism is a morphism of pointed objects. We do this by chasing the following diagram,

whose question marked subdiagram commutes as follows.

??

(3)

The double question marked subdiagram of the latter diagram in turn commutes as follows.

⊗

It remains to prove that both large subdiagrams at the bottom of Figure 23 commute. For the lefthand one, the first term is almost trivial, and the second term is easy:

In order to prove the right-hand one, we need the following lemma.

L F.2. For any object , the following diagram commutes.

⊗ ⊗ ⊗ ⊗ ⊗

Γ , Γ ,

P

. We resort to the definition of from , and proceed by diagram chasing, as follows.

We may now prove that the bottom right subdiagram of Figure 23 commutes.

+Σ( ⊗ )

[

(3) Fig. 24. Coherence of 2

The right-hand, double question-marked subdiagram has a coproduct as its domain, so we proceed termwise. The second term is chased as follows.

Σ( ⊗ )

Σ + ( ⊗ ) ( ⊗ ) ( ⊗ ) ( ⊗ + + )

Σ( ⊗ 1)

The first term is chased as follows.

Σ + ( ⊗ ) ( ⊗ ) ( ⊗ ) ( ⊗ + + ) Again, the domain is a coproduct, so we proceed termwise. The first term is chased as follows.

⊗ Σ + ( ⊗ ) ( ⊗ ) ( ⊗ ) ( ⊗ + + )