pith. sign in

arxiv: 2602.22135 · v2 · submitted 2026-02-25 · 🧮 math.LO · cs.LO

Sheaves as oracle computations

Danel Ahman , Andrej Bauer This is my paper

Pith reviewed 2026-05-15 19:09 UTC · model grok-4.3

classification 🧮 math.LO cs.LO
keywords oracle modalitypropositional containeradjoint retractionsheafificationcomputation treeLawvere-Tierney topologyrealizability topos
0
0 comments X

The pith

Every modality in type theory arises as the least oracle modality forcing some predicate.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that an oracle modality, defined from a predicate on queries, is exactly the least modality that forces the predicate to hold. It proves an adjoint retraction linking arbitrary modalities to propositional containers, which immediately yields that every modality is an oracle modality. This view turns suprema of modalities into easy computations when the modalities are presented as oracle ones. It further equips oracle modalities with a concrete description of their sheaves via quotient-inductive computation trees, where sheaves appear as algebras for the induced monad. Equifoliate trees supply an intensional layer that covers the sheaves, and the whole apparatus yields explicit descriptions of all Lawvere-Tierney topologies inside a realizability topos.

Core claim

An oracle modality is the least modality forcing a given predicate on oracle queries. An adjoint retraction exists between the poset of modalities and the poset of propositional containers; its unit and counit witness that every modality is an oracle modality. The left adjoint sends sums of modalities to their suprema, so suprema become computable from oracle presentations. Sheafification for an oracle modality is given by a quotient-inductive type of computation trees, and the sheaves are precisely the algebras for the associated monad. Equifoliate trees form a non-propositional intensional container whose quotient yields the sheaves and whose modal cover is the identity on them. This gives

What carries the argument

The adjoint retraction between modalities and propositional containers, with the left adjoint sending sums to suprema.

Load-bearing premise

The ambient type theory must contain modalities, propositional containers, and quotient-inductive types that define computation trees.

What would settle it

Exhibit a modality that is not the least one forcing any single predicate on queries.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper characterizes an oracle modality in type theory as the least modality forcing a given predicate on oracle queries. It proves an adjoint retraction between modalities and propositional containers, from which every modality is an oracle modality follows; the left adjoint sends sums to suprema. Sheafification for oracle modalities is described via a quotient-inductive type of computation trees, with sheaves as algebras for the induced monad. Equifoliate trees are introduced as an intensional (non-propositional) container for oracle computations that descend to sheaves and modally cover them. As an application, all Lawvere-Tierney topologies in a realizability topos receive a concrete description, related to Kihara's game-theoretic characterization.

Significance. If the adjoint retraction and the QIT-based monad constructions hold, the work supplies a constructive, computational account of modalities and sheaves that makes suprema of modalities computable when expressed via oracle modalities. The explicit description of sheafification and the link to realizability toposes strengthen connections between type theory, topos theory, and oracle computation, with potential for further applications in synthetic domain theory or realizability models. The use of quotient-inductive types for computation trees and the parameter-free universal-property characterizations are notable strengths.

minor comments (3)
  1. [equifoliate trees] The definition of equifoliate trees (introduced as a non-propositional container) would benefit from an explicit comparison to the propositional containers used in the adjoint retraction, ideally with a small diagram or example in the section introducing them.
  2. [adjoint retraction] The claim that the left adjoint maps sums to suprema is central to the computational utility; a short worked example (e.g., the supremum of two simple oracle modalities) would make this concrete without lengthening the paper.
  3. [application to realizability toposes] Ensure the bibliography includes the precise reference to Takayuki Kihara's game-theoretic characterization of Lawvere-Tierney topologies, and add a sentence clarifying how the new description differs from or refines it.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the manuscript, the assessment of its significance, and the recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper defines oracle modalities from predicates on queries and answers, then proves an adjoint retraction to propositional containers using the ambient type theory's modalities, propositional containers, and quotient-inductive types. The central results (every modality is an oracle modality, sheafification via computation trees, sheaves as monad algebras, and the Lawvere-Tierney application) follow directly from these definitions and the induced monad structures without any equation or construction reducing a claim to a fitted parameter, self-referential normalization, or load-bearing self-citation. External references (e.g., to Kihara) are non-essential to the core derivation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claims rest on standard type-theoretic background plus newly introduced notions of oracle modalities and equifoliate trees; no numerical parameters are fitted.

axioms (1)
  • domain assumption Type theory admits modalities, propositional containers, and quotient-inductive types
    Invoked throughout the abstract to define oracle modalities and computation trees.
invented entities (2)
  • Oracle modality no independent evidence
    purpose: Captures computational intuition of querying oracles step by step
    Defined as the least modality forcing the oracle predicate.
  • Equifoliate trees no independent evidence
    purpose: Provide intensional, non-propositional notion of oracle computation
    Introduced as a container that descends to sheaves.

pith-pipeline@v0.9.0 · 5520 in / 1355 out tokens · 51290 ms · 2026-05-15T19:09:31.502068+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

  1. [1]

    Demaine, Takehiro Ito, Jun Kawahara, Masashi Kiyomi, Yoshio Okamoto, Toshiki Saitoh, Akira Suzuki, Kei Uchizawa, and Takeaki Uno

    1 Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types.Theoretical Computer Science, 342(1):3–27, 2005.doi:10.1016/J.TCS. 2005.06.002. 2 Danel Ahman and Andrej Bauer. Comodule representations of second-order functionals. Journal of Logical and Algebraic Methods in Programming, 146:101071, 2025.doi:10...

    work page doi:10.1016/j.tcs 2005

  2. [2]

    16 Sheaves as oracle computations 5 Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot

    Association for Computing Machinery.doi:doi.org/10.1145/2914770.2837638. 16 Sheaves as oracle computations 5 Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the Pythia A Model of Continuity in a Dependent Setting. In Florin Manea and Alex Simpson, editors,30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216...

    work page doi:10.1145/2914770.2837638 2022

  3. [3]

    6 Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot

    Schloss Dagstuhl – Leibniz-Zentrum für Informatik.doi:10.4230/LIPIcs.CSL.2022.5. 6 Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. In Cantor Space No One Can Hear You Stream. In35th European Symposium on Programming (ESOP 2026), Turin, Italy,

    work page doi:10.4230/lipics.csl.2022.5 2022

  4. [4]

    8 Andrej Bauer

    doi:10.1007/BF01111838. 8 Andrej Bauer. Instance reducibility and Weihrauch degrees.Logical Methods in Computer Science, 18(3), 2022.doi:10.46298/LMCS-18(3:20)2022. 9E. Bishop.Foundations of Constructive Analysis. McGraw-Hill,

    work page doi:10.1007/bf01111838 2022

  5. [5]

    Weihrauch degrees, omniscience principles and weak com- putability.The Journal of Symbolic Logic, 76(1):143–176, 2011.doi:10.2178/jsl/1294170993

    10 Vasco Brattka and Guido Gherardi. Weihrauch degrees, omniscience principles and weak com- putability.The Journal of Symbolic Logic, 76(1):143–176, 2011.doi:10.2178/jsl/1294170993. 11 Thierry Coquand, Fabian Ruch, and Christian Sattler. Constructive sheaf models of type theory.Mathematical Structures in Computer Science, 31(9):979–1002, 2021.doi:10.1017...

    work page doi:10.2178/jsl/1294170993 2011

  6. [6]

    doi:10.1016/j.entcs.2018.03.019

    The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII). doi:10.1016/j.entcs.2018.03.019. 13 Martín H. Escardó. Joins in the frame of nuclei.Applied Categorical Structures, 11:117–124, April 2003.doi:10.1023/A:1023555514029. 14 Marcelo P. Fiore, Andrew M. Pitts, and S. C. Steenkamp. Quotients, inductive types, an...

    work page doi:10.1016/j.entcs.2018.03.019 2018

  7. [7]

    15 NicolaGambinoandJoachimKock

    doi: 10.46298/lmcs-18(2:15)2022. 15 NicolaGambinoandJoachimKock. Polynomialfunctorsandpolynomialmonads.Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013.doi:10.1017/ S0305004112000394. 16 J.M.E. Hyland. The effective topos. In A.S. Troelstra and D. van Dalen, editors,The L. E. J. Brouwer Centenary Symposium, volume 110 ...

    work page doi:10.46298/lmcs-18(2:15)2022 2022

  8. [8]

    Lawvere-

    18 Takayuki Kihara. Lawvere-tierney topologies for computability theorists.Transactions of the American Mathematical Society Series B, 10:48–85, January 2023.doi:10.1090/btran/134. 19 S. C. Kleene. Recursive predicates and quantifiers.Transactions of the American Mathematical Society, 53:41–73, 1943.doi:10.2307/1990131. 20 Saunders Mac Lane and Ieke Moerd...

    work page doi:10.1090/btran/134 2023

  9. [9]

    Type theories, toposes and constructive set theory: predicative aspects of ast.Annals of Pure and Applied Logic, 114(1):155–201, 2002.doi: 10.1016/S0168-0072(01)00079-3

    22 Ieke Moerdijk and Erik Palmgren. Type theories, toposes and constructive set theory: predicative aspects of ast.Annals of Pure and Applied Logic, 114(1):155–201, 2002.doi: 10.1016/S0168-0072(01)00079-3. 23 Nelson Niu and David I. Spivak.Polynomial Functors: A Mathematical Theory of Interaction. Topos Institute,

    work page doi:10.1016/s0168-0072(01)00079-3 2002

  10. [10]

    25 Christine Paulin-Mohring

    doi:10.1002/malq.19970430304. 25 Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. In Bruno Woltzenlogel Paleo and David Delahaye, editors,All about Proofs, Proofs for All, D. Ahman and A. Bauer 17 volume 55 ofStudies in Logic (Mathematical logic and foundations). College Publications, January

    work page doi:10.1002/malq.19970430304

  11. [11]

    Springer, 2002.doi:10.1007/3-540-45931-6 _24

    Grenoble, France, April 8–12, 2002, Proceedings, volume 2303 ofLecture Notes in Computer Science, pages 342–356. Springer, 2002.doi:10.1007/3-540-45931-6 _24. 27 Kevin Quirin and Nicolas Tabareau. Lawvere-Tierney sheafification in Homotopy Type Theory. Journal of Formalized Reasoning, 9(2):131–161, January 2016.doi:10.6092/issn.1972-5787/

    work page doi:10.1007/3-540-45931-6 2002

  12. [12]

    Modalities in homotopy type theory

    28 Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory.Logical Methods in Computer Science, 16, January 2020.doi:10.23638/LMCS-16(1:2)2020. 29 Andrew W. Swan. Oracle modalities. Preprint arXiv:2406.05818, June 2024.doi:10.48550/ arXiv.2406.05818. 30 A. Tarski. A lattice-theoretical fixpoint theorem and its applications.Paci...

    work page doi:10.23638/lmcs-16(1:2)2020 2020

  13. [13]

    A proof of the associated sheaf theorem by means of categorical logic.The Journal of Symbolic Logic, 46(1):44–55, March 1981.doi:10.2307/2273255

    33 Barbara Veit. A proof of the associated sheaf theorem by means of categorical logic.The Journal of Symbolic Logic, 46(1):44–55, March 1981.doi:10.2307/2273255. 34 Chuangjie Xu and Martín Escardó. A constructive model of uniform continuity. InTyped Lambda Calculi and Applications (TLCA), volume 7941 ofLecture Notes in Computer Science, pages 236–249. Sp...

    work page doi:10.2307/2273255 1981