Open Research Index

Sheaves as oracle computations

Danel Ahman, Andrej Bauer

arXivarxiv/2602.22135Feb 25, 2026math.LOscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2602.22135
curl -X POST /api/v1/records/arxiv/2602.22135/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2602.22135/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'