Universal algebra uniformly captures various algebraic structures, by expressing them as equational theories or abstract clones. The ubiquity of algebraic structures in mathematics and related fields has given rise to several variants of universal algebra, such as theories of symmetric operads, non-symmetric operads, generalised operads, PROPs, PROs, and monads. These variants of universal algebra are called notions of algebraic theory. In this paper, we develop a unified framework for them. The key observation is that each notion of algebraic theory can be identified with a monoidal category, in such a way that algebraic theories correspond to monoid objects therein. To incorporate semantics, we introduce a categorical structure called metamodel, which formalises a definition of models of algebraic theories. We also define morphisms between notions of algebraic theory, which are a monoidal version of profunctors. Every strong monoidal functor gives rise to an adjoint pair of such morphisms, and provides a uniform method to establish isomorphisms between categories of models in different notions of algebraic theory. A general structure-semantics adjointness result and a double categorical universal property of categories of models are also shown.
The papers by Curien @cite_6 and Hyland @cite_15 concentrate on clones, symmetric operads and non-symmetric operads, and concern primarily the conceptual understanding of the substitution monoidal structures. Via the theory of pseudo-distributive laws @cite_19 , they reduce substitution monoidal structures to certain 2-monads on @math , for example the free cartesian category 2-monad in the case of clones. Their work illuminates the relationship between the notions of algebraic theory they treat and their standard metamodels, because the standard metamodels arise as Eilenberg--Moore algebras of the 2-monad from which the corresponding substitution monoidal structure is induced. On the other hand, monads and generalised operads do not seem to be captured by their framework.
@cite_19 @cite_15 @cite_6
2040355822 1989039217
We give a general category theoretic formulation of the substitution structure underlying the category theoretic study of variable binding proposed by Fiore, Plotkin, and Turi. This general formulation provides the foundation for their work on variable binding, as well as Tanaka's linear variable binding and variable binding for other binders and for mixtures of binders as for instance in the Logic of Bunched Implications. The key structure developed by was a substitution monoidal structure, from which their formulation of binding was derived; so we give an abstract formulation of a substitution monoidal structure, then, at that level of generality, derive the various category theoretic structures they considered. The central construction we use is that of a pseudo-distributive law between 2-monads on Cat, which suffices to induce a pseudo-monad on Cat, and hence a substitution monoidal structure on the free object on 1. We routinely generalise that construction to account for types. We study Kan extensions in three weakenings of the Eilenberg-Moore dou- ble category associated to a double monad, that was introduced by Grandis and Par e. To be precise, given a normal oplax double monad T on a double categoryK, we consider the double categories consisting of pseudo T -algebras, 'weak' vertical T -morphisms, hor- izontal T -morphisms and T -cells, where 'weak' means either 'lax', 'colax' or 'pseudo'. Denoting these double categories by Algw(T ), where w = l, c or ps accordingly, our main result gives, in each of these cases, conditions ensuring that (pointwise) Kan extensions can be lifted along the forgetful double functor Algw(T ) ! K. As an application we recover and generalise a result by Getzler, on the lifting of pointwise left Kan extensions along symmetric monoidal enriched functors. As an application of Getzler's result we prove, in suitable symmetric monoidal categories, the existence of bicommutative Hopf monoids that are freely generated by cocommutative comonoids. An algebraic left Kan extension is a left Kan extension which interacts well with the algebraic structure present in the given situation, and these appear in various subjects such as the homotopy theory of operads and in the study of conformal field theories. In the most interesting examples, the functor along which we left Kan extend goes between categories that enjoy universal properties which express the meaning of the calculation we are trying to understand. These universal properties say that the categories in question are universal examples of some categorical structure possessing some kind of internal structure, and so fall within the theory of internal algebra classifiers described in earlier work of the author. In this article conditions of a monad-theoretic nature are identified which give rise to morphisms between such universal objects, which satisfy the key condition of Guitart-exactness, which guarantees the algebraicness of left Kan extending along them. The resulting setting explains the algebraicness of the left Kan extensions arising in operad theory, for instance from the theory of Feynman categories of Kaufmann and Ward, generalisations thereof, and also includes the situations considered by Batanin and Berger in their work on the homotopy theory of algebras of polynomial monads.