Weihrauch reducibility is a notion of reducibility between computational problems that is useful to calibrate the uniform computational strength of a multi-valued 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 of 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.

The study of categories that abstract the structural properties of relations has been extensively developed over the years, resulting in a rich and diverse body of work. This paper strives to provide a modern presentation of these ``categories for relations'', including their enriched version, further showing how they arise as Kleisli categories of symmetric monoidal monads. The resulting taxonomy aims at bringing clarity and organisation to the many related concepts and frameworks occurring in the literature.

Abstract It is well known that over Heyting arithmetic with finite types, the effective principle of the formal Church thesis, stating that all number-theoretic functional relations are computable, is inconsistent with Brouwer’s intuitionistic principles on the continuum, in particular, the fan theorem. Here, we build two arithmetic quasi-toposes, validating on the one hand Brouwer’s continuity principles, including the Fan theorem, and on the other hand, a restricted form of Church’s Thesis, called the Type-theoretic Church Thesis and written $\textsf{TCT}$ , expressing that all morphisms of the considered quasi-topos are computable. One quasi-topos is constructed by formalizing the category of assemblies $\mathbf{Asm}$ within Hyland’s effective topos using intuitionistic Zermelo-Fraenkel set theory $\mathbf{IZF}$ extended with Brouwer’s continuity principles as our meta-theory. The other quasi-topos is obtained as an elementary quotient completion in the same intuitionistic meta-theory. While in previous work by the first author with F. Pasquali and G. Rosolini, it has been shown that these two quasi-toposes are equivalent when working within the classical $\mathbf{ZFC}$ set theory; here, we show that this is no longer the case when working within $\mathbf{IZF}$ . We also observe that the aforementioned inconsistency is resolved in such quasi-toposes by the non-validity of the axiom of unique choice on the natural numbers and that no non-trivial topos can validate the effective principle $\textsf{TCT}$ together with Brouwer’s continuity principles altogether.

This paper presents categorical formulations of Turing, Medvedev, Muchnik, and Weihrauch reducibilities in Computability Theory, utilizing Lawvere doctrines. While the first notions lend themselves to a smooth categorical presentation, essentially dualizing the traditional idea of realizability doctrines, Weihrauch reducibility and its extensions to represented and multi-represented spaces require a separate investigation. Our abstract analysis of these concepts highlights a shared characteristic among all these reducibilities. Specifically, we demonstrate that all these doctrines stemming from computability concepts can be proven to be instances of completions of quantifiers for doctrines, analogous to what occurs for doctrines for realizability. As a corollary of these results, we will be able to formally compare Weihrauch reducibility with the dialectica doctrine constructed from a doctrine representing Turing degrees.

Fo-bicategories are a categorification of Peirce's calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere's hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.

Implicative algebras have been recently introduced by Miquel in order to provide a unifying notion of model, encompassing the most relevant and used ones, such as realizability (both classical and intuitionistic), and forcing. In this work, we initially approach implicative algebras as a generalization of locales, and we extend several topological-like concepts to the realm of implicative algebras, accompanied by various concrete examples. Then, we shift our focus to viewing implicative algebras as a generalization of partial combinatory algebras. We abstract the notion of a category of assemblies, partition assemblies, and modest sets to arbitrary implicative algebras, and thoroughly investigate their categorical properties and interrelationships.

Introduced in the 1990s in the context of the algebraic approach to graph rewriting, gs-monoidal categories are symmetric monoidal categories where each object is equipped with the structure of a commutative comonoid. They arise for example as Kleisli categories of commutative monads on cartesian categories, and as such they provide a general framework for effectful computation. Recently proposed in the context of categorical probability, Markov categories are gs-monoidal categories where the monoidal unit is also terminal, and they arise for example as Kleisli categories of commutative affine monads, where affine means that the monad preserves the monoidal unit. The aim of this paper is to study a new condition on the gs-monoidal structure, resulting in the concept of weakly Markov categories, which is intermediate between gs-monoidal categories and Markov ones. In a weakly Markov category, the morphisms to the monoidal unit are not necessarily unique, but form a group. As we show, these categories exhibit a rich theory of conditional independence for morphisms, generalising the known theory for Markov categories. We also introduce the corresponding notion for commutative monads, which we call weakly affine, and for which we give two equivalent characterisations. The paper argues that these monads are relevant to the study of categorical probability. A case at hand is the monad of finite non-zero measures, which is weakly affine but not affine. Such structures allow to investigate probability without normalisation within an elegant categorical framework.

Abstract Gödel’s Dialectica interpretation was designed to obtain the consistency of Peano arithmetic via a proof of consistency of Heyting arithmetic and double negation. In recent years, proof theoretic transformations (the so-called proof interpretations) based on Gödel’s Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on ‘Gödel fibrations’, we present a (hyper)doctrine characterization of the Dialectica, which corresponds exactly to the logical description of the interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra, in the categorical model. This requires extra logical principles, going beyond intuitionistic logic, namely Markov Principle and the Independence of Premise principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. We make sure that this tight correspondence extends to the use of the principles above, instead of the weaker rules we had proved earlier on. This tight correspondence should come handy not only when discussing the traditional applications of the Dialectica but also when dealing with newer uses in modelling games or concurrency theory.

We introduce the notion of a Gödel fibration, which is a fibration categorically embodying both the logical principle of traditional Skolemization (we can exchange the order of quantifiers paying the price of a functional) and the existence of a prenex normal form presentation for every logical formula. Building up from Hofstra's earlier fibrational characterization of the de Paiva's categorical Dialectica construction, we show that a fibration is an instance of the Dialectica construction if and only if it is a Gödel fibration. This result establishes an internal presentation of the dialectica construction. Then we provide a deep structural analysis of the Dialectica construction producing a full description of which categorical structure behaves well with respect to this construction, focusing on (weak) finite products and coproducts. We conclude describing the applications we envisage for this generalized fibrational version of the Dialectica construction.