BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Higher-order algebraic theories and relative monads - Nathanael Ar
 kor (University of Cambridge)
DTSTART:20210507T100000Z
DTEND:20210507T110000Z
UID:TALK160237@talks.cam.ac.uk
CONTACT:Nathanael Arkor
DESCRIPTION:(This is a practice talk for an external seminar: feedback is 
 very much appreciated!)\n\nThere have traditionally been two ways to reaso
 n about universal algebraic structure categorically: via algebraic theorie
 s\, and via monads. It is well known that the two are tightly related: in 
 particular\, there is a correspondence between algebraic theories and a cl
 ass of monads on the category of sets.\n\nMotivated by the study of simple
  type theories\, Fiore and Mahmoud introduced second-order algebraic theor
 ies\, which extend classical (first-order) algebraic theories by variable-
 binding operators\, such as the existential quantifier of first-order logi
 c\; the differential operators of analysis\; and the lambda-abstraction op
 erator of the unityped lambda-calculus. Fiore and Mahmoud established a co
 rrespondence between second-order algebraic theories and a second-order eq
 uational logic\, but did not pursue a general understanding of the structu
 re 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.\n\nIn this talk\, I will present a
  generalisation of algebraic theories to higher-order structure\, in parti
 cular 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 alg
 ebraic theories and a class of relative monads on the category of nth-orde
 r algebraic theories\, which extends to a monad correspondence subsuming t
 hat 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.\n\nThis is a report on joint work with Dyla
 n McDermott.
LOCATION:https://meet.google.com/jxy-edcv-wgx
END:VEVENT
END:VCALENDAR