Abstract

(This is a practice talk for an external seminar: feedback is very much appreciated!)

There have traditionally been two ways to reason about universal algebraic structure categorically: via algebraic theories, and via monads. It is well known that the two are tightly related: in particular, there is a correspondence between algebraic theories and a class of monads on the category of sets.

Motivated by the study of simple type theories, Fiore and Mahmoud introduced second-order algebraic theories, which extend classical (first-order) algebraic theories by variable-binding operators, such as the existential quantifier of first-order logic; the differential operators of analysis; and the lambda-abstraction operator of the unityped lambda-calculus. Fiore and Mahmoud established a correspondence between second-order algebraic theories and a second-order equational logic, but did not pursue a general understanding of the structure of the category of second-order algebraic theories. In particular, the possibility of a monad–theory correspondence for second-order algebraic theories was left as an open question.

In this talk, I will present a generalisation of algebraic theories to higher-order structure, in particular subsuming the second-order algebraic theories of Fiore and Mahmoud, and describe a universal property of the category of nth-order algebraic theories. The central result is a correspondence between (n+1)th-order algebraic theories and a class of relative monads on the category of nth-order algebraic theories, which extends to a monad correspondence subsuming that of the classical setting. Finally, I will discuss how the perspective lent by higher-order algebraic theories sheds new light on the classical monad–theory correspondence.

This is a report on joint work with Dylan McDermott.