# Categorifying Computable Reducibilities

Davide Trotta  University of Pisa, Italy<EMAIL_ADDRESS>,  Manlio
Valenti  University of Wisconsin - Madison, USA Swansea University, UK
<EMAIL_ADDRESS>and  Valeria de Paiva  Topos Institute, California
<EMAIL_ADDRESS>
###### Abstract.

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 notion of realizability doctrines,
Weihrauch reducibility and its extensions for represented and multi-
represented spaces require a thorough investigation and the formulation of a
new appropriate extension of the category of assemblies as a foundation for
the respective doctrine.

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 formally able to compare Weihrauch
reducibility with the dialectica doctrine constructed from a doctrine
representing Turing degrees.

Davide Trotta’s research has been partially supported by the Italian MIUR
project PRIN 2017FTXR7S _IT-MATTERS (Methods and Tools for Trustworthy Smart
Systems)_. Manlio Valenti’s research was partially supported by the Italian
PRIN 2017 Grant _Mathematical Logic: models, sets, computability_. The authors
would like to thank Jonas Frey, Takayuki Kihara, and Arno Pauly for useful
conversation on the topic of the paper.

##  1\. Introduction

Categorical methods and language have been employed in many areas of
Mathematics. In Mathematical Logic, they are widely used in Model Theory and
Proof Theory. In Recursion or Computability Theory, there is a long tradition
of categorical methods in Realizability studies, expounded in van Oosten’s
book [46]. One of the key tools employed in such a setting is the notion of
_tripos_ , introduced by Hyland, Johnstone, and Pitts in [19], which is a
specific instance of the notion of _hyperdoctrine_ introduced by Lawvere [26,
24, 25] to synthesize the structural properties of logical systems.

The use of categorical methods in Realizability includes, for example,
Hofstra’s work [16], where he proved that most well-known realizability-like
triposes, (e.g. the “effective” tripos [19], the “modified realizability”
tripos [45] and the “dialectica” tripos [2]) are instances of a more general
notion of tripos associated to a given ordered partial combinatory algebra
(PCA) (equipped with a filter). It is worth recalling that the notion of PCA
presents a generalization of both Kleene’s first and second models. His point
was that all these triposes can be presented as “triposes for a given PCA”,
hence all these notions differ only in the choice of the associated PCA, and
we could say that all realizability is relative to a choice of a PCA.

Hofstra’s formulation explains and systematizes the different kinds of
triposes for realizability developed independently before.

Over the years, several authors observed that realizability triposes are
instances of a free construction adding “generalized existential quantifiers”
to a given doctrine. For instance, we refer to Hofstra’s work [16], Trotta and
Maietti’s work [30], and Frey’s works [11, 12]. So every realizability tripos
is obtained by freely adding left adjoints along the class of all morphisms of
the base category. Hence, combining this result with the previous analysis by
Hofstra, we have that realizability-like triposes are instances of the
generalized existential completion. These results bring to light the abstract,
structural property that lay behind all the various forms of realizability.

Despite the long tradition of studying realizability and its variants from a
categorical perspective, a systematic and in-depth analysis of computability-
like reducibilities, such as Turing [33, 38], Medvedev [39, 15], Muchnik [15],
and Weihrauch reducibilities [4], from a categorical perspective is still
lacking. A categorical presentation of these notions is useful to highlight
some of their abstract structural properties. Moreover, this work provides a
common language for the categorical logic community and the computability
theorists. These are two fields that traditionally employ very different
languages and notations, so a categorical understanding of reducibility in
computability with categorical logic descriptions in terms of doctrines has
the positive effect of fostering collaborations between the two communities.

A first approach to Medvedev and Muchnik reducibility via hyperdoctrines has
been recently introduced in [23], while Weihrauch reducibility for assemblies
(or multi-represented spaces) has been introduced only very recently in [20,
36] through the notion of realizer-based Weihrauch reducibility and, in [1],
A. Bauer introduced another generalization of Weihrauch reducibility, called
extended Weihrauch reducibility.

In this paper, we want to extend the use of the categorical tools of doctrines
to computability, by presenting a specific doctrine for every previously
mentioned notion of reducibility and studying their universal properties. In
detail, we first introduce a doctrine for Turing, Medvedev, and Muchnik
reducibility. After showing that these doctrines provide a proper
categorification of these notions, we prove that both Medvedev and Muchnik
reducibility are instances of the categorical construction called “universal
completion” which freely adds “generalized universal quantifiers” to a given
doctrine. This construction is a natural generalization of the “pure universal
completion” used to characterize dialectica doctrines in [42, 44]. As a
corollary of these results, we show that the Medvedev doctrine is obtained as
the full universal completion of the doctrine of Turing degrees.

We then focus on the notion of Weihrauch reducibility (and its strong version)
from a categorical perspective. Following the same line, we start our analysis
by defining a doctrine abstracting the ordinary notion of Weihrauch
reducibility, and then we prove that this doctrine can be obtained as the pure
existential completion of a more basic doctrine. The crucial difference
between this setting and the previous one regards the base category of the
doctrine we have to consider. Indeed, while for Medvedev and Muchnik
reducibility, the base category of the doctrines is the category
$\mathsf{Set}$ of sets and functions, for Weihrauch we will use the category
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$ whose objects are
subsets of the PCA $\mathbb{A}$, and whose morphisms are computable functions.
This change of perspective is necessary to fully abstract the details of a
Weihrauch reduction (in particular, it captures the role of the _forward
functional_).

The last part of our work is devoted to studying Weihrauch reducibility in the
more general context of partial multi-valued functions on represented spaces,
which is a quite common setting for people working in computable analysis.
However, the problem of generalizing our previous approach to this setting is
non-trivial. The main problem is that the ordinary notion of category of
_assemblies_ $\mathsf{Asm}(\mathbb{A},\mathbb{A}^{\prime})$ and of _modest
sets_ $\mathsf{Mod}(\mathbb{A},\mathbb{A}^{\prime})$, often used in
categorical logic when reasoning about represented spaces, are not able to
properly support the required properties of the forward functional in
Weihrauch reducibility. In particular, the main problem is not the notion of
assembly or modest sets themself, but the notion of _morphism_ of assemblies.

Therefore, to fully abstract Weihrauch reducibility for represented spaces in
the language of doctrines, we have to introduce a new suitable extension of
the category of assemblies, which we denote by
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$. The objects of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ are still assemblies, but
the morphisms are better suited to abstract the properties of the forward
functional. This new category will play a key role in the rest of our work.
Indeed, taking this as base category for our doctrines, we will present a
doctrine abstracting the notion of realizer-based Weihrauch reducibility (a
generalization of Weihrauch reducibility to assemblies), and one for extended
Weihrauch reducibility. The standard notion of reducibility in the setting of
represented spaced can be obtained by restricting such doctrines to the full
subcategory of $\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ whose objects
are modest sets, while that for non-represented spaces (i.e. the first we
showed), can be obtained again by considering just modest sets which are also
partitioned assemblies.

Once the issue concerning the base category is resolved and the doctrines are
appropriately defined, we finally demonstrate that all these doctrines are
instances of pure existential complementation, following the same line adopted
for the first Weihrauch doctrine we introduced.

Our abstract analysis systemathizes all these variants of Weihrauch
reducibility and shows a clear connection between all of them. In particular,
we highlight how extended Weihrauch reducibility can be seen as the most
general variant, and all the others can be obtained from it by considering
suitable restrictions of such doctrine.

We conclude our work by highlighting an interesting connection between
Medvedev and extended Weihrauch reducibility, and discussing how the notion of
extended strong Weihrauch is related to Gödel’s Dialectica interpretation
[14]. In particular, our presentation allows us to provide a formal
explanation of the resemblance between the structure of Dialectica categories
and some known notions of computability (extended Weihrauch reducibility),
which has been observed by several authors over the years.

The outline of this paper is as follows: in Section 2 and Section 3, we recall
the background notions of partial combinatory algebra and quantifier
completions. In Section 4 we reformulate Medvedev and Muchnik reducibility in
categorical terms. In Section 5 we categorify Weihrauch reducibility and, in
Section 6, we consider the above-mentioned generalizations of Weihrauch
reducibility. Finally, we draw some final comments in Section 7.

##  2\. Partial combinatory algebras

Realizability theory originated with Kleene’s interpretation of intuitionistic
number theory [21] and has since developed into a large body of work in logic
and theoretical computer science. We focus on two basic flavours of
realizability, number realizability, and function realizability, which were
both due to Kleene.

In this section, we recall some standard notions within realizability and
computability. We follow the approach suggested by van Oosten [46], as we want
to fix a suitable notation for both category theorists and computability
logicians.

We describe _partial combinatory algebras_ and discuss some important
examples. For more details, we refer the reader to van Oosten’s work on
categorical realizability (see [46] and the references therein).

We start by introducing the basic concept of a _partial applicative structure_
or PAS, due to Feferman, which may be viewed as a universe for computation.

######  Definition 2.1 (PAS).

A partial applicative structure, or PAS for short, is a set $\mathbb{A}$
equipped with a partial binary operation
$\cdot:\subseteq\mathbb{A}\times\mathbb{A}\to\mathbb{A}$.

Some conventions and terminology: given two elements $a,b$ in $\mathbb{A}$, we
think of $a\cdot b$ (which we often abbreviate $ab$) as “$a$ applied to $b$”.
The partiality of the operation $\cdot$ means that this application need not
always be defined. We write $f:\subseteq A\to B$ to say that $f$ is a partial
function with domain a subset of $A$, $\operatorname{dom}(f)\subseteq A$ and
range $\operatorname{ran}(f)=B$. If $(a,b)\in\operatorname{dom}(\cdot)$, that
is, when the application is defined, then we write $a\cdot b\downarrow$ or
$ab\downarrow$.

We usually omit brackets, assuming associativity of application to the left.
Thus $abc$ stands for $(ab)c$. Moreover, for two expressions $x$ and $y$ we
write $x\simeq y$ to indicate that $x$ is defined whenever $y$ is, in which
case they are equal.

Even though these partial applicative structures do not possess many
interesting properties (they have no axioms for application), they already
highlight one of the key features of combinatorial structures, namely the fact
that we have a domain of elements that can act both as functions and as
arguments, just as in untyped $\lambda$-calculus. This behaviour can be traced
back to Von Neumann’s idea that programs (functions, operations) live in the
same realm and are represented in the same way as the data (arguments) that
they act upon. In particular, programs can act on other programs.

######  Definition 2.2 (PCA).

A partial combinatory algebra (PCA) is a PAS $\mathbb{A}$ for which there
exist elements $k,s\in\mathbb{A}$ such that for all $a,b,c\in\mathbb{A}$ we
have that

$ka\downarrow\mbox{ and }kab\simeq a$

and

$sa\downarrow\mbox{, }sab\downarrow\mbox{, and }sabc\simeq ac(bc)$

The elements $k$ and $s$ are generalizations of the homonymous combinators in
Combinatory Logic. Note that appropriate elements $k,s$ are not considered
part of the structure of the partial combinatory algebra, so they need not be
preserved under homomorphisms.

Every PCA $\mathbb{A}$ is combinatory complete in the sense of [10, 46],
namely: for every term $t(x_{1},\dots,x_{n+1})$ built from variables
$x_{1},\dots,x_{n+1}$, constants $\bar{c}$ for $c\in\mathbb{A}$, and
application operator $\cdot$, there is an element $a\in\mathbb{A}$ such that
for all elements $b_{1},\dots,b_{n+1}\in\mathbb{A}$ we have that $ab_{1}\cdots
b_{n}\downarrow$ and $ab_{1}\cdots b_{n+1}\simeq t(b_{1},\dots,b_{n+1})$.

In particular, we can use this result and the elements $k$ and $s$ to
construct elements $\mathsf{pair},\mathsf{fst},\mathsf{snd}$ of $\mathbb{A}$
so that $(a,b)\mapsto\mathsf{pair}\cdot a\cdot b$ is an injection of
$\mathbb{A}\times\mathbb{A}$ to $\mathbb{A}$ with left inverse
$a\mapsto(\mathsf{fst}\cdot a,\mathsf{snd}\cdot a)$. Hence, we can use
$\mathsf{pair}ab$ as an element of $\mathbb{A}$ which codes the pair $(a,b)$.
For this reason, the elements $\mathsf{pair},\mathsf{fst},\mathsf{snd}$ are
usually called _pairing_ and _projection_ operators. For the sake of
readability, we write $\langle a,b\rangle$ in place of $\mathsf{pair}ab$ (as
it is more customary in computability theory).

Using $s$ and $k$, we can prove the analogues of the Universal Turing Machine
(UTM) and the SMN theorems in computability in an arbitrary PCA. A PCA
$\mathbb{A}$ is called extensional if for all $x$ in $\mathbb{A}$, $(ax\simeq
bx)$ implies $a=b$.

By definition, in every extensional PCA, if two elements represent the same
partial function, then they must be equal.

Next we recall the notion of _elementary sub-PCA_ (see for example [46, Sec.
2.6.9]). Many definitions in the computability context refer to a concept and
a subset of the given concept, as one needs to pay attention to the computable
functions (and elements) included in the original concept.

######  Definition 2.3 (elementary sub-PCA).

Let $\mathbb{A}$ be a PCA. A subset $\mathbb{A}^{\prime}\subseteq\mathbb{A}$
is called an elementary sub-PCA of $\mathbb{A}$ if $\mathbb{A}^{\prime}$ is a
PCA with the partial applicative structure induced by $\mathbb{A}$ (namely,
the elements $k$ and $s$ as in 2.2 can be found in $\mathbb{A}^{\prime}$). In
particular, it is closed under the application of $\mathbb{A}$, that means: if
$a,b\in\mathbb{A}^{\prime}$ and $ab\downarrow$ in $\mathbb{A}$ then
$ab\in\mathbb{A}^{\prime}$.

In particular, elements of the sub-PCA will play the role of the computable
functions.

######  Example 2.4 (_Kleene’s first model_).

Fix an effective enumeration $(\varphi_{a})_{a\in\mathbb{N}}$ of the partial
recursive functions $\mathbb{N}\to\mathbb{N}$ (i.e. a Gödel numbering). The
set $\mathbb{N}$ with partial recursive application
$(a,b)\mapsto\varphi_{a}(b)$ is a PCA, and it is called _Kleene’s first model_
$\mathcal{K}_{1}$ (see e.g. [38]).

######  Example 2.5 (_Kleene’s second model_).

The PCA $\mathcal{K}_{2}$ is often used for function realizability [46, Sec.
1.4.3]. This PCA is given by the Baire space $\mathbb{N}^{\mathbb{N}}$,
endowed with the product topology. The partial binary operation of application
$\cdot:\subseteq\mathbb{N}^{\mathbb{N}}\times\mathbb{N}^{\mathbb{N}}\to\mathbb{N}^{\mathbb{N}}$
corresponds to the one used in Type-$2$ Theory of Effectivity [48]. This can
be described as follows. Let $\alpha[n]$ denote the string
$(\alpha(0),\ldots,\alpha(n-1))$. Every $\alpha\in\mathbb{N}^{\mathbb{N}}$
induces a function $F_{\alpha}:\subseteq\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$
defined as $F_{\alpha}(\beta)=k$ if there is $n\in\mathbb{N}$ such that
$\alpha(\langle\beta[n]\rangle)=k+1$ and $(\forall
m<n)(\alpha(\langle\beta[n]\rangle)=0)$, and undefined otherwise. The
application $\alpha\cdot\beta$ can then be defined as the map $n\mapsto
F_{\alpha}((n)\smash{\raisebox{3.87495pt}{$\smallfrown$}}\beta)$, where
$(n)\smash{\raisebox{3.87495pt}{$\smallfrown$}}\beta$ is the string $\sigma$
defined as $\sigma(0):=n$ and $\sigma(k+1):=\beta(k)$.

When working with Kleene’s second model, we usually consider the elementary
sub-PCA $\mathcal{K}_{2}^{rec}$ consisting of all the
$\alpha\in\mathbb{N}^{\mathbb{N}}$ such that $\beta\mapsto\alpha\cdot\beta$ is
computable. For more details and examples, also of non-elementary sub-PCAs for
Kleene’s second model, we refer to [47].

######  Remark 2.6.

Kleene’s $\mathcal{K}_{1}$ and $\mathcal{K}_{2}$ presented above are not
extensional, since there are many codes (programs) that compute the same
function. In fact, every function has infinitely many representatives.

##  3\. Categorical Doctrines

We want to connect the notions of computability described in the previous
subsection to work on (logical) categorical doctrines in [42]. We recap only
the essential definitions from the doctrines work in the text; further details
and explanation can be found in [41, 42].

Several generalizations of the notion of a (Lawvere) hyperdoctrine have been
considered recently, we refer, for example, to the works of Rosolini and
Maietti [27, 28, 29], or to [35, 19] for higher-order versions. In this work
we consider a natural generalization of the notion of hyperdoctrine, which we
call simply a _doctrine_.

######  Definition 3.1 (doctrine).

A doctrine is a contravariant functor:

$\textstyle{P\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$

where the category $\mathcal{C}$ has finite products and $\mathsf{Pos}$ is the
category of (partially ordered sets or) posets.

######  Definition 3.2 (morphism of doctrines).

A morphism of doctrines is a pair $\mathfrak{L}:=(F,\mathfrak{b})$

|
---|---
$\textstyle{\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P}$$\scriptstyle{F^{\operatorname{op}}}$$\textstyle{\mathsf{Pos}}$$\textstyle{\mathcal{D}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R}$$\scriptstyle{\mathfrak{b}}$

such that $F\colon\mathcal{C}\to\mathcal{D}$ is a finite product preserving
functor and:

$\mathfrak{b}\colon P\to RF^{\operatorname{op}}$

is a natural transformation.

######  Example 3.3.

Let $\mathbb{A}$ be a PCA. We can define a functor
$\textstyle{\mathbb{A}^{(-)}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
assigning to a set $X$ the set $\mathbb{A}^{X}$ of functions from $X$ to
$\mathbb{A}$. By standard properties of PCAs, given two elements
$\alpha,\beta\in\mathbb{A}^{X}$, we have the following preorder:
$\alpha\leq\beta$ if there exists an element $a\in\mathbb{A}$ such that for
every $x\in X$ we have that $a\cdot\alpha(x)$ is defined and
$a\cdot\alpha(x)=\beta(x)$. The doctrine given by considering the poset
reflection of such a preorder is the _doctrine associated to the PCA
$\mathbb{A}$_. Notice that this construction can be generalized in the context
of relative realizability, see for example [16, p. 253].

We recall the following example from [35, 19].

######  Example 3.4.

Given a PCA $\mathbb{A}$, we can consider the realizability doctrine
$\textstyle{\mathcal{R}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
over $\mathsf{Set}$. For each set $X$, the partial order
$(\mathcal{R}(X),\leq)$ is defined as the set of functions
$\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})^{X}$ from $X$ to the powerset
$\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})$ of $\mathbb{A}$. Given two
elements $\alpha$ and $\beta$ of $\mathcal{R}(X)$, we say that
$\alpha\leq\beta$ if there exists an element $\overline{a}\in\mathbb{A}$ such
that for all $x\in X$ and all $a\in\alpha(x)$, $\overline{a}\cdot a$ is
defined and it is an element of $\beta(x)$. By standard properties of PCAs
this relation is reflexive and transitive, i.e. it is a preorder. Then
$\mathcal{R}(X)$ is defined as the quotient of
$\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})^{X}$ by the equivalence
relation generated by the $\leq$. The partial order on the equivalence classes
$[\alpha]$ is the one induced by $\leq$.

We also need to recall the general definitions of existential and universal
doctrines.

######  Definition 3.5 ($\mathcal{D}$-existential/universal doctrines).

Let $\mathcal{C}$ be a category with finite products, and let $\mathcal{D}$ a
class of morphisms of $\mathcal{C}$ closed under composition, pullbacks and
identities. A doctrine
$\textstyle{P\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
is $\mathcal{D}$-existential (resp. $\mathcal{D}$-universal) if, for every
arrow $f\colon X\to A$ of $\mathcal{D}$, the functor

$P_{f}\colon PA\to PX$

has a left adjoint $\exists_{f}$ (resp. a right adjoint $\forall_{f}$), and
these satisfy the Beck-Chevalley condition BC: for any pullback diagram

$\textstyle{X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f^{\prime}}$$\scriptstyle{h^{\prime}}$$\textstyle{A^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{A}$

and any $\beta$ in $P(X)$ the equality

$\exists_{f^{\prime}}P_{h^{\prime}}\beta=P_{h}\exists_{f}\beta\,\,\,\,\textnormal{
(resp.
}\forall_{f^{\prime}}P_{h^{\prime}}\beta=P_{h}\forall_{f}\beta\textnormal{ )}$

holds. When $\mathcal{D}$ is the class of all the morphisms of $\mathcal{C}$
we say that the doctrine $P$ is full existential (resp. full universal), while
when $\mathcal{D}$ is the class of product projections, we will say that $P$
is pure existential (resp. pure universal).

Next we summarise the main properties of the generic full existential and
universal completions in the following theorems and refer to [40] for more
details.

Generalized existential completion. Let
$\textstyle{P\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
be a doctrine and let $\mathcal{D}$ be a class of morphisms of $\mathcal{C}$
closed under composition, pullbacks and containing identities. For every
object $A$ of $\mathcal{C}$ consider the following preorder:

  * •

objects: pairs $(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.0434pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
8.79947pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{f\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.0434pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.0434pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\alpha)$,
where $f\colon B\to A$ is an arrow of $\mathcal{D}$ and $\alpha\in P(B)$.

  * •

order: $(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.0434pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
8.79947pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{f\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.0434pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.0434pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\alpha)\leq(\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
6.93124pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
9.03871pt\raise 6.07222pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.71112pt\hbox{$\scriptstyle{g\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.93124pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.93124pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\beta)$ if
there exists an arrow $\textstyle{h\colon
B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{C}$ of
$\mathcal{C}$ such that the diagram

$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{h}$$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{A}$

commutes and

$\alpha\leq P_{h}(\beta).$

It is easy to see that the previous construction gives a preorder. We denote
by $P^{\exists_{\mathcal{D}}}(A)$ the partial order obtained by identifying
two objects when

$(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.0434pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
8.8732pt\raise 5.5674pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.29372pt\hbox{$\scriptstyle{h\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.0434pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.0434pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\alpha)\gtreqless(\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
7.27847pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{D\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
8.917pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{f\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.27847pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.27847pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\gamma)$

in the usual way. With a small abuse of notation, we identify an equivalence
class with one of its representatives.

Given a morphism $f\colon A\to B$ in $\mathcal{C}$, let
$P^{\exists_{\mathcal{D}}}_{f}(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.93124pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.19237pt\raise 5.1875pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.93124pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.93124pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{B}$}}}}}}}\ignorespaces}}}}\ignorespaces,\beta)$ be the
object

$(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.27847pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{D\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
6.12204pt\raise 6.57639pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.21529pt\hbox{$\scriptstyle{f^{\ast}g\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.27847pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.27847pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\;P_{g^{*}f}(\beta))$

where $f^{*}g$ and $g^{*}f$ are defined by the pullback

$\textstyle{D\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f^{*}g}$$\scriptstyle{g^{*}f}$$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{B.}$

The assignment
$\textstyle{P^{\exists_{\mathcal{D}}}\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
is called the generalized existential completion of $P$. Following [40, 30],
when $\mathcal{D}$ is the class of all the morphisms of the base category, we
will speak of full existential completion, and we will use the notation
$\textstyle{{P}^{\exists_{\mathsf{f}}}\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$.
Moreover, when $\mathcal{D}$ is the class of all product projections, we will
speak of pure existential completion, and we will use the notation
$\textstyle{{P}^{\exists}\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$.

######  Theorem 3.6 ([40]).

The doctrine $P^{\exists_{\mathcal{D}}}$ is $\mathcal{D}$-existential.
Moreover, for every doctrine $P$ we have a canonical inclusion
$\eta_{P}^{\exists_{\mathcal{D}}}\colon P\to P^{\exists_{\mathcal{D}}}$ such
that, for every morphism of doctrines $\mathfrak{L}\colon P\to R$, where $R$
is $\mathcal{D}^{\prime}$-existential and the functor between the bases sends
arrows of $\mathcal{D}$ into arrows of $\mathcal{D}^{\prime}$, there exists a
unique (up to isomorphism) existential morphism doctrine (i.e. preserving
existential quantifiers along $\mathcal{D}$) such that the diagram

$\textstyle{P^{\exists_{\mathcal{D}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{P}^{\exists_{\mathcal{D}}}}$$\scriptstyle{\mathfrak{L}}$$\textstyle{R}$

commutes.

######  Example 3.7.

Realizability doctrines are relevant examples of doctrines arising as full
existential completions. The original observation of this result is due to
Hofstra [16], while a more general analysis of doctrines arising as full
existential completions can be found in [30, 12].

By dualizing the previous construction, we can define the
$\mathcal{D}$-_universal completion_ of a doctrine.

Generalized universal completion. Let
$\textstyle{P\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
be a doctrine and let $\mathcal{D}$ be a class of morphisms of $\mathcal{C}$
closed under composition, pullbacks and containing identities. For every
object $A$ of $\mathcal{C}$ consider the following preorder:

  * •

objects: pairs $(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.0434pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
8.79947pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{f\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.0434pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.0434pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\alpha)$,
where $f\colon B\to A$ is an arrow of $\mathcal{D}$ and $\alpha\in P(B)$.

  * •

order: $(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.0434pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
8.79947pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{f\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.0434pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.0434pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\alpha)\leq(\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
6.93124pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
9.03871pt\raise 6.07222pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.71112pt\hbox{$\scriptstyle{g\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.93124pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.93124pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\beta)$ if
there exists an arrow $\textstyle{h\colon
C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{B}$ of
$\mathcal{C}$ such that the diagram

$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\scriptstyle{h}$$\textstyle{A}$

commutes and

$P_{h}(\alpha)\leq\beta.$

Again, it is easy to see that the previous data gives us a preorder. We denote
by $P^{\forall_{\mathcal{D}}}(A)$ the partial order obtained by identifying
two objects when

$(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.0434pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
8.8732pt\raise 5.5674pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.29372pt\hbox{$\scriptstyle{h\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.0434pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.0434pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\alpha)\gtreqless(\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
7.27847pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{D\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
8.917pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{f\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.27847pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.27847pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\gamma)$

in the usual way. As before, with a small abuse of notation, we identfy an
equivalence class with one of its representatives.

Given a morphism $f\colon A\to B$ in $\mathcal{C}$, let
$P^{\forall_{\mathcal{D}}}_{f}(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.93124pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
9.18541pt\raise 6.07222pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.71112pt\hbox{$\scriptstyle{g\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.93124pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.93124pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{B}$}}}}}}}\ignorespaces}}}}\ignorespaces,\beta)$ be the
object

$(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.27847pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{D\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
6.12204pt\raise 6.57639pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.21529pt\hbox{$\scriptstyle{f^{\ast}g\in\mathcal{D}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.27847pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.27847pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces,\;P_{g^{*}f}(\beta))$

where $f^{*}g$ and $g^{*}f$ are defined by the pullback

$\textstyle{D\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f^{*}g}$$\scriptstyle{g^{*}f}$$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{B.}$

The assignment
$\textstyle{{P}^{\forall_{\mathsf{f}}}\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
is called the $\mathcal{D}$-universal completion of $P$. As before, when
$\mathcal{D}$ is the class of all the morphisms of the base category, we will
speak of full universal completion, and we will use the notation
$\textstyle{{P}^{\forall_{\mathsf{f}}}\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$.
Moreover, when $\mathcal{D}$ is the class of all product projections, we will
speak of pure universal completion, and we will use the notation
$\textstyle{{P}^{\forall}\colon\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$.

######  Theorem 3.8 ([40]).

The doctrine $P^{\forall_{\mathcal{D}}}$ is $\mathcal{D}$-universal. Moreover,
for every doctrine $P$ we have a canonical inclusion
$\eta_{P}^{\forall_{\mathcal{D}}}\colon P\to P^{\forall_{\mathcal{D}}}$ such
that, for every morphism of doctrines $\mathfrak{L}\colon P\to R$, where $R$
is $\mathcal{D}^{\prime}$-universal and the functor between the bases sends
arrows of $\mathcal{D}$ into arrows of $\mathcal{D}^{\prime}$, there exists a
unique (up to isomorphism) universal morphism doctrine (i.e. preserving
universal quantifiers along $\mathcal{D}$) such that the diagram

$\textstyle{P^{\forall_{\mathcal{D}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{P}^{\forall_{\mathcal{D}}}}$$\scriptstyle{\mathfrak{L}}$$\textstyle{R}$

commutes.

######  Remark 3.9.

Notice that the previous free completions, in particular, the pure and the
full existential completions, have been proved to be related to the so-called
regular and exact completions of a category with finite limits [6, 7]. We
refer to [32] and [31] for a precise analysis and characterization of these
results.

Now that we recalled both basic concepts of computability and the tools we
need from Lawvere doctrines we can start on the computability concepts we want
to categorify here. First we recall Medvedev reducibility and show it can be
reformulated as a Medvedev doctrine.

##  4\. Medvedev doctrines

The notion of Medvedev reducibility was introduced in the 50s, associated to a
calculus of mathematical problems111Recently de Paiva and Da Silva showed that
Kolmogorov problems can be seen as a variant of the Dialectica construction
[9]. in the style of Kolmogorov [22], and now it is well established in the
computability literature. We briefly introduce the main notions and
definitions on the topic. For a more thorough presentation, the reader is
referred to [39, 15].

A set $A\subseteq\mathbb{N}^{\mathbb{N}}$ is sometimes called a _mass
problem_. The intuition is that a mass problem corresponds to the set of
solutions for a specific computational problem. For example, the problem of
deciding membership in a particular $P\subseteq\mathbb{N}$ corresponds to the
mass problem $\\{\chi_{P}\\}$, where $\chi_{P}$ is the characteristic function
of $P$. Similarly, the problem of enumerating $P$ corresponds to the family
$\\{f\colon\mathbb{N}\to P:f\text{ is surjective}\\}$.

While Medvedev reducibility is usually defined in the context of Type-$2$
computability, we can give a slightly more general definition in the context
of PCAs.

######  Definition 4.1 (Medvedev reducible set).

Let $\mathbb{A}$ be a PCA and let $\mathbb{A}^{\prime}$ be an elementary sub-
PCA of $\mathbb{A}$. If $A,B\subseteq\mathbb{A}$, we say that $A$ is Medvedev
reducible to $B$, and write $A\leq_{\mathrm{M}}B$, if there is an effective
functional $\Phi\in\mathbb{A}^{\prime}$ such that $\Phi(B)\subseteq A$, i.e.
$(\forall b\in B)(\Phi(b)\in A)$.

The notion of Medvedev reducibility induces a preorder on the powerset of
$\mathbb{A}$, whose quotient is the _Medvedev lattice_. In the following,
whenever there is no ambiguity, we identify a degree with any of its
representatives.

We will now introduce a _Medvedev doctrine_ that generalizes the notion of
Medvedev reducibility. Intuitively, the Medvedev doctrine maps every singleton
$X$ to an isomorphic copy of the Medvedev lattice. However, if $X$ is not a
singleton, we obtain a somewhat different structure, corresponding to having
several Medvedev reductions all witnessed by the same map.

To define the Medvedev doctrine we first introduce the _Turing doctrine_.

######  Definition 4.2.

Let $\mathbb{A}$ be a PCA and $\mathbb{A}^{\prime}$ be an elementary sub-PCA.
We can define a functor
$\textstyle{\mathfrak{T}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
mapping a set $X$ to the set $\mathbb{A}^{X}$ of functions from $X$ to
$\mathbb{A}$. Given two elements $\alpha,\beta\in\mathfrak{T}(X)$, we define
$\alpha\leq_{\mathsf{T}}\beta$ if there exists an element
$\overline{a}\in\mathbb{A}^{\prime}$ such that for every $x\in X$ we have that
$\overline{a}\cdot\beta(x)$ is defined and
$\overline{a}\cdot\beta(x)=\alpha(x)$. The functor
$\textstyle{\mathfrak{T}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
is called Turing doctrine.

######  Remark 4.3.

The name “Turing doctrine” is motivated by the fact that, when working with
Kleene’s second model, then $\mathfrak{T}(1)$ can be identified with
$\mathbb{N}^{\mathbb{N}}$, and the reduction $\alpha\leq_{\mathsf{T}}\beta$
holds whenever there is a computable functional $\Phi$ such that
$\Phi(\beta)=\alpha$, i.e. $(\forall n)(\Phi(\beta)(n)=\alpha(n))$. This
corresponds precisely to the notion of Turing reducibility between functions
$\mathbb{N}\to\mathbb{N}$.

Notice also that, in the previous example, it is important to consider
Kleene’s second model. Indeed, if we instead work with Kleene’s first model,
$\mathfrak{T}(1)$ would be trivial (all numbers are computable) and
$\mathfrak{T}(\mathbb{N})$ would give rise to a somewhat unnatural notion of
reducibility: given $f,g\colon\mathbb{N}\to\mathbb{N}$, $f\leq_{\mathsf{T}}g$
iff there is a computable functional $\Phi$ such that $(\forall
n)(\Phi(g(n))=f(n))$. This is clearly a stronger notion than Turing
reducibility (only the value of $g(n)$ is needed to compute $f(n)$), but it is
incomparable with (weak)-truth table reducibility (it is not hard to build
$f,g$ such that $f\leq_{\mathsf{T}}g$ but the use of the computations
$\Phi(g(n))$ cannot be computably bounded).

######  Definition 4.4 (Medvedev doctrine).

Given a PCA $\mathbb{A}$ with elementary sub-PCA $\mathbb{A}^{\prime}$, we
define the Medvedev doctrine
$\textstyle{\mathfrak{M}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
over $\mathsf{Set}$ as follows: for every set $X$ and every pair of functions
$\varphi,\psi$ in $\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})^{X}$, we
define

$\displaystyle\varphi\leq_{\mathrm{M}}\psi:\iff$
$\displaystyle(\exists\overline{a}\in\mathbb{A}^{\prime})(\forall x\in
X)(\forall b\in\psi(x))(\exists a\in\varphi(x))(\overline{a}\cdot b=a)$
$\displaystyle\iff$
$\displaystyle(\exists\overline{a}\in\mathbb{A}^{\prime})(\forall x\in
X)(\overline{a}\cdot\psi(x)\subseteq\varphi(x)).$

This preorder induces an equivalence relation on functions in
$\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})^{X}$. The poset
$\mathfrak{M}(X)$ is defined as the quotient of
$\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})^{X}$ by the equivalence
relation generated by $\leq_{\mathrm{M}}$. The partial order on the
equivalence classes $[\varphi]$ is the one induced by the Medvedev order
$\leq_{\mathrm{M}}$. Moreover, given a function $f\colon X\to Y$, the functor
$\mathfrak{M}_{f}\colon\mathfrak{M}(Y)\to\mathfrak{M}(X)$ is defined as
$\mathfrak{M}_{f}(\psi):=\psi\circ f$.

Observe that, when working with Kleene’s second PCA, if $X$ is a singleton
then $\mathfrak{M}(X)$ corresponds exactly to the Medvedev degrees. For an
arbitrary set $X$, the reduction $\varphi,\psi\in\mathfrak{M}(X)$ corresponds
to a uniform Medvedev reducibility between $\varphi(x)$ and $\psi(x)$, where
$x\in X$. In particular, if $X\subseteq\mathbb{N}^{\mathbb{N}}$, we can think
of $\varphi$ and $\psi$ as computational problems on the Baire space. In this
case, the reduction $\varphi\leq_{\mathrm{M}}\psi$ corresponds to a strong
Weihrauch reduction where the forward functional is simply the identity
function. We will discuss strong Weihrauch reducibility and its connections
with the Medvedev doctrine more in details in Sections 5.1, 6.

We also show that, for every $X$, $\mathfrak{M}(X)$ is a distributive lattice
with $\bot=\\{\mathbb{A}\\}$ and $\top=\emptyset$, where the join and the meet
of the lattice are induced respectively by the following operation on mass
problems:

  * •

$A\lor B:=\\{\langle a,b\rangle:a\in A\text{ and }b\in B\\}$,

  * •

$A\land B:=A\sqcup B=\\{(0)\smash{\raisebox{3.87495pt}{$\smallfrown$}}a:a\in
A\\}\cup\\{(1)\smash{\raisebox{3.87495pt}{$\smallfrown$}}b:b\in B\\}$, where
$(n)\smash{\raisebox{3.87495pt}{$\smallfrown$}}f(0):=n$ and
$(n)\smash{\raisebox{3.87495pt}{$\smallfrown$}}f(i+1):=f(i)$.

Next we want to show that the lattice of Medvedev degrees is not a Heyting
algebra (see [39, Thm. 9.2]) but only a co-Heyting algebra (i.e. a Brouwer
algebra, see [39, Thm. 9.1]), where the subtraction operation is defined as
$A\backslash B:=\min\\{C:B\leq A\lor B\\}$. In other words, this subtraction
is an ‘implication’ with respect to the join of the lattice.

######  Proposition 4.5 (Medvedev co-Heyting algebra).

For every set $X$, $\mathfrak{M}(X)$ is a co-Heyting algebra, where:

  1. (1)

$\bot:=x\mapsto\mathbb{A}$

  2. (2)

$\top:=x\mapsto\emptyset$;

  3. (3)

$(\varphi\wedge\psi)(x):=\\{\langle
p_{1},a\rangle:a\in\varphi(x)\\}\cup\\{\langle p_{2},b\rangle:b\in\psi(x)\\}$,
where $p_{1},p_{2}$ are two fixed (different) elements in
$\mathbb{A}^{\prime}$.

  4. (4)

$(\varphi\vee\psi)(x):=\\{\langle a,b\rangle:a\in\varphi(x)\text{ and
}b\in\psi(x)\\}$;

  5. (5)

$(\varphi\backslash\psi)(x):=\\{c\in\mathbb{A}:(\forall b\in\psi(x))(c\cdot
b\in\varphi(x))\\}$.

###### Proof.

This proposition can be proved essentially the same way one proves that the
Medvedev degrees form a co-Heyting algebra (see [39, Thm. 1.3]). Let
$\varphi,\psi\in\mathfrak{M}(X)$.

  1. (1)

The reduction $\bot\leq_{\mathrm{M}}\varphi$ is witnessed by the identity
functional.

  2. (2)

The reduction $\varphi\leq_{\mathrm{M}}\top$ is trivially witnessed by any
$\overline{a}\in\mathbb{A}^{\prime}$, as the quantification on $b\in\top(x)$
is vacuously true.

  3. (3)

The reductions $\varphi\land\psi\leq_{\mathrm{M}}\varphi$ and
$\varphi\land\psi\leq_{\mathrm{M}}\psi$ are witnessed respectively by the maps
$a\mapsto\langle p_{1},a\rangle$ and $b\mapsto\langle p_{2},b\rangle$.
Moreover, if $\rho\leq_{\mathrm{M}}\varphi$ via $a_{\varphi}$ and
$\rho\leq_{\mathrm{M}}\psi$ via $a_{\psi}$ then the reduction
$\rho\leq_{\mathrm{M}}\varphi\land\psi$ is witnessed by the map that, upon
input $\langle p,c\rangle$, if $p=p_{1}$ returns $a_{\varphi}\cdot c$,
otherwise returns $a_{\psi}\cdot c$.

  4. (4)

The reductions $\varphi\leq_{\mathrm{M}}\varphi\lor\psi$ and
$\psi\leq_{\mathrm{M}}\varphi\lor\psi$ are witnessed by the projections.
Moreover, if $\varphi\leq_{\mathrm{M}}\rho$ via $a_{\varphi}$ and
$\psi\leq_{\mathrm{M}}\rho$ via $a_{\psi}$ then
$\varphi\lor\psi\leq_{\mathrm{M}}\rho$ is witnessed by the map
$x\mapsto\langle a_{\varphi}\cdot x,a_{\psi}\cdot x\rangle$.

  5. (5)

We need to show that, for every $\rho$,
$\varphi\backslash\psi\leq_{\mathrm{M}}\rho\iff\varphi\leq_{\mathrm{M}}\psi\lor\rho$.
To prove the left-to-right implication, observe that if
$\overline{a}\in\mathbb{A}^{\prime}$ witnesses the reduction
$\varphi\backslash\psi\leq_{\mathrm{M}}\rho$, then, for every $\langle
b,d\rangle\in(\psi\lor\rho)(x)$, $\overline{a}\cdot
d\in(\varphi\backslash\psi)(x)$, and therefore $(\overline{a}\cdot d)\cdot
b\in\varphi(x)$. To prove the right-to-left implication, notice that if
$\overline{b}$ witnesses $\varphi\leq_{\mathrm{M}}\psi\lor\rho$, then, by
definition, for every $\langle b,c\rangle\in(\psi\lor\rho)(x)$,
$\overline{b}\cdot\langle b,c\rangle\in\varphi(x)$. This implies that the map
$b\mapsto\overline{b}\cdot\langle b,c\rangle\in(\varphi\backslash\psi)(x)$,
therefore concluding the proof. ∎

Now we want to show some structural properties of Medvedev doctrines. Using
the two theorems we recalled from previous work, we can show:

######  Proposition 4.6.

The Medvedev doctrine
$\textstyle{\mathfrak{M}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
is a full universal and pure existential doctrine. In particular, for every
function $f\colon X\to Y$, the morphism
$\forall_{f}\colon\mathfrak{M}(X)\to\mathfrak{M}(Y)$ sending an element
$\varphi\in\mathfrak{M}(X)$ to the element
$\forall_{f}(\varphi)\in\mathfrak{M}(Y)$ defined as

$\forall_{f}(\varphi)(y):=\bigcup_{x\in f^{-1}(y)}\varphi(x)$

is right adjoint to $\mathfrak{M}_{f}$, i.e.
$\psi\leq_{\mathrm{M}}\forall_{f}(\varphi)\iff\mathfrak{M}_{f}(\psi)\leq_{\mathrm{M}}\varphi$
for any $\psi\in\mathfrak{M}(Y)$ and $\varphi\in\mathfrak{M}(X)$.

Similarly, if $f$ is surjective then the assignment

$\exists_{f}(\varphi)(y):=\bigcap_{x\in f^{-1}(y)}\varphi(x)$

determines a left adjoint to $\mathfrak{M}_{f}$, i.e.
$\exists_{f}(\varphi)\leq_{\mathrm{M}}\psi\iff\varphi\leq_{\mathrm{M}}\mathfrak{M}_{f}(\psi)$
for any $\psi\in\mathfrak{M}(Y)$ and $\varphi\in\mathfrak{M}(X)$.

###### Proof.

This is essentially a definition-chasing exercise. Let us first show that, for
every $\psi\in\mathfrak{M}(Y)$ and $\varphi\in\mathfrak{M}(X)$,
$\psi\leq_{\mathrm{M}}\forall_{f}(\varphi)\iff\mathfrak{M}_{f}(\psi)\leq_{\mathrm{M}}\varphi$.
Assume first that the reduction $\psi\leq_{\mathrm{M}}\forall_{f}(\varphi)$ is
witnessed by $\overline{a}\in\mathbb{A}^{\prime}$. The same $\overline{a}$
witnesses $\mathfrak{M}_{f}(\psi)\leq_{\mathrm{M}}\varphi$: indeed, for every
$x\in X$ and every $a\in\varphi(x)$, we have $a\in\forall_{f}(\varphi)(f(x))$,
and therefore $\overline{a}\cdot a\in\psi(f(x))=\mathfrak{M}_{f}(\psi)(x)$. On
the other hand, assume $\overline{b}$ witnesses
$\mathfrak{M}_{f}(\psi)\leq_{\mathrm{M}}\varphi$. For every $y\in Y$, if
$b\in\forall_{f}(\varphi)(y)$ then $b\in\varphi(x)$ for some $x\in f^{-1}(y)$.
In particular, $\overline{b}\cdot b\in\mathfrak{M}_{f}(\psi)(x)=\psi(y)$, i.e.
$\overline{b}$ witnesses $\psi\leq_{\mathrm{M}}\forall_{f}(\varphi)$.

The second part of the statement is proved analogously. Assume first that
$\exists_{f}(\varphi)\leq_{\mathrm{M}}\psi$ is witnessed by $\overline{c}$.
Fix $x\in X$ and $a\in\mathfrak{M}_{f}(\psi)(x)=\psi(f(x))$. In particular,
$\overline{c}\cdot a\in\exists_{f}(\varphi)(f(x))$, and hence
$\overline{c}\cdot a\in\varphi(x)$. Finally, assume $\overline{d}$ witnesses
$\varphi\leq_{\mathrm{M}}\mathfrak{M}_{f}(\psi)$, and let $y\in Y$ and
$b\in\psi(y)$. Since $f$ is surjective, there is $x\in X$ s.t. $f(x)=y$.
Moreover, for every $x\in f^{-1}(y)$ we have $b\in\psi(f(x))$ and, hence,
$\overline{d}\cdot b\in\varphi(x)$. This implies that $\overline{d}\cdot
b\in\bigcap_{x\in f^{-1}(y)}\varphi(x)=\exists_{f}(\varphi)(y)$. ∎

The rest of this section is devoted to studying abstract universal properties
of Medvedev doctrines.

######  Theorem 4.7 (Medvedev isomorphism).

Let
$\textstyle{\mathfrak{M}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
be the Medvedev doctrine for a given PCA $\mathbb{A}$. Then we have the
isomorphism of full universal doctrines

$\mathfrak{M}\equiv{\mathfrak{T}}^{\forall_{\mathsf{f}}}.$

In particular, for every set $X$, the map

$(f,\alpha)\mapsto\alpha\circ f^{-1}$

is a surjective (pre)order homomorphism between
$({\mathfrak{T}}^{\forall_{\mathsf{f}}}(X),\leq_{\forall_{\mathsf{f}}})$ and
$(\mathfrak{M}(X),\leq_{\mathrm{M}})$.

###### Proof.

Observe that the full universal completion
${\mathfrak{T}}^{\forall_{\mathsf{f}}}$ of $\mathfrak{T}$ can be described as
follows:

  * •

${\mathfrak{T}}^{\forall_{\mathsf{f}}}(X)=\\{(f,\alpha):f\colon Y\to X\text{
and }\alpha\in\mathfrak{T}(Y)\\},$

  * •

if $f\colon Y\to X$, $\alpha\in\mathfrak{T}(Y)$, $g\colon Z\to X$, and
$\beta\in\mathfrak{T}(Z)$, then

$(f,\alpha)\leq_{\forall_{\mathsf{f}}}(g,\beta)\iff(\exists h\colon Z\to
Y)((\forall z\in Z)(g(z)=f\circ h(z))\text{ and
}(\mathfrak{T})_{h}(\alpha)\leq_{\mathsf{T}}\beta).$

In other words, $(f,\alpha)\leq_{\forall_{\mathsf{f}}}(g,\beta)$ if and only
if there are $h\colon Z\to Y$ and $\overline{a}\in\mathbb{A}$ such that the
following diagram commutes

${Y}$${Z}$${X}$${\mathbb{A}}$${\mathbb{A}}$$\scriptstyle{f}$$\scriptstyle{\alpha}$$\scriptstyle{g}$$\scriptstyle{h}$$\scriptstyle{\beta}$$\scriptstyle{\overline{a}}$

If we define $\varphi:=\alpha\circ f^{-1}$ and $\psi:=\beta\circ g^{-1}$. we
obtain the following diagram:

${Y}$${Z}$${X}$${\mathbb{A}}$${\mathbb{A}}$$\scriptstyle{f}$$\scriptstyle{\alpha}$$\scriptstyle{g}$$\scriptstyle{h}$$\scriptstyle{\beta}$$\scriptstyle{\varphi}$$\scriptstyle{\psi}$$\scriptstyle{\overline{a}}$

where $\varphi$ and $\psi$ are represented as double arrows to stress the fact
that they are maps into $\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})$.

Let us first show that $(f,\alpha)\leq_{\forall_{\mathsf{f}}}(g,\beta)$
implies $\varphi\leq_{\mathrm{M}}\psi$. Fix two witnesses $h\colon Z\to Y$ and
$\overline{a}\in\mathbb{A}^{\prime}$ for
$(f,\alpha)\leq_{\forall_{\mathsf{f}}}(g,\beta)$ and fix $x\in X$. If
$x\notin\operatorname{ran}(g)$ then $\psi(x)=\emptyset$, hence there is
nothing to prove. Assume therefore that $x\in\operatorname{ran}(g)$. By
definition, $\psi(x)=\beta(g^{-1}(x))\neq\emptyset$. Fix $b\in\psi(x)$ and let
$z\in g^{-1}(x)$ be s.t. $\beta(z)=b$. Since
$(f,\alpha)\leq_{\forall_{\mathsf{f}}}(g,\beta)$, we can write

$\overline{a}\cdot b=\overline{a}\cdot\beta(z)=\alpha\circ h(z)=\alpha(y),$

for some $y\in f^{-1}(x)$. In particular, $\alpha(y)\in\varphi(x)$, and
therefore $\overline{a}$ witnesses $\varphi\leq_{\mathrm{M}}\psi$.

Let us now prove the other direction. Let $\overline{b}\in\mathbb{A}^{\prime}$
be a witness for $\varphi\leq_{\mathrm{M}}\psi$. Fix $z\in Z$. Clearly,
letting $x_{z}:=g(z)$, $\psi(x_{z})\neq\emptyset$. Moreover,
$\psi(x_{z})\neq\emptyset$ implies
$\varphi(x_{z})=\alpha(f^{-1}(x_{z}))\neq\emptyset$ (as
$\overline{b}\cdot\psi(x_{z})\subseteq\varphi(x_{z})$). We define $h$ as a
choice function that maps $z$ to some $y\in f^{-1}(x_{z})$ such that
$\alpha(y)\in\overline{b}\cdot\psi(x_{z})$. Observe that $h$ is well-defined
as if $a\in\overline{b}\cdot\psi(x_{z})$ then $a=\alpha(y)$ for some $y\in
f^{-1}(x_{z})$. This also shows that $h$ and $\overline{b}$ witness
$(f,\alpha)\leq_{\forall_{\mathsf{f}}}(g,\beta)$.

Finally, to show that the homomorphism is surjective it is enough to notice
that every $\varphi\colon X\to\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})$
is the image of the pair $(\pi_{X},\pi_{\mathbb{A}})$, where $Y:=\\{(x,a)\in
X\times\mathbb{A}:a\in\varphi(x)\\}$, and $\pi_{X}\colon Y\to X$ and
$\pi_{\mathbb{A}}\colon Y\to\mathbb{A}$ are the two projections. ∎

In other words, when working with Kleene’s second model, the Medvedev degrees
are isomorphic to the full universal completion of the Turing doctrine.

######  Remark 4.8.

Notice that, when we consider a PCA $\mathbb{A}$ and the trivial elementary
sub-PCA given by $\mathbb{A}$ itself, we have that the Medvedev doctrine
$\textstyle{\mathfrak{M}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
can be presented as the functor obtained by composing the realizability
doctrine
$\textstyle{\mathcal{R}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
defined in 3.4 with the op-functor
$(-)^{\operatorname{op}}:\mathsf{Pos}\to\mathsf{Pos}$ inverting the order of
posets.

Since it is known that the fibres of the realizability doctrine have the
Heyting structure, this presentation provides, for example, an abstract
explanation of the co-Heyting structure of the fibres of Medvedev doctrines
presented in 4.5.

Moreover, as it happens for the realizability triposes, notice that the
Medvedev doctrine
$\textstyle{\mathfrak{M}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
can be equivalently presented in a second equivalent way via the well-known
embedding (called _constant objects functor_)
$\nabla:\mathsf{Set}\to\mathsf{RT}(\mathbb{A}^{\prime},\mathbb{A})$ of the
category of sets into a (relative) realizability topos (see e.g. [46]). We
also refer to [13] for a careful analysis and generalization of this approach
to triposes. In particular, the doctrine $\mathfrak{M}$ happens to be
equivalent to the functor mapping a given set $X$ into the poset given by
$\mathsf{Sub}(\nabla(X))^{\operatorname{op}}$.

In the specific case of the _Kleene-Vesley topos_
$\mathsf{RT}(\mathcal{K}_{2}^{rec},\mathcal{K}_{2})$ (see for example [46, p.
279] and the references therein) the fact that the poset given by
$\mathsf{Sub}(\nabla(1))^{\operatorname{op}}$ provides exactly the Medvedev
lattice has been already observed in [46, p. 280].

###  4.1. Muchnik Doctrines

Using a very similar strategy, we now show that the Muchnik lattice is
isomorphic to the full universal completion of a doctrine. The notion of
_Muchnik reducibility_ formally dates back to 1963 (but it was probably known
earlier) and can be thought of as the non-uniform version of Medvedev
reducibility. More precisely, given two mass problems
$P,Q\subseteq\mathbb{N}^{\mathbb{N}}$, we say that $P$ is Muchnik reducible to
$Q$, and write $P\leq_{w}Q$, if for every $q\in Q$ there is a functional
$\Phi$ such that $\Phi(q)\in P$. In other words, $P\leq_{w}Q$ if every element
of $Q$ computes some element of $P$. Muchnik reducibility is sometimes called
“weak reducibility” (which motivates the choice of the symbol $\leq_{w}$) to
contrast with Medvedev reducibility, sometimes called “strong reducibility”
[15].

Similarly to the Medvedev degrees, the Muchnik degrees form a distributive
lattice, where the join and the meet operations are induced by the same
operations on subsets of $\mathbb{N}^{\mathbb{N}}$ that induce the join and
the meet in the Medvedev degrees. Unlike the Medvedev lattice, the Muchnik
lattice is both a Heyting and a co-Heyting algebra [15, Prop. 4.3 and 4.7].

######  Definition 4.9 (Muchnik doctrine of singletons).

Let $\mathbb{A}$ be a PCA and let $\mathbb{A}^{\prime}$ be an elementary sub-
PCA. We can define a doctrine
$\textstyle{\mathbb{A}_{w}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
mapping a set $X$ to the set $\mathbb{A}^{X}$ of functions from $X$ to
$\mathbb{A}$. Given two elements $\alpha,\beta\in\mathbb{A}_{w}(X)$, we define
$\alpha\leq_{\mathsf{dw}}\beta$ if

$(\forall x\in
X)(\exists\overline{a}\in\mathbb{A}^{\prime})(\overline{a}\cdot\beta(x)=\alpha(x)).$

The functor
$\textstyle{\mathbb{A}_{w}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
is called Muchnik doctrine of singletons.

Observe that the order $\leq_{\mathsf{dw}}$ is just the non-uniform version of
the order $\leq_{\mathsf{T}}$ induced by the Turing doctrine. In particular,
if $X$ is a singleton then $\mathbb{A}_{w}(1)=\mathfrak{T}(1)$. This implies
that Remark 4.3 applies to the Muchnik doctrine of singletons as well. On the
other hand, both $\mathbb{A}_{w}(1)$ and $\mathbb{A}_{w}(\mathbb{N})$ are
trivial when working with Kleene’s first model.

######  Definition 4.10 (Muchnik doctrine).

We define the Muchnik doctrine
$\textstyle{\mathfrak{M}_{w}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
over $\mathsf{Set}$ as follows. For every set $X$ and every pair of functions
$\varphi,\psi\in\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})^{X}$, we define

$\varphi\leq_{w}\psi:\iff(\forall x\in X)(\forall
b\in\psi(x))(\exists\overline{a}\in\mathbb{A}^{\prime})(\overline{a}\cdot
b\in\varphi(x)).$

This preorder induces an equivalence relation on functions in
$\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})^{X}$. The doctrine
$\mathfrak{M}_{w}(X)$ is defined as the quotient of
$\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})^{X}$ by the equivalence
relation generated by $\leq_{w}$. The partial order on the equivalence classes
$[\varphi]$ is the one induced by $\leq_{w}$.

######  Proposition 4.11.

For every set $X$, $\mathfrak{M}_{w}(X)$ is both a Heyting and a co-Heyting
algebra, where:

  1. (1)

$\bot:=x\mapsto\mathbb{A}$

  2. (2)

$\top:=x\mapsto\emptyset$;

  3. (3)

$(\varphi\wedge\psi)(x):=\\{\langle
p_{1},a\rangle:a\in\varphi(x)\\}\cup\\{\langle p_{2},b\rangle:b\in\psi(x)\\}$,
where $p_{1},p_{2}$ are two fixed (different) elements in
$\mathbb{A}^{\prime}$.

  4. (4)

$(\varphi\vee\psi)(x):=\\{\langle a,b\rangle:a\in\varphi(x)\text{ and
}b\in\psi(x)\\}$;

  5. (5)

$(\varphi\backslash\psi)(x):=\\{c\in\mathbb{A}:(\forall b\in\psi(x))(c\cdot
b\in\varphi(x))\\}$.

  6. (6)

$(\varphi\rightarrow\psi)(x):=\\{b\in\psi(x):(\forall\overline{a}\in\mathbb{A}^{\prime})(\overline{a}\cdot
b\notin\varphi(x))\\}$.

###### Proof.

The points (1)-(5) can be proved as in the proof of 4.5, so we only prove
point (6). The argument is a straightforward generalization of [15, Prop.
4.3]. We need to show that, for every $\rho$,
$\rho\leq_{w}\varphi\rightarrow\psi\iff\varphi\wedge\rho\leq_{w}\psi$. Observe
that,

$\displaystyle\rho\leq_{w}\varphi\rightarrow\psi$ $\displaystyle\iff(\forall
x\in X)(\forall
b\in(\varphi\rightarrow\psi)(x))(\exists\overline{a}\in\mathbb{A}^{\prime})(\overline{a}\cdot
b\in\rho(x))$ $\displaystyle\iff(\forall x\in X)(\forall
b\in\psi(x))((\forall\overline{a}\in\mathbb{A}^{\prime})(\overline{a}\cdot
b\notin\varphi(x))\Rightarrow(\exists\overline{b}\in\mathbb{A}^{\prime})(\overline{b}\cdot
b\in\rho(x)))$ $\displaystyle\iff(\forall x\in X)(\forall
b\in\psi(x))((\exists\overline{a}\in\mathbb{A}^{\prime})(\overline{a}\cdot
b\in\varphi(x))\lor(\exists\overline{b}\in\mathbb{A}^{\prime})(\overline{b}\cdot
b\in\rho(x)))$ $\displaystyle\iff(\forall x\in X)(\forall
b\in\psi(x))(\exists\overline{c}\in\mathbb{A}^{\prime})((\exists
a\in\varphi(x))(\overline{c}\cdot b=\langle p_{1},a\rangle)\lor(\exists
d\in\rho(x))(\overline{c}\cdot b=\langle p_{2},d\rangle))$
$\displaystyle\iff(\forall x\in X)(\forall
b\in\psi(x))(\exists\overline{c}\in\mathbb{A}^{\prime})(\overline{c}\cdot
b\in\varphi\wedge\rho(x))$
$\displaystyle\iff\varphi\wedge\rho\leq_{w}\psi.\qed$

It is straightforward to adapt the proof of 4.7 to show the following:

######  Theorem 4.12 (Muchnik isomorphism).

The Muchnik doctrine $\mathfrak{M}_{w}$ is isomorphic to the full universal
completion ${(\mathbb{A}_{w})}^{\forall_{\mathsf{f}}}$.

Observe that the Turing doctrine
$\textstyle{\mathfrak{T}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
can be embedded in the Muchnik doctrine of singletons
$\textstyle{\mathbb{A}_{w}\colon\mathsf{Set}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$.
Let us denote such a morphism of doctrines by
$\mathfrak{I}\colon\mathfrak{T}\to\mathbb{A}_{w}$. By 3.8 we can employ the
universal property of the full universal completion and conclude the following
corollary.

######  Corollary 4.13.

Let $\mathbb{A}$ be a given PCA and let $\mathbb{A}^{\prime}$ be an elementary
sub-PCA. Then there exists a morphism of full universal doctrines such that
the diagram

$\textstyle{\mathfrak{M}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathfrak{T}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{\mathfrak{T}}^{\forall_{\mathsf{f}}}}$$\scriptstyle{\mathfrak{I}}$$\textstyle{\mathbb{A}_{w}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{\mathbb{A}_{w}}^{\forall_{\mathsf{f}}}}$$\textstyle{\mathfrak{M}_{w}}$

commutes.

This corollary is the categorical version of how Medvedev (strong)
reducibility is the uniform version of Muchnik (weak) reducibility.

######  Remark 4.14.

Notice that the results and considerations presented for Muchnik doctrines
could be presented in a more general setting. In particular, if we consider
doctrines with pointwise order, e.g. Muchnik doctrines and localic doctrines,
the full universal completion of these doctrines is given precisely by the
doctrine of their pointwise domination order (Smyth order [37]). Intuitively,
the full universal completion can be seen as a generalization of the
construction of the Smyth preorder on the powerset of a given preorder.

##  5\. Weihrauch Doctrines

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. Weihrauch
reducibility provides a framework where to formalize questions like “which
theorems can be transformed continuously or computably into another?” [4].
This provides a purely topological or computational approach to
metamathematics that sheds new light on the nature of theorems. Given the
connection between Medvedev and Weihrauch reducibility, it is natural to ask
whether, with a similar approach as the one from the last section, we can also
describe Weihrauch reducibility as the completion of some existential
doctrine.

We start by recalling the main objects of interest of Weihrauch reducibility,
and by fixing the notation for the rest of this section:

######  Definition 5.1.

A (partial) multi-valued function from a set $X$ to a set $Y$, written as
$f:\subseteq X\rightrightarrows Y$, is a function $f\colon
X\to\raisebox{1.70717pt}{\Large$\wp$}(Y)$ into the powerset of $Y$. The domain
of $f$ is the set $\operatorname{dom}(f)=\\{x\in X:f(x)\neq\emptyset\\}$.
Whenever $f(x)$ is a singleton for every $x\in\operatorname{dom}(f)$, we write
$f(x)=y$ instead of $f(x)=\\{y\\}$.

It helps the intuition to think of multi-valued functions as computational
problems, namely instance-solution pairs, where a single problem instance can
have multiple solutions.

While Weihrauch reducibility is often introduced in the context of Type-$2$
computability, we will introduce it in the more general context of PCAs, as we
did for the Medvedev reducibility relation.

######  Definition 5.2 (Weihrauch reducibilty).

Let $\mathbb{A}$ be a PCA, $\mathbb{A}^{\prime}$ be an elementary sub-PCA of
$\mathbb{A}$ and let $f,g:\subseteq\mathbb{A}\rightrightarrows\mathbb{A}$ be
partial multi-valued functions on $\mathbb{A}$. We say that $f$ is Weihrauch
reducible to $g$, and write $f\leq_{\mathrm{W}}g$, if there are
$\overline{h},\overline{k}\in\mathbb{A}^{\prime}$ such that

$(\forall G\vdash g)(\overline{h}(\operatorname{id},G\overline{k})\vdash f),$

where
$\overline{h}(\operatorname{id},G\overline{k}):=p\mapsto\overline{h}\cdot\langle
p,G(\overline{k}\cdot p)\rangle$ and $G\vdash g$ means that
$G:\subseteq\mathbb{A}\to\mathbb{A}$ is such that, for every
$p\in\operatorname{dom}(g)$, $G(p)\in g(p)$. This corresponds to saying that
$G$ is a _realizer_ 222The notion of realizers will be introduced more
generally in 6.2 in the context of (multi-)represented spaces. The existence
of a realizer for every multi-valued function depends on a (relatively) weak
form of the axiom of choice. of $g$. The functionals
$\overline{k},\overline{h}$ are sometimes referred to as _forward_ and
_backward_ functional respectively.

To properly introduce a Lawvere doctrine abstracting the notion of Weihrauch
reducibility into the categorical setting, we start by defining a category
which will play the role of the base category of the doctrine.

######  Definition 5.3.

Let $\mathbb{A}$ be a PCA, and let $\mathbb{A}^{\prime}$ be an elementary sub-
PCA of $\mathbb{A}$. We say that a function $f\colon X\to Y$ is
$\mathbb{A}^{\prime}$-computable333This notation can be found in [3, Sec. 1].
if there exists an element $a\in\mathbb{A}^{\prime}$ such that for every
element $x\in X$, $a\cdot x\downarrow$ and $f(x)=a\cdot x$. We avoid
explicitly mentioning $\mathbb{A}^{\prime}$ and simply write _computable_
whenever the elementary sub-PCA is clear from the context.

Throuhgout this section, with a small abuse of notation, we will often replace
a computable function $f$ with the element of the elementary sup-PCA that
realizes it.

Observe that, since $\mathbb{A}^{\prime}$ is an _elementary_ sub-PCA of
$\mathbb{A}$, we have that the identity function is computable, and that the
composition of computable functions is well-behaved. Hence, we can define the
following category:

######  Definition 5.4.

Let $\mathbb{A}$ be a PCA, and let $\mathbb{A}^{\prime}$ be an elementary sub-
PCA of $\mathbb{A}$. We denote444The choice of the notation
$\mathsf{Mod}_{\mathsf{p}}$ is motivated by the fact that, as we will see
later in 6.9, $\mathsf{Mod}_{\mathsf{p}}$ is precisely the full subcategory of
the category of modest sets which are partitioned. by
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$ the category whose
objects are subsets $X\subseteq\mathbb{A}$. A morphism
$f\in\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})(X,Y)$ is a
computable function $f\colon X\to Y$.

######  Remark 5.5.

Notice that the category
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$ has finite
products. This follows from the fact that $\mathbb{A}^{\prime}$ is an
_elementary_ sub-PCA of $\mathbb{A}$, and hence all the standard operations of
pairing and projections, which allows us to define the categorical products,
are computable morphisms. In particular, the categorical product between
$X,Y\in\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$ is given by
the set $X\times Y:=\\{\langle x,y\rangle:x\in X\text{ and }y\in Y\\}$ and the
projections are the maps $\mathsf{fst},\mathsf{snd}$ defined after 2.2. We
also denote with $\overline{1}$ the terminal object of
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$, defined as
$\overline{1}:=\\{k\\}$, where $k$ is the identity functional (2.2).

For our purposes, it is convenient to rewrite the ordinary definition of
Weihrauch reducibility as follows:

######  Definition 5.6 (Weihrauch reducibility).

Let $X,Z$ be two object of
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$. Given two
functions $f\colon X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ and
$g\colon Z\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$,
$f\leq_{\mathrm{W}}g$ if and only if there is a computable function
$\overline{k}\colon X\to Z$ and an element
$\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall p\in X)(\forall q\in g(\overline{k}\cdot
p))(\overline{h}\cdot\langle p,q\rangle\in f(p)).$

It is well-known that there is a close connection between Weihrauch and
Medvedev reducibility. Indeed, if $f\leq_{\mathrm{W}}g$ via the functionals
$\overline{k}$ and $\overline{h}$, then $\overline{k}$ witnesses the reduction
$\operatorname{dom}(g)\leq_{\mathrm{M}}\operatorname{dom}(f)$. Besides, for
every $p\in\operatorname{dom}(f)$ there is a uniform continuous Medvedev
reduction between $f(p)$ and $g(\overline{k}\cdot p)$. Indeed, the map
$q\mapsto\overline{h}\cdot\langle p,q\rangle$ maps every element of
$g(\overline{k}\cdot p)$ to some element of $f(p)$. If the map $\overline{h}$
need not receive $p$ as part of its input, then $\overline{h}$ would witness a
uniform (computable) Medvedev reducibility between $f(p)$ and
$g(\overline{k}\cdot p)$. This stronger requirement leads to the notion of
_strong Weihrauch reducibility_ , which will be studied more in detail in the
next section.

Now we generalize the notion of Weihrauch reducibility similarly to what we
did for the Medvedev reducibility. To this end, we introduce the following
doctrine.

######  Definition 5.7 (elementary Weihrauch doctrine).

We define the elementary Weihrauch doctrine
$\textstyle{\mathfrak{eW}\colon\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
as follows: for every object $X$ of
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$, the objects
$\mathfrak{eW}(X)$ are functions $f\colon
X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$. For every pair of maps
$f,g$ in $\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{X}$, we define
$f\leq_{\mathsf{dW}}g$ iff there is $\overline{h}\in\mathbb{A}^{\prime}$ such
that

$(\forall p\in X)(\forall q\in g(p))(\overline{h}\cdot\langle p,q\rangle\in
f(p)).$

This preorder induces an equivalence relation on functions in
$\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{X}$. The doctrine
$\mathfrak{eW}(X)$ is defined as the quotient of
$\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{X}$ by the equivalence
relation generated by $\leq_{\mathsf{dW}}$. The partial order on the
equivalence class $[f]$ is the one induced by $\leq_{\mathsf{dW}}$. The action
of $\mathfrak{eW}$ on the morphisms of
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$ is defined by the
pre-composition.

Notice that a reduction $f\leq_{\mathsf{dW}}g$ corresponds to a Weihrauch
reducibility between $f$ and $g$ defined on the same set $X$, where the
forward functional is witnessed by the identity functional.

Observe that the doctrine $\mathfrak{eW}$ is well-defined as a functor between
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})^{\mathrm{op}}$ and
$\mathsf{Pos}$. Indeed, it is straightforward to check that, for every
$X,Z\in\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$, every
$f,g\in\mathfrak{eW}(X)$, and every morphism
$\overline{k}\in\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})(Z,X)$,
any function $\overline{h}\in\mathbb{A}^{\prime}$ witnessing
$f\leq_{\mathsf{dW}}g$ is a witness for
$f\circ\overline{k}=\mathfrak{eW}_{\overline{k}}(f)\leq_{\mathsf{dW}}\mathfrak{eW}_{\overline{k}}(g)=g\circ\overline{k}$.
While Weihrauch reductions are not, in general, preserved under pre-
composition, the reduction $f\leq_{\mathsf{dW}}g$ essentially establishes a
“layerwise” relation between $f$ and $g$, namely to solve $f(x)$ we only need
to look at $g(x)$. It is therefore apparent that this relation is not affected
by pre-compositions.

######  Proposition 5.8.

The elementary Weihrauch doctrine
$\textstyle{\mathfrak{eW}\colon\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
is a pure universal doctrine. In particular, for every product projection
$\pi_{Z}\colon X\times Z\to Z$, the morphism
$\forall_{\pi_{Z}}\colon\mathfrak{eW}(X\times Z)\to\mathfrak{eW}(Z)$ sending
an element $f\in\mathfrak{eW}(X\times Z)$ to the element
$\forall_{\pi_{Z}}(f)\in\mathfrak{eW}(Z)$ defined as

$\forall_{\pi_{Z}}(f)(z):=\bigcup_{x\in X}\left\\{\langle x,y\rangle:y\in
f(x,z)\right\\}$

is right-adjoint to $\mathfrak{eW}_{\pi_{Z}}(g)$, i.e. for every
$f\in\mathfrak{eW}(X\times Z)$ and $g\in\mathfrak{eW}(Z)$,

$g\leq_{\mathsf{dW}}\forall_{\pi_{Z}}(f)\iff\mathfrak{eW}_{\pi_{Z}}(g)\leq_{\mathsf{dW}}f.$

###### Proof.

Assume first that $g\leq_{\mathsf{dW}}\forall_{\pi_{Z}}(f)$ via
$\overline{a}$. Let $\overline{b}\in\mathbb{A}^{\prime}$ be defined as
$\overline{b}\cdot\langle\langle t,p\rangle,s\rangle:=\overline{a}\cdot\langle
p,\langle t,s\rangle\rangle$. We want to show that for every $(x,z)\in X\times
Z$,

$(\forall y\in f(x,z))(\overline{b}\cdot\langle\langle x,z\rangle,y\rangle\in
g\circ\pi_{Z}(x,z)=g(z)).$

To this end, fix $(x,z)\in X\times Z$. Since $f$ is total on $X\times Z$, we
only need to show that for every $y\in f(x,z)$,
$\overline{b}\cdot\langle\langle x,z\rangle,y\rangle\in g(z)$. This follows
immediately from the definition of $\overline{b}$, as
$g\leq_{\mathsf{dW}}\forall_{\pi_{Z}}(f)$ and $\langle
x,y\rangle\in\forall_{\pi_{Z}}(f)(z)$.

For the right-to-left direction, we proceed analogously: assume
$\mathfrak{eW}_{\pi_{Z}}(g)\leq_{\mathsf{dW}}f$ via $\overline{c}$. Define
$\overline{d}\cdot\langle p,\langle
t,s\rangle\rangle:=\overline{c}\cdot\langle\langle t,p\rangle,s\rangle$. To
show that $g\leq_{\mathsf{dW}}\forall_{\pi_{Z}}(f)$, simply notice that for
every $z\in Z$, and every $\langle x,y\rangle\in\forall_{\pi_{Z}}(f)(z)$, the
fact that $\mathfrak{eW}_{\pi_{Z}}(g)\leq_{\mathsf{dW}}f$ via $\overline{c}$
implies that $\overline{d}\cdot\langle z,\langle
x,y\rangle\rangle=\overline{c}\cdot\langle\langle
x,z\rangle,y\rangle\in\mathfrak{eW}_{\pi_{Z}}(g)(x,z)=g(z)$. ∎

Now we introduce the Weihrauch doctrine. To this end, we introduce first the
notion of _generalized Weihrauch predicate_.

######  Definition 5.9 (Weihrauch predicate).

A generalized Weihrauch predicate on $X\subseteq\mathbb{A}$ is a function

$F\colon X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{Y}$

for some $Y\subseteq\mathbb{A}$.

Given a generalized Weihrauch predicate $F$, we denote by $F_{x}\colon
Y\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ the function $F(x)$.
Moreover, with a small abuse of notation, we can write $F(x,y)$ for $F(x)(y)$.

######  Definition 5.10 (Weihrauch doctrine).

Given a PCA $\mathbb{A}$ with elementary sub-PCA $\mathbb{A}^{\prime}$, the
Weihrauch doctrine is the functor
$\textstyle{\mathfrak{W}\colon\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
that maps $X\subseteq\mathbb{A}$ to the preorder $\mathfrak{W}(X)$ defined as
follows:

  * •

objects are generalized Weihrauch predicates on $X$;

  * •

the partial order is given by the poset reflection of the preorder defined as
follows: let $Y,Z\subseteq\mathbb{A}$. For every $F\colon
X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{Y}$ and $G\colon
X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{Z}$, we say that
$F\leq_{\mathsf{W}}G$ if there exist a computable function $\overline{k}\colon
X\times Y\to Z$ and $\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall\langle x,y\rangle\in X\times Y)(\forall q\in
G(x,\overline{k}\cdot\langle x,y\rangle))(\overline{h}\cdot\langle\langle
x,y\rangle,q\rangle\in F(x,y)).$

Intuitively, if $F$ and $G$ are generalized Weihrauch predicates, the
reduction $F\leq_{\mathsf{W}}G$ can be seen as a uniform sequence of Weihrauch
reductions, one for each $x\in X$, all witnessed by the same reduction
functionals. Observe that the doctrine is well-defined as pre-composition with
a morphism $\overline{j}\colon W\to X$ preserves the reduction
$F\leq_{\mathsf{W}}G$.

The following result is immediate.

######  Theorem 5.11 (Weihrauch lattice).

The Weihrauch lattice is isomorphic to $\mathfrak{W}(\overline{1})$.

###### Proof.

By definition of Weihrauch doctrine, the objects of the poset
$\mathfrak{W}(\overline{1})$ can be identified with functions
$Y\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$. Moreover, if $F\colon
Y\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ and $G\colon
Z\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ are in
$\mathfrak{W}(\overline{1})$ then $F\leq_{\mathsf{W}}G$ iff there are a
computable function $\overline{k}\colon Y\to Z$ and
$\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall y\in Y)(\forall q\in G(\overline{k}\cdot
y))(\overline{h}\cdot\langle y,q\rangle\in F(y)),$

which corresponds to 5.6. ∎

In particular, when working with Kleene’s second model,
$\mathfrak{W}(\overline{1})$ yields precisely the classical Weihrauch degrees.

Now we show that the Weihrauch doctrine is isomorphic to the pure existential
completion of the elementary Weihrauch doctrine. Recall that, by definition,
the elements of ${\mathfrak{eW}}^{\exists}(X)$ are pairs of the form
$(\pi,f)$, where $\pi\colon X\times Y\to X$ is the projection on $X$ and
$f\in\mathfrak{eW}(X\times Y)$, i.e. $f\colon X\times
Y\to\raisebox{1.70717pt}{\Large$\wp$}^{*}{\mathbb{(}A)}$. Moreover,

$(\pi,f)\leq_{\exists}(\pi^{\prime},g)\iff(\exists\overline{k}\in\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})(X\times
Y,Z))(f\leq_{\mathsf{dW}}\mathfrak{eW}_{\langle\pi_{X},k\rangle}(g)),$

where $\mathfrak{eW}_{\langle\pi_{X},k\rangle}(g)\colon=(x,y)\mapsto
g(x,\overline{k}(x,y))$.

######  Theorem 5.12 (Weihrauch isomorphism).

The Weihrauch doctrine is isomorphic to the pure existential completion of the
elementary Weihrauch doctrine. In symbols:

$\mathfrak{W}\equiv{\mathfrak{eW}}^{\exists}.$

In particular, fixed a PCA $\mathbb{A}$ with elementary sub-PCA
$\mathbb{A}^{\prime}$, for every $X\subseteq\mathbb{A}$ the map

$(\pi_{X},f)\mapsto F$

where $F\colon X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{Y}$ is
defined as $F(x):=f(x,\cdot)$, is an isomorphism of posets between
$({\mathfrak{eW}}^{\exists}(X),\leq_{\exists})$ and
$(\mathfrak{W}(X),\leq_{\mathsf{W}})$.

###### Proof.

We first show that the assignment $(\pi_{X},f)\mapsto F$ preserves and
reflects the order. Let $(\pi,f)$ and $(\pi^{\prime},g)$ be two elements of
${\mathfrak{eW}}^{\exists}(X)$. By expanding the definition of
$\leq_{\mathsf{dW}}$ and writing $g(x,k(x,y))$ in place of
$\mathfrak{eW}_{\langle\pi_{X},k\rangle}(g)(x,y)$, we obtain that
$(\pi,f)\leq_{\exists}(\pi^{\prime},g)$ iff there is a morphism
$\overline{k}\colon X\times Y\to Z$ and $\overline{h}\in\mathbb{A}^{\prime}$
such that

$(\forall(x,y)\in X\times Y)(\forall q\in g(x,\overline{k}\cdot\langle
x,y\rangle))(\overline{h}\cdot\langle\langle x,y\rangle,q\rangle\in f(x,y))$

Let $F\colon X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{Y}$ and
$G\colon X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{Z}$ be the
images of $(\pi,f)$ and $(\pi^{\prime},g)$ respectively. Observe that, writing
$F(x,y)=f(x,y)$ (analogously for $G$) and substituting $F$ and $G$ in
($\star$), it is straightforward to check that
$(\pi,f)\leq_{\exists}(\pi^{\prime},g)$ iff $F\leq_{\mathsf{W}}G$ (see 5.10).

This shows that the embedding preserves and reflects the partial order.
Finally, it is easy to see that the map $(\pi_{X},f)\mapsto F$ is surjective,
since any function $H\colon
X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{V}$ can be obtained via
our embedding as the image of the pair $(\pi_{X},h)$, where $h\colon X\times
V\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ is defined as
$h(x,v):=H(x,v)$. Therefore, since the map is a surjective homomorphism of
posets which also reflects the order, we can conclude that it is an
isomorphism. ∎

###  5.1. Strong Weihrauch Doctrines

We now show that we can adapt the techniques of the previous section to
provide a categorical presentation of _strong Weihrauch reducibility_.

######  Definition 5.13 (Strong Weihrauch reducibilty).

Let $\mathbb{A}$ be a PCA, $\mathbb{A}^{\prime}$ be an elementary sub-PCA of
$\mathbb{A}$ and let $f,g:\subseteq\mathbb{A}\rightrightarrows\mathbb{A}$ be
partial multi-valued functions on $\mathbb{A}$. We say that $f$ is strongly
Weihrauch reducible to $g$, and write $f\leq_{\mathrm{sW}}g$, if there are
$\overline{h},\overline{k}\in\mathbb{A}^{\prime}$ such that

$(\forall G\vdash g)(\overline{h}G\overline{k}\vdash f).$

As anticipated, the intuition behind the strong Weihrauch reducibility is that
a Weihrauch reduction $f\leq_{\mathrm{W}}g$ is strong if the backward
functional $\overline{h}$ does not have access to the original input for $f$,
but only to the solution of $g$.

Analogously to what already observed in the context of Weihrauch reducibility,
if $\overline{h}$ and $\overline{k}$ witness the reduction
$f\leq_{\mathrm{sW}}g$ then $\overline{h}$ witnesses the reduction
$\operatorname{dom}(g)\leq_{\mathrm{M}}\operatorname{dom}(f)$. However, unlike
what happens in the case of Weihrauch reducibility, the backward functional
$\overline{k}$ now witnesses a uniform Medvedev reduction between $f(p)$ and
$g(\overline{k}\cdot p)$.

We observe that the results of the previous subsection can be adapted to show
that the strong Weihrauch degrees are isomorphic to the pure existential
completion of another doctrine. Again, it is convenient to rewrite the
ordinary definition of strong Weihrauch reducibility as follows:

######  Definition 5.14 (Strong Weihrauch reducibility).

Let $X,Z$ be two object of
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$. Given two
functions $f\colon X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ and
$g\colon Z\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ then
$f\leq_{\mathrm{sW}}g$ if and only if there is a computable function
$\overline{k}\colon X\to Z$ and an element
$\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall p\in X)(\forall q\in g(\overline{k}\cdot p))(\overline{h}\cdot q\in
f(p)).$

Now we adapt the definition of the (elementary) Weihrauch doctrine requiring
that the map $\overline{h}$ does not have access to the original input $p$.

######  Definition 5.15.

Given a PCA $\mathbb{A}$ with elementary sub-PCA $\mathbb{A}^{\prime}$, we
define the elementary strong Weihrauch doctrine
$\textstyle{\mathfrak{sW}\colon\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
as follows. For every $X\subseteq\mathbb{A}$ and every pair of functions
$f,g\in\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{X}$, we define
$f\leq_{\mathsf{dsW}}g$ iff there is $\overline{h}\in\mathbb{A}^{\prime}$ such
that

$(\forall p\in X)(\forall q\in g(p))(\overline{h}\cdot q\in f(p)).$

This preorder induces an equivalence relation on functions in
$\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{X}$. The doctrine
$\mathfrak{sW}(X)$ is defined as the quotient of
$\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{X}$ by the equivalence
relation generated by $\leq_{\mathsf{dsW}}$. The partial order on the
equivalence classes $[f]$ is the one induced by $\leq_{\mathsf{dsW}}$.

######  Definition 5.16 (Strong Weihrauch doctrine).

Given a PCA $\mathbb{A}$ with elementary sub-PCA $\mathbb{A}^{\prime}$, the
strong Weihrauch doctrine is the functor
$\textstyle{\mathfrak{SW}\colon\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
that maps $X\subseteq\mathbb{A}$ to the preorder $\mathfrak{SW}(X)$ defined as
follows:

  * •

objects are generalized Weihrauch predicates on $X$;

  * •

the partial order is given by the poset reflection of the preorder defined as
follows: let $Y,Z\subseteq\mathbb{A}$. We say that $F\leq_{\mathsf{sW}}G$,
where $F\colon X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{Y}$ and
$G\colon X\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{Z}$, if there
exists a computable function $\overline{k}\colon X\times Y\to Z$ and
$\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall\langle x,y\rangle\in X\times Y)(\forall q\in
G(x,\overline{k}\cdot\langle x,y\rangle))(\bar{h}\cdot q\in F(x,y)).$

In light of 5.11 and 5.12, the following results are straightforward:

######  Theorem 5.17.

The strong Weihrauch lattice is isomorphic to $\mathfrak{SW}(\overline{1})$.

In particular, the (classical) strong Weihrauch degrees correspond to
$\mathfrak{SW}(\overline{1})$, when working with Kleene’s second model.

######  Theorem 5.18 (Strong Weihrauch isomorphism).

Let $\mathbb{A}$ be a PCA and let $\mathbb{A}^{\prime}$ be an elementary sub-
PCA of $\mathbb{A}$. The strong Weihrauch doctrine is isomorphic to the pure
existential completion of the elementary strong Weihrauch doctrine. In
symbols:

$\mathfrak{SW}\equiv{\mathfrak{sW}}^{\exists}.$

##  6\. Generalizations of Weihrauch reducibility

Weihrauch reducibility is often introduced in the more general context of
partial multi-valued functions on represented spaces . We now briefly recall a
few definitions in the context of computable analysis. For a more thorough
presentation, the reader is referred to [5, 48].

######  Definition 6.1 (represented space).

A represented space is a pair $(X,\delta_{X})$, where $X$ is a set and
$\delta_{X}:\subseteq\mathbb{N}^{\mathbb{N}}\to X$ is a subjective (partial)
map called a representation map.

For any given $x$ in $X$, the set $\delta_{X}^{-1}(x)$ is the set of
$\delta_{X}$-names or $\delta_{X}$-codes for $x$. We avoid mentioning
explicitly the representation map whenever there is no ambiguity.

######  Definition 6.2 (realizer).

Let $f:\subseteq X\rightrightarrows Y$ be a multi-valued function between the
represented spaces $(X,\delta_{X})$ and $(Y,\delta_{Y})$. A realizer $F$ for
$f$ (we write $F\vdash f$) is a function
$F:\subseteq\mathbb{N}^{\mathbb{N}}\to\mathbb{N}^{\mathbb{N}}$ such that for
all $p$ in the domain of $(f\circ\delta_{X})$ we have that
$(\delta_{Y}(F(p))\in f(\delta_{X}(p)))$.

Realizers are useful as they help us transfer properties of functions on the
Baire space (such as computability or continuity) to multi-valued functions on
the represented spaces. 5.2 can be immediately extended to the case of multi-
valued functions on represented spaces. We rewrite the definition here for the
sake of readability.

######  Definition 6.3 (Weihrauch reducibility for represented spaces).

Let $X,Y,Z,W$ be represented spaces and let $f:\subseteq X\rightrightarrows Y$
$g:\subseteq Z\rightrightarrows W$ be partial multi-valued functions. We say
that $f$ is Weihrauch reducible to $g$, and write $f\leq_{\mathrm{W}}g$, if
there are two computable functionals $\Phi,\Psi\in\mathbb{A}^{\prime}$ s.t.

$(\forall G\vdash g)(\overline{h}(\operatorname{id},G\overline{k})\vdash f),$

where
$\overline{h}(\operatorname{id},G\overline{k}):=p\mapsto\overline{h}\cdot\langle
p,G(\overline{k}\cdot p)\rangle$ and $G\vdash g$ means that $G$ is a realizer
of $g$ (as defined in 6.2).

Observe the notion of Weihrauch reducibility for represented spaces depends on
the representation maps. Indeed, expanding the previous definition, we obtain
that $f\leq_{\mathrm{W}}g$ iff if there are two computable functionals
$\Phi,\Psi\in\mathbb{A}^{\prime}$ s.t.

$(\forall
p\in\operatorname{dom}(f\circ\delta_{X}))(\Phi(p)\in\operatorname{dom}(g\circ\delta_{Z})\text{
and }(\forall q\in g\circ\delta_{Z}(\Phi(p)))(\overline{h}\cdot\langle
p,q\rangle\in f\circ\delta_{X}(p))).$

While it is well-known that every Weihrauch degree has a representative that
is a partial multi-valued function on $\mathbb{A}$, it is quite natural to ask
whether the results of the previous sections could have been presented for
doctrines whose base category is the one of represented spaces, i.e. modest
sets, or more generally, assemblies.

The main purpose of this section is to show how our approach can be adapted to
these settings. As we will explain in detail later, there are however some
non-trivial technical obstacles in developing the theory using the ordinary
categories of assemblies and modest sets. In particular, such obstacles regard
the notion of morphism of assemblies which, as it is usually defined, is not
able to properly support the notion of Weihrauch reducibility in the context
of doctrines.

###  6.1. Assemblies and Modest sets

We briefly recall some useful definitions regarding the notion of _assembly_
and _modest sets_ (in relative realizability), explaining how these can be
seen as a categorification (and a generalization) of the notion of represented
space. We refer to [46] for a complete presentation of these notions, and to
[1, 11, 18, 3] for more specific applications. In the following definition, we
mainly follow the notation used in [1], which is closer to the usual used in
computability.

######  Definition 6.4 (Assemblies and Modest sets).

Let $\mathbb{A}$ be a PCA. An assembly is a pair $X=(|X|,\Vdash_{X})$ where
$|X|$ is a set and $\Vdash_{X}\subseteq\mathbb{A}\times|X|$ is a total
relation, i.e. $(\forall x\in|X|)(\exists r\in\mathbb{A})(r\Vdash_{X}x)$. An
assembly $X$ is a modest set if $r\Vdash_{X}y$ and $r\Vdash_{X}x$ implies
$x=y$, i.e. no two elements share a name. An assembly $X$ is partitioned if
$r\Vdash_{X}x$ and $r^{\prime}\Vdash_{X}x$ implies $r=r^{\prime}$, i.e. every
element has exactly one name.

Given an assembly $X$, we will denote by $\|X\|$ the _support_ of $X$, namely
the set $\|X\|:=\\{a\in\mathbb{A}:(\exists x\in|X|)(a\Vdash_{X}x)\\}$.

Clearly, every represented space $(X,\delta_{X})$ (6.1) gives rise to a unique
modest set as in 6.4, and vice-versa. In other words, the names “modest set”
and “represented space” can be used interchangeably. The notion of realizer
for represented spaces (6.2) can be straightforwardly extended to the notion
of realizer for assemblies as follows:

######  Definition 6.5 (realizer for assemblies).

Let $X$ and $Y$ be two assemblies, and let
$f:\subseteq|X|\rightrightarrows|Y|$ be a multi-valued function between their
underlying sets. A realizer $F$ for $f$ (we write $F\vdash f$) is a (partial)
function $F:\subseteq\mathbb{A}\to\mathbb{A}$ such that for all $r\Vdash_{X}x$
implies $r\in\operatorname{dom}(F)$ and $F(r)\Vdash_{Y}f(x)$.

######  Remark 6.6.

As mentioned, if $X$ and $Y$ are modest sets then every multi-valued function
$f:\subseteq|X|\rightrightarrows|Y|$ has a realizer (assuming the axiom of
choice). However, not every multi-valued function between assemblies admits a
realizer.

######  Definition 6.7 (Morphism of assemblies).

Let $\mathbb{A}$ be a PCA and $\mathbb{A}^{\prime}\subseteq\mathbb{A}$ be an
elementary sub-PCA of $\mathbb{A}$. A morphism of assemblies $f\colon X\to Y$
is a function $f\colon|X|\to|Y|$ which has a realizer in
$\mathbb{A}^{\prime}$, i.e. it is a function such that there exists an element
$a\in\mathbb{A}^{\prime}$ with the property that for every $r\Vdash_{X}x$ then
$a\cdot r\downarrow$ and $a\cdot r\Vdash_{X}f(x)$.

######  Definition 6.8.

Let $\mathbb{A}$ be a PCA and $\mathbb{A}^{\prime}$ be an elementary sub-PCA
of $\mathbb{A}$. We define the category of assemblies
$\mathsf{Asm}(\mathbb{A},\mathbb{A}^{\prime})$ as the subcategory of
$\mathsf{Asm}(\mathbb{A})$ having assemblies as objects and where morphisms
are morphisms of assemblies. The category of modest sets is defined as the
full subcategory $\mathsf{Mod}(\mathbb{A},\mathbb{A}^{\prime})$ of
$\mathsf{Asm}(\mathbb{A},\mathbb{A}^{\prime})$ whose objects are modest sets.
The category of partitioned assemblies
$\mathsf{ParAsm}(\mathbb{A},\mathbb{A}^{\prime})$ is the full subcategory of
$\mathsf{Asm}(\mathbb{A},\mathbb{A}^{\prime})$ whose objects are partitioned
assemblies.

######  Remark 6.9.

Observe that the full subcategory of
$\mathsf{Mod}(\mathbb{A},\mathbb{A}^{\prime})$ whose objects are partitioned,
modest sets, corresponds exactly to the category
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$ defined in 5.4.

###  6.2. Realizer-based Weihrauch

The notion of Weihrauch reducibility for assemblies has been introduced only
very recently in [20, 36]. While the definition is formally the same as 6.3,
there are some important differences with the classical notion of Weihrauch
reducibility for represented spaces.

######  Definition 6.10 (Realizer-based Weihrauch reducibility [36]).

Let $\mathbb{A}$ be a PCA and $\mathbb{A}^{\prime}\subseteq\mathbb{A}$ be an
elementary sub-PCA of $\mathbb{A}$. Let $X,Y,Z,W$ be assemblies and let
$f:\subseteq|X|\rightrightarrows|Y|$ and $g:\subseteq|Z|\rightrightarrows|W|$
be partial multi-valued functions. We say that $f$ is realizer-based Weihrauch
reducible to $g$, and write $f\leq_{\mathrm{rW}}g$, if there are
$\overline{h},\overline{k}\in\mathbb{A}^{\prime}$ such that

$(\forall G\vdash g)(\overline{h}(\operatorname{id},G\overline{k})\vdash f),$

where
$\overline{h}(\operatorname{id},G\overline{k}):=p\mapsto\overline{h}\cdot\langle
p,G(\overline{k}\cdot p)\rangle$ and where $G\vdash g$ means that $G$ is a
realizer of $g$ (6.5).

######  Remark 6.11.

Notice that this coincides trivially with the standard definition of Weihrauch
reducibility for represented spaces (see 6.3) whenever $X,Y,Z,W$ are modest
sets. However, while being a modest set is a special case of being an
assembly, the notion of realizer for multi-valued functions on modest sets is
“weaker” than the corresponding notion for assemblies. In fact, while every
multi-valued function on modest sets has a realizer, the same is not true for
multi-valued functions on assemblies, as mentioned in 6.6.

The definition of realizer-based Weihrauch reducibility corresponds precisely
to the generalization of Weihrauch reducibility for multi-represented spaces
introduced in [20, Def. 5.1]. For the sake of readability, this definition can
be restated as follows: $f\leq_{\mathrm{rW}}g$ iff there are
$\overline{h},\overline{k}\in\mathbb{A}^{\prime}$ such that:

  * •

for every $x\in\operatorname{dom}(f)$ and $p\Vdash_{X}x$, $\overline{k}\cdot
p\downarrow$ and there is $z\in\operatorname{dom}(g)$ such that
$\overline{k}\cdot p\Vdash_{X}z$ and

  * •

for every $w\in g(z)$ and $q\Vdash_{W}w$ there exists
$\overline{h}\cdot\langle p,q\rangle\Vdash_{Y}y$ such that $y\in f(x)$.

The variable $z$ in the second line is the same variable existentially
quantified in the first line.

The previous description of realizer-based Weihrauch reducibility highlights a
crucial aspect, namely that the forward functional $\overline{k}$ witnessing
the reduction $f\leq_{\mathrm{rW}}g$, in general, is not realizer of a
function between (the underlying sets of) the assemblies, i.e. it is not part
of a morphism of assemblies. This is because different names for the same
$x\in\operatorname{dom}(f)$ could be mapped to names for _different_
$z\in\operatorname{dom}(g)$ while, by definition, a morphism of assemblies has
to send names of a given $x$ into names of another element $z$. This simple,
but crucial fact, provides a serious technical obstacle in trying to adopt the
ordinary categories of assemblies and modest sets as base categories for
defining new doctrines abstracting realizer-based Weihrauch reducibility.

This observation would suggest that, to present a doctrine abstracting the
notion of Weihrauch reducibility for represented spaces and assemblies, a
natural choice could be that of considering a category whose objects are
represented spaces and whose morphisms are multi-valued functions. However,
this approach does not align well with the categorical framework of doctrines,
primarily because represented spaces and multi-valued functions lack the
structure of cartesian products.

Indeed, the category Mult of multi-valued functions between sets has been
studied in [34]. In [34, Sec. 3.1], Pauly observes that the category Mult has
a categorical product, but this product does not preserve computability, and
so it does not work well for our purposes.

In summary, the challenge in extending our approach to assemblies and modest
sets lies in defining a new notion of “morphism of assemblies”, so as to
obtain a new category with cartesian products whose morphisms allow for a
categorical presentation of realizer-based Weihrauch reducibility.

To this end, we introduce the following category where, as in the case of
Weihrauch reducibility, the notion of morphism of the category is inspired by
the properties of the forward functional.

######  Definition 6.12.

Let $\mathbb{A}$ be a PCA, and let $\mathbb{A}^{\prime}$ be an elementary sub-
PCA of $\mathbb{A}$. We denote by
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ the category defined as
follows:

  * •

objects are assemblies $X=(|X|,\Vdash_{X})$;

  * •

a morphism between $X$ and $Y$ is a pair $(a,\varphi)$, where
$a\in\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})(\|X\|,\|Y\|)$
and $\varphi\colon\Vdash_{X}\to Y$ is a function such that, for every
$p\Vdash_{X}x$, $a\cdot p\Vdash_{Y}\varphi(p,x)$.

######  Remark 6.13.

Observe that morphism $(a,\varphi)\colon X\to Y$ of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ induces a function
$\Vdash_{X}\to\Vdash_{Y}$ assigning $(p,x)\mapsto(a\cdot p,\varphi(p,x))$.

In other words, the objects of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ are the same as of
$\mathsf{Asm}(\mathbb{A},\mathbb{A}^{\prime})$, the difference is in the
notion of morphisms.

It is straightforward to check that 6.12 provides a well-defined category,
where the identity morphism $X\to X$ is given by the pair $(k,\pi_{X})$, where
$\pi_{X}\colon\Vdash_{X}\to X$ is the function mapping $(a,x)\mapsto x$, and
the composition of $(a_{1},\varphi_{1})\colon X\to Y$ and
$(a_{2},\varphi_{2})\colon Y\to Z$ is given by the morphism
$(a_{3},\varphi_{3})\colon X\to Z$ where $a_{3}$ is given by the composition
of $a_{1}$ and $a_{2}$ in the category
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$, while
$\psi_{3}\colon\Vdash_{X}\to Z$ is given by the assignment
$(p,x)\mapsto\varphi_{2}(a_{1}\cdot p,\varphi_{1}(p,x))$ (this is well-defined
since, by definition of morphism, for every $p\Vdash_{X}x$, $a_{1}\cdot
p\Vdash_{Y}\varphi_{1}(p,x)$).

######  Lemma 6.14.

The category $\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ has finite
products. In particular, the product of X$\times Y$ is given by the assembly
$(|X|\times|Y|,\Vdash_{X\times Y})$ where $\Vdash_{X\times
Y}\subseteq\mathbb{A}\times(|X|\times|Y|)$ is defined as

$\Vdash_{X\times Y}:=\\{(\langle
p_{1},p_{2}\rangle,(x,y))\in\mathbb{A}\times(|X|\times|Y|):p_{1}\Vdash_{X}x\mbox{
and }p_{2}\Vdash_{Y}y\\},$

and the product projections are given by $(\mathsf{fst},\pi_{X})\colon X\times
Y\to X$ and $(\mathsf{snd},\pi_{Y})\colon X\times Y\to Y$. The terminal object
is the assembly $\mathbf{1}:=(1,\Vdash_{1})$.

###### Proof.

Let $X,Y,Z$ be assemblies. For every arrow $(a_{1},\varphi_{1})\colon Z\to X$
and $(a_{2},\varphi_{2})\colon Z\to Y$ we show that there exists a unique
arrow $(a_{3},\varphi_{3})\colon Z\to X\times Y$ such that the diagram

${X}$${X\times
Y}$${Y}$${Z}$$\scriptstyle{(a_{1},\varphi_{1})}$$\scriptstyle{(\mathsf{fst},\pi_{X})}$$\scriptstyle{(a_{2},\varphi_{2})}$$\scriptstyle{(\mathsf{snd},\pi_{Y})}$$\scriptstyle{(a_{3},\varphi_{3})}$

commutes. Given $a_{1}$ and $a_{2}$, we have that $a_{3}$ is uniquely
determined by the cartesian products of the category
$\mathsf{Mod}_{\mathsf{p}}(\mathbb{A},\mathbb{A}^{\prime})$, while the
function $\varphi_{3}\colon\Vdash_{Z}\to|X|\times|Y|$ is given by the
assignment $(p,z)\mapsto(\varphi_{1}(p,z),\varphi_{2}(p,z))$. It is direct to
check that this is a well-defined arrow of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$, and that the previous
diagram commutes. Similarly, it is straightforward to check the uniqueness of
$(a_{3},\varphi_{3})\colon Z\to X\times Y$. ∎

This category $\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ allows us to
give a unified categorical presentation of $\leq_{\mathrm{rW}}$ (and later,
also to extended Weihrauch reducibility $\leq_{\mathsf{extW}}$.)

The intuition is that a computation with a multi-valued function $f:\subseteq
X\rightrightarrows Z$ between assemblies requires a (non-computable) step, as
$p\in\|X\|$ may correspond to more than one $x\in\operatorname{dom}(f)$. In
other words, on top of the computable maps $\overline{k}$ and $\overline{h}$,
the reduction $f\leq_{\mathrm{rW}}g$ involves a (possibly non-computable)
choice function $\varphi$ mapping $(p,x)$ with
$p\Vdash_{X}x\in\operatorname{dom}(f)$ to some element in
$\operatorname{dom}(g)$.

It is sometimes easier to think of a map between assemblies can be seen as
having a “public” input (the name $p$ of some $x\in\operatorname{dom}(f)$) and
a “private” input (the element $x$ of the assembly), where only the “public”
input can be used in the computation (see also [20, Observation 5.4 and the
discussion thereafter]).

Now, in order to show that the realizer-based Weihrauch reducibility can
presented in the language of doctrines, we first rephrase 6.10 in terms of
reducibility of functions
$F\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ and
$G\colon\Vdash_{Z}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$, for
some assemblies $X$ and $Y$.

######  Proposition 6.15.

For every partial multi-valued function $f:\subseteq X\rightrightarrows Y$
between assemblies, let us define the map
$F\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ as
follows: for every $p\Vdash_{X}x$,

$F(p,x):=\bigcup_{y\in f(x)}\\{q\in\mathbb{A}:q\Vdash_{Y}y\\}.$

Then $f\equiv_{\mathrm{rW}}F$. Moreover, let $g:\subseteq Z\rightrightarrows
W$ be a partial multi-valued function between assemblies and let
$G\colon\Vdash_{Z}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ be its
corresponding map. Then $f\leq_{\mathrm{rW}}g$ iff there are a morphism
$(\overline{k},\varphi)\in\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})(X,Z)$
and $\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall p\Vdash_{X}x)(\forall q\in G(\overline{k}\cdot
p,\varphi(p,x)))(\overline{h}\cdot\langle p,q\rangle\in F(p,x)).$

###### Proof.

The equivalence $f\equiv_{\mathrm{rW}}F$ is straightforward from the
definition. Let us show the equivalence between $f\leq_{\mathrm{rW}}g$ and
$(\star)$.

For the right-to-left direction, it is immediate to see that $\overline{k}$
and $\overline{h}$ witness $f\leq_{\mathrm{rW}}g$. For the converse direction,
assume $f\leq_{\mathrm{rW}}g$ via $\overline{k},\overline{h}$. For every
$x\in\operatorname{dom}(f)$ and $p\Vdash_{X}x$, let us define
$\varphi(p,x):=z$, where $z\in\operatorname{dom}(g)$ is an element of $Z$
named by $\overline{k}\cdot p$ witnessing the reduction
$f\leq_{\mathrm{rW}}g$. In particular, the pair $(\overline{k},\varphi)$ is a
morphism of $\mathsf{extAsm}$ between $X$ and $Z$. To show that
$(\overline{k},\varphi)$ and $\overline{h}$ prove the claim, fix
$p\Vdash_{X}x$. By definition, $\overline{k}\cdot p\Vdash_{Z}\varphi(p,x)$,
and hence $G(\overline{k}\cdot p,\varphi(p,x))=\bigcup_{y\in
f(x)}\\{q\in\mathbb{A}:q\Vdash_{Y}y\\}$. In particular, any $q\in
G(\overline{k}\cdot p,\varphi(p,x))$ is a name for some $t\in
g(\varphi(p,x))$. This implies that $\overline{h}\cdot\langle
p,q\rangle\Vdash_{Y}y\in f(x)$, i.e. $\overline{h}\cdot\langle p,q\rangle\in
F(p,x)$. ∎

The previous proposition establishes an equivalent formulation of realizer-
based Weihrauch reducibility, which is better suited to presentation in the
language of doctrines.

######  Definition 6.16 (elementary realizer-based Weihrauch doctrine).

We define the elementary realizer-based Weihrauch doctrine
$\textstyle{\mathfrak{erW}\colon\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
as follows: for every object $X$ of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$, the objects
$\mathfrak{erW}(X)$ are functions
$f\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$. For
every pair of maps $f,g$ in
$\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{X}}$, we define
$f\leq_{\mathsf{drW}}g$ iff there is $\overline{h}\in\mathbb{A}^{\prime}$ such
that

$(\forall p\Vdash_{X}x)(\forall q\in g(p,x))(\overline{h}\cdot\langle
p,q\rangle\in f(p,x)).$

As usual, the doctrine $\mathfrak{erW}(X)$ is the quotient of
$\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{X}}$ by
$\leq_{\mathsf{drW}}$, and the action of $\mathfrak{erW}$ on a morphism
$(a,\varphi)\colon X\to Y$ of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ is defined by the pre-
composition with the function $\Vdash_{X}\to\Vdash_{Y}$ induced by
$(a,\varphi)$ (see 6.13).

Following the same idea of 5.8, we can check that the elementary realizer-
based Weihrauch doctrine is pure universal:

######  Proposition 6.17.

The elementary realizer-based Weihrauch doctrine
$\textstyle{\mathfrak{erW}\colon\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
is a pure universal doctrine: for every projection $\pi_{Z}\colon X\times Z\to
Z$, the morphism $\forall_{\pi_{Z}}\colon\mathfrak{erW}(X\times
Z)\to\mathfrak{erW}(Z)$ sending an element $f\in\mathfrak{erW}(X\times Z)$ to
the element $\forall_{\pi_{Z}}(f)\in\mathfrak{erW}(Z)$ defined as

$\forall_{\pi_{Z}}(f)(s,z):=\bigcup_{x\in X}\left\\{\langle
p,q\rangle:p\Vdash_{X}x\text{ and }q\in f((p,x),(s,z))\right\\}$

is right-adjoint to $\mathfrak{erW}_{\pi_{Z}}(g)$, i.e. for every
$f\in\mathfrak{erW}(X\times Z)$ and $g\in\mathfrak{erW}(Z)$,

$g\leq_{\mathsf{drW}}\forall_{\pi_{Z}}(f)\iff\mathfrak{erW}_{\pi_{Z}}(g)\leq_{\mathsf{drW}}f.$

###### Proof.

Assume first that $g\leq_{\mathsf{drW}}\forall_{\pi_{Z}}(f)$ via
$\overline{a}$. Let $\overline{b}\in\mathbb{A}^{\prime}$ be defined as
$\overline{b}\cdot\langle\langle p,s\rangle,q\rangle:=\overline{a}\cdot\langle
s,\langle p,q\rangle\rangle$. We want to show that for every $\langle
p,s\rangle\Vdash_{X\times Z}(x,z)$,

$(\forall q\in f((p,x),(s,z)))(\overline{b}\cdot\langle\langle
p,s\rangle,q\rangle\in g\circ\pi_{Z}((p,x),(s,z))=g(s,z)).$

To this end, fix $\langle p,s\rangle\Vdash_{X\times Z}(x,z)$. Since $f$ is
total on $X\times Z$, we only need to show that for every $q\in
f((p,x),(s,z))$, $\overline{b}\cdot\langle\langle p,s\rangle,q\rangle\in
g(s,z)$. This follows immediately from the definition of $\overline{b}$, as
$g\leq_{\mathsf{dW}}\forall_{\pi_{Z}}(f)$ and $\langle
p,q\rangle\in\forall_{\pi_{Z}}(f)(s,z)$.

For the right-to-left direction, we proceed analogously: assume
$\mathfrak{erW}_{\pi_{Z}}(g)\leq_{\mathsf{drW}}f$ via $\overline{c}$. Define
$\overline{d}\cdot\langle s,\langle
p,q\rangle\rangle:=\overline{c}\cdot\langle\langle p,s\rangle,q\rangle$. To
show that $g\leq_{\mathsf{drW}}\forall_{\pi_{Z}}(f)$, simply notice that for
every $s\Vdash_{Z}z$, and every $\langle
p,q\rangle\in\forall_{\pi_{Z}}(f)(s,z)$, the fact that
$\mathfrak{erW}_{\pi_{Z}}(g)\leq_{\mathsf{drW}}f$ via $\overline{c}$ implies
that $\overline{d}\cdot\langle s,\langle
p,q\rangle\rangle=\overline{c}\cdot\langle\langle
p,s\rangle,q\rangle\in\mathfrak{erW}_{\pi_{Z}}(g)((p,x),(s,z))=g(s,z)$. ∎

Now we introduce the realizer-based Weihrauch doctrine. For this, we introduce
first the notion of _generalized assembly-based Weihrauch predicate_.

######  Definition 6.18 (generalized assembly-based Weihrauch predicate).

A generalized assembly-based Weihrauch predicate on an assembly $X$ is a
function

$F\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{Y}}$

for some assembly $Y$.

######  Definition 6.19 (Realizer-based Weihrauch doctrine).

Given a PCA $\mathbb{A}$ with elementary sub-PCA $\mathbb{A}^{\prime}$, the
realizer- based Weihrauch doctrine is the functor
$\textstyle{\mathfrak{rW}\colon\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Pos}}$
that maps $(X,\Vdash_{X})$ to the preorder $\mathfrak{rW}(X)$ defined as
follows:

  * •

objects are generalized assembly-based Weihrauch predicates on $X$;

  * •

the partial order is given by the poset reflection of the preorder defined as
follows: let $(Y,\Vdash_{Y})$ and $(Z,\Vdash_{Z})$ be objects of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$. For every
$F\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{Y}}$
and
$G\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{Z}}$,
we say that $F\leq_{\mathsf{rW}}G$ if there exist a morphism
$(\overline{k},\varphi)\in\mathsf{Hom}_{\mathsf{extAsm}}(X\times Y,Z)$ and
$\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall\langle p,q\rangle\Vdash_{X\times Y}(x,y))(\forall t\in
G((p,x),(\overline{k}\cdot\langle p,q\rangle,\varphi(\langle
p,q\rangle,(x,y)))))(\overline{h}\cdot\langle\langle p,q\rangle,t\rangle\in
F((p,x),(q,y))).$

As before, the action of $\mathfrak{rW}$ on a morphism $(a,\varphi)\colon X\to
Y$ of $\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ is defined by the pre-
composition with the function $\Vdash_{X}\to\Vdash_{Y}$ induced by
$(a,\varphi)$ (see 6.13).

We now show that the previous doctrine provides the right categorification of
realizer-based Weihrauch degrees.

######  Theorem 6.20 (Realizer-based Weihrauch degrees).

The realizer-based Weihrauch degrees are isomorphic to
$\mathfrak{rW}(\mathbf{1})$, where $\mathbf{1}$ is the terminal object as
defined in 6.14.

###### Proof.

By definition of realizer-based Weihrauch doctrine, the objects of the poset
$\mathfrak{rW}(\mathbf{1})$ can be identified with functions
$\Vdash_{Y}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$. Moreover, if
$F\colon\Vdash_{Y}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ and
$G\colon\Vdash_{Z}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$ are in
$\mathfrak{rW}(\mathbf{1})$ then $F\leq_{\mathsf{rW}}G$ iff there are a
morphism $(\overline{k},\varphi)$ between $Y$ and $Z$ and
$\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall p\Vdash_{Y}y)(\forall q\in G(\overline{k}\cdot
p,\varphi(p,y)))(\overline{h}\cdot\langle p,q\rangle\in F(p,y)),$

which corresponds to 6.10. ∎

As before, when working with Kleene’s second model,
$\mathfrak{rW}(\mathbf{1})$ corresponds precisely to the realizer-based
Weihrauch degrees.

We conclude our analysis of realizer-based Weihrauch reducibility by showing
that the realizer-based Weihrauch doctrine is a pure existential completion.

######  Theorem 6.21.

The realizer-based Weihrauch doctrine is isomorphic to the pure existential
completion of the elementary realizer-based Weihrauch doctrine. In symbols:

$\mathfrak{rW}\equiv{\mathfrak{erW}}^{\exists}.$

In particular, for every PCA $\mathbb{A}$ with elementary sub-PCA
$\mathbb{A}^{\prime}$ and for every object $(X,\Vdash_{X})$ of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$, the map

$(\pi_{X},f)\mapsto F$

where
$F\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{Y}}$
is defined as $F(p,x):=f((p,x),\cdot)$, is an isomorphism of posets between
$({\mathfrak{erW}}^{\exists}(X),\leq_{\exists})$ and
$(\mathfrak{rW}(X),\leq_{\mathsf{rW}})$.

###### Proof.

Recall that

$(\pi,f)\leq_{\exists}(\pi^{\prime},g)\iff(\exists(\overline{k},\varphi)\in\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})(X\times
Y,Z))(f\leq_{\mathsf{drW}}\mathfrak{erW}_{\langle\pi_{X},k\rangle}(g)),$

where $\mathfrak{erW}_{\langle\pi_{X},k\rangle}(g)\colon=((p,x),(q,y))\mapsto
g((p,x),(\overline{k}\cdot\langle p,q\rangle,\varphi((p,x),(q,y)))$.

We first show that the assignment $(\pi_{X},f)\mapsto F$ preserves and
reverses the order. Let $(\pi,f)$ and $(\pi^{\prime},g)$ be two elements of
${\mathfrak{erW}}^{\exists}(X)$. By expanding the definition of
$\leq_{\mathsf{drW}}$, we obtain that $(\pi,f)\leq_{\exists}(\pi^{\prime},g)$
iff there is a morphism
$(\overline{k},\varphi)\in\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})(X\times
Y,Z)$ and $\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall\langle p,q\rangle\Vdash_{X\times Y}(x,y))(\forall t\in
g((p,x),(\overline{k}\cdot\langle p,q\rangle,\varphi(\langle
p,q\rangle,(x,y)))))(\overline{h}\cdot\langle\langle p,q\rangle,t\rangle\in
f((p,x),(q,y)))$

Let
$F\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{Y}}$
and
$G\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{Z}}$
be the images of $(\pi,f)$ and $(\pi^{\prime},g)$ respectively. Observe that,
writing $F((p,x),(q,y))=f((p,x),(q,y))$ (analogously for $G$) and substituting
$F$ and $G$ in ($\star$), it is straightforward to check that
$(\pi,f)\leq_{\exists}(\pi^{\prime},g)$ iff $F\leq_{\mathsf{rW}}G$ (see the
definition).

This shows that the embedding preserves and reflects the partial order.
Finally, it is easy to see that the map $(\pi_{X},f)\mapsto F$ is surjective,
since any function
$H\colon\Vdash_{X}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})^{\Vdash_{V}}$
can be obtained via our embedding as the image of the pair $(\pi_{X},h)$,
where
$h\colon\Vdash_{X}\times\Vdash_{V}\to\raisebox{1.70717pt}{\Large$\wp$}^{*}(\mathbb{A})$
is defined as $h((p,x),(q,v)):=H((p,x),(q,v))$. Therefore, since the map is a
surjective homomorphism of posets which also reflects the order, we can
conclude that it is an isomorphism. ∎

######  Remark 6.22.

As anticipated 6.11, if consider the realizer-based Weihrauch doctrine
restricted to the full subcategory of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ whose objects are modest
sets, we obtain precisely a doctrine abstracting the notion of Weihrauch
reducibility for represented spaces.

###  6.3. Extended Weihrauch reducibility

Recently Bauer [1] introduced another generalization of Weihrauch
reducibility, called _extended Weihrauch reducibility_ , that can be seen as
another way to generalize Weihrauch reducibility to multi-represented spaces.
As anticipated, we show that the category
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ can be used to describe the
extended Weihrauch degrees in terms of doctrines.

We start by recalling the main definitions from [1]:

######  Definition 6.23 (Extended Weihrauch reducibility [1, Def. 3.7]).

Let $\mathbb{A}$ be a PCA. An extended Weihrauch predicates is a function
$f\colon\mathbb{A}\to\raisebox{1.70717pt}{\Large$\wp$}\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})$.

Given two extended Weihrauch predicates $f,g$, we say that$f$ is extended-
Weihrauch reducible to $g$, and write $f\leq_{\mathsf{extW}}g$ if there are
$\overline{k},\overline{h}\in\mathbb{A}^{\prime}$ such that

  * •

for every $p\in\mathbb{A}$ such that $f(p)\neq\emptyset$, $\overline{k}\cdot
p\downarrow$ and $g(\overline{k}\cdot p)\neq\emptyset$;

  * •

for every $A\in f(p)$ there is $B\in g(\overline{k}\cdot p)$ such that for
every $q\in B$, $\overline{h}\cdot\langle p,q\rangle\downarrow$ and
$\overline{h}\cdot\langle p,q\rangle\in A$.

Observe that, while extended Weihrauch reducibility applies to extended
Weihrauch predicates, we can rewrite the above definition as a preorder on
partial multi-valued functions on elements of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$. This follows the same ideas
used in the proof of [1, Prop. 3.8]: given
$f\colon\mathbb{A}\to\raisebox{1.70717pt}{\Large$\wp$}\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})$,
let $X_{f}=(|X_{f}|,\Vdash_{X_{f}})$ be the object of
$\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})$ defined as follows:

$\displaystyle|X_{f}|:=\bigcup_{p\in\operatorname{dom}(f)}f(p)=\\{A\in\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A}):(\exists
p\in\operatorname{dom}(f))(A\in f(p))\\};$ $\displaystyle
p\Vdash_{X_{f}}A:\iff A\in f(p).$

We then define
$F\colon\Vdash_{X_{f}}\to\raisebox{1.70717pt}{\Large$\wp$}(\mathbb{A})$ as
$F(p,A):=A$.

Observe that, unlike what happens for $\leq_{\mathrm{rW}}$, $F$ need not be a
total map. In other words, it could be that $F(p,A)=\emptyset$ for some
$p\Vdash_{X_{f}}A$. This is a crucial difference between $\leq_{\mathrm{rW}}$
and $\leq_{\mathsf{extW}}$.

######  Proposition 6.24.

Given two extended predicates $f,g$, $f\leq_{\mathsf{extW}}g$ iff there are a
morphism
$(\overline{k},\varphi)\in\mathsf{extAsm}(\mathbb{A},\mathbb{A}^{\prime})(X_{f},X_{g})$
and $\overline{h}\in\mathbb{A}^{\prime}$ such that

$(\forall p\Vdash_{X_{f}}A)(\forall q\in G(\overline{k}\cdot
p,\varphi(p,A)))(\overline{h}\cdot\langle p,q\rangle\in F(p,A)).$

This characterization is formally identical to $(\star)$ in 6.15, and it can
be proved using the same ideas. However, the fact that we do not require $F$
and $G$ to be total implies that $f\leq_{\mathsf{extW}}g$ is vacuously true
whenever $\emptyset\in g(q)$ for every $q\in\operatorname{dom}(g)$. In fact,
the top extended Weihrauch degree has a representative $g$ with
$\operatorname{dom}(g)=\\{\overline{a}\\}$ for some
$\overline{a}\in\mathbb{A}^{\prime}$ and $g(\overline{a})=\\{\emptyset\\}$. In