Journal of Functional Programming

Articles

Gabriel–Ulmer duality and Lawvere theories enriched over a general base

STEPHEN LACKa1 and JOHN POWERa2

a1 School of Computing and Mathematics, University of Western Sydney, Locked Bag 1797, Penrith South DC, NSW 1797, Australia (e-mail: s.lack@uws.edu.au)

a2 Department of Computer Science, University of Bath, Claverton Down, Bath BA2 7AY, UK (e-mail: a.j.power@bath.ac.uk)

Abstract

Motivated by the search for a body of mathematical theory to support the semantics of computational effects, we first recall the relationship between Lawvere theories and monads on Set. We generalise that relationship from Set to an arbitrary locally presentable category such as Poset and ωCpo or functor categories such as [Inj, Set] and [Inj, ωCpo]. That involves allowing the arities of Lawvere theories to be extended to being size-restricted objects of the locally presentable category. We develop a body of theory at this level of generality, in particular explaining how the relationship between generalised Lawvere theories and monads extends Gabriel–Ulmer duality.