Online algebra seminar - May 13th, 1pm Print

We will continue online on Thursday, May 13th, at 13.00 CEST on ZOOM platform (for information how to acces seminar and next programme visit this page) by the talk:

Nathanael Arkor

Higher-order algebraic theories and relative monads

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 ∃x of first-order logic; the differential operators d/dx analysis; and the λ-abstraction operator of the untyped λ-calculus. Fiore and Mahmoud estab- lished a correspondence between second-order algebraic theories and a second-order equational logic, but did not pursue a general understanding of the categorical structure 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.

Last Updated on Wednesday, 12 May 2021 15:57