BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Danel Ahman DTSTART:20260409T170000Z DTEND:20260409T180000Z DTSTAMP:20260423T145347Z UID:ToposInstituteColloquium/209 DESCRIPTION:Title: Containers and Comodule Representations of Second-Order Functionals\nby Danel Ahman as part of Topos Institute Colloquium\n\n \nAbstract\nIn information-theoretic terms\, a map is continuous when a fi nite\namount of information about its input suffices for computing a finit e\namount of information about its output. Already Brouwer observed that\n this allows one to represent a continuous functional from sequences to\nnu mbers with a certain well-founded question-answer tree.\n\nIn type theory\ , a second-order functional is a (dependently typed) map\n\nF : (∏(a : A ) . P a) → (∏(b : B) . Q b).\n\nIts continuity is once again witnessed by B-many well-founded trees\nwhose nodes are “questions” a : A\, the branches are indexed by\n“answers” p : P a\, and the leaves are “re sults” Q b. In this work\, we\nobserve that such tree representations ca n be expressed in purely\ncategory-theoretic terms\, using the notion of r ight T-comodules for\nthe monad T of well-founded trees on the category of containers. A\ntree representation for F is then just a Kleisli map for t he monad T.\n\nDoing so exposes a rich underlying structure\, and immediat ely suggests\ngeneralisations: any right T-comodule for any monad T on con tainers\ngives rise to a corresponding representation theorem for second-o rder\nfunctionals. We give several examples of these\, ranging from finite ly\nsupported functionals\, to functionals that can query their input just \nonce (or sometimes not at all)\, to functionals that can additionally\ni nteract with their environment\, to partial functionals\, to observing\nth at any functional can be trivially represented by itself.\n\nThis is joint work with Andrej Bauer from the University of Ljubljana.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/209/ END:VEVENT END:VCALENDAR