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
Higherorder algebraic theories and relative monads
Abstract: 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 secondorder algebraic theories, which extend classical (firstorder) algebraic theories by variablebinding operators, such as the existential quantifier ∃x of firstorder logic; the differential operators d/dx analysis; and the λabstraction operator of the untyped λcalculus. Fiore and Mahmoud estab lished a correspondence between secondorder algebraic theories and a secondorder equational logic, but did not pursue a general understanding of the categorical structure of secondorder 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 higherorder structure, in particular subsuming the secondorder algebraic theories of Fiore and Mahmoud, and describe a universal property of the category of nthorder algebraic theories. The central result is a correspondence between (n + 1)thorder algebraic theories and a class of relative monads on the category of nthorder algebraic theories, which extends to a monad correspondence subsuming that of the classical setting. Finally, I will discuss how the perspective lent by higherorder algebraic theories sheds new light on the classical monad–theory correspondence.
This is a report on joint work with Dylan McDermott.
