We develop and investigate a general theory of representations of second-order functionals, based on a notion of a right comodule for a monad on the category of containers. We show how the notion of comodule representability naturally subsumes classic representations of continuous functionals with well-founded trees. We find other kinds of representations by varying the monad, the comodule, and in some cases the underlying category of containers. Examples include uniformly continuous or finitely supported functionals, functionals querying their arguments precisely once, or at most once, functionals interacting with an ambient environment through computational effects, as well as functionals trivially representing themselves. Many of these rely on our construction of a monad on containers from a monad on shapes and a weak Mendler-style monad algebra on the universe for positions. We show that comodule representability on the category of propositional containers, which have positions valued in a universe of propositions, is closely related to instance reducibility in constructive mathematics, and through it to Weihrauch reducibility in computability theory.

翻译：基于容器范畴上幺半群右余模的概念，我们发展并研究了一种二阶函子表示的一般理论。我们展示了余模可表示性如何自然地包含具有良基树的连续函子的经典表示。通过改变幺半群、余模，在某些情况下改变底层容器范畴，我们发现了其他类型的表示。示例包括一致连续或有限支持的函子、精确查询其参数一次或至多一次的函子、通过计算效应与环境交互的函子，以及平凡表示自身的函子。其中许多表示依赖于我们构造的容器幺半群，该构造基于形状上的幺半群以及位置宇宙上的弱Mendler风格幺半群代数。我们证明，在命题容器范畴（其位置值位于命题宇宙中）上的余模可表示性与构造数学中的实例可约性密切相关，并通过该联系与可计算性理论中的Weihrauch可约性相关联。