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 modally cover them. 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的博弈论刻画密切相关。