Comparing the existing formulations of universal algebra and their levels of generality

Question

I am a newcomer to universal algebra and I just read this (very good, IMO) book on the topic:

Adámek, J., Rosický, J., & Vitale, E. M. (2010). Algebraic theories: a categorical introduction to general algebra (Vol. 184). Cambridge University Press.

The authors most notably treat the case of 1-sorted first-order finitary Lawvere theories (equivalently: finitary monads). This is, as I understand it, the most common level of generality appearing in the literature to deal with (categorical) universal algebra.

Additionally the authors explain the relation between "old-fashioned" universal algebra -- which we'll call equational theories here -- and Lawvere theories, as well as the relation between Lawvere theories and categories of models of Lawvere theories. The quick and informal upshot is that there is a pair of such adjunctions: old universal algebra, lawvere thies, models Where $\mathrm{EqTh}$ is the category of equational theories (that is: signatures + equations), $\mathrm{AlgTh}$ is the category of Lawvere theories, $\mathrm{AlgCat}$ is the category of algebraic categories. Algebraic categories are basically defined to be categories of models of Lawvere theories. The first adjunction connects particular presentations of theories to Lawvere theories. The second adjunction is some kind of Gabriel-Ulmer duality and links theories to their models.

My questions is: what are the existing ways we can generalize this picture? And is there an ultimate framework encompassing all those generalizations? For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Some examples of generalisations (either on the presentation side or on the Lawvere theory side or on both sides): higher-order logic, enriched Lawvere theories, sketches, Makkai's first order logic dependent sorts (FOLDS), infinitary theories. I'm sure there are a lot more!

EDIT: Here is a paper about higher order algebraic theories

Answer 1

There are many satisfying answers, but not a single satisfying answer. I'll just drop a bunch of relevant literature without much explanation, and without much specific context; I'll maybe come back later for adjustments. Better than nothing, I hope!

• https://arxiv.org/abs/1904.08541
• https://arxiv.org/abs/1805.04346 (this is in a very precise sense the sharpest monad-theory correspondence one can get, by construction; yet, the notion of "theory" is quite general: no assumption on $\cal A$.)
• https://arxiv.org/abs/1112.3076 the upshot: if a Lawvere theory is a finitary monad, what's a distributive law between monads in terms of the associated identity on object functors /slash/ promonads? Answer: a certain type of factorisation system on the theory/category associated to the composite monad.
• https://arxiv.org/abs/0907.2460 Example 4.17, and below that for the multisorted version.
• https://arxiv.org/abs/1511.02920 (if you ask me, this is the sharpest one can go while keeping at least some of the essential features of what an "algebraic theory" shall be)
• https://arxiv.org/abs/1307.2963 (if you ask me, this is a brilliant characterisation of Lawvere theories as categories enriched over $[{\sf Fin,Set}]$).
• https://arxiv.org/abs/1507.08710 see section 5, and below, where the authors a neat conceptual criterion for when an algebraic theory is the tensor product of two given ones.

The implicit starting point of all these different development deserves at least a word of explanation.

The idea is more or less the following: let's say that a "Lawvere theory" is an identity-on-object functor ${\sf Fin}^o \to L$, where $\sf Fin$ is the category of finite sets and functions. These functors form a category, the category $\sf Law$ of Lawvere theories, of which a brilliant survey is this paper by Hyland and Power https://www.sciencedirect.com/science/article/pii/S1571066107000874

Then there is an equivalence of categories between

1. The category $\sf Law$ defined as above.
2. The category of promonads on the object $\sf Fin$, regarded as an object of the bicategory $\sf Prof$ of profunctors
3. The category of finitary monads on $\sf Set$ (all sets, and functions)
4. The category of "convolution monoidal cocontinuous" monads on $[{\sf Fin,Set}]$, i.e. monads $T : [{\sf Fin,Set}] \to [{\sf Fin,Set}]$ that are colimit preserving and monoidal functors with respect to Day convolution
5. The category of "clones" (also called, "cartesian operads"), i.e. monoids with respect to a certain monoidal structure on $[{\sf Fin,Set}]$ called "substitution product".
6. The category of relative monads in the (skew)monoidal category $[{\sf Fin,Set}]$.

Here we're in the same situation of the famous parable of the elephant and the blind men: various approaches have tried to generalise, to various extents, each of these different perspectives on the notion of Lawvere theory. Some of them work better when changing the base of enrichment; some others work better when you try to internalise the notion of algebraic theory (surprisingly, the first notion of internal algebraic theory was given taking 2 as primary definition, in a brilliant paper by Johnstone and Wraith https://link.springer.com/chapter/10.1007%2FBFb0061363 ), some other work best when your abstract setting for CT is double categorical, some others are exquisitely combinatorial.

Another possible generalisation is the following (of which I know no single, comprehensive reference): $\sf Fin$ is the free category with finite coproducts over the point, and dually ${\sf Fin}^o$ is the free category with products over the point. so, call ${\sf Fin} = P1$ and replace $\sf Fin$, above, with another category $D1$, the free category with $D$-structure over the point, where $D$ s just another 2-monad on $\sf Cat$ (for example, completion under other shapes of colimits). Which parts of the correspondence above break down?

Do all these different approaches converge in a truly comprehensive, unified framework? I don't know! I would say some people do, but...

Answer 2

fosco gives a good overview of the general theory in their answer. I would like to point out two different generalisations of algebraic theory that are not, as far as I am aware, subsumed by any of these, but are relevant to your comment:

For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Simple type theories may be described as algebraic structures with multisorted binding operators and algebraic sort structure. A step in this direction, from the perspective of algebraic theories, is taken by Fiore and Mahmoud in Second-Order Algebraic Theories. They consider a generalisation of algebraic theory in which one considers categories with finite products and an exponentiable object. The exponentiable object permits the representation of second-order operators, like the $\lambda$-abstraction operator from the simply-typed $\lambda$-calculus. They only consider the single-sorted setting, but it is easy enough to extend to the multisorted setting. The equivalence with an equational logic is contained in Fiore and Hur's Second-Order Equational Logic.

For type operators (including type operators with binding, as are found in the polymorphic $\lambda$-calculus), an operadic/presheaf-theoretic approach is contained in Fiore and Hamana's Multiversal Polymorphic Algebraic Theories, which also contains the equivalence with an equational logic.

For substructural type theories, one starting point is the work of Power and Tanaka, such as Pseudo-distributive laws and axiomatics for variable binding, which is also based on the operadic/presheaf-theoretic approach.

Representing other kinds of type theory in this way, such as dependent type theories, is mostly an open question. (By "type theory", I mean at least some structure with a notion of variable binding operator.)

Answer 3

@focso’s answer and @varkor’s answer give excellent answers covering most aspects of your question. I’ll just add a little more on extending these frameworks to cover “type theories” — i.e. to include both sort-dependence and variable binding. This is a quite new and open topic, but a good bit of groundwork has been laid.

The well-established part dates back to the 80’s, starting with Cartmell’s work. This defines contextual categories, and later various slight variants (categories with attributes (CwA’s), categories with families (CwF’s)…) corresponding to a so-called “generalised algebraic theory” or “dependent algebraic theory”. This gives a nice treatment of dependent sorts, but not yet of variable binding. Specific type theories with binders then correspond to extra algebraic structure on contextual categories (or CwA’s, CwF’s, etc). A good introduction is Martin Hofmann’s chapter Syntax and semantics of dependent types, doi:10.1007/978-1-4471-0963-1_2, un-paywalled pdf here.

For individual type theories, this correspondence works satisfactorily (and has been developed by many authors — I won’t try to give a bibliography here); but until quite recently, it wasn’t generalised to a general notion of “type theory”. Approaches to that so far include:

• Isaev, Algebraic Presentations of Dependent Type Theories, arXiv:1602.08504. This defines type theories directly as certain essentially-algebraic extensions of CwA’s.

• Uemura, A General Framework for the Semantics of Type Theory, arXiv:1904.04097. This in my opinion is the most powerful and best developed approach so far. It gives a categorical abstract definition of type theories as representable map categories (an imaginative and far-reaching generalisation of Fiore/Awodey’s re-analysis of CwF’s), and a corresponding syntactic treatment (based on the “logical framework” approach). It’s much more general than either of the other approaches I mention here, and very cleanly set up.

• Bauer–Lumsdaine–Haselwarter, A general definition of dependent type theories, arXiv:2009.05539. A syntactic definition of general type theories, taking variable binding seriously as primitive, and written with a categorical analysis strongly in mind (though not given in the paper). This should correspond to a slight variant of Isaev’s algebraic definition, and to a subclass of Uemura’s.

I very much hope that these and the connections between them will be developed further in the near future, and that this part of your question will have a better answer in five years than it does now!