In information-theoretic terms, a map is continuous when a finite amount of information about the input suffices for computing a finite amount of information about the output. Already Brouwer observed that this allows one to represent a continuous functional from sequences to numbers with a certain well-founded question-answer tree. The idea has been extended to other kinds of second-order functionals, such as stream transformers, continuous functionals on final coalgebras, sequentially realizable functionals, and others.
In type theory a second-order functional is a map F : (∏(a : A), P a) → (∏(b : B) → Q b). Its continuity is once again witnessed by a well-founded tree whose nodes are “questions” a : A, the branches are indexed by “answers” P a, and the leaves are “results” Q b. Such tree representations can be expressed in purely category-theoretic terms, using the notion of right T-comodules for the monad T of well-founded trees on the category of containers. Doing so exposes a rich underlying structure, and immediately suggests generalizations: any right T-comodule for any monad T on containers gives rise to a representation theorem for second-order functionals. We give several examples of these.
Joint work with Danel Ahman, University of Tartu, https://danel.ahman.ee/
