A topos for extended Weihrauch degrees

A topos for extended Weihrauch degrees Samuele Maschio and Davide Trotta Categorical methods are applied in many areas of mathematical logic, however an area that has been less influenced by this categorical approach is computability, although there is a long tradition of application of categorical methods in realizability studies, see e.g. [10]. In recent years, there have been some works starting to approach computability-like notions from a categorical perspective (see e.g. [6,5,8,9]). In [1], Bauer introduced an abstract notion of reducibility between predicates, called instance reducibility, which commonly appears in reverse constructive mathematics. In a relative realizability topos, the instance degrees correspond to a generalization of (realizer-based) Weihrauch reducibility, called extended Weihrauch degrees, and the “classical” Weihrauch degrees [3] correspond precisely to the ¬¬-dense modest instance degrees in Kleene-Vesley realizability. Upon closer inspection, it is not hard to check that realizer-based Weihrauch reducibility is a particular case of Bauer’s notion. The main goal of this talk is to show how one can define a topos for extended Weihrauch degrees, providing a suitable universe for studying this reducibility categorically. Then, we take advantage from this categorical presentation, and we establish the precise connection between extended Weihrauch degrees and realizability. The main tools we adopt to construct such a topos are: (i) the tripos-totopos construction [4], which produces a topos from a given tripos (that is, a particular kind of Lawvere hyperdoctrine which has enough structure to deal with higher-order logic properly), and (ii) the (full) existential completion, a construction that freely adds left adjoints along all the morphisms of the base of a given doctrine. In fact, we first define a doctrine iR over the category of partitioned assemblies abstracting Bauer’s notion of instance reducibility between realizability predicates, and we prove that it is a tripos. This doctrine is defined as the (full) existential completion eiR∃of a more basic doctrine eiR, following the same idea used in [9] for defining doctrines abstracting computability reducibility. Then we introduce a second doctrine eW which provides a direct categorification of the notion of extended Weihrauch degrees and we prove that eW ∼ =iR. This equivalence shows in particular that eW is a tripos. This result can be seen as a fibrational version of Bauer’s result showing that Weihrauch reductions and instance reductions are equivalent [1]. Indeed, the order of the fibres of iR corresponds to the notion of instance reduction, while 1 that of eW corresponds to the extended Weirhauch reduction. Finally, once we have proved that the extended Weihrauch doctrine is a tripos, we can define the topos of extended Weirhauch degrees as the topos obtained by applying the tripos-to-topos to the tripos eW and study the connections with (relative) realizability toposes. In particular, we prove that the relative realizability topos RT[A,A′] [2] is equivalent to a topos shj(EW[A,A′]) of j-sheaves for a Lawvere-Tierney topology jover EW[A,A′]. To prove this result, there are two facts playing a key role: first that the extended Weihrauch tripos is a (full) existential completion; second, that realizability toposes can be presented as exact completions of the category or partitioned assemblies [7]. References [1] A. Bauer. Instance reducibility and Weihrauch degrees. Logical Methods in Computer Science, 18(3):20:1–20:18, 2022. [2] L. Birkedal and J. van Oosten. Relative and modified relative realizability. Annals of Pure and Applied Logic, 118(1-2):115–132, 2002. [3] V. Brattka, G. Gherardi, and A. Pauly. Weihrauch complexity in computable analysis. In Vasco Brattka and Peter Hertling, editors, Handbook of Computability and Complexity in Analysis, pages 367–417. Springer International Publishing, Jul 2021. [4] J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts. Tripos theory. Mathematical Proceedings of the Cambridge Philosophical Society, 88(2):205–231, 1980. [5] T. Kihara. Rethinking the notion of oracle: A prequel to lawveretierney topologies for computability theorists. preprint, available at https: //arxiv.org/abs/2202.00188v4, 2022. [6] R. Kuyper. First-order logic in the Medvedev lattice. Studia Logica. An International Journal for Symbolic Logic, 103(6):1185–1224, 2015. [7] E. Robinson and G. Rosolini. Colimit completions and the effective topos. The Journal of Symbolic Logic, 55(2):678–699, 1990. [8] M. Schr¨oder. Weihrauch reducibility on assemblies. Extended abstract presented at CCA2022 (Computability and Complexity in Analysis 2022), 2022. [9] D. Trotta, M. Valenti, and V. de Paiva. Categorifying computable reducibilities. Logical Methods in Computer Science, Volume 21, Issue 1, Feb 2025. [10] J. van Oosten. Realizability: an introduction to its categorical side, volume 152 of Studies in Logic and the Foundations of Mathematics. Elsevier B. V., Amsterdam, 2008. 2