A topos for extended Weihrauch degrees

TL;DR

This paper develops a categorical framework, including a tripos and a topos, for extended Weihrauch degrees, broadening the understanding of computational problem reducibility.

Contribution

It introduces a tripos and a topos for extended Weihrauch degrees, providing a categorical perspective on this generalized reducibility notion.

Findings

Constructed a tripos abstracting extended Weihrauch degrees.

Applied tripos-to-topos construction to obtain a topos.

Showed Kleene-Vesley topos as a topos of $j$-sheaves for a Lawvere-Tierney topology.

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.