In type theory, an oracle may be specified abstractly by a predicate whose domain is the type of queries asked of the oracle, and whose proofs are the oracle answers. Such a specification induces an oracle modality that captures a computational intuition about oracles: at each step of reasoning we either know the result, or we ask the oracle a query and proceed upon receiving an answer. We characterize an oracle modality as the least one forcing the given predicate. We establish an adjoint retraction between modalities and propositional containers, from which it follows that every modality is an oracle modality. The left adjoint maps sums to suprema, which makes suprema of modalities easy to compute when they are given in terms of oracle modalities. We also study sheaves for oracle modalities. We describe sheafification in terms of a quotient-inductive type of computation trees, and describe sheaves as algebras for the corresponding monad. We also introduce equifoliate trees, an intensional notion of oracle computation given by a (non-propositional) container. Equifoliate trees descend to sheaves, and lift from sheaves in case the container is projective. As an application, we give a concrete description of all Lawvere-Tierney topologies in a realizability topos, closely related to a game-theoretic characterization by Takayuki Kihara.

翻译：在类型论中，预言机可以通过一个谓词抽象地指定，其定义域是向预言机提出的查询类型，而其证明则是预言机的回答。这种规范会导出一个预言机模态，它捕捉了关于预言机的计算直觉：在推理的每一步，我们要么知道结果，要么向预言机提出查询并在收到回答后继续。我们将预言机模态刻画为强制给定谓词的最小模态。我们在模态与命题容器之间建立了一个伴随收缩，由此得出每个模态都是一个预言机模态。左伴随将和映射为上确界，这使得当模态以预言机模态的形式给出时，其上确界易于计算。我们还研究了预言机模态的层。我们通过计算树的商归纳类型描述了层化过程，并将层描述为相应单子的代数。我们还引入了等叶树，这是一种由（非命题）容器给出的预言机计算的内涵概念。等叶树可下降到层，并在容器是投射的情况下可从层提升。作为一个应用，我们在可实现性拓扑中给出了所有Lawvere-Tierney拓扑的具体描述，这与Takayuki Kihara提出的博弈论刻画密切相关。