Sheaves as oracle computations

TL;DR

This paper explores the concept of sheaves in the context of oracle computations within type theory, establishing a formal framework and analyzing their properties and applications.

Contribution

It introduces a novel characterization of oracle modalities, studies sheaves for these modalities, and connects them to Lawvere-Tierney topologies in realizability toposes.

Findings

Every modality is an oracle modality.

Sheafification described via computation trees.

All Lawvere-Tierney topologies characterized in a realizability topos.

Abstract

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.