Theory and Applications of Categories, Vol. 27, No. 18, 2013, pp. 464–492.

AN EQUATIONAL METALOGIC FOR MONADIC EQUATIONAL SYSTEMS

MARCELO FIORE

Abstract. The paper presents algebraic and logical developments. From the algebraic viewpoint, we introduce Monadic Equational Systems as an abstract enriched notion of equational presentation. From the logical viewpoint, we provide Equational Metalogic as a general formal deductive system for the derivability of equational consequences. Relating the two, a canonical model theory for Monadic Equational Systems is given and for it the soundness of Equational Metalogic is established. This development involves a study of clone and double-dualization structures. We also show that in the presence of free algebras the model theory of Monadic Equational Systems satisfies an internal strong-completeness property.

1. Introduction

Background The modern understanding of equationally defined algebraic structure, i.e. universal algebra, considers the subject as a trinity from the interrelated viewpoints of: (I) equational presentations and their varieties; (II) algebraic theories and their models; and (III) monads and their algebras.

The subject was first considered from the viewpoint (I) by [Birkhoff (1935)]. There the notion of abstract algebra was introduced and two fundamental results were proved. The first one, so-called variety (or HSP) theorem, falls within the tradition of universal algebra and characterises the classes of equationally defined algebras, i.e. algebraic categories. The second one, the soundness and completeness of equational reasoning, falls within the tradition of logic and establishes the correspondence between the semantic notion of validity in all models and the syntactic notion of derivability in a formal system of inference rules.

The viewpoints (II) and (III) only became available with the advent of category theory. Concerning (II), [Lawvere (1963)] shifted attention from equational presentations to their invariants in the form of algebraic theories, the categorical counterparts of the abstract clones of P. Hall in universal algebra (see e.g. [Cohn (1965), Chapter III, page 132]). This

This paper gives a new development of results announced in [Fiore and Hur (2008)] and elaborated upon in [Hur (2010)]. I am grateful to Chung-Kil Hur for our collaboration on the subject matter of this work.

Received by the editors 2012-05-01 and, in revised form, 2013-09-15. Published on 2013-09-22 in the volume of articles from CT2011. 2010 Mathematics Subject Classification: 18A15; 18C10; 18C15; 18C20; 18C50; 18D20; 18D25;

68Q55; 03B22.

Key words and phrases: Monoidal action; strong monad; clones; double dualization; equational presentation; free algebra; equational logic; soundness; (strong) completeness.

\begin{matrix}c \\ ◯ \end{matrix} Marcelo Fiore, 2013. Permission to copy for private use granted.

opened up a new spectrum of possibilities. In particular, the notion of algebraic category got extended to that of algebraic functor, and these were put in correspondence with the concept of map (or translation) between algebraic theories. Furthermore, the central result that algebraic functors have left adjoints pave the way for the monadic viewpoint (III). In this respect, fundamental results of Linton and of Beck, see e.g. [Linton (1966), Section 6] and [Hyland and Power (2007), Section 4], established the equivalence between bounded infinitary algebraic theories and their set-theoretic models with accessible monads on sets and their algebras. Incidentally, the notion of (co)monad had arisen earlier, in the late 1950s, in the different algebraic contexts of homological algebra and algebraic topology (see e.g. [Mac Lane (1997), Chapter VI Notes]).

Developments Since the afore-mentioned original seminal works much has been advanced. Specifically, the mathematical theories of algebraic theories and monads have been consolidated and vastly generalised. Such developments include extensions to categories with structure, to enriched category theory, and to further notions of algebraic structure. See, for instance, the developments of [Mac Lane (1965), Ehresmann (1968), Burroni (1971), Kelly (1972), Borceux and Day (1980), Kelly and Power (1993), Power (1999), Lack and Power (2009), Lack and Rosický (2011)] and the recent accounts in [Adámek and Rosický (1994), Robinson (2002), MacDonald and Sobral (2004), Pedicchio and Rovatti (2004), Hyland and Power (2007), Adámek, Rosický and Vitale (2010)].

By comparison, however, the logical aspect of algebraic theories provided by equational deduction has been paid less attention to, especially from the categorical perspective. An exception is the work of [Roşu (2001), Adámek, Hébert and Sousa (2007), Adámek, Sobral and Sousa (2009)]. In these, equational presentations are abstracted as sets of maps (which in the example of universal algebra correspond to quotients of free algebras identifying pairs of terms) and sound and complete deduction systems for the derivability of morphisms that are injective consequences (which in the example of universal algebra amount to equational implications) are considered.

Contribution The aim of this work is to contribute to the logical theory of equationally defined algebraic structure. Our approach in this direction [Fiore and Hur (2008), Hur (2010), Fiore and Hur (2011)] is novel in that it combines various aspects of the trinity (I–III).

In the first instance, we rely on the concept of monad as an abstract notion for describing algebraic structure. On this basis, we introduce a general notion of equational presentation, referred to here as Monadic Equational System (MES). This is roughly given by sets of equations in the form of parallel pairs of Kleisli maps for the monad. The role played by Kleisli maps here is that of a categorical form of syntactic term, very much as the role played by the Kleisli category when distilling a Lawvere theory out of a finitary monad.

It is of crucial importance, both for applications and theory, that the categorical development is done in the enriched setting. In this paper, as in [Hur (2010)] and unlike in the extended abstract [Fiore and Hur (2008)], we do so from the technically more elementary and at the same time more general perspective of monoidal actions, i.e. categories 𝒞 equipped with an action ∗ : 𝒱 × 𝒞 → 𝒞 for a monoidal category 𝒱 , see Section 2. In applications, the enrichment is needed, for instance, when moving from mono to multi sorted algebra, see [Fiore (2008), Part I] and [Fiore and Hur (2008)]. As for the theoretical development, in Section 5, a MES is then defined to consist of a strong monad 𝕋 on a biclosed action (𝒞 , ∗ : 𝒱 × 𝒞 → 𝒞 ) for a monoidal category 𝒱 together with a set of equations { u_{e} ≡ v_{e} : C_{e} → T A_{e} }_{e∈E} for the endofunctor T underlying the monad 𝕋 (see Definition 5.10). Here the biclosed structure amounts to right adjoints (−) ∗ C ⊣ \underline{𝒞} (C, −) : 𝒞 → 𝒱 and V ∗ (−) ⊣ [V, −] : 𝒞 → 𝒞 for all C ∈ 𝒞 and V ∈ 𝒱 .

In Section 3, generalising seminal work of [Kock (1970a)] (see also [Kock (2012)]), we show that the biclosed structure of the monoidal action provides a double-dualization strong monad 𝕂_{X} for every X ∈ 𝒞, with underlying endofunctor K_{X} = [\underline{𝒞} (−, X), X], establishing a bijective correspondence between 𝕋-algebra structures s : T X → X and strong monad morphisms σ(s) : 𝕋 → 𝕂_{X}. It follows that Kleisli maps t : C → T A have a canonical internal semantic interpretation in Eilenberg-Moore algebras (X, s) as morphisms σ(s)_{A} ∘ t : C → [\underline{𝒞} (A, X), X] (cf. Definition 5.2 and Remark 5.5), in the same way that in universal algebra syntactic terms admit algebraic interpretations. One thus obtains a canonical notion of satisfaction between algebras and equations, whereby an equation u ≡ v : C → T A is satisfied in an algebra (X, s) iff its semantic interpretation is an identity, that is σ(s)_{A} ∘ u = σ(s)_{A} ∘ v : C → [\underline{𝒞} (A, X), X] (see Definition 5.7).

In Section 7, the model theory of MESs is put to use from the logical perspective, and we introduce a deductive system, referred to here as Equational Metalogic (EML), for the formal reasoning about equations in MESs. The core of EML are three inference rules—two of congruence and one of local-character—that embody algebraic properties of the semantic interpretation. Hence, EML is sound by design.

In the direction of completeness, Section 8 establishes a strong-completeness result (Theorem 8.6) to the effect that an equation is satisfied by all models iff it is satisfied by a freely generated one. This requires the availability of free constructions, a framework for which is outlined in Sections 4 and 6.

Strong completeness is the paradigmatic approach to completeness proofs, and we have in fact already used it to this purpose. Indeed, the categorical theory of the paper has been shaped not only by reworking the traditional example of universal algebra in it [Fiore and Hur (2011), Part II] but also by developing two novel applications. Specifically, the companion paper [Fiore and Hur (2011), Part II] considers the framework in the topos of nominal sets [Gabbay and Pitts (2001)], which is equivalent to the Schanuel topos (see e.g. [Mac Lane and Moerdijk (1992), page 155]), and studies nominal algebraic theories providing a sound and complete nominal equational logic for reasoning about algebraic structure with name-binding operators. Furthermore, the companion paper [Fiore and Hur (2010)] considers the framework in the object classifier topos, introducing a conservative extension of universal algebra from first to second order, i.e. to languages with variable binding and parameterised metavariables, and thereby synthesising a sound and complete second-order equational logic. Second-order algebraic theories are the subject of [Fiore and Mahmoud (2010)].

2. Strong monads

We briefly review the notion of strong monad (and their morphisms) for an action of a monoidal category on a category (see e.g. [Kock (1970b), Kock (1972), Pareigis (1977)]), and recall its relationship to the notion of enriched monad on an enriched category (see e.g. [Janelidze and Kelly (2001)]).

Monoidal actions A 𝒱 -action 𝒞 = (𝒞 , ∗, \underline{α}, \underline{λ}) for a monoidal category 𝒱 = (𝒱 , I, ·, α, λ, ρ) consists of a category 𝒞, a functor ∗ : 𝒱 × 𝒞 → 𝒞 and natural isomorphisms \underline{λ}_{C} : I ∗ C ⟶^{≅} C and \underline{α}_{U,V,C} : (U · V) ∗ C ⟶^{≅} U ∗ (V ∗ C) subject to the following coherence conditions:

\xymatrix{(I · V) ∗ C \ar[dr]_{λ_{V} ∗C} \ar[r]^{^{\underline{α}^{I,V,C}}} & I ∗ (V ∗ C) \ar[d]^{_{\underline{λ}_{V ∗C}}} & (V · I) ∗ C \ar[dr]_{ρ_{V} ∗C} \ar[r]^{^{\underline{α}^{V,I,C}}} & V ∗ (I ∗ C) \ar[d]^{V ∗\underline{λ}_{C}} \\  & V ∗ C &  & V ∗ C}

\xymatrix{((U · V) · W) ∗ C \ar[r]^{α_{U,V,W} ∗C} \ar[d]^{_{\underline{α}_{U·V,W,C}}} & (U · (V · W)) ∗ C \ar[r]^{^{\underline{α}^{U,V ·W,C}}} & U ∗ ((V · W) ∗ C) \ar[d]^{U∗\underline{α}_{V,W,C}} \\ (U · V) ∗ (W ∗ C) \ar[rr]_{_{\underline{α}_{U,V,W ∗C}}} &  & U ∗ (V ∗ (W ∗ C))}

Such an action is said to be right closed if for all C ∈ 𝒞 the functor (−) ∗ C : 𝒱 → 𝒞 has a right adjoint \underline{𝒞} (C, −) : 𝒞 → 𝒱 referred to as a right-hom. The action is said to be left closed if for all V ∈ 𝒱 the functor V ∗ (−) : 𝒞 → 𝒞 has a right adjoint [V, −] : 𝒞 → 𝒞 referred to as a left-hom. When an action is both right and left closed, it is said to be biclosed.

2.1. Examples. We will be mainly interested in biclosed actions, examples of which follow.

1. Every category 𝒞 with small coproducts and products gives rise to a biclosed Set -action (𝒞 , ·), for Set equipped with the cartesian structure, where the actions V · C, right-homs \underline{𝒞} (C, D), and left-homs [V, C] are respectively given by the coproducts ∐_{v∈V} C, the hom-sets 𝒞 (C, D), and the products ∏_{v∈V} C.

2. Every monoidal biclosed category (𝒞 , I, ⊗) induces the biclosed 𝒞 -action (𝒞 , ⊗) with right-homs and left-homs respectively given by the right and left closed structures.

3. For 𝒱 monoidal closed, every 𝒱 -category 𝒦 with tensor ⊗ and cotensor ∩| gives rise to the biclosed 𝒱 -action (𝒦_{0}, ⊗_{0}) for 𝒦_{0} and ⊗_{0} respectively the underlying ordinary category and functor of 𝒦 and ⊗, where the right-homs \underline{𝒦_{0}} (X, Y) and left-homs [V, X] are respectively given by the hom-objects 𝒦 (X, Y) and the cotensors V ∩| X.

4. From a family of biclosed 𝒱 -actions { (𝒞_{i}, ∗_{i}) }_{i∈I} for a small set I, when 𝒱 has I-indexed products, we obtain the product biclosed 𝒱 -action ∏_{i∈I}(𝒞_{i}, ∗_{i}) = (𝒞 , ∗), where the category 𝒞 is given by the product category ∏_{i∈I} 𝒞_{i} and where the actions V ∗ \{C_{i}\}_{i∈I}, right-homs \underline{𝒞} (\{C_{i}\}_{i∈I}, \{D_{i}\}_{i∈I}), and left-homs [V, \{C_{i}\}_{i∈I}] are respectively given pointwise by \{V ∗_{i} C_{i}\}_{i∈I}, ∏_{i∈I} \underline{𝒞_{i}} (C_{i}, D_{i}), and \{[V, C_{i}]_{i}\}_{i∈I}.

Strong functors A strong functor (F, φ) : (𝒞 , ∗, \underline{α}, \underline{λ}) → (𝒞′, ∗′, \underline{α}′, \underline{λ}′) between 𝒱 -act-ions consists of a functor F : 𝒞 → 𝒞′ and a strength φ for F, i.e. a natural transformation φ_{V,C} : V ∗′ F C → F (V ∗ C) : 𝒱 × 𝒞 → 𝒞 subject to the following coherence conditions:

\xymatrix{I ∗′ F C \ar[r]^{φ_{I,C}} \ar[dr]_{_{\underline{λ}{′ \atop F C}}} & F (I ∗ C) \ar[d]^{F (\underline{λ}_{C})} & (U · V) ∗′ F C \ar[r]^{^{\underline{α}{′ \atop U,V,F C}}} \ar[d]^{φ_{U·V,C}} & U ∗′ (V ∗′ F C) \ar[r]^{U∗′φ_{V,C}} & U ∗′ F (V ∗ C) \ar[d]^{φ_{U,V ∗C}} \\  & F C & F ((U · V) ∗ C) \ar[rr]_{F (\underline{α}_{U,V,C})} &  & F (U ∗ (V ∗ C))}

A strong functor morphism τ : (F, φ) → (F′, φ′) between strong functors is a natural transformation τ : F → F′ satisfying the coherence condition

\xymatrix{V ∗ F C \ar[r]^{V ∗τ_{C}} \ar[d]_{φ_{V,C}} & V ∗ F′C \ar[d]^{φ_{V,C}} \\ F (V ∗ C) \ar[r]_{τ_{V ∗C}} & F′(V ∗ C)}

Strong monads A strong monad 𝕋 = (T, φ, η, μ) on a 𝒱 -action (𝒞 , ∗) consists of a strong endofunctor (T, φ) and a monad (T, η, μ) both on 𝒞 for which the unit η and the multiplication μ are strong functor morphisms (Id_{𝒞} , { id_{V ∗X} }_{V ∈𝒱 ,X∈𝒞} ) → (T, φ) and (T T, T φ ∘ φT) → (T, φ); i.e. they satisfy the coherence conditions below:

\xymatrix{V ∗ T C \ar[r]^{φ_{V,C}} & T (V ∗ C) & V ∗ T T C \ar[r]^{φ_{V,T C}} \ar[d]^{V ∗μ_{C}} & T (V ∗ T C) \ar[r]^{T (φ_{V,C})} & T T (V ∗ C) \ar[d]^{μ_{V ∗C}} \\ V ∗ C \ar[u]^{V ∗η_{C}} \ar@{-->}[ur]_{η_{V ∗C}} &  & V ∗ T C \ar[rr]_{φ_{V,C}} &  & T (V ∗ C)}

2.2. Proposition. For every strong monad 𝕋 on a 𝒱 -action (𝒞 , ∗), the 𝒱 -action structure on 𝒞 lifts to a 𝒱 -action structure on the Kleisli category 𝒞_{𝕋} making the canonical adjunction [figure: 𝒞; ⊥; 𝒞_{𝕋}] into an adjunction of strong functors.

The action functor ∗_{𝕋} : 𝒱 × 𝒞_{𝕋} → 𝒞_{𝕋} is given, for h : V → V′ in 𝒱 and f : A → T A′ in 𝒞, by h ∗_{𝕋} f = φ_{V′,A′} ∘ (h ∗ f) : V ∗ A → T (V′ ∗ A′) in 𝒞.

A strong monad morphism τ : (T, φ, η, μ) → (T′, φ′, η′, μ′) between strong monads on a monoidal action 𝒞 is a natural transformation τ : T → T′ that is both a strong functor morphism τ : (T, φ) → (T′, φ′) and a monad morphism τ : (T, η, μ) → (T′, η′, μ′), in that the further coherence conditions hold:

\xymatrix{ & C \ar[dl]_{η_{C}} \ar[dr]^{η′_{C}} &  & T T C \ar[r]^{(ττ)_{C}} \ar[d]_{μ_{C}} & T′T′C \ar[d]^{μ′_{C}} \\ T C \ar[rr]_{τ_{C}} &  & T′C & T C \ar[r]_{τ_{C}} & T′C}

2.3. Proposition. Every morphism τ : 𝕋 → 𝕋′ of strong monads on a 𝒱 -action (𝒞 , ∗) induces a strong functor (τ^{⋆}, φ_{τ}) : (𝒞_{𝕋} , ∗_{𝕋}) → (𝒞_{𝕋′} , ∗_{𝕋′}) of 𝒱 -actions.

Proof. For f : A → T B in 𝒞, τ^{⋆}(f) = τ_{B} ∘ f : A → T′B in 𝒞, and (φ_{τ})_{V,C} = id_{V ∗C} in 𝒞_{𝕋′}. In particular, the diagram

\xymatrix{𝒱 × 𝒞_{𝕋} \ar[d]_{_{∗_{𝕋}}} \ar[r]^{𝒱 ×τ^{⋆}} & 𝒱 × 𝒞_{𝕋′} \ar[d]^{_{∗_{𝕋′}}} \\ 𝒞_{𝕋} \ar[r]_{τ^{⋆}} & 𝒞_{𝕋′}}

commutes.

2.4. Proposition. Every morphism τ : 𝕋 → 𝕋′ of strong monads on a monoidal action 𝒞 contravariantly induces a functor 𝒞^{𝕋′} → 𝒞^{𝕋} : (X, s) ↦ (X, s ∘ τ_{X}) between the categories of Eilenberg-Moore algebras.

Enrichment For a monoidal category 𝒱 , every right-closed 𝒱 -action induces a 𝒱 -cat-egory, whose hom-objects are given by the right-homs. Furthermore, we have the following correspondences.

• To give a strong functor between right-closed 𝒱 -actions is equivalent to give a 𝒱 -functor between the associated 𝒱 -categories.

• To give a strong monad between right-closed 𝒱 -actions is equivalent to give a 𝒱 -monad between the associated 𝒱 -categories.

When 𝒱 is monoidal closed, the notion of right-closed 𝒱 -action essentially amounts to that of tensored 𝒱 -category (see [Janelidze and Kelly (2001), Section 6]). However, requiring left-closedness for right-closed 𝒱 -actions is weaker than requiring cotensors for the corresponding tensored 𝒱 -categories; as the former requires the action functors V ∗(−) to have a right adjoint, whilst the latter further asks that the adjunction be enriched. The difference between the two conditions vanishes when 𝒱 is symmetric monoidal closed. For example, every monoidal biclosed category 𝒱 yields a biclosed 𝒱 -action on itself, but not necessarily a tensored and cotensored 𝒱 -category unless 𝒱 is symmetric.

3. Clones and double dualization

We consider and study a class of monads that are important in the semantics of algebraic theories and play a prominent role in the developments of Sections 5, 7, and 8. These monads will be seen to arise from two different constructions, respectively introduced by [Kock (1970a)] for symmetric monoidal closed categories and by [Kelly and Power (1993)] for locally finitely presentable categories enriched over symmetric monoidal closed categories that are locally finitely presentable as closed categories. Here we generalize these developments to the setting of biclosed monoidal actions.

Kock’s approach sees these monads as arising from a double-dualization adjunction, while Kelly and Power’s approach induces them as endo-hom monoids for a clone closed structure. The latter viewpoint is more general and allows one to give abstract proofs; hence we introduce it first. The former viewpoint is elementary and allows one to apply it more directly. Both perspectives complement each other.

Clone monads The constructions of this subsection were motivated by the developments in [Kelly and Power (1993), Sections 4 and 5].

3.1. Definition. For 𝒱 -actions 𝒜 and ℬ, let St(𝒜 , ℬ) be the category of strong functors 𝒜 → ℬ and morphisms between them.

Note that the category St(𝒜 , ℬ) is a 𝒱 -action with structure given pointwise.

3.2. Theorem. Let 𝒜 be a right-closed 𝒱 -action and ℬ a left-closed 𝒱 -action. For every X ∈ 𝒜, the evaluation at X functor E_{X} : St(𝒜 , ℬ) → ℬ : (F, φ) ↦ F X has the clone functor ⟨X, −⟩ : ℬ → St(𝒜 , ℬ) : Y ↦ ([\underline{𝒜} (−, X), Y], γ^{X,Y} ) as right adjoint, where the strength γV,A^{X,Y} : V ∗ ⟨X, Y ⟩A → ⟨X, Y ⟩(V ∗ A) is given by the transpose of

\underline{𝒜} (V ∗ A, X) ∗ (V ∗ [\underline{𝒜} (A, X), Y]) \underline{α}_{−1}

(\underline{𝒜} (V ∗ A, X) · V) ∗ [\underline{𝒜} (A, X), Y]

ϵ_{X}^{V,A}∗[\underline{𝒜} (A,X),Y]
\underline{𝒜} (A, X) ∗ [\underline{𝒜} (A, X), Y]
ε_{Y}^{\underline{𝒜} (A,X)}
Y

with ϵ_{X}^{V,A} : \underline{𝒜} (V ∗ A, X) · V → \underline{𝒜} (A, X) in turn the transpose of

\xymatrix{(\underline{𝒜} (V ∗ A, X) · V) ∗ A \ar[r]^{\underline{α}} & \underline{𝒜} (V ∗ A, X) ∗ (V ∗ A) \ar[r]^{^{\underline{ε}{V ∗A \atop X}}} & X .}

Proof. The main lemmas needed for showing the naturality and coherence conditions of the strength are as follows:

\xymatrix{\underline{𝒜} (V ∗ A, X) · U \ar[r]^{\underline{𝒜} (h∗A,X)·U} \ar[d]_{\underline{𝒜} (V ∗A,X)·h} & \underline{𝒜} (U ∗ A, X) · U \ar[d]^{ϵ_{X}^{U,A}} \\ \underline{𝒜} (V ∗ A, X) · V \ar[r]_{ϵ_{X}^{V,A}} & \underline{𝒜} (A, X)} (h : U → V in 𝒱 )

\xymatrix{ & \underline{𝒜} (A, X) · I \ar[dl]_{\underline{𝒜} (\underline{λ}_{A},X)·I} \ar[dr]^{ρ_{\underline{𝒜} (A,X)}} \\ \underline{𝒜} (I ∗ A, X) · I \ar[rr]_{ϵ_{X}^{I,A}} &  & \underline{𝒜} (A, X)}

\xymatrix{ & (\underline{𝒜} (U ∗ (V ∗ A), X) · U) · V \ar[dl]_{α} \ar[dr]^{ϵ_{X}^{U,V ∗A}·V} \\ \underline{𝒜} (U ∗ (V ∗ A), X) · (U · V) \ar[d]_{\underline{𝒜} (\underline{α},X)·(U·V)} &  & \underline{𝒜} (V ∗ A, X) · V \ar[d]^{ϵ_{X}^{V,A}} \\ \underline{𝒜} ((U · V) ∗ A, X) · (U · V) \ar[rr]_{ϵ_{X}^{U·V,A}} &  & \underline{𝒜} (A, X)}

The natural bijective correspondence

ς_{F,Y}^{X} : St(𝒜 , ℬ)(F, [\underline{𝒜} (−, X), Y]) ≅ ℬ(F X, Y) : σ_{F,Y}^{X}

is a form of Yoneda lemma. Indeed, for a strong functor morphism τ : F → ⟨X, Y ⟩, one sets

ς(τ) = ( \xymatrix{F X \ar[r]^{τ_{X}} & [\underline{𝒜} (X, X), Y] \ar[r]^{ν_{Y}^{X}} & Y} )

where the counit ν_{Y}^{X} is the composite

\xymatrix{[\underline{𝒜} (X, X), Y] \ar[r]^{[ı_{X},Y]} & [I, Y] \ar[r]^{^{\underline{λ}^{−1}}}_{≅} & I ∗ [I, Y] \ar[r]^{ε_{Y}^{I}}_{≅} & Y}

for ı_{X} the transpose of \underline{λ}_{X} : I ∗ X → X, while for a morphism f : F X → Y one lets σ(f) have components given by the transpose of

ι(f)_{A} = ( \xymatrix{\underline{𝒜} (A, X) ∗ F A \ar[r]^{φ_{\underline{𝒜} (A,X),A}} & F (\underline{𝒜} (A, X) ∗ A) \ar[r]^{F (\underline{ε}_{X}^{A})} & F X \ar[r]^{f} & Y} ) . (1)

3.3. Corollary. For a biclosed monoidal action 𝒞, the evaluation functor St(𝒞 , 𝒞) × 𝒞 → 𝒞 gives a right-closed monoidal action structure on 𝒞 for St(𝒞 , 𝒞) equipped with the composition monoidal structure.

Applying the general fact that every object of a right-closed 𝒱 -action canonically induces an endo right-hom monoid in 𝒱 to the situation above, we have that every object of a biclosed monoidal action 𝒞 canonically induces a monoid in St(𝒞 , 𝒞), i.e. a strong monad on 𝒞, and we are lead to the following.

3.4. Definition. For every object X of a monoidal action 𝒞, the strong monad ℂ_{X} on 𝒞, henceforth referred to as the clone monad, has structure given by:

• the endofunctor C_{X} = ⟨X, X⟩ with strength κ^{X} = γ^{X,X},

• the unit η^{ℂ_{X}} : Id → C_{X}, and

• the multiplication μ^{ℂ_{X}} : C_{X}C_{X} → C_{X}

with the latter two respectively arising as the transposes of

\xymatrix{Id(X) \ar[r]^{^{id^{X}}} & X} and \xymatrix{C_{X}C_{X}X \ar[r]^{C_{X}ν_{X}^{X}} & C_{X}X \ar[r]^{ν_{X}^{X}} & X .}

Double-dualization monads For an object X of a biclosed 𝒱 -action 𝒞, the monad on 𝒞 induced by the adjunction

\underline{𝒞} (−, X) ⊣ [−, X] : 𝒱 ^{op} → 𝒞  (2)

will be referred to as the double-dualization monad. This notion and terminology were introduced by [Kock (1970a)] in the context of symmetric monoidal closed categories.^{1}

3.5. Definition. The double-dualization monad 𝕂_{X} on a biclosed monoidal action 𝒞 is explicitly given by:

• the endofunctor K_{X}(A) = [\underline{𝒞} (A, X), X],

• the unit η_{A}^{𝕂_{X}} : A → K_{X}(A) with components the transpose of \underline{ε}_{X}^{A} : \underline{𝒞} (A, X)∗A → X, and

• the multiplication

μ_{A}^{𝕂_{X}} = [δ_{\underline{𝒞} (A,X)}, X] : K_{X}(K_{X}A) → K_{X}(A)

where δ_{V} : V → \underline{𝒞} ([V, X], X) is the counit of the adjunction (2) given by the transpose of ε_{X}^{V} : V ∗ [V, X] → X.

We observe that, as expected, the clone and double-dualization monads coincide, from which one has as a by-product that the latter is strong.

1The standard terminology used in the theoretical computer science literature for these monads is (linear) continuation monads.

3.6. Theorem. For every object X of a biclosed monoidal action 𝒞,

ℂ_{X} = 𝕂_{X} .

Proof. Since ι(id_{X})_{A} = ε_{X}^{A} : \underline{𝒞} (A, X) ∗ A → X from (1), the units coincide. To establish the coincidence of the multiplications, we need show that the diagram

\xymatrix{\underline{𝒞} (A, X) ∗ C_{X}C_{X}A \ar[ddd]_{δ∗id} \ar[r]^{κ} & C_{X}(\underline{𝒞} (A, X) ∗ C_{X}A) \ar[r]^{C_{X}(κ)} & C_{X}C_{X}(\underline{𝒞} (A, X) ∗ A) \ar[d]^{C_{X}C_{X}(\underline{ε})} \\  &  & C_{X}C_{X}X \ar[d]^{C_{X}(ν_{X}^{X})} \\  &  & C_{X}X \ar[d]^{ν_{X}^{X}} \\ \underline{𝒞} (K_{X}A, X) ∗ K_{X}K_{X}A \ar[rr]_{ε} &  & X}

commutes. This is done using the following fact

[figure: C_{X}Y; [f̂,X]; C_{X}f; C_{X}X; ν_{X}^{X}; [I, X]; ≅; X; where; Y; f; X; I ∗ Y; f∘\underline{λ}_{Y}; X; I; f̂; \underline{𝒞} (Y, X)]

twice, with f being \underline{ε}_{X}^{A} : \underline{𝒞} (A, X) ∗ A → X and ε_{X}^{\underline{𝒞} (A,X)} : \underline{𝒞} (A, X) ∗ C_{X}(A) → X, together with the commuting diagrams

\xymatrix{\underline{𝒞} (A, X) ∗ C_{X}A \ar[d]_{ε} \ar[r]^{κ} & C_{X}(\underline{𝒞} (A, X) ∗ A) \ar[d]^{[ˆ\underline{ε},X]} \\ X \ar[r]|{≅} & [I, X]}

and

\xymatrix{\underline{𝒞} (A, X) ∗ C_{X}C_{X}A \ar[dd]_{δ∗id} \ar[r]^{κ} & C_{X}(\underline{𝒞} (A, X) ∗ C_{X}A) \ar[d]^{[ε̂,X]} \\  & [I, X] \ar[d]|{≅} \\ \underline{𝒞} (K_{X}A, X) ∗ K_{X}K_{X}A \ar[r]_{ε} & X}

Algebras By a T -algebra for an endofunctor T we mean an object X together with a map T X → X; while a 𝕋-algebra for a monad 𝕋 refers to an Eilenberg-Moore algebra.

3.7. Theorem. For every strong endofunctor T (resp. strong monad 𝕋) on a biclosed monoidal action 𝒞, the T -algebra (resp. 𝕋-algebra) structures on an object X ∈ 𝒞 are in bijective correspondence with the strong endofunctor (resp. strong monad) morphisms T → C_{X} (resp. 𝕋 → ℂ_{X}).

Proof. For endofunctor algebras and strong endofunctor morphisms, the result follows from Theorem 3.2, while for monad algebras s and strong monad morphisms τ one has that ς(τ) = ν_{X}^{X} ∘ τ_{X} is a 𝕋-algebra because ν_{X}^{X} is a ℂ_{X}-algebra, and that σ(s) is a strong monad morphism because the diagram

\xymatrix{T T X \ar[ddr]_{μ_{X}} \ar[dr]^{T s} \ar[rr]^{σ(s)_{T X}} &  & C_{X}T X \ar[dr]^{C_{X}s} \ar[rr]^{C_{X}σ(s)_{X}} &  & C_{X}C_{X}X \ar[ddl]^{μ^{ℂ_{X}}} \ar[dl]_{C_{X}ν_{X}^{X}} \\  & T X \ar[drr]_{s} \ar[rr]^{σ(s)_{X}} &  & C_{X}X \ar[d]_{ν_{X}^{X}} \\  & T X \ar[rr]_{s} &  & X}

commutes and because the commutativity of the diagram on the left below

[figure: X; _{id_{X}}; η_{X}; T X; s; σ(s)_{X}; C_{X}X; ν_{X}^{X}; X; Id; η^{ℂ_{X}}; η; T; σ(s); C_{X}]

implies that of the one on the right above.

3.8. Corollary. Let T (resp. 𝕋) be a strong functor (resp. strong monad) on a biclosed monoidal action 𝒞. For every T -algebra (resp. 𝕋-algebra) (X, s) and K_{X}-algebra (resp. 𝕂_{X}-algebra) (Y, k), we have

\xymatrix{ & T \ar[dl]_{σ(s)} \ar[dr]^{σ(s_{k})} \\ K_{X} \ar[rr]_{σ(k)} &  & K_{Y}}

where s_{k} is the T -algebra (resp. 𝕋-algebra)

\xymatrix{T Y \ar[r]^{σ(s)_{Y}} & K_{X}(Y) \ar[r]^{k} & Y .}

3.9. Example. For every X ∈ 𝒞 and V ∈ 𝒱 , the map

[δ_{V} , X] : [\underline{𝒞} ([V, X], X), X] → [V, X]

provides a 𝕂_{X}-algebra structure on [V, X], and we have the following.

1. The associated strong monad morphism σ([δ_{V} , X]) : (𝕂_{X}, κ^{X}) → (𝕂_{[V,X]}, κ^{[V,X]}) has components [\underline{𝒞} (A, X), X] → [\underline{𝒞} (A, [V, X]), [V, X]] given by the double transpose of the composite

V ∗ (\underline{𝒞} (A, [V, X]) ∗ [\underline{𝒞} (A, X), X]) \underline{α}_{−1}

(V · \underline{𝒞} (A, [V, X])) ∗ [\underline{𝒞} (A, X), X]

ϵ_{A}^{′V} ∗[\underline{𝒞} (A,X),X]
\underline{𝒞} (A, X) ∗ [\underline{𝒞} (A, X), X]
ε_{X}^{\underline{𝒞} (A,X)}
X

where ϵ_{A}^{′V} : V · \underline{𝒞} (A, [V, X]) → \underline{𝒞} (A, X) is in turn the transpose of

\xymatrix{(V · \underline{𝒞} (A, [V, X])) ∗ A \ar[r]^{\underline{α}} & V ∗ (\underline{𝒞} (A, [V, X]) ∗ A) \ar[r]^{V ∗\underline{ε}_{[V,X]}^{A}} & V ∗ [V, X] \ar[r]^{ε_{X}^{V}} & X} .

2. For every strong functor T (resp. strong monad 𝕋) and T -algebra (resp. 𝕋-algebra) (X, s), the T -algebra (resp. 𝕋-algebra) s_{[δ_{V} ,X]} on [V, X], for which we will henceforth simply write

s_{V} : T [V, X] → [V, X] ,

is the transpose of the composite

\xymatrix{V ∗ T [V, X] \ar[r]^{φ_{V,[V,X]}} & T (V ∗ [V, X]) \ar[r]^{T (ε_{X}^{V})} & T X \ar[r]^{s} & X .}

4. Free algebras

The category of algebras for an endofunctor is said to admit free algebras whenever the forgetful functor has a left adjoint. In this case, the induced monad is the free monad on the endofunctor. A wide class of examples of strong monads arises as such, since the strength of an endofunctor on a left-closed monoidal action canonically lifts to the free monad on the endofunctor. This section establishes a general form of this result (Theorem 4.4), showing that it holds for every monad arising from free algebras with respect to full subcategories of the endofunctor algebras that are closed under lefthoms.

Endofunctor algebras For an endofunctor T on a category 𝒞, the category T -Alg has T -algebras as objects and morphisms h : (X, s) → (Y, t) given by maps h : X → Y such that h ∘ s = t ∘ T h. We write U_{T} for the forgetful functor T -Alg → 𝒞 : (X, s) ↦ X.

4.1. Definition. For a strong endofunctor (T, φ) on a left-closed 𝒱 -action (𝒞 , ∗), for every V ∈ 𝒱 , the left-hom endofunctor [V, −] on 𝒞 lifts to T -Alg by setting

[V, (X, s : T X → X)] = ( [V, X] , s_{V} : T [V, X] → [V, X] )

for s_{V} as given in Example 3.9 (2).

For a strong monad 𝕋 on a left-closed monoidal action 𝒞, the left-homs do not only lift to T -Alg but also to the category of Eilenberg-Moore algebras 𝒞^{𝕋}.

4.2. Lemma. Let 𝕋 be a strong monad on a left-closed 𝒱 -action 𝒞. For every T -algebra (X, s),

(X, s) ∈ 𝒞^{𝕋} iff ([V, X], s_{V}) ∈ 𝒞^{𝕋} for all V ∈ 𝒱 .

Proof. (⇒) For (X, s) ∈ 𝒞^{𝕋}, the equalities

\begin{aligned}s_{V} ∘ η_{[V,X]} & = & id_{[V,X]} & : & [V, X] → [V, X] , \\ μ_{[V,X]} ∘ s_{V} & = & T (s_{V}) ∘ s_{V} & : & T T [V, X] → [V, X] \end{aligned}  (3)

are readily established by considering their transposes.

(⇐) Since the canonical isomorphism X ≅ [I, X] is a T -algebra isomorphism (X, s) ≅ ([I, X], s_{I}), it follows that ([I, X], s_{I}) ∈ 𝒞^{𝕋} implies (X, s) ∈ 𝒞^{𝕋}.

4.3. Remark. Under the assumption that the action is biclosed, (3) already follows from Corollary 3.8 and Example 3.9 (2).

Strong free algebras The main result of the section [Fiore and Hur (2008), Hur (2010)] follows.

4.4. Theorem. Let (F, φ) be a strong endofunctor on a left-closed 𝒱 -action (𝒞 , ∗), and consider a full subcategory 𝒜 of F -Alg such that the forgetful functor 𝒜 → 𝒞 has a left adjoint, say mapping objects X ∈ 𝒞 to F -algebras (T X, τ_{X} : F T X → T X) ∈ 𝒜 .

[figure: 𝒜; F -Alg; U_{F}; 𝒞; ⋋]  (4)

If 𝒜 is closed under the left-hom endofunctor [V, −] for all V ∈ 𝒱 , then 1. for every (Y, t) ∈ 𝒜 and map f : V ∗ X → Y in 𝒞, there exists a unique extension

map f^{#} : V ∗ T X → Y in 𝒞 such that the diagram

\xymatrix{V ∗ F T X \ar[d]_{V ∗τ_{X}} \ar[r]^{φ_{V,T X}} & F (V ∗ T X) \ar[r]^{F f^{#}} & F Y \ar[d]^{t} \\ V ∗ T X \ar[rr]^{∃! f^{#}} &  & Y \\ V ∗ X \ar[u]^{V ∗η_{X}} \ar@{-->}[urr]_{f}}  (5)

commutes, and

2. the monad 𝕋 = (T, η, μ) induced by the adjunction (4) canonically becomes a strong monad, with the components of the lifted strength φ̂ given by the unique maps such that the diagram

\xymatrix{V ∗ F T C \ar[r]^{φ_{V,T C}} \ar[d]_{V ∗τ_{C}} & F (V ∗ T C) \ar[r]^{F (φ̂_{V,C})} & F T (V ∗ C) \ar[d]^{τ_{V ∗C}} \\ V ∗ T C \ar@{-->}[rr]^{∃! φ̂_{V,C}} &  & T (V ∗ C) \\ V ∗ C \ar[u]^{V ∗η_{C}} \ar@{-->}[urr]_{η_{V ∗C}}}  (6)

commutes.

Proof. (1) For every F -algebra (Y, t) in 𝒜 also the F -algebra ([V, Y], t_{V}) is in 𝒜. Thus, for every map f : V ∗ X → Y, by the universal property of the adjunction, there exists a unique extension map f^{#} : V ∗ T X → Y making the following diagram commutative

\xymatrix{F (T X) \ar[r]^{F (\overline{f^{#}})} \ar[d]_{τ_{X}} & F [V, Y] \ar[d]^{t_{V}} \\ T X \ar[r]^{\overline{f^{#}}} & [V, Y] \\ X \ar[u]^{η_{X}} \ar[ur]_{\overline{f}}}

where \overline{f} and \overline{f^{#}} respectively denote the transposes of the maps f and f^{#}. Transposing this diagram, we obtain diagram (5) and we are done.

(2) The above item guarantees the unique existence of the maps φ̂_{V,C}. We need show that these are natural in V and C, and satisfy the four coherence conditions of strengths.

The naturality of φ̂, i.e. that T (f ∗ g) ∘ φ̂_{V,C} = φ̂_{V′,C′} ∘ (f ∗ T (g)) for f : V → V′ in 𝒱 and g : C → C′ in 𝒞, is shown by establishing that both these maps are the unique

extension of the composite \xymatrix{V ∗ C \ar[r]^{f∗g} & V′ ∗ C′ \ar[r]^{η_{V′∗C′}} & T (V′ ∗ C′)} .

The first coherence condition T (\underline{λ}_{C}) ∘ φ̂_{I,C} = \underline{λ}_{T C} is shown by establishing that both

these maps are the unique extension of the composite \xymatrix{I ∗ C \ar[r]^{^{\underline{λ}^{C}}} & C \ar[r]^{η_{C}} & T C} .

The second coherence condition T (\underline{α}_{U,V,C}) ∘ φ̂_{U·V,C} = φ̂_{U,V ∗C} ∘ (U ∗ φ̂_{V,C}) ∘ \underline{α}_{U,V,T C} is shown by establishing that both these maps are the unique extension of the composite

\xymatrix{(U · V) ∗ C \ar[r]^{\underline{α}} & U ∗ (V ∗ C) \ar[r]^{η_{U∗(V ∗C)}} & T (U ∗ (V ∗ C))} .

The third coherence condition φ̂_{V,C} ∘ (V ∗ η_{C}) = η_{V ∗C} is the bottom of diagram (6). The last coherence condition φ̂_{V,C} ∘ (V ∗ μ_{C}) = μ_{V ∗C} ∘ T (φ̂_{V,C}) ∘ φ̂_{V,T C} is shown by

establishing that both these maps are the unique extension of φ̂_{V,C} : V ∗T C → T (V ∗C).

4.5. Corollary. For a strong endofunctor F on a left-closed monoidal action 𝒞 for which the forgetful functor U_{F} has a left adjoint, the induced monad on 𝒞 is strong.

5. Monadic Equational Systems

As in [Fiore and Hur (2008), Hur (2010)], we introduce a general abstract enriched notion of equational presentation. This is here referred to as Monadic Equational System (Definition 5.10), with the terminology chosen to indicate the central role played by the concept of monad, which is to be regarded as encapsulating algebraic structure. In this context, equations are specified by pairs of Kleisli maps.

5.1. Definition. A Kleisli map for an endofunctor T on a category 𝒞 of arity A and coarity C is a morphism C → T A in 𝒞.

5.2. Definition. For a strong endofunctor (T, φ) on a right-closed 𝒱 -action (𝒞 , ∗), the interpretation of a Kleisli map t : C → T A in 𝒞 with respect to a T -algebra (X, s) is defined as

⟦t⟧_{(X,s)} = ι(s)_{A} ∘ (\underline{𝒞} (A, X) ∗ t) : \underline{𝒞} (A, X) ∗ C → X  (7)

where the interpretation map ι(s)_{A} : \underline{𝒞} (A, X) ∗ T A → X is that defined in (1).

Two basic properties of interpretation maps follow.

5.3. Proposition. Let T be a strong endofunctor on a right-closed 𝒱 -action (𝒞 , ∗). For h : (X, s) → (Y, t) in T -Alg, h ∘ ι(s)_{A} = ι(t)_{A} ∘ (\underline{𝒞} (A, h) ∗ T A).

5.4. Proposition. Let τ : S → T be a morphism between strong endofunctors on a rightclosed 𝒱 -action (𝒞 , ∗). For every T-algebra (X, s), the interpretation map ι(s ∘ τ_{X})_{A} : \underline{𝒞} (A, X) ∗ SA → X factors as the composite ι(s)_{A} ∘ (\underline{𝒞} (A, X) ∗ τ_{A}).

5.5. Remark. When considering a biclosed 𝒱 -action 𝒞, the interpretation maps

ι(s)_{A} : \underline{𝒞} (A, X) ∗ T A → X

transpose to yield a semantics transformation

σ(s) : T → K_{X}  (8)

as introduced in Theorem 3.2 and also studied in Theorem 3.7.

The interpretation of Kleisli maps in algebras induces a satisfaction relation (Definition 5.7) between algebras and equations.

5.6. Definition. For an endofunctor T, a parallel pair u ≡ v : C → T A of Kleisli maps is referred to as a T -equation.

5.7. Definition. Let T be a strong endofunctor on a right-closed 𝒱 -action (𝒞 , ∗). For all T -algebras (X, s) and T -equations u ≡ v : C → T A,

(X, s) ⊧ u ≡ v : C → T A iff ⟦u⟧_{(X,s)} = ⟦v⟧_{(X,s)} : \underline{𝒞} (A, X) ∗ C → X .

More generally, for a set of T -algebras 𝒜, we set 𝒜 ⊧ u ≡ v iff (X, s) ⊧ u ≡ v for all (X, s) ∈ 𝒜 .

5.8. Corollary. Let T be a strong endofunctor on a right-closed 𝒱 -action 𝒞. For every h : (X, s) → (Y, t) in T -Alg with h : X → Y a monomorphism in 𝒞, if (Y, t) ⊧ u ≡ v then (X, s) ⊧ u ≡ v.

Proof. By Proposition 5.3.

5.9. Corollary. Let T be a strong functor on a biclosed 𝒱 -action. For every T -algebra (X, s),

(X, s) ⊧ u ≡ v iff ([V, X], s_{V}) ⊧ u ≡ v for all V ∈ 𝒱 .

Proof. (⇒) Because, by Corollary 3.8 and Example 3.9, one has that ⟦t⟧_{([V,X],s_{V} )} is the transpose of the composite

\xymatrix{V ∗ (\underline{𝒞} (A, [V, X]) ∗ C) \ar[r]^{^{\underline{α}^{−1}}} & (V · \underline{𝒞} (A, [V, X])) ∗ C \ar[r]^{ϵ_{A}^{′V} ∗C} & \underline{𝒞} (A, X) ∗ C \ar[r]^{^{⟦t⟧^{(X,s)}}} & X}

for all t : C → T A.

(⇐) By Corollary 5.8 using that the canonical isomorphism X ≅ [I, X] is a T -algebra isomorphism (X, s) ≅ ([I, X], s_{I}).

Monadic Equational Systems The idea behind the definition of Monadic Equational System (MES) is that of providing a 𝒱 -enriched universe of discourse 𝒞 together with algebraic structure 𝕋 for specifying equational presentations E.

5.10. Definition. A Monadic Equational System (𝒱 , 𝒞 , 𝕋, E) consists of

• a monoidal category 𝒱 = (𝒱 , ·, I, α, λ, ρ),

• a biclosed 𝒱 -action 𝒞 = (𝒞 , ∗, \underline{α}, \underline{λ}, \underline{𝒞} (−, =), [−, =]),

• a strong monad 𝕋 = (T, φ, η, μ) on 𝒞, and

• a set of T -equations E.

5.11. Remark. Let 𝕋 be a strong monad on a biclosed 𝒱 -action (𝒞 , ∗). For a 𝕋-algebra (X, s), by Theorem 3.7, the semantics transformation (8) is a strong monad morphism

σ(s) : 𝕋 → 𝕂_{X}

that, by Proposition 2.3, induces the following situation

\xymatrix{𝒱 × 𝒞_{𝕋} \ar[r]^{𝒱 ×σ(s)^{⋆}} \ar[d]_{_{∗_{𝕋}}} & 𝒱 × 𝒞_{𝕂_{X}} \ar[d]^{_{∗_{𝕂_{X}}}} \\ 𝒞_{𝕋} \ar[r]_{_{σ(s)_{⋆}}} & 𝒞_{𝕂_{X}}}  (9)

where the functorial action of σ(s)^{⋆} : 𝒞_{𝕋} (C, A) → 𝒞_{𝕂_{X}} (C, A) is the transpose of the interpretation function of Kleisli maps (7).

5.12. Definition. An S-algebra for a MES S = (𝒱 , 𝒞 , 𝕋, E) is a 𝕋-algebra (X, s) satisfying the equations in E, i.e. such that (X, s) ⊧ u ≡ v for all (u ≡ v) ∈ E or, equivalently, such that σ(s) coequalizes every parallel pair of Kleisli maps in E.

The full subcategory of 𝒞^{𝕋} consisting of the S-algebras is denoted S-Alg, and we write U_{S} for the forgetful functor S-Alg → 𝒞.

5.13. Examples.

1. Every set of T -equations E for a monad 𝕋 on a category 𝒞 with small coproducts and products yields a MES (Set , 𝒞 , 𝕋, E). In particular, bounded infinitary algebraic presentations, see e.g. [Słominski (1959), Wraith (1975)], yield such MESs on complete and cocomplete categories.

2. An enriched algebraic theory [Kelly and Power (1993)] consists of: a locally finitely presentable category 𝒦 enriched over a symmetric monoidal closed category 𝒱 that is locally finitely presentable as a closed category together with a small set 𝒦_{f} representing the isomorphism classes of the finitely presentable objects of 𝒦 ; a 𝒦_{f}-i ndexed family of 𝒦 -o bjects O = { O_{c} }_{c∈𝒦_{f}} ; and a 𝒦_{f}-i ndexed family of parallel pairs of 𝒦_{0}-m orphisms ℰ = { u_{c} ≡ v_{c} : E_{c} → T_{O}(c) }_{c∈𝒦_{f}} for 𝕋_{O} the free finitary monad on the endofunctor ∐_{c∈𝒦_{f}} 𝒦 (c, −) ⊗ O_{c} on 𝒦 .

The structure (𝒱 , 𝒦_{0}, 𝕋_{O}, ℰ) yields a MES, an algebra for which is a 𝕋_{O}-algebra (X, s) such that σ(s)_{c} : T_{O}(c) → K_{X}(c) coequalizes u_{c} and v_{c} for all c ∈ 𝒦_{f}. This coincides with the notion of algebra for the finitary monad presented by ℰ (by means of a coequaliser of a parallel pair 𝕋_{E} ⇉ 𝕋_{O} induced by the parallel pairs in ℰ) as discussed in [Kelly and Power (1993), Section 5].

Nominal equational systems are MESs of this kind on the topos of nominal sets (equivalently the Schanuel topos) that feature in [Fiore and Hur (2011), Section 5].

3. We exemplify how MESs may be used to provide presentations of algebraic structure on symmetric operads. For this purpose, we need consider the category of symmetric sequences Seq = Set^{𝔹}, for 𝔹 the groupoid of finite cardinals and bijections, together with its product and coproduct structures and the following two monoidal structures:

• Day’s convolution symmetric monoidal closed structure [Day (1970), Im and Kelly (1986)] given by

(X ⊗ Y)(n) = ∫^{n_{1},n_{2}∈𝔹} X(n_{1}) × Y (n_{2}) × 𝔹(n_{1} + n_{2}, n)

with unit I = 𝔹(0, −); and

• the substitution (or composition) monoidal structure [Kelly (1972), Joyal (1981), Fiore, Gambino, Hyland, and Winskel (2008)] given by

(X • Y)(n) = ∫^{k∈𝔹} X(k) × Y^{⊗k}(n)

with unit J = 𝔹(1, −).

We identify the category of symmetric operads Op with its well-known description as the category of monoids for the substitution tensor product, and proceed to consider algebraic structure on it. In doing so, one crucially needs to require that the algebraic and monoid structures are compatible with each other, see [Fiore, Plotkin and Turi (1999), Fiore (2008)]. For example, the consideration of symmetric operads with a cartesian binary operation + and a linear binary operation ∗ leads to defining the category Op(+, ∗) with objects A ∈ Seq equipped with

• a monoid structure ν : J → A, μ : A^{•2} → A, and

• an algebra structure + : A^{2} → A, ∗ : A^{⊗2} → A

that are compatible in the sense that the diagrams

\xymatrix{A^{2} • A \ar[d]_{+ • id} \ar[r]^{⟨π_{1}•id,π_{2}•id⟩} & (A • A)^{2} \ar[r]^{μ^{2}} & A^{2} \ar[d]^{+} & A^{⊗2} • A \ar[d]_{∗ • id} \ar[r]^{≅} & (A • A)^{⊗2} \ar[r]^{μ^{⊗2}} & A^{⊗2} \ar[d]^{∗} \\ A • A \ar[rr]_{μ} &  & A & A • A \ar[rr]_{μ} &  & A}

commute. (Morphisms are both monoid and algebra homomorphisms.) Then, as follows from the general treatment given in [Fiore (2008)], the forgetful functor Op(+, ∗) → Seq has a left adjoint, for which the induced monad on Seq will be denoted 𝕄.

Algebraic laws correspond to M-equations, and give rise to MESs (Set , Seq , 𝕄, E). For example, the left-linearity law

(x_{1} + x_{2}) ∗ x_{3} = x_{1} ∗ x_{3} + x_{2} ∗ x_{3}

corresponds to the M-equation

J^{⊗2} [figure: ⟨η ι_{1},η ι_{2}⟩ ⊗ η ι_{3}](M(3·J))^{2} ⊗ M(3·J) [figure: + ⊗ id](M(3·J))^{⊗2} [figure: ∗]M(3·J) ≡

J^{⊗2} [figure: ⟨η ι_{1}⊗ η ι_{3},η ι_{2}⊗ η ι_{3}⟩]((M(3·J))^{⊗2})^{2} [figure: ∗^{2}](M(3·J))^{2} [figure: +]M(3·J)

while the additive pre-Lie law

(x_{1} ∗ x_{2}) ∗ x_{3} + x_{1} ∗ (x_{3} ∗ x_{2}) = x_{1} ∗ (x_{2} ∗ x_{3}) + (x_{1} ∗ x_{3}) ∗ x_{2}

corresponds to the M-equation

J^{⊗3} [figure: ⟨ηι_{1}⊗ηι_{2}⊗ηι_{3},ηι_{1}⊗ηι_{3}⊗ηι_{2}⟩]((M(3·J))^{⊗3})^{2} [figure: (∗(∗⊗id))×(∗(id⊗∗))](M(3·J))^{2} [figure: +]M(3·J) ≡

J^{⊗3} [figure: ⟨ηι_{1}⊗ηι_{2}⊗ηι_{3},ηι_{1}⊗ηι_{3}⊗ηι_{2}⟩]((M(3·J))^{⊗3})^{2} [figure: (∗(id⊗∗))×(∗(∗⊗id))](M(3·J))^{2} [figure: +]M(3·J)

This can in fact be extended to a MES whose algebras are symmetric operads over vector spaces equipped with a pre-Lie operation. The MES framework allows however for greater generality, being able to further incorporate linear algebraic theories with variable binding operators [Tanaka (2000)] and/or with parameterised metavariables [Hamana (2004), Fiore (2008)]. Details may appear elsewhere. Here, as a simple application of the latter, we limit ourselves to show that one can exhibit an equation

u_{m,n} ≡ v_{n,m} : J^{⊗(m·n)} → T (J^{⊗m} + J^{⊗n}) (m, n ∈ ℕ)

for 𝕋 the monad on Seq induced by the left adjoint to the forgetful functor Op → Seq , that is satisfied by a symmetric operad iff every two operations respectively of arities m and n commute with each other. Indeed, one lets

u_{m,n} = J^{⊗(m·n)} ≅ J^{⊗m} • J^{⊗n} [figure: (η ι_{1})•(η ι_{2})](T (J^{⊗m} + J^{⊗n}))^{•2} [figure: μ]T (J^{⊗m} + J^{⊗n})

and

v_{n,m} = J^{⊗(n·m)} ≅ J^{⊗n} • J^{⊗m} [figure: (η ι_{2})•(η ι_{1})](T (J^{⊗m} + J^{⊗n}))^{•2} [figure: μ]T (J^{⊗m} + J^{⊗n})

where, for k, ℓ ∈ ℕ and X ∈ Seq , the isomorphism X^{⊗(k·ℓ)} ≅ J^{⊗k} • X^{⊗ℓ} is given by the following composite of canonical isomorphisms:

X^{⊗(k·ℓ)} ≅ (X^{⊗ℓ})^{⊗k} ≅ (J • X^{⊗ℓ})^{⊗k} ≅ J^{⊗k} • X^{⊗ℓ} .

4. The companion papers [Fiore and Hur (2010)] and [Fiore and Mahmoud (2010)] consider MESs for an extension of universal algebra from first to second order, i.e. to algebraic languages with variable binding and parameterised metavariables. This work generalises the semantics of both (first-order) algebraic theories and of (untyped and simply-typed) lambda calculi.

Strong free algebras A MES S = (𝒱 , 𝒞 , 𝕋, E) is said to admit free algebras whenever the forgetful functor U_{S} has a left adjoint, so that we have the following situation:

[figure: S-Alg; U_{S}; 𝒞^{𝕋}; U_{𝕋}; 𝒞; ⋋; ⋌]

We write 𝕋_{S} for the induced free S-algebra monad on 𝒞.

5.14. Theorem. For a MES S that admits free algebras, the free S-algebra monad is strong.

Proof. By Lemma 4.2 and Corollary 5.9, applying Theorem 4.4 to the full subcategory S-Alg of T -Alg for T the endofunctor underlying the monad in S.

6. Free constructions

To establish the wide applicability of Theorem 5.14, we give conditions under which MESs admit free algebras. The results of this section follow from the theory developed in [Fiore and Hur (2009)]; proofs are thereby omitted.

6.1. Definition. An object A of a right-closed 𝒱 -action 𝒞 is respectively said to be κcompact, for κ an infinite limit ordinal, and projective if the functor \underline{𝒞} (A, −) : 𝒞 → 𝒱 respectively preserves colimits of κ-chains and epimorphisms.

6.2. Definition. A MES (𝒱 , 𝒞 , 𝕋, E) is called κ-finitary, for κ an infinite limit ordinal, if the category 𝒞 is cocomplete, the endofunctor T on 𝒞 preserves colimits of κ-chains, and the arity A of every T -equation u ≡ v : C → T A in E is κ-compact. Such a MES is called κ-inductive if furthermore T preserves epimorphisms and the arity A of every T -equation u ≡ v : C → T A in E is projective.

6.3. Theorem. For every κ-finitary MES S = (𝒱 , 𝒞 , 𝕋, E), the embedding S-Alg [figure] 𝒞^{𝕋} has a left adjoint, the forgetful functor U_{S} : S-Alg → 𝒞 is monadic, the category S-Alg is cocomplete, and the underlying functor T_{S} of the monad 𝕋_{S} representing S-Alg preserves colimits of κ-chains. If, furthermore, S is κ-finitary then T_{S} preserves epimorphisms, the universal homomorphism from (T X, μ_{X}) to its free S-algebra is epimorphic in 𝒞, and free S-algebras on 𝕋-algebras can be constructed in κ steps.

6.4. Remark. The theorem above applies to all the examples of 5.13.

6.5. In the case of ω-inductive MESs, the free S-algebra (T_{S}X, τ_{X}^{S} : T T_{S}X → T_{S}X) on X ∈ 𝒞 is constructed as follows:

[figure: ∀ (u ≡ v : C → T A) ∈ E; T (T X); p_{0}; T (q_{0}); μ_{X}; po; T (T X)_{1}; p_{1}; T (q_{1}); po; T (T X)_{2}; T (q_{2}); p_{2}; T (T X)_{3}; ······; T (T_{S}X); τ_{X}^{S}; \underline{𝒞} (A, T X) ∗ C; _{⟦u⟧_{(T X,μ_{X})}}; _{⟦v⟧_{(T X,μ_{X})}}; ⋮; ⋮; T X; q_{0}; coeq; (T X)_{1}; q_{1}; (T X)_{2}; q_{2}; (T X)_{3}; _{······}; colim; T_{S}X]

where q_{0} is the universal map that coequalizes every pair ⟦u⟧_{(T X,μ_{X})} and ⟦v⟧_{(T X,μ_{X})} with (u ≡ v) ∈ E; the parallelograms are pushouts; and T_{S}X is the colimit of the ω-chain of q_{i}.

Furthermore, when the strong monad 𝕋 arises from free algebras for a strong endofunctor F which is ω-cocontinuous and preserves epimorphisms, the construction simplifies as follows:

[figure: ∀ (u ≡ v : C → T A) ∈ E; F (T X); p_{0}; F (q_{0}); μ̂_{X}; po; F (T X)_{1}; p_{1}; F (q_{1}); po; F (T X)_{2}; F (q_{2}); p_{2}; F (T X)_{3}; ······; F (T_{S}X); τ_{X}^{S}; \underline{𝒞} (A, T X) ∗ C; _{⟦u⟧_{(T X,μ_{X})}}; _{⟦v⟧_{(T X,μ_{X})}}; ⋮; ⋮; T X; q_{0}; coeq; (T X)_{1}; q_{1}; (T X)_{2}; q_{2}; (T X)_{3}; _{······}; colim; T_{S}X]

where (T X, μ̂_{X}) and (T_{S}X, τ̂_{X}^{S}) are the F -algebras respectively corresponding to the Eilenberg-Moore algebras (T X, μ_{X}) and (T_{S}X, τ_{X}^{S}) for the monad 𝕋.

7. Equational Metalogic

The algebraic developments of the paper are put to use in a logical context. Specifically, as in [Fiore and Hur (2008), Hur (2010)], we introduce a deductive system, here referred to as Equational Metalogic (EML), for the formal reasoning about equations in Monadic Equational Systems. The envisaged use of EML is to serve as a metalogical framework for the synthesis of equational logics by instantiating concrete mathematical models. This is explained and exemplified in [Fiore and Hur (2011), Part II] and [Fiore and Hur (2010)].

Equational Metalogic The Equational Metalogic associated to a MES (𝒱 , 𝒞 , 𝕋, E) consists of inference rules that inductively define the derivable equational consequences

E ⊢ u ≡ v : C → T A ,

for u and v Kleisli maps of arity A and coarity C, that follow from the equational presentation E.

EML has been synthesised from the model theory, in that each inference rule reflects a model-theoretic property of equational satisfaction arising from the algebraic structure of the semantic interpretation. The inference rules of EML, besides those of equality and axioms, consist of congruence rules for composition and monoidal action, and a rule for the local character (see e.g. [Mac Lane and Moerdijk (1992), page 316]) of derivability. Formally, these are as follows.

1. Equality rules.

\begin{aligned}Ref \\ & E ⊢ u ≡ u : C → T A \end{aligned}  \begin{aligned}& E ⊢ u ≡ v : C → T A \\ Sym \\ & E ⊢ v ≡ u : C → T A \end{aligned}

E ⊢ u ≡ v : C → T A E ⊢ v ≡ w : C → T A Trans E ⊢ u ≡ w : C → T A

2. Axioms.

(u ≡ v : C → T A) ∈ E Axiom E ⊢ u ≡ v : C → T A

3. Congruence of composition.

E ⊢ u_{1} ≡ v_{1} : C → T B E ⊢ u_{2} ≡ v_{2} : B → T A Comp E ⊢ u_{1}{u_{2}} ≡ v_{1}{v_{2}} : C → T A

where w_{1}\{w_{2}\} denotes the Kleisli composite \xymatrix{C \ar[r]^{w_{1}} & T B \ar[r]^{T (w_{2})} & T (T A) \ar[r]^{μ_{A}} & T A} .

4. Congruence of monoidal action.

E ⊢ u ≡ v : C → T A Ext  (V ∈ 𝒱 )

E ⊢ ⟨V ⟩u ≡ ⟨V ⟩v : V ∗ C → T (V ∗ A)

where ⟨V ⟩w denotes the composite \xymatrix{V ∗ C \ar[r]^{V ∗w} & V ∗ T A \ar[r]^{φ_{V,A}} & T (V ∗ A)} .

5. Local character.

E ⊢ u ∘ e_{i} ≡ v ∘ e_{i} : C_{i} → T A (i ∈ I) Local  ({ e_{i} : C_{i} → C }_{i∈I} jointly epi)

E ⊢ u ≡ v : C → T A

(Recall that a family of maps { e_{i} : C_{i} → C }_{i∈I} is said to be jointly epi if, for any f, g : C → X such that ∀_{i∈I} f ∘ e_{i} = g ∘ e_{i} : C_{i} → X, it follows that f = g.)

7.1. Remark. In the presence of coproducts and under the rule Ref, the rules Comp and Local are inter-derivable with the rules

E ⊢ u ≡ v : C → T ( ∐_{i∈I} B_{i}) E ⊢ u_{i} ≡ v_{i} : B_{i} → T A (i ∈ I) Comp_{⨿}

E ⊢ u{[u_{i}]_{i∈I}} ≡ v{[v_{i}]_{i∈I}} : C → T A

and

E ⊢ u ∘ e ≡ v ∘ e : C′ → T A Local_{1}  (e : C′ [figure] C epi)

E ⊢ u ≡ v : C → T A

Soundness The minimal requirement for a deductive system to be of interest is that of soundness; i.e. that derivability entails validity.

We show that EML is sound for the model theory of MESs.

7.2. Theorem. For a MES S = (𝒱 , 𝒞 , 𝕋, E),

if E ⊢ u ≡ v : C → T A is derivable in EML then S-Alg ⊧ u ≡ v : C → T A .

Proof. One shows the soundness of each rule of EML; i.e. that every S-algebra satisfying the premises of an EML rule also satisfies its conclusion.

The soundness of the rules Ref, Sym, Trans, and Axiom is trivial.

For the rest of the proof, let \overline{f} : Z → [V, Y] denote the transpose of f : V ∗ Z → Y; so that \overline{⟦t⟧_{(X,s)}} = σ(s)_{A} ∘ t : C → [\underline{𝒞} (A, X), X] for all t : C → T A.

The soundness of the rule Comp is a consequence of the functoriality of σ(s)^{⋆} : 𝒞_{𝕋} → 𝒞_{𝕂_{X}} , see Remark 5.11, from which we have that

\overline{⟦w_{1}\{w_{2}\}⟧_{(X,s)}} = \overline{⟦w_{2}⟧_{(X,s)}} ∘_{𝒞_{𝕂_{X}}} \overline{⟦w_{1}⟧_{(X,s)}} : C → [\underline{𝒞} (A, X), X]

for all w_{1} : C → T B and w_{2} : B → T A in 𝒞.

The soundness of the rule Ext is a consequence of the commutativity of (9), from which we have that

\overline{⟦⟨V ⟩t⟧_{(X,s)}} = κV,A^{X} ∘ (V ∗ \overline{⟦t⟧_{(X,s)}}) : C → [\underline{𝒞} (A, X), X]

for all t : C → T A in 𝒞.

Finally, the soundness of the rule Local is a consequence of the fact that \overline{⟦t ∘ e⟧_{(X,s)}} = \overline{⟦t⟧_{(X,s)}} ∘ e.

8. Internal strong completeness

The completeness of EML, i.e. the converse to the soundness theorem, cannot be established at the abstract level of generality that we are working in. We do however have an internal form of strong completeness for Monadic Equational Systems admitting free algebras. The main development of this section is to state and prove this result.

The internal strong completeness theorem in conjunction with the construction of free algebras provides a main mathematical tool for establishing the completeness of concrete instantiations of EML, see [Fiore and Hur (2011), Part II] and [Fiore and Hur (2010)].

8.1. Notation. For a MES S = (𝒱 , 𝒞 , 𝕋, E) admitting free algebras, write (T_{S}X, τ_{X}^{S} : T T_{S}X → T_{S}X) for the free S-algebra on an object X ∈ 𝒞.

Then, the family τ^{S} = { τ_{X}^{S} }_{X∈𝒞} yields a natural transformation τ^{S} : T T_{S} → T_{S}.

Quotient maps Let S be a MES admitting free algebras. The universal property of free 𝕋-algebras induces a family of morphisms q^{S} = { q_{X}^{S} : T X → T_{S}X }_{X∈𝒞} , referred to as the quotient maps of S, defined as the unique homomorphic extensions (T X, μ_{X}) → (T_{S}X, τ_{X}^{S}) of η_{X}^{S}; i.e. the unique maps such that the diagram

\xymatrix{T T X \ar[r]^{T (q_{X}^{S})} \ar[d]_{μ_{X}} & T T_{S}X \ar[d]^{τ_{X}^{S}} \\ T X \ar[r]^{∃! q_{X}^{S}} & T_{S}X \\ X \ar[u]^{η_{X}} \ar[ur]_{η_{X}^{S}}}  (10)

commutes. As a general 2-categorical fact, the family { q_{X}^{S} }_{X∈𝒞} yields a monad morphism q^{S} : 𝕋 → 𝕋_{S}. By Theorem 5.14, the free S-algebra monad 𝕋_{S} is strong, and we proceed to show that so is the monad morphism q^{S}.

8.2. Theorem. For a MES S = (𝒱 , 𝒞 , 𝕋, E), the monad morphism q^{S} : T → T_{S} is strong.

Proof. The result follows from Theorem 4.4 (1) applied in the case 𝒜 = 𝒞^{𝕋} by virtue of Lemma 4.2, showing that the composites

\xymatrix{V ∗ T X \ar[r]^{φ_{V,X}} & T (V ∗ X) \ar[r]^{q_{V ∗X}^{S}} & T_{S}(V ∗ X)}

and

\xymatrix{V ∗ T X \ar[r]^{V ∗q_{X}^{S}} & V ∗ T_{S}X \ar[r]^{φ_{V,X}^{S}} & T_{S}(V ∗ X)}

are the unique extension of η_{V ∗X}^{S} : V ∗ X → T_{S}(V ∗ X).

8.3. Proposition. For a MES S admitting free algebras, the quotient maps q_{X}^{S} factor as

\xymatrix{T X \ar[r]^{(\underline{λ}_{T X})^{−1}} & I ∗ T X \ar[r]^{n_{X}∗T X} & \underline{𝒞} (X, T_{S}X) ∗ T X \ar[r]^{ι(τ_{X}^{S})} & X}

where n_{X} is the transpose of \xymatrix{I ∗ X \ar[r]^{^{\underline{λ}^{X}}} & X \ar[r]^{η_{X}^{S}} & T_{S}X} .

Proof. Noting that q_{X}^{S} factors as τ_{X}^{S} ∘ T (η_{X}^{S}), since this map is also an homomorphic extension (T X, μ_{X}) → (T_{S}X, τ_{X}^{S}) of η_{X}^{S}, one calculates as follows

\xymatrix{ & T X \ar[dl]_{(\underline{λ}_{T X})^{−1}} \ar[r]^{q_{X}^{S}} \ar[dr]_{T (η_{X}^{S})} \ar[d]^{T ((\underline{λ}_{X})^{−1})} & T_{S}X \\ I ∗ T X \ar[r]^{φ_{I,X}} \ar[dr]_{n_{X}∗T X} & T (I ∗ X) \ar[dr]^{T (n_{X}∗X)} & T T_{S}X \ar[u]_{τ_{X}^{S}} \\  & \underline{𝒞} (X, T_{S}X) ∗ T X \ar[r]_{φ_{\underline{𝒞} (X,T_{S} X),X}} & T (\underline{𝒞} (X, T_{S}X) ∗ X) \ar[u]_{T (\underline{ε}_{T_{S} X}^{X})}}

8.4. Definition. Let S be a MES admitting free algebras. For an S-algebra s : T X → X, let s̃: T_{S}X → X be the unique homomorphic extension (T_{S}X, τ_{X}^{S}) → (X, s) of the identity on X, so that

\xymatrix{T T_{S}X \ar[r]^{T (s̃)} \ar[d]_{τ_{X}^{S}} & T X \ar[d]^{s} \\ T_{S}X \ar[r]^{∃! s̃} & X \\ X \ar[u]^{η_{X}^{S}} \ar[ur]_{_{id_{X}}}}

8.5. Proposition. For a MES S admitting free algebras, every S-algebra s : T X → X factors as the composite

\xymatrix{T X \ar[r]^{q_{X}^{S}} & T_{S}X \ar[r]^{s̃} & X .}

Proof. As both morphisms are the unique homomorphic extension (T X, μ_{X}) → (X, s) of id_{X}.

Internal strong completeness The main result of the section [Fiore and Hur (2008), Hur (2010)] follows.

8.6. Theorem. For a MES S = (𝒱 , 𝒞 , 𝕋, E) admitting free algebras, the following are equivalent.

1. S-Alg ⊧ u ≡ v : C → T A.

2. (T_{S}A, τ_{A}^{S}) ⊧ u ≡ v : C → T A.

3. q_{A}^{S} ∘ u = q_{A}^{S} ∘ v : C → T_{S}A.

Here, the equivalence of the first two statements is an internal form of so-called strong completeness, stating that an equation is satisfied by all models if and only if it is satisfied by a freely generated one.

Proof. (1) ⇒ (2). Holds vacuously.

(2) ⇒ (3). Because q_{A}^{S} ∘t = ⟦t⟧_{(T_{S}A,τ_{A}^{S})} ∘(n_{A} ∗C)∘(\underline{λ}_{C})^{−1} for all t : C → T A, as follows from Proposition 8.3.

(3) ⇒ (1). Because ⟦t⟧_{(X,s)} = ⟦q_{A}^{S} ∘ t⟧_{(X,s̃)} for all t : C → T A, as follows from the identity

ι(s)_{A} = ι(s̃∘ q_{X}^{S})_{A}  , by Proposition 8.5
= ι(s̃)_{A} ∘ (\underline{𝒞} (A, X) ∗ q_{A}^{S}) , by Proposition 5.4

References

J. Adámek, M. Hébert and L. Sousa. A logic of injectivity. Journal of Homotopy and Related Topics, 2:13–47, 2007.

J. Adámek and J. Rosický. Locally presentable and accessible categories. Cambridge University Press, 1994.

J. Adámek, J. Rosický and E. Vitale. Algebraic theories: A categorical introduction to general algebra. Cambridge University Press, 2010.

J. Adámek, M. Sobral and L. Sousa. A logic of implications in algebra and coalgebra. Algebra Universalis, 61:313–337, 2009.

G. Birkhoff. On the structure of abstract algebras. Mathematical Proceedings of the Cambridge Philosophical Society, 31(4):433–454, 1935.

F. Borceux and B. Day. Universal algebra in a closed category. Journal of Pure and Applied Algebra, 16:133–147, 1980.

A. Burroni. T -catégories (Catégories dans un triple). Cahiers de Topologie et Géométrie Différentielle, XII(3):245–321, 1971.

P. Cohn. Universal algebra. Harper & Row, 1965.

B. Day. On closed categories of functors. Reports of the Midwest Category Seminar IV, volume 137 of Lecture Notes in Mathematics, pages 1–38. Springer-Verlag, 1970.

C. Ehresmann. Esquisses et types des structures algébriques. Bul. Inst. Polit. Iasi, XIV, 1968.

M. Fiore, G. Plotkin and D. Turi. Abstract syntax and variable binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS’99), pages 193–202. IEEE, Computer Society Press, 1999.

M. Fiore. Second-order and dependently-sorted abstract syntax. In Logic in Computer Science Conf. (LICS’08), pages 57–68. IEEE, Computer Society Press, 2008.

M. Fiore, N. Gambino, M. Hyland, and G. Winskel. The cartesian closed bicategory of generalised species of structures. J. London Math. Soc., 77:203-220, 2008.

M. Fiore and C.-K. Hur. Term equational systems and logics. In Proceedings of the Twenty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS’08), volume 218 of Electronic Notes in Theoretical Computer Science, pages 171–192. Elsevier, 2008.

M. Fiore and C.-K. Hur. On the construction of free algebras for equational systems. Theoretical Computer Science, 410(18):1704–1729, 2009.

M. Fiore and C.-K. Hur. Second-order equational logic. In Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010), volume 6247 of Lecture Notes in Computer Science, pages 320–335. Springer-Verlag, 2010.

M. Fiore and C.-K. Hur. On the mathematical synthesis of equational logics. Logical Methods in Computer Science, 7(3:12), 2011.

M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS 2010), volume 6281 of Lecture Notes in Computer Science, pages 368–380. Springer-Verlag, 2010.

M. J. Gabbay and A. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13:341–363, 2001.

M. Hamana. Free Σ-monoids: A higher-order syntax with metavariables. In Second ASIAN Symposium on Programming Languages and Systems (APLAS 2004), volume 3302 of Lecture Notes in Computer Science, pages 348–363, 2004.

C.-K. Hur. Categorical equational systems: Algebraic models and equational reasoning. PhD thesis, Computer Laboratory, University of Cambridge, 2010.

M. Hyland and A. J. Power. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science, 172:437–458, 2007.

G. Im and G. M. Kelly. A universal property of the convolution monoidal structure. Journal of Pure and Applied Algebra, 43:75–88, 1986.

G. Janelidze and G. M. Kelly. A note on actions of a monoidal category. Theory and Applications of Categories, 9(4):61–91, 2001.

A. Joyal. Une theorie combinatoire des séries formelles. Advances in Mathematics, 42:1–82, G. M. Kelly. On the operads of J. P. May. Unpublished manuscript, 1972. (Reprints in

Theory and Applications of Categories, No. 13, pages 1–13, 2005.)

G. M. Kelly and A. J. Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 89:163–179, 1993.

A. Kock. On double dualization monads. Math. Scand., 27:151–165, 1970.

A. Kock. Monads on symmetric monoidal closed categories. Archiv der Mathematik, XXI:1–10, 1970.

A. Kock. Strong functors and monoidal monads. Archiv der Math., XXIII:113–120, 1972.

A. Kock. Commutative monads as a theory of distributions. Theory and Applications of Categories, 26(4):97–131, 2012.

S. Lack and A. J. Power. Gabriel-Ulmer duality and Lawvere theories enriched over a general base. J. Funct. Programming, 19(3–4):265–286, 2009.

S. Lack and J. Rosický. Notions of Lawvere theory. Appl. Categor. Struct., 19:363–391, 2011.

F. W. Lawvere. Functorial semantics of algebraic theories. PhD thesis, Columbia University, 1963. (Republished in Reprints in Theory and Applications of Categories, 5:1–121, 2004.)

F. Linton. Some aspects of equational theories. Proc. Conf. on Categorical Algebra at La Jolla, pages 84–95, 1966.

S. Mac Lane. Categorical algebra. Bulletin of the American Mathematical Society 71(1):40–106, 1965.

S. Mac Lane. Categories for the working mathematician (second edition). Springer-Verlag, 1997.

S. Mac Lane and I. Moerdijk. Sheaves in geometry and logic. Springer-Verlag, 1992.

J. MacDonald and M. Sobral. Aspects of monads. Chapter 5 of Categorical Foundations: Special Topics in Order, Topology, Algebra, and Sheaf Theory. Cambridge University Press, 2004.

B. Pareigis. Non-additive ring and module theory II. 𝒞 -categories, 𝒞 -functors and 𝒞 -morphisms. Publicationes Mathematicae, 25:351–361, 1977.

M. C. Pedicchio and F. Rovatti. Algebraic categories. Chapter 6 of Categorical Foundations: Special Topics in Order, Topology, Algebra, and Sheaf Theory. Cambridge University Press, 2004.

A. J. Power. Enriched Lawvere theories. Theory and Applications of Categories, 6:83–93, 1999.

E. Robinson. Variations on algebra: Monadicity and generalisations of equational theories. Formal Aspects of Computing, 13(3–5):308–326, 2002.

G. Roşu. Complete categorical equational deduction. In Computer Science Logic, volume 2142 of Lecture Notes in Computer Science, pages 528–538. Springer-Verlag, 2001.

J. Słominski. The theory of abstract algebras with infinitary operations. Rozprawy Mat. 18, 1959.

M. Tanaka. Abstract syntax and variable binding for linear binders. In Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS’00), volume 1893 of Lecture Notes in Computer Science, pages 670–679. Springer-Verlag, 2000.

G. Wraith. Algebraic theories. Lecture Notes Series No. 22. Matematisk Institut, Aarhus Universitet, 1975.

University of Cambridge, Computer Laboratory, 15 JJ Thomson Avenue, Cambridge CB3 0FD, UK

Email: Marcelo.Fiore@cl.cam.ac.uk

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/27/18/27-18.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors

Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com

Valeria de Paiva: valeria.depaiva@gmail.com

Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Radboud University Nijmegen: i.moerdijk@math.ru.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Edinburgh: Alex.Simpson@ed.ac.uk James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca