BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Comodule representations of Second-order functionals - Andrej Baue
 r\, University of Ljubljana
DTSTART:20240501T090000Z
DTEND:20240501T100000Z
UID:TALK215896@talks.cam.ac.uk
CONTACT:Jon Sterling
DESCRIPTION:In information-theoretic terms\, a map is continuous when a fi
 nite amount of information about the input suffices for computing a finite
  amount of information about the output. Already Brouwer observed that thi
 s allows one to represent a continuous functional from sequences to number
 s with a certain well-founded question-answer tree. The idea has been exte
 nded to other kinds of second-order functionals\, such as stream transform
 ers\, continuous functionals on final coalgebras\, sequentially realizable
  functionals\, and others.\n\nIn type theory a second-order functional is 
 a map F : (∏(a : A)\, P a) → (∏(b : B) → Q b). Its continuity is o
 nce again witnessed by a well-founded tree whose nodes are “questions”
  a : A\, the branches are indexed by “answers” P a\, and the leaves ar
 e “results” Q b. Such tree representations can be expressed in purely 
 category-theoretic terms\, using the notion of right T-comodules for the m
 onad T of well-founded trees on the category of containers. Doing so expos
 es a rich underlying structure\, and immediately suggests generalizations:
  any right T-comodule for any monad T on containers gives rise to a repres
 entation theorem for second-order functionals. We give several examples of
  these.\n\nJoint work with Danel Ahman\, University of Tartu\, https://dan
 el.ahman.ee/
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR