BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic &\; Semantics for Dummies
SUMMARY:Higher-order algebraic theories and relative monad
s - Nathanael Arkor (University of Cambridge)
DTSTART;TZID=Europe/London:20210507T110000
DTEND;TZID=Europe/London:20210507T120000
UID:TALK160237AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/160237
DESCRIPTION:(This is a practice talk for an external seminar:
feedback is very much appreciated!)\n\nThere have
traditionally been two ways to reason about univer
sal algebraic structure categorically: via algebra
ic theories\, and via monads. It is well known tha
t the two are tightly related: in particular\, the
re is a correspondence between algebraic theories
and a class of monads on the category of sets.\n\n
Motivated by the study of simple type theories\, F
iore and Mahmoud introduced second-order algebraic
theories\, which extend classical (first-order) a
lgebraic theories by variable-binding operators\,
such as the existential quantifier of first-order
logic\; the differential operators of analysis\; a
nd the lambda-abstraction operator of the unityped
lambda-calculus. Fiore and Mahmoud established a
correspondence between second-order algebraic theo
ries and a second-order equational logic\, but did
not pursue a general understanding of the structu
re of the category of second-order algebraic theor
ies. In particular\, the possibility of a monadâ€“th
eory correspondence for second-order algebraic the
ories was left as an open question.\n\nIn this tal
k\, I will present a generalisation of algebraic t
heories to higher-order structure\, in particular
subsuming the second-order algebraic theories of F
iore and Mahmoud\, and describe a universal proper
ty 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 rel
ative monads on the category of nth-order algebrai
c theories\, which extends to a monad corresponden
ce subsuming that of the classical setting. Finall
y\, I will discuss how the perspective lent by hig
her-order algebraic theories sheds new light on th
e classical monadâ€“theory correspondence.\n\nThis i
s a report on joint work with Dylan McDermott.
LOCATION:https://meet.google.com/jxy-edcv-wgx
CONTACT:Nathanael Arkor
END:VEVENT
END:VCALENDAR