pith. sign in

arxiv: 2505.08697 · v2 · submitted 2025-05-13 · 🧮 math.CT · math.LO

A topos for extended Weihrauch degrees

Samuele Maschio , Davide Trotta This is my paper

Pith reviewed 2026-05-22 15:36 UTC · model grok-4.3

classification 🧮 math.CT math.LO
keywords Weihrauch reducibilityextended Weihrauch degreestripostoposKleene-Vesley toposLawvere-Tierney topologyrealizability
0
0 comments X

The pith

The authors build a topos whose predicates are extended Weihrauch degrees and show the Kleene-Vesley topos arises as its sheaves for a Lawvere-Tierney topology.

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

This paper seeks to give a categorical account of extended Weihrauch reducibility, a notion that compares the uniform computational strength of problems. It constructs a new tripos in which the predicates directly encode these degrees and their reducibility relation. The standard tripos-to-topos construction is then applied to produce a topos that organizes the degrees. The work further proves that the Kleene-Vesley topos is recovered as the category of sheaves for a particular Lawvere-Tierney topology on this new topos. A sympathetic reader would care because the construction embeds the study of computational problems into the internal logic and geometry of a topos, potentially allowing transfer of methods between realizability and Weihrauch analysis.

Core claim

We present a tripos and a topos for extended Weihrauch degrees. We start by defining a new tripos, abstracting the notion of extended Weihrauch degrees, and then we apply the tripos-to-topos construction to obtain the desired topos. Then we show that the Kleene-Vesley topos is a topos of j-sheaves for a certain Lawvere-Tierney topology over the topos of extended Weihrauch degrees.

What carries the argument

The tripos whose predicates correspond to extended Weihrauch degrees; it encodes the reducibility preorder and serves as the input to the tripos-to-topos construction, after which a Lawvere-Tierney topology extracts the Kleene-Vesley topos as the sheaf subtopos.

Load-bearing premise

The standard definition of extended Weihrauch reducibility admits a direct abstraction into the structure of a tripos whose predicates correspond to degrees.

What would settle it

A concrete computational problem for which the proposed predicates fail to satisfy a tripos axiom such as the Beck-Chevalley condition for substitution, or an explicit counterexample showing that the Kleene-Vesley topos does not coincide with the j-sheaves for the stated topology.

read the original abstract

Weihrauch reducibility is a notion of reducibility between computational problems that is useful to calibrate the uniform computational strength of a multivalued function. It complements the analysis of mathematical theorems done in reverse mathematics, as multi-valued functions on represented spaces can be considered as realizers of theorems in a natural way. Despite the rich literature and the relevance of the applications of category theory in logic and realizability, actually there are just a few works starting to study the Weihrauch reducibility from a categorical point of view. The main purpose of this work is to provide a full categorical account to the notion of extended Weihrauch reducibility introduced by A. Bauer, which generalizes the original notion of Weihrauch reducibility. In particular, we present a tripos and a topos for extended Weihrauch degrees. We start by defining a new tripos, abstracting the notion of extended Weihrauch degrees, and then we apply the tripos-to-topos construction to obtain the desired topos. Then we show that the Kleene-Vesley topos is a topos of $j$-sheaves for a certain Lawvere-Tierney topology over the topos of extended Weihrauch degrees.

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

3 major / 2 minor

Summary. The paper constructs a tripos by abstracting the definition of extended Weihrauch reducibility (due to Bauer) on represented spaces and multivalued functions, applies the tripos-to-topos construction to obtain a topos whose objects and morphisms are intended to classify extended Weihrauch degrees, and proves that the Kleene-Vesley topos arises as the category of j-sheaves for a suitable Lawvere-Tierney topology j on this new topos.

Significance. If the central constructions are verified, the work supplies a topos-theoretic setting for extended Weihrauch degrees that could integrate uniform reducibility with realizability methods and permit categorical analysis of computational strength for theorems realized by multivalued functions. The explicit link to the Kleene-Vesley topos is a concrete bridge between Weihrauch analysis and existing realizability toposes.

major comments (3)
  1. [§3] §3 (Tripos construction): the definition of the indexed category and the entailment relation abstracts extended Weihrauch reducibility, but the manuscript does not explicitly verify the Beck-Chevalley condition for the universal quantifier when the predicates involve multi-valued functions; this condition is required for the structure to be a tripos and is load-bearing for the subsequent topos construction.
  2. [§4] §4 (Tripos-to-topos): the objects of the resulting topos are claimed to encode uniform computational strength via the degree ordering, yet the paper provides no explicit check that the subobject classifier and the internal logic preserve the exact reducibility relation without extra assumptions on the representations; a mismatch here would undermine the claim that the topos classifies precisely the extended Weihrauch degrees.
  3. [§5] §5 (Lawvere-Tierney topology and Kleene-Vesley): the proof that the Kleene-Vesley topos is the topos of j-sheaves relies on the correspondence between the topology j and the extended degrees, but no concrete example (e.g., for a specific multivalued function such as closed choice) is worked out to confirm that the sheaf condition matches the known properties of the Kleene-Vesley topos.
minor comments (2)
  1. [§2] Notation for the fibration or indexed category in §2 should be clarified to distinguish the base category of represented spaces from the fiber predicates.
  2. [Introduction] The abstract mentions 'a full categorical account' but the introduction does not cite the few existing categorical works on Weihrauch reducibility; adding these references would improve context.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the detailed and constructive report. We address each major comment in turn, indicating where we will revise the manuscript to strengthen the presentation and where we maintain that the existing arguments suffice.

read point-by-point responses

  1. Referee: [§3] §3 (Tripos construction): the definition of the indexed category and the entailment relation abstracts extended Weihrauch reducibility, but the manuscript does not explicitly verify the Beck-Chevalley condition for the universal quantifier when the predicates involve multi-valued functions; this condition is required for the structure to be a tripos and is load-bearing for the subsequent topos construction.

    Authors: We agree that an explicit verification strengthens the claim that the structure is a tripos. The entailment relation is defined directly by abstraction from extended Weihrauch reducibility on represented spaces, and the Beck-Chevalley condition follows from the stability of the representation of multi-valued functions under pullback along continuous maps. In the revised manuscript we will add a short lemma (with proof) confirming that the universal quantifier satisfies Beck-Chevalley for predicates involving multi-valued functions, using only the standard properties of represented spaces already assumed in the paper. revision: yes

  2. Referee: [§4] §4 (Tripos-to-topos): the objects of the resulting topos are claimed to encode uniform computational strength via the degree ordering, yet the paper provides no explicit check that the subobject classifier and the internal logic preserve the exact reducibility relation without extra assumptions on the representations; a mismatch here would undermine the claim that the topos classifies precisely the extended Weihrauch degrees.

    Authors: The tripos-to-topos construction guarantees that the subobject classifier and the internal logic of the topos are determined exactly by the entailment relation of the tripos. Because the tripos is defined so that its entailment coincides with extended Weihrauch reducibility, the degree ordering is preserved by construction. We will nevertheless insert an explicit proposition in §4 stating that, under the standing hypotheses on representations (continuous realizers and admissible representations), no additional assumptions are needed for the correspondence to hold exactly. revision: yes

  3. Referee: [§5] §5 (Lawvere-Tierney topology and Kleene-Vesley): the proof that the Kleene-Vesley topos is the topos of j-sheaves relies on the correspondence between the topology j and the extended degrees, but no concrete example (e.g., for a specific multivalued function such as closed choice) is worked out to confirm that the sheaf condition matches the known properties of the Kleene-Vesley topos.

    Authors: A concrete example would indeed make the correspondence more transparent. In the revised version we will add a worked example in §5 for the multivalued function of closed choice on the reals. We will verify that the sheaf condition for the associated Lawvere-Tierney topology j reproduces the known realizability interpretation of closed choice in the Kleene-Vesley topos, thereby confirming that the sheafification step aligns with the expected computational properties. revision: yes

Circularity Check

0 steps flagged

Tripos defined by direct abstraction of external Bauer definition; topos and sheaf relation follow from standard constructions without reduction to inputs.

full rationale

The paper starts from the external definition of extended Weihrauch reducibility (due to Bauer) and defines a new tripos by abstracting that notion, with predicates corresponding to degrees. It then applies the standard tripos-to-topos construction. The claim that the Kleene-Vesley topos is the topos of j-sheaves for a Lawvere-Tierney topology over this topos is presented as a derived result. No quoted step reduces a central claim to a self-definition, fitted parameter renamed as prediction, or load-bearing self-citation chain; the derivation is self-contained against the external reducibility notion and categorical machinery.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on the prior definition of extended Weihrauch reducibility and standard tripos and topos constructions; no free parameters or invented entities are visible from the abstract.

axioms (1)
  • domain assumption Extended Weihrauch reducibility forms a preorder that can be lifted to a tripos structure.
    Invoked when abstracting the degrees into the tripos.

pith-pipeline@v0.9.0 · 5749 in / 1172 out tokens · 25977 ms · 2026-05-22T15:36:21.542027+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages

  1. [1]

    Instance reducibility and Weihrauch degrees.Logical Meth- ods in Computer Science, 18(3):20:1–20:18, 2022

    Andrej Bauer. Instance reducibility and Weihrauch degrees.Logical Meth- ods in Computer Science, 18(3):20:1–20:18, 2022

    work page 2022

  2. [2]

    Relative and modified relative realiz- ability.Annals of Pure and Applied Logic, 118(1-2):115–132, 2002

    Lars Birkedal and Jaap van Oosten. Relative and modified relative realiz- ability.Annals of Pure and Applied Logic, 118(1-2):115–132, 2002

    work page 2002

  3. [3]

    Weihrauch complexity in computable analysis

    Vasco Brattka, Guido Gherardi, and Arno Pauly. Weihrauch complexity in computable analysis. In Vasco Brattka and Peter Hertling, editors,Hand- book of Computability and Complexity in Analysis, pages 367–417. Springer International Publishing, Jul 2021

    work page 2021

  4. [4]

    Aurelio Carboni and Enrico M. Vitale. Regular and exact completions. Journal of Pure and Applied Algebra, 125(1-3):79–116, 1998

    work page 1998

  5. [5]

    The Dialectica categories

    Valeria de Paiva. The Dialectica categories. InCategories in computer science and logic (Boulder, CO, 1987), volume 92 ofContemp. Math., pages 47–62. Amer. Math. Soc., Providence, RI, 1989

    work page 1987

  6. [6]

    A language and axioms for explicit mathematics

    Solomon Feferman. A language and axioms for explicit mathematics. In Algebra and logic (Fourteenth Summer Res. Inst., Austral. Math. Soc., Monash Univ., Clayton, 1974), volume Vol. 450 ofLecture Notes in Math., pages 87–139. Springer, Berlin-New York, 1975. 32

    work page 1974

  7. [7]

    A 2-categorical analysis of the tripos-to-topos construction

    Jonas Frey. A 2-categorical analysis of the tripos-to-topos construction. 2011

    work page 2011

  8. [8]

    PhD thesis, Universite Paris Diderot – Paris 7, 2014

    Jonas Frey.A fibrational study of realizability toposes (PhD Thesis). PhD thesis, Universite Paris Diderot – Paris 7, 2014

    work page 2014

  9. [9]

    Triposes, q-toposes and toposes.Annals of Pure and Applied Logic, 166(2):232–259, 2015

    Jonas Frey. Triposes, q-toposes and toposes.Annals of Pure and Applied Logic, 166(2):232–259, 2015

    work page 2015

  10. [10]

    Categories of partial equivalence relations as localizations

    Jonas Frey. Categories of partial equivalence relations as localizations. Journal of Pure and Applied Algebra, 227(8):Paper No. 107115, 25, 2023

    work page 2023

  11. [11]

    D. Higgs. Injectivity in the topos of complete heyting algebra valued sets. Canadian Journal of Mathematics, 36(3):550–568, 1984

    work page 1984

  12. [12]

    The degree structure of Weihrauch- reducibility.Logical Methods in Computer Science, Volume 9, Issue 2, 2013

    Kojiro Higuchi and Arno Pauly. The degree structure of Weihrauch- reducibility.Logical Methods in Computer Science, Volume 9, Issue 2, 2013

    work page 2013

  13. [13]

    Pieter J. W. Hofstra. All realizability is relative.Mathematical Proceedings of the Cambridge Philosophical Society, 141:239 – 264, 2006

    work page 2006

  14. [14]

    Pieter J. W. Hofstra. The dialectica monad and its cousins. InModels, logics, and higher-dimensional categories, volume 53 ofCRM Proc. Lecture Notes, pages 107–137. Amer. Math. Soc., Providence, RI, 2011

    work page 2011

  15. [15]

    Martin E

    J. Martin E. Hyland. The effective topos. InStudies in Logic and the Foundations of Mathematics, volume 110, pages 165–216. Elsevier, 1982

    work page 1982

  16. [16]

    Martin E

    J. Martin E. Hyland. A small complete category.Annals of Pure and Applied Logic, 40(2):135–165, 1988

    work page 1988

  17. [17]

    Martin E

    J. Martin E. Hyland, Peter T. Johnstone, and Andrew M. Pitts. Tripos theory.Mathematical Proceedings of the Cambridge Philosophical Society, 88(2):205–231, 1980

    work page 1980

  18. [18]

    Rethinking the notion of oracle: A prequel to Lawvere- Tierney topologies for computability theorists

    Takayuki Kihara. Rethinking the notion of oracle: A prequel to Lawvere- Tierney topologies for computability theorists. preprint, available at https://arxiv.org/abs/2202.00188v4, 2022

    work page arXiv 2022

  19. [19]

    Searching for an analogue of atr0 in the weihrauch lattice.The Journal of Symbolic Logic, 85(3):1006–1043, 2020

    Takayuki Kihara, Alberto Marcone, and Arno Pauly. Searching for an analogue of atr0 in the weihrauch lattice.The Journal of Symbolic Logic, 85(3):1006–1043, 2020

    work page 2020

  20. [20]

    Stephen C. Kleene. On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10:109–124, 1945

    work page 1945

  21. [21]

    First-order logic in the Medvedev lattice.Studia Logica

    Rutger Kuyper. First-order logic in the Medvedev lattice.Studia Logica. An International Journal for Symbolic Logic, 103(6):1185–1224, 2015. 33

    work page 2015

  22. [22]

    William Lawvere

    F. William Lawvere. Diagonal arguments and cartesian closed categories. InCategory Theory, Homology Theory and their Applications, II (Battelle Institute Conference, Seattle, Wash., 1968, Vol. Two), volume No. 92 of Lecture Notes in Math., pages 134–145. Springer, Berlin-New York, 1969

    work page 1968

  23. [23]

    William Lawvere

    F. William Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. InApplications of Categorical Algebra (Proc. Sympos. Pure Math., Vol. XVII, New York, 1968), volume XVII ofProc. Sympos. Pure Math., pages 1–14. Amer. Math. Soc., Providence, RI, 1970

    work page 1968

  24. [24]

    William Lawvere

    F. William Lawvere. Adjointness in foundations.Repr. Theory Appl. Categ., (16):1–16, 2006. Reprinted from Dialectica23(1969)

    work page 2006

  25. [25]

    A First Introduction to Topos Theory

    Saunders MacLane and Ieke Moerdijk.Sheaves in Geometry and Logic. A First Introduction to Topos Theory. Spinger, 1992

    work page 1992

  26. [26]

    Triposes, exact completions, and Hilbert’sε-operator.Tbilisi Mathematical Journal, 10(3):141–166, 2017

    Maria Emilia Maietti, Fabio Pasquali, and Giuseppe Rosolini. Triposes, exact completions, and Hilbert’sε-operator.Tbilisi Mathematical Journal, 10(3):141–166, 2017

    work page 2017

  27. [27]

    Elementary quotient completions, Church’s thesis, and partioned assemblies.Logical Methods in Computer Science, Volume 15, Issue 2, Jun 2019

    Maria Emilia Maietti, Fabio Pasquali, and Giuseppe Rosolini. Elementary quotient completions, Church’s thesis, and partioned assemblies.Logical Methods in Computer Science, Volume 15, Issue 2, Jun 2019

    work page 2019

  28. [28]

    Quotient completion for the foundation of constructive mathematics.Logica Universalis, 7(3):371–402, 2013

    Maria Emilia Maietti and Giuseppe Rosolini. Quotient completion for the foundation of constructive mathematics.Logica Universalis, 7(3):371–402, 2013

    work page 2013

  29. [29]

    Unifying exact completions

    Maria Emilia Maietti and Giuseppe Rosolini. Unifying exact completions. Applied Categorical Structures. A Journal Devoted to Applications of Cat- egorical Methods in Algebra, Analysis, Order, Topology and Computer Sci- ence, 23(1):43–52, 2015

    work page 2015

  30. [30]

    A characterization of generalized existential completions.Annals of Pure and Applied Logic, 174(4):Paper No

    Maria Emilia Maietti and Davide Trotta. A characterization of generalized existential completions.Annals of Pure and Applied Logic, 174(4):Paper No. 103234, 37, 2023

    work page 2023

  31. [31]

    More exact completions that are toposes.Annals of Pure and Applied Logic, 116(1):187–203, 2002

    Matias Menni. More exact completions that are toposes.Annals of Pure and Applied Logic, 116(1):187–203, 2002

    work page 2002

  32. [32]

    Andrew M. Pitts. Tripos theory in retrospect.Mathematical Structures in Computer Science, 12(3):265–279, 2002

    work page 2002

  33. [33]

    Weihrauch problems as containers.arXiv, preprinthttps: // arxiv

    C´ ecilia Pradic and Ian Price. Weihrauch problems as containers.arXiv, preprinthttps: // arxiv. org/ abs/ 2501. 17250, 2025

    work page 2025

  34. [34]

    Colimit completions and the effective topos.The Journal of Symbolic Logic, 55(2):678–699, 1990

    Edmund Robinson and Giuseppe Rosolini. Colimit completions and the effective topos.The Journal of Symbolic Logic, 55(2):678–699, 1990. 34

    work page 1990

  35. [35]

    Weihrauch reducibility on assemblies

    Matthias Schr¨ oder. Weihrauch reducibility on assemblies. Extended ab- stract presented at CCA2022 (Computability and Complexity in Analysis 2022), 2022

    work page 2022

  36. [36]

    Soare.Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets

    Robert I. Soare.Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets. Perspectives in Mathematical Logic. Springer-Verlag Berlin Heidelberg, 1 edition, 1987

    work page 1987

  37. [37]

    The Medvedev lattice of degrees of difficulty

    Andrea Sorbi. The Medvedev lattice of degrees of difficulty. In S. B. Cooper, T. A. Slaman, and S. S. Wainer, editors,Computability, Enumerability, Unsolvability, volume 224 ofLondon Math. Soc. Lecture Note Ser., pages 289–312. Cambridge University Press, Cambridge, New York, NY, USA, 1996

    work page 1996

  38. [38]

    The existential completion.Theory Appl

    Davide Trotta. The existential completion.Theory Appl. Categ., 35:Paper No. 43, 1576–1607, 2020

    work page 2020

  39. [39]

    Dialectica logical principles

    Davide Trotta, Matteo Spadetto, and Valeria de Paiva. Dialectica logical principles. InLogical foundations of computer science, volume 13137 of Lecture Notes in Comput. Sci., pages 346–363. Springer, Cham, 2022

    work page 2022

  40. [40]

    Dialectica principles via G¨ odel doctrines.Theoretical Computer Science, 947:Paper No

    Davide Trotta, Matteo Spadetto, and Valeria de Paiva. Dialectica principles via G¨ odel doctrines.Theoretical Computer Science, 947:Paper No. 113692, 25, 2023

    work page 2023

  41. [41]

    Categorifying com- putable reducibilities.Logical Methods in Computer Science, Volume 21, Issue 1, Feb 2025

    Davide Trotta, Manlio Valenti, and Valeria de Paiva. Categorifying com- putable reducibilities.Logical Methods in Computer Science, Volume 21, Issue 1, Feb 2025

    work page 2025

  42. [42]

    Elsevier B

    Jaap van Oosten.Realizability: an introduction to its categorical side, vol- ume 152 ofStudies in Logic and the Foundations of Mathematics. Elsevier B. V., Amsterdam, 2008

    work page 2008

  43. [43]

    Partial combinatory algebras of functions.Notre Dame Journal of Formal Logic, 52(4):431–448, 2011

    Jaap van Oosten. Partial combinatory algebras of functions.Notre Dame Journal of Formal Logic, 52(4):431–448, 2011

    work page 2011

  44. [44]

    Texts in The- oretical Computer Science

    Klaus Weihrauch.Computable Analysis: An Introduction. Texts in The- oretical Computer Science. An EATCS Series. Springer-Verlag, Berlin, 1 edition, November 2000. 35

    work page 2000