# A CATEGORY OF ARROW ALGEBRAS FOR MODIFIED REALIZABILITY

Umberto Tarantino  Dipartimento di Matematica ‘Federigo Enriques’, Università
degli Studi di Milano<EMAIL_ADDRESS>
(Date: August 28, 2024)

###### Abstract.

In this paper we further the study of arrow algebras, simple algebraic
structures inducing toposes through the tripos-to-topos construction, by
defining appropriate notions of morphisms between them which correspond to
morphisms of the associated triposes. Specializing to geometric inclusions, we
characterize subtriposes of an arrow tripos in terms of nuclei on the
underlying arrow algebra, recovering a classical locale-theoretic result. As
an example of application, we lift modified realizability to the setting of
arrow algebras, and we establish its functoriality.

###### Key words and phrases:

arrow algebras, topos theory, realizability, geometric morphisms

The purpose of this paper is to develop the theory of arrow algebras as a
framework to study realizability toposes from a more concrete, ‘algebraic’,
point of view which can also take localic toposes into account.

Arrow algebras were introduced in [vdBB23], of which this paper can be seen as
a follow-up, generalizing Alexandre Miquel’s _implicative algebras_ [Miq20a,
Miq20b] as algebraic structures which induce triposes and hence toposes. The
main advantage of arrow algebras, compared to implicative algebras, lies in
the fact that they perfectly factor through the construction of realizability
triposes coming from partial combinatory algebras111From now on, PCAs. which
are actually _partial_ , whereas implicative algebras are the intermediate
structure only in the case of _total_ combinatory algebras.

The aim of the following is then to define appropriate notions of morphisms
between arrow algebras which correspond to morphisms of the associated
triposes, so to determine a category of arrow algebras which factors through
the construction of both realizability and localic triposes in a 2-functorial
way.

Specializing the previous correspondence to geometric inclusion, we will
characterize subtriposes of triposes arising from arrow algebras – that is,
_arrow triposes_ – as arrow triposes themselves, generalizing the locale-
theoretic concept of a _nucleus_ and the correspondence between nuclei on a
locale and sublocales. As subtriposes exactly correspond to subtoposes, this
means in particular that we can study subtoposes of realizability toposes by
studying nuclei on the underlying arrow algebras. To do this, we will make use
of a particularly simple construction which does not work for implicative
algebras and which was also part of the original motivation for the
introduction of arrow algebras.

As an example of application of this framework, we will study modified
realizability ([Kre59] and [Gra81, vO97b, Bv02, Joh17]) at the level of arrow
algebras, rephrasing and extending results partially known in the literature
at the level of PCAs.

##  1\. Preliminary on tripos theory

We begin by reviewing the necessary background on tripos theory, mainly
following the account given in [vO08] on the basis of Pitts’ PhD thesis
[Pit81]; the reader is instead assumed to be familiar with topos theory, for
which standard references are [MM92, Bor94, Joh02].

###  1.1. Preorder-enriched categories

First, we need to establish our terminology for 2-dimensional categories.
Following [Zoe22], with _2-category_ we mean a 2-dimensional category which is
also an ordinary category, meaning that the unit and associativity laws for
1-cells hold on the nose. Instead, we speak of _bicategories_ for
2-dimensional categories where the axioms of an ordinary category only hold up
to (coherent) invertible 2-cells.

We can now introduce the most important kind of 2-dimensional category in the
context of this paper.

######  Definition 1.1.

A _preorder-enriched_ category is a locally small 2-category with at most one
2-cell between any pair of 1-cells.222As in [Zoe22], we will also speak
improperly of _preorder-enriched bicategories_ for bicategories whose
homcategories are preorders.

Explicitly, this means that a preorder-enriched category
$\operatorname{\mathsf{C}}$ is a category endowed with a preorder structure on
each homset $\operatorname{\mathsf{C}}(A,B)$, in such a way that the
composition map

$\operatorname{\mathsf{C}}(B,C)\times\operatorname{\mathsf{C}}(A,B)\to\operatorname{\mathsf{C}}(A,C)$

is order-preserving for all $A,B,C\in\operatorname{\mathsf{C}}$.

In a preorder-enriched category, a morphism $f:X\to Y$ is _left adjoint_ to a
morphism $g:Y\to X$ – equivalently, $g$ is _right adjoint_ to $f$ – if
$\operatorname{id}_{X}\leq gf$ and $fg\leq\operatorname{id}_{Y}$, in which
case we write $f\dashv g$. Two parallel morphisms $f,g$ are _isomorphic_ if
$f\leq g$ and $g\leq f$, in which case we write $f\simeq g$.

######  Example 1.2.

Every category is preorder-enriched with respect to the discrete order.

######  Example 1.3.

The category $\operatorname{\mathsf{Preord}}$ of preordered sets and monotone
functions is preorder-enriched with respect to the pointwise order.

######  Definition 1.4.

Let $\operatorname{\mathsf{C}}$ and $\operatorname{\mathsf{D}}$ be preorder-
enriched categories. A _pseudofunctor_
$F:\operatorname{\mathsf{C}}\to\operatorname{\mathsf{D}}$ maps every object
$X$ in $\operatorname{\mathsf{C}}$ to some object $F(X)$ in
$\operatorname{\mathsf{D}}$ and every morphism $f:X\to Y$ in
$\operatorname{\mathsf{C}}$ to some morphism $F(f):F(X)\to F(Y)$ in
$\operatorname{\mathsf{D}}$, in such a way that:

  1. i.

the association
${\operatorname{\mathsf{C}}}({X},{Y})\to{\operatorname{\mathsf{D}}}({F(X)},{F(Y)})$
is order-preserving for all objects $X,Y$ in $\operatorname{\mathsf{C}}$;

  2. ii.

$F(\operatorname{id}_{X})\simeq\operatorname{id}_{F(X)}$ for all objects $X$
in $\operatorname{\mathsf{C}}$;

  3. iii.

$F(gf)\simeq F(g)F(f)$ for all composable arrows $f,g$ in
$\operatorname{\mathsf{C}}$.

In particular, $F$ is a _2-functor_ 333This is called an _enriched functor_ in
[vO08]. if it is an actual functor, i.e. if the equalities in (ii) and (iii)
hold on the nose rather than up to isomorphism.

######  Definition 1.5.

Let $F$ and $G$ be pseudofunctors
$\operatorname{\mathsf{C}}\to\operatorname{\mathsf{D}}$. A _pseudonatural
transformation_ $\Phi:F\Rightarrow G$ is given by a morphism $\Phi_{X}:F(X)\to
G(X)$ in $\operatorname{\mathsf{D}}$ for every object $X$ in
$\operatorname{\mathsf{C}}$ in such a way that, for all morphisms $f:X\to Y$
in $\operatorname{\mathsf{C}}$, the square

${{F(X)}}$${{G(X)}}$${{F(Y)}}$${{G(Y)}}$$\scriptstyle{\Phi_{X}}$$\scriptstyle{F(f)}$$\scriptstyle{G(f)}$$\scriptstyle{\Phi_{Y}}$

commutes up to isomorphism.

######  Remark 1.6.

We will also have to deal with _pseudomonads_ on a preorder-enriched category
$\operatorname{\mathsf{C}}$, that is, the datum of a pseudofunctor
$T:\operatorname{\mathsf{C}}\to\operatorname{\mathsf{C}}$ and two
pseudonatural transformations $\eta:\operatorname{id}_{T}\Rightarrow T$ and
$\mu:T^{2}\Rightarrow T$ satisfying the usual monad laws up to (coherent)
invertible modifications. We will not go into any detail about the theory of
pseudomonads, which will serve us only _en passant_ : for reference, see
[JY20].

We will then consider _pseudoalgebras_ over a pseudomonad $T$, that is,
objects $X$ endowed with a morphism $T(X)\to X$ in $\operatorname{\mathsf{C}}$
satisfying the usual algebra laws up to isomorphism. In complete analogy with
the 1-dimensional case, pseudoalgebras determine the _Kleisli bicategory_
$\mathsf{Kl}({T})$ of the pseudomonad $T$: the critical point here is
precisely that $\mathsf{Kl}({T})$ is not necessarily a 2-category, but we will
see how this will not really be an issue for our purposes.

The following preorder-enriched category plays a key role in the theory of
triposes.

######  Definition 1.7.

A _Heyting prealgebra_ is a preorder whose poset reflection is a Heyting
algebra; in other words, it is a (small) thin cartesian closed category which
admits finite coproducts.

A morphism of Heyting prealgebras is a monotone function which is a morphism
of Heyting algebras between the poset reflections of domain and codomain; in
other words, it is a functor which preserves finite products and coproducts
and exponential objects.

We denote with $\operatorname{\mathsf{HeytPre}}$ the category of Heyting
prealgebras, which is preorder-enriched with respect to the pointwise order.

###  1.2. Triposes

In this paper, we will only consider $\operatorname{\mathsf{Set}}$-based
triposes.

######  Definition 1.8.

A _( $\operatorname{\mathsf{Set}}$-)tripos_ is a pseudofunctor
$P:{\operatorname{\mathsf{Set}}}^{\operatorname{op}}\to\operatorname{\mathsf{HeytPre}}$
satisfying the following axioms.

  1. i.

For every function $f:X\to Y$, the map $f^{*}\coloneqq P(f):P(Y)\to P(X)$ has
both a left adjoint $\exists_{f}$ and a right adjoint $\forall_{f}$ in
$\operatorname{\mathsf{Preord}}$.444That is, $\exists_{f}$ and $\forall_{f}$
need not preserve the Heyting structure. Moreover, these adjoints satisfy the
_Beck-Chevalley condition_ , which means that for every pullback square in
$\operatorname{\mathsf{Set}}$ as the left one, the induced square on the right
commutes up to isomorphism in $\operatorname{\mathsf{Preord}}$:555This also
implies the same condition for left adjoints, namely that $\exists_{f}\circ
g^{*}\simeq h^{*}\circ\exists_{k}$.

${X}$${Y}$${Z}$${W}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{k}$$\scriptstyle{h}$$\scriptstyle{\lrcorner}$
${{P(X)}}$${{P(Y)}}$${{P(Z)}}$${{P(W)}}$$\scriptstyle{\forall_{g}}$$\scriptstyle{f^{*}}$$\scriptstyle{\forall_{h}}$$\scriptstyle{k^{*}}$

  2. ii.

There exists a _generic element_ in $P$, which is an element $\sigma\in
P(\Sigma)$ for some set $\Sigma$ with the property that, for every set $X$ and
every element $\phi\in P(X)$, there exists a function $[\phi]:X\to\Sigma$ such
that $\phi$ and $[\phi]^{*}(\sigma)$ are isomorphic elements of $P(X)$.

A tripos $P$ such that $P(X)$ is the set $\Sigma^{X}$ of functions
$X\to\Sigma$ for some set $\Sigma$ is said to be _canonically presented_.

######  Example 1.9.

Let $H$ be a complete Heyting algebra. We define the
$\operatorname{\mathsf{Set}}$-tripos of $H$-valued predicates $P_{H}$ as
follows.

For any set $X$, we let $P_{H}(X)\coloneqq H^{X}$, which is a Heyting algebra
under pointwise order and operations; for any function $f:X\to Y$, the
precomposition map $f^{*}:P_{H}(Y)\to P_{H}(X)$ is then a morphism of Heyting
algebras. Adjoints for $f^{*}$ are provided by completeness as, for $\phi\in
P_{H}(X)$ and $y\in Y$:

$\exists_{f}(\phi)(y)\coloneqq\bigvee_{x\in{f}^{\kern
0.50003pt\text{-}1}(y)}\phi(x)\qquad\forall_{f}(\phi)(y)\coloneqq\bigwedge_{x\in{f}^{\kern
0.50003pt\text{-}1}(y)}\phi(x)$

which also satisfy the Beck-Chevalley condition. A generic element is
trivially given by $\operatorname{id}_{H}\in P_{H}(H)$.

######  Definition 1.10.

Let $P$ and $Q$ be triposes. A _transformation_ $\Phi:P\to Q$ is a
pseudonatural transformation $P\Rightarrow Q$ where $P$ and $Q$ are considered
as pseudofunctors
${\operatorname{\mathsf{Set}}}^{\operatorname{op}}\to\operatorname{\mathsf{Preord}}$;
in other words, this means that each component $\Phi_{X}:P(X)\to Q(X)$ is an
order-preserving function but not necessarily a morphism of Heyting
prealgebras.

Transformations $P\Rightarrow Q$ can be ordered by letting $\Phi\leq\Psi$ if
$\Phi_{X}\leq\Psi_{X}$ pointwise for every set $X$, therefore making triposes
and transformations into a preorder-enriched category which we denote as
$\mathsf{Trip}({\operatorname{\mathsf{Set}}})$.

A transformation $\Phi:P\to Q$ is an _equivalence_ if there exists another
transformation $\Psi:Q\to P$ such that
$\Phi\circ\Psi\simeq\operatorname{id}_{Q}$ and
$\Psi\circ\Phi\simeq\operatorname{id}_{P}$.

######  Remark 1.11.

Through the generic element, every tripos is equivalent to a canonically
presented one.

######  Remark 1.12.

$\mathsf{Trip}({\operatorname{\mathsf{Set}}})$ is essentially locally small:
in fact, a transformation $\Phi:P\to Q$ is determined up to isomorphism by
$\Phi_{\Sigma}(\sigma)\in Q(\Sigma)$, since for any $\phi\in P(X)$ we have
that $\Phi_{X}(\phi)\dashv\vdash_{X}Q([\phi])(\Phi_{\Sigma}(\sigma))$.

Every tripos $P$ gives rise to a topos $\operatorname{\mathsf{Set}}[P]$ in a
process called the _tripos-to-topos construction_ , which we will not describe
here as it does not serve any purpose for the sake of this paper. The
interested reader can find all the details in [vO08].

######  Example 1.13.

For a complete Heyting algebra $H$, $\operatorname{\mathsf{Set}}[P_{H}]$ is
the topos of $H$-valued sets, proved in [Hig73] to be equivalent to the topos
$\operatorname{Sh}(H)$ of sheaves over $H$.

###  1.3. Geometric morphisms of triposes

The most important notion of morphism between toposes is arguably that of a
_geometric morphism_ , which by now has a vast and standard theory. Much more
niche, instead, is the theory of geometric morphisms of triposes, and how they
relate with geometric morphisms of toposes: with no aim for a complete
treatment, we review here the notions we will need in the following.

######  Definition 1.14.

Let $P$ and $Q$ be triposes. A transformation $\Phi:P\to Q$ is _cartesian_ if
each component $\Phi_{X}:P(X)\to Q(X)$ preserves finite meets up to
isomorphism. We denote with
$\mathsf{Trip}_{\mathsf{cart}}({\operatorname{\mathsf{Set}}})$ the wide
subcategory of $\mathsf{Trip}({\operatorname{\mathsf{Set}}})$ on cartesian
transformations.

A transformation $\Phi^{+}:P\to Q$ admits a _right adjoint_ if there exists
another transformation $\Phi_{+}:Q\to P$ such that
$(\Phi^{+})_{X}\dashv(\Phi_{+})_{X}$ in $\operatorname{\mathsf{Preord}}$ for
all $X$ in $\operatorname{\mathsf{Set}}$, in which case we write
$\Phi^{+}\dashv\Phi_{+}$. If $\Phi^{+}$ is moreover cartesian, then the pair
$(\Phi^{+},\Phi_{+})$ defines a _geometric morphism_ $Q\to P$666The direction
is conventional and follows the same convention for geometric morphisms of
toposes., of which $\Phi_{+}$ and $\Phi^{+}$ constitute respectively the
_direct_ and _inverse image_. For practical reasons, we denote with
$\mathsf{Trip}_{\mathsf{geom}}({\operatorname{\mathsf{Set}}})$ the wide
subcategory of $\mathsf{Trip}_{\mathsf{cart}}({\operatorname{\mathsf{Set}}})$
on transformations having a right adjoint; a morphism $P\to Q$ in
$\mathsf{Trip}_{\mathsf{geom}}({\operatorname{\mathsf{Set}}})$ is hence a
geometric morphism $Q\to P$.

######  Remark 1.15.

Let $\Phi:P\to Q$ be an equivalence and let $\Psi:Q\to P$ be such that
$\Phi\circ\Psi\simeq\operatorname{id}_{Q}$ and
$\Psi\circ\Phi\simeq\operatorname{id}_{P}$. Then, $(\Phi,\Psi):Q\to P$ and
$(\Psi,\Phi):P\to Q$ are both geometric morphisms.

######  Theorem 1.16.

Every geometric morphism of triposes $Q\to P$ induces a geometric morphism
$\operatorname{\mathsf{Set}}[Q]\to\operatorname{\mathsf{Set}}[P]$.

######  Remark 1.17.

The converse is not true in general: a geometric morphism
$\operatorname{\mathsf{Set}}[Q]\to\operatorname{\mathsf{Set}}[P]$ is induced
by a geometric morphism of triposes $Q\to P$ if and only if its inverse image
part _preserves constant objects_ ; again, we refer the reader to [vO08].

######  Example 1.18.

Let $X,Y$ be two complete Heyting algebras regarded as locales. Then,
geometric morphisms $P_{X}\to P_{Y}$ correspond to locale homomorphisms $X\to
Y$.

More precisely, given any geometric morphism
$\Phi=(\Phi^{+},\Phi_{+}):P_{X}\to P_{Y}$, there exists an essentially unique
morphism of locales $f:X\to Y$ such that, regarding $f$ as a morphism of
frames $f^{*}:\operatorname{\mathcal{O}}(Y)\to\operatorname{\mathcal{O}}(X)$
and letting
$f_{*}:\operatorname{\mathcal{O}}(X)\to\operatorname{\mathcal{O}}(Y)$ be its
right adjoint, $\Phi^{+}$ is given by postcomposition with $f^{*}$ and
$\Phi_{+}$ is given by postcomposition with $f_{*}$.

###  1.4. Subtriposes

Geometric inclusions and surjections of toposes admit analogs on the level of
triposes.

######  Definition 1.19.

A geometric morphism of triposes $\Phi=(\Phi^{+},\Phi_{+}):Q\to P$ is an
_inclusion_ if either of the following equivalent conditions hold:

  * –

for every set $X$, $(\Phi_{+})_{X}$ reflects the order;

  * –

$\Phi^{+}\circ\Phi_{+}\simeq\operatorname{id}_{Q}$,

Dually, $\Phi$ is a _surjection_ if either of the following equivalent
conditions hold:

  * –

for every set $X$, $(\Phi^{+})_{X}$ reflects the order;

  * –

$\Phi_{+}\circ\Phi^{+}\simeq\operatorname{id}_{P}$.

######  Proposition 1.20.

Every geometric inclusion (resp. surjection) of triposes $Q\to P$ induces a
geometric inclusion (resp. surjection)
$\operatorname{\mathsf{Set}}[Q]\to\operatorname{\mathsf{Set}}[P]$.

Moreover, every geometric inclusion into $\operatorname{\mathsf{Set}}[P]$ is
induced, up to equivalence, by an essentially unique geometric inclusion of
triposes into $P$.

######  Definition 1.21.

Let $\mathsf{SubTrip}({P})$ be the set of _subtriposes_ of $P$, that is,
triposes endowed with a geometric inclusions into $P$.777For practical
reasons, we identify a subtripos with the inclusion itself. Given two
geometric inclusions $\Phi:Q\hookrightarrow P$ and $\Psi:R\hookrightarrow P$,
we write $\Phi\subseteq\Psi$ if there exists a geometric morphism $\Theta:Q\to
R$ such that $\Phi\simeq\Psi\circ\Theta$ – meaning that
$\Phi_{+}\simeq\Psi_{+}\circ\Theta_{+}$ or equivalently
$\Phi^{+}\simeq\Theta^{+}\circ\Psi^{+}$ –, in which case $\Theta$ is an
inclusion itself. This relation obviously makes $\mathsf{SubTrip}({P})$ into a
preorder.

Two subtriposes $\Phi:Q\hookrightarrow P$ and $\Psi:R\hookrightarrow P$ are
_equivalent_ if they are isomorphic elements of $\mathsf{SubTrip}({P})$, that
is, if both $\Phi\subseteq\Psi$ and $\Psi\subseteq\Phi$ hold; equivalently,
this means that there exists an equivalence $\Theta:Q\to R$ such that
$\Phi\simeq\Psi\circ\Theta$.

As it is known, subtoposes of a topos $\operatorname{\mathsf{E}}$ correspond
up to equivalence to _local operators_ in $\operatorname{\mathsf{E}}$, that
is, morphisms $j:\Omega\to\Omega$ such that, in the internal logic of
$\operatorname{\mathsf{E}}$:

  1. i.

$j(\operatorname{t})=\operatorname{t}$;

  2. ii.

$jj=j$;

  3. iii.

$j(a\land b)=j(a)\land j(b)$,

In a topos of the form $\operatorname{\mathsf{Set}}[P]$ for a canonically
presented tripos $P\coloneqq{\operatorname{\mathsf{Set}}}({-},{\Sigma})$, such
a morphism corresponds to an essentially unique transformation $\Phi_{j}:P\to
P$ which is:

  1. i.

cartesian;

  2. ii.

_inflationary_ , that is, $\operatorname{id}_{P}\leq\Phi_{j}$;

  3. iii.

_idempotent_ , that is, $\Phi_{j}\Phi_{j}\simeq\Phi_{j}$.

Such $\Phi_{j}$ is called a _closure transformation_ on $P$; conversely, every
closure transformation on $P$ determines a local operator on
$\operatorname{\mathsf{Set}}[P]$.

These correspondences lead to the following result.

######  Theorem 1.22.

Let $P$ be a canonically presented tripos and let $\mathsf{ClTrans}({P})$ be
the set of closure transformations on $P$, ordered as above.

  1. (1)

Geometric inclusions into $P$ correspond, up to equivalence, to closure
transformations on $P$; in particular, there is an equivalence of preorder
categories:

$\mathsf{SubTrip}({P})\simeq{\mathsf{ClTrans}({P})}^{\operatorname{op}}$

  2. (2)

Every geometric inclusion of toposes into $\operatorname{\mathsf{Set}}[P]$ is,
up to equivalence, of the form
$\operatorname{\mathsf{Set}}[Q]\to\operatorname{\mathsf{Set}}[P]$, induced by
a geometric inclusion of triposes $Q\to P$; in particular, there is an
equivalence of preorder categories:

$\mathsf{SubTop}({\operatorname{\mathsf{Set}}[P]})\simeq\mathsf{SubTrip}({P})$

######  Remark 1.23.

Note then that the poset reflection of $\mathsf{SubTrip}({P})$ is a bounded
distributive lattice, since so is the set of subtoposes of any topos
considered up to equivalence.

In the case of a canonically presented tripos $P\coloneqq\Sigma^{-}$, we can
even give an explicit description of the inclusion $Q\to P$ inducing a
geometric inclusion into $\operatorname{\mathsf{Set}}[P]$.

Let $(\operatorname{\mathsf{Set}}[P])_{j}$ be the subtopos of
$\operatorname{\mathsf{Set}}[P]$ corresponding to a closure transformation
$\Phi_{j}:P\to P$ and let
$J\coloneqq(\Phi_{j})_{\Sigma}(\operatorname{id}_{\Sigma}):\Sigma\to\Sigma$.
Then, $(\operatorname{\mathsf{Set}}[P])_{j}$ is equivalent over
$\operatorname{\mathsf{Set}}$ to $\operatorname{\mathsf{Set}}[P_{j}]$, where
$P_{j}$ is the canonically presented tripos defined as follows:

  * –

the underlying pseudofunctor is still $\Sigma^{-}$;

  * –

the order $\vdash^{j}$ is redefined as $\phi\vdash_{I}^{j}\psi$ if and only if
$\phi\vdash_{I}J\psi$;

  * –

the implication $\to_{j}$ is redefined as

${{\Sigma\times\Sigma}}$${\Sigma\times\Sigma}$${\Sigma}$$\scriptstyle{\operatorname{id}_{\Sigma}\times
J}$$\scriptstyle{\to}$

while $\top,\bot,\land,\lor$ remain unchanged.888Left and right adjoints for
$f^{*}$ can then be defined as $\phi\mapsto\exists_{f}(\phi)$ and
$\phi\mapsto\forall_{f}(J\phi)$.

This means that we can restate the previous theorem as follows.

######  Corollary 1.24.

Let $P$ be a canonically presented tripos.

Then, every geometric inclusion of toposes into
$\operatorname{\mathsf{Set}}[P]$ is induced, up to equivalence, by a geometric
inclusion of triposes of the form:

${{P_{j}}}$${{P}}$$\scriptstyle{\operatorname{id}_{\Sigma}\circ-}$$\scriptstyle{J\circ-}$$\scriptstyle{\dashv}$

for some $J:\Sigma\to\Sigma$ corresponding as above to a closure
transformation $\Phi_{j}$ on $P$.

######  Example 1.25.

Let $X$ be a complete Heyting algebra regarded as a locale. Then, closure
transformations on $P_{X}$ correspond to _nuclei_ on $X$, that is, monotone,
inflationary and idempotent endofunctions on the underlying frame of $X$;
therefore, they also correspond to _sublocales_ of $X$.

Another important notion from topos theory which can be recovered at the level
of triposes is that of _open_ and _closed_ subtoposes.

######  Definition 1.26.

A subtripos $\Phi:Q\hookrightarrow P$ is _open_ if there exists an element
$\alpha\in P(1)$ such that, for any $\phi\in P(I)$:

$\Phi_{+}\Phi^{+}(\phi)\simeq P(!)(\alpha)\to\phi$

where $!$ is the unique function $I\to 1$.

Dually, a geometric inclusion of triposes $\Psi:R\hookrightarrow P$ is
_closed_ if there exists an element $\beta\in P(1)$ such that, for any
$\phi\in P(I)$:

$\Psi_{+}\Psi^{+}(\phi)\simeq\phi\lor P(!)(\beta)$

where $!$ is the unique function $I\to 1$.

For $\alpha=\beta$, $\Phi$ and $\Psi$ define each other’s complement in the
lattice of subtriposes of $P$ considered up to equivalence.

######  Corollary 1.27.

Through the correspondence in Theorem 1.22, open (resp. closed) subtriposes
correspond to open (resp. closed) subtoposes.

######  Example 1.28.

Let $X$ be a complete Heyting algebra regarded as a locale. Then, open (resp.
closed) subtriposes of $P_{X}$ correspond to _open_ (resp. _closed_)
_sublocales_ of $X$.

##  2\. Arrow algebras

###  2.1. Arrow algebras

We now review the theory of arrow algebras presented in [vdBB23].

######  Definition 2.1.

An _arrow structure_ is a complete meet-semilattice $(A,\preccurlyeq)$ endowed
with a binary operation $\to\ :A\times A\to A$ such that if
$a^{\prime}\preccurlyeq a$ and $b\preccurlyeq b^{\prime}$, then $a\to
b\preccurlyeq a^{\prime}\to b^{\prime}$.

A _separator_ on an arrow structure $(A,\preccurlyeq,\to)$ is a subset
$S\subseteq A$ such that:

  1. i.

it is _upward closed_ , i.e. if $a\in S$ and $a\preccurlyeq b$ then $b\in S$;

  2. ii.

it is _closed under modus ponens_ , i.e. if $a\to b\in S$ and $a\in S$ then
$b\in S$;

  3. iii.

it contains the _combinators_ :

$\displaystyle\mathbf{k}$
$\displaystyle\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}a\to b\to a$ $\displaystyle\mathbf{s}$
$\displaystyle\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b,c\in
A}(a\to b\to c)\to(a\to b)\to(a\to c)$ $\displaystyle\mathbf{a}$
$\displaystyle\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,(b_{i})_{i\in
I},(c_{i})_{i\in I}\in
A}\left(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}a\to b_{i}\to c_{i}\right)\to
a\to\left(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}b_{i}\to c_{i}\right)$

An _arrow algebra_ is a quadruple $(A,\preccurlyeq,\to,S)$ where
$(A,\preccurlyeq,\to)$ is an arrow structure and $S$ is a separator on it.

######  Notation.

We will assume that $\to$ associates to the right, as it is common in type
theory, and binds stronger than
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@$.
This means that, for example, the combinator $\mathbf{k}$ is given by
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}(a\to(b\to a))$.

A fundamental property of arrow algebras is given by the following.

######  Proposition 2.2.

Let $\operatorname{\mathcal{A}}=(A,\preccurlyeq,\to,S)$ be an arrow algebra.

  1. (1)

Let $(x_{i})_{i\in I},(y_{i})_{i\in I}$ and $(z_{i})_{i\in I}$ be $I$-indexed
families of elements in $A$. If:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}x_{i}\to y_{i}\to z_{i}\in
S\quad\mbox{and}\quad\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}x_{i}\in S$

then:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}y_{i}\to z_{i}\in S$

  2. (2)

Let $\phi$ be a propositional formula built from propositional variables
$p_{1},\dots,p_{n}$ using implications only. If $\phi$ is an intuitionistic
tautology, then:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a_{1},\dots,a_{n}\in
A}\phi(a_{i}/p_{i})\in S$

######  Remark 2.3.

In the following, we will make extensive use of the previous proposition,
which we will justify simply as _intuitionistic reasoning_.

The idea, in essence, is to find a suitable propositional intuitionistic
tautology built of implications, in general of the shape $\phi\to\psi\to\chi$,
so that
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@\phi\to\psi\to\chi\in
S$ as in (2); then, from the knowledge of
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@\phi\in
S$, we can deduce
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@\psi\to\chi\in
S$ as in (1).

######  Corollary 2.4.

Let $(A,\preccurlyeq,\to,S)$ be an arrow algebra. Then, $S$ contains the
combinators:

$\displaystyle\mathbf{i}$
$\displaystyle\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}a\to a$ $\displaystyle\mathbf{b}$
$\displaystyle\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b,c\in
A}(b\to c)\to(a\to b)\to(a\to c)$

######  Definition 2.5.

An arrow algebra $\operatorname{\mathcal{A}}=(A,\preccurlyeq,\to,S)$ is
_compatible with joins_ if, for all $a\in A$ and all $B\subseteq A$:

$(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlyvee$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlyvee$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlyvee$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlyvee$}}}}}\slimits@_{b\in
B}b)\to
a=\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{b\in
B}b\to a$

###  2.2. Nuclei

We now introduce _nuclei_ , a generalization of the locale-theoretical notion
which will correspond to closure transformations on (and hence subtriposes of)
arrow triposes.

######  Definition 2.6.

Let $\mathcal{A}=(A,\preccurlyeq,\to,S)$ be an arrow algebra. A _nucleus_ on
$\mathcal{A}$ is a function $j:A\to A$ such that:

  1. i.

if $a\preccurlyeq b$ then $ja\preccurlyeq jb$;

  2. ii.

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}a\to ja\in S$;

  3. iii.

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}(a\to jb)\to ja\to jb\in S$.

In particular, these properties imply:

  1. iv.

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}jja\to ja\in S$;

  2. v.

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}(a\to b)\to ja\to jb\in S$;

  3. vi.

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}j(a\to b)\to ja\to jb\in S$,

and we can also substitute (iii) in the definition with the conjunction of
(iv) and (vi).

Just as every nucleus $j$ on a frame induces the quotient frame of $j$-closed
elements, starting from every nucleus $j$ on an arrow algebra
$\operatorname{\mathcal{A}}$ we can define a new arrow algebra
$\operatorname{\mathcal{A}}_{j}$. We will see later how these arrow algebras
can be thought of as “quotients” of $\operatorname{\mathcal{A}}$.

######  Proposition 2.7.

Let $\mathcal{A}=(A,\preccurlyeq,\to,S)$ be an arrow algebra and let $j:A\to
A$ be a nucleus on it. Then, $\mathcal{A}_{j}=(A,\preccurlyeq,\to_{j},S_{j})$
with

$a\to_{j}b\coloneqq a\to jb\qquad S_{j}\coloneqq\Set{a\in A}{ja\in S}$

is also an arrow algebra, which is compatible with joins whenever so is
$\mathcal{A}$.

######  Remark 2.8.

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}a\to ja\in S$ implies that $S\subseteq S_{j}$: in fact, if $a\in S$, then by
modus ponens $ja\in S$, which precisely means $a\in S_{j}$.

######  Example 2.9.

For any arrow algebra $\mathcal{A}=(A,\preccurlyeq,\to,S)$ and all $c\in A$,
the following are nuclei on $\operatorname{\mathcal{A}}$:

  1. (1)

$ja\coloneqq c\to a$;

  2. (2)

$ja\coloneqq(a\to c)\to c$;

  3. (3)

$ja\coloneqq(a\to c)\to a$.

Particularly relevant in the theory of arrow algebras is the nucleus:

$\partial a\coloneqq\top\to a$

which is the special case of (1) above for $c=\top$. Note that it satisfies
the extra property:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}(\top\to a)\to a\in S$

This follows by intuitionistic reasoning since $q\to(q\to p)\to p$ is an
intuitionistic tautology and $\top\in S$.

###  2.3. The interpretation of $\lambda$-terms

As for implicative algebras, we can interpret $\lambda$-terms in any arrow
algebra $\operatorname{\mathcal{A}}=(A,\preccurlyeq,\to,S)$. To do this, we
need to interpret applications and abstractions.

######  Definition 2.10.

For $a,b\in A$, we define the _application_ :

$ab\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@\Set{c\to
d\in A}{a\preccurlyeq b\to c\to d}$

######  Lemma 2.11.

The application enjoys the following properties.

  1. (1)

If $a\preccurlyeq a^{\prime}$ and $b\preccurlyeq b^{\prime}$, then
$ab\preccurlyeq a^{\prime}b^{\prime}$.

  2. (2)

$(a\to b\to c)a\preccurlyeq b\to c$.

  3. (3)

$(a\to\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}b_{i}\to
c_{i})a\preccurlyeq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}b_{i}\to c_{i}$.

  4. (4)

If $a,b\in S$, then $ab\in S$.

######  Definition 2.12.

For a function $f:A\to A$, we define the _abstraction_ :

$\lambda
f\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{x\in
A}x\to\partial f(x)$

######  Lemma 2.13.

Let $f,g:A\to A$ be functions; the abstraction enjoys the following
properties.

  1. (1)

If $f(a)\preccurlyeq g(a)$ for all $a\in A$, then $\lambda
f\preccurlyeq\lambda g$.

  2. (2)

$(\lambda f)a\preccurlyeq\partial f(a)$ for all $a\in A$.

######  Notation.

We will assume that application associates to the left and binds stronger than
$\to$, which binds stronger than $\partial$, which binds stronger than
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@$.
In particular, this means that $a\to bc$ stands for $a\to(bc)$, $\partial ab$
stands for $\partial(ab)$, and $\partial a\to b$ stands for $\top\to a\to b$
rather than $(\top\to a)\to b$.

We can now recursively define an interpretation of $\lambda$-terms in
$\operatorname{\mathcal{A}}$.

######  Definition 2.14.

Let $M$ be a $\lambda$-term with free variables among $x_{1},\dots,x_{n}$. The
_interpretation_ ot $M$ in $\mathcal{A}$ is a function
$M^{\mathcal{A}}:A^{n}\to A$ defined recursively as follows:

  1. (1)

if $M=x_{i}$, then $M^{\mathcal{A}}$ is the projection onto the $i$-th
coordinate;

  2. (2)

if $M=N_{1}N_{2}$, then:

$M^{\mathcal{A}}(\underline{a})\coloneqq
N_{1}^{\mathcal{A}}(\underline{a})N_{2}^{\mathcal{A}}(\underline{a})$

  3. (3)

if $M=\lambda x.N$ where the free variables of $N$ are among
$x_{1},\dots,x_{n},x$, then:

$M^{\mathcal{A}}(\underline{a})\coloneqq\lambda(b\mapsto
N^{\mathcal{A}}(\underline{a},b))$

The proof of the following nontrivial result needs a detour which is carried
out in full details in [vdBB23].

######  Theorem 2.15.

Let $\mathcal{A}=(A,\preccurlyeq,\to,S)$ be an arrow algebra and let $M$ be a
$\lambda$-term with free variables among $x_{1},\dots,x_{n}$. Then, for any
$a_{1},\dots,a_{n}\in S$:

$M^{\mathcal{A}}(a_{1},\dots,a_{n})\in S$

###  2.4. The logical order

Although arrow algebras are defined in terms of $\preccurlyeq$, which we refer
to as the _evidential order_ , there is another – arguably more important –
order which can be defined in terms of implications and separators. As we will
see, this order will be the only relevant one in the construction of the arrow
tripos.

######  Definition 2.16.

Let $\operatorname{\mathcal{A}}=(A,\preccurlyeq,\to,S)$ be an arrow algebra.
We define the _logical order_ $\vdash$ on $A$ by letting:

$a\vdash b\iff a\to b\in S$

which is weaker than the evidential order since $\mathbf{i}\in S$ gives $a\to
a\in S$ for all $a\in A$ and therefore if $a\preccurlyeq b$ then $a\to
a\preccurlyeq a\to b\in S$ i.e. $a\vdash b$.

Note that $\vdash$ allows us to recover the separator999In hindsight, this
characterizes the separator as what Pitts calls the set of _designated truth
values_ of the induced arrow tripos. as:

$S=\Set{a\in A}{\top\vdash a}$

Indeed, if $a\in A$ is such that $\top\vdash a$, then $a\in S$ follows by
modus ponens from $\top,\top\to a\in S$; conversely, if $a\in S$, then the
intuitionistic tautology $p\to q\to p$ gives $a\to\top\to a\in S$ and hence
$\top\to a\in S$ by modus ponens.

######  Remark 2.17.

We denote with $\vdash^{j}$ the logical order in the arrow algebra
$\operatorname{\mathcal{A}}_{j}$ induced by a nucleus $j$ on
$\operatorname{\mathcal{A}}$. Explicitly, $a\vdash^{j}b$ if and only if
$j(a\to jb)\in S$, which by the properties of nuclei and separators is
equivalent to $a\to jb\in S$ and hence to $a\vdash jb$.

######  Proposition 2.18.

$(A,\vdash)$ is a Heyting prealgebra, with $\to$ being the Heyting
implication.

###### Proof (sketch).

The combinators $\mathbf{i},\mathbf{b}\in S$ respectively express reflexivity
and transitivity of $\vdash$, making $(A,\vdash)$ into a preorder, which is
bounded by $\top$ and $\bot$ since $\bot\preccurlyeq a\preccurlyeq\top$ for
all $a\in A$. For $a,b\in A$, a meet of $a$ and $b$ can be defined as:

$\displaystyle a\times b\coloneqq{}$ $\displaystyle(\lambda z.z(\partial
a)(\partial b))^{\operatorname{\mathcal{A}}}$ $\displaystyle={}$
$\displaystyle\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{z\in
A}z\to\partial z(\partial a)(\partial b)$

while a join can be defined as:

$a+b\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{c\in
A}(a\to\partial c)\to(b\to\partial c)\to\partial c$

∎

###  2.5. The arrow tripos

Let $\operatorname{\mathcal{A}}=(A,\preccurlyeq,\to,S)$ be an arrow algebra.

######  Definition 2.19.

For any set $I$, the set $A^{I}$ of functions $I\to A$ can be given an arrow
structure by choosing pointwise order and implication, and the _uniform power
separator_ 101010The name comes from the analog for implicative algebras in
[Miq20a].:

$S^{I}\coloneqq\Set{\phi:I\to
A}{\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}\phi(i)\in S}$

makes it into an arrow algebra which we denote as
$\operatorname{\mathcal{A}}^{I}$.

The logical order in $\mathcal{A}^{I}$, which we denote as $\vdash_{I}$, is
therefore given explicitly by:

$\phi\vdash_{I}\psi\iff\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i\in
I}\phi(i)\to\psi(i)\in S$

and, by 2.18, $(A^{I},\vdash_{I})$ is a Heyting prealgebra.

######  Remark 2.20.

As above, given some nucleus $j$ on $\operatorname{\mathcal{A}}$, we denote
with $\vdash^{j}_{I}$ the logical order in
$\operatorname{\mathcal{A}}_{j}^{I}$. Again by the properties of nuclei and
separators, $\phi\vdash^{j}_{I}\psi$ explicitly means $\phi\vdash_{I}j\psi$.

######  Remark 2.21.

In general, $\vdash_{I}$ is stronger than the pointwise version of $\vdash$:
the two coincide only if the separator is closed under arbitrary meets.
However, it is easy to see that all the Heyting structure in
$(A^{I},\vdash_{I})$ is determined pointwise by that of $(A,\vdash)$.

We can finally define the _arrow tripos_ induced by
$\operatorname{\mathcal{A}}$, of which the Heyting prealgebras
$(A^{I},\vdash_{I})$ are the components at each level $I$.

######  Theorem 2.22.

Let $\mathcal{A}=(A,\preccurlyeq,\to,S)$ be an arrow algebra. The functor:

$P_{\operatorname{\mathcal{A}}}:{\operatorname{\mathsf{Set}}}^{\operatorname{op}}\to\operatorname{\mathsf{HeytPre}}\qquad\leavevmode\hbox
to81.98pt{\vbox to55.23pt{\pgfpicture\makeatletter\hbox{\hskip
41.5522pt\lower-27.66592pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-40.4251pt}{-27.56609pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
6.89581pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.59027pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${I}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
6.89581pt\hfil&\hfil\hskip 44.12328pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.81776pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${{(A^{I},\vdash_{I})}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
20.1233pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
7.559pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.25346pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${J}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.559pt\hfil&\hfil\hskip 44.86607pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.56056pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${{(A^{J},\vdash_{J})}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
20.8661pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-32.86609pt}{-16.87306pt}\pgfsys@lineto{-32.86609pt}{4.74036pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-32.86609pt}{4.94034pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-39.39943pt}{-7.61638pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{f}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{19.55899pt}{2.64032pt}\pgfsys@lineto{19.55899pt}{-14.55977pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{19.55899pt}{-14.75975pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.91176pt}{-7.9097pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{-\circ
f}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{{
{\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@miterjoin{} {}
\pgfsys@moveto{0.0pt}{1.63991pt}\pgfsys@lineto{0.0pt}{-1.63991pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{-25.4703pt}{11.50003pt}\pgfsys@lineto{-1.16428pt}{11.50003pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-25.5703pt}{11.50003pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-0.9643pt}{11.50003pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{-24.80711pt}{-25.06609pt}\pgfsys@lineto{-1.90707pt}{-25.06609pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-24.9071pt}{-25.06609pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.70709pt}{-25.06609pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

is a (canonically presented) tripos.

In particular, left and right adjoints to
$f^{*}:P_{\operatorname{\mathcal{A}}}(I)\to P_{\operatorname{\mathcal{A}}}(J)$
are given by:

$\displaystyle\exists_{f}(\alpha)(i)$
$\displaystyle\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}\left(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{j\in{f}^{\kern
0.50003pt\text{-}1}(i)}\alpha(j)\to\partial a\right)\to\partial\partial a$
$\displaystyle\forall_{f}(\alpha)(i)$
$\displaystyle\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{j\in{f}^{\kern
0.50003pt\text{-}1}(i)}\partial\alpha(j)$

while a generic element is trivially given by $\operatorname{id}_{A}:A\to A\in
P_{\operatorname{\mathcal{A}}}(A)$.

######  Remark 2.23.

If $\operatorname{\mathcal{A}}$ is compatible with joins, a left adjoint to
$f^{*}:P_{\operatorname{\mathcal{A}}}(I)\to P_{\operatorname{\mathcal{A}}}(J)$
can also be defined as:

$\exists_{f}(\alpha)(i)\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlyvee$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlyvee$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlyvee$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlyvee$}}}}}\slimits@_{j\in{f}^{\kern
0.50003pt\text{-}1}(i)}\alpha(j)$

######  Notation.

We denote with $\mathsf{AT}({\operatorname{\mathcal{A}}})$ the _arrow topos_
induced by $\operatorname{\mathcal{A}}$, that is:

$\mathsf{AT}({\operatorname{\mathcal{A}}})\coloneqq\operatorname{\mathsf{Set}}[P_{\operatorname{\mathcal{A}}}]$

##  3\. Examples of arrow algebras

###  3.1. Implicative algebras

Implicative algebras can be characterized as arrow algebras where the
equality:

$a\to\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{b\in
B}b=\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{b\in
B}a\to b$

holds for all elements $a$ and subsets $B$.

###  3.2. Frames

Every frame $\operatorname{\mathcal{O}}(X)$ can be canonically seen as an
arrow algebra111111In particular, compatible with joins. by using its order
and its Heyting implication as the arrow structure, and $\\{\top\\}$ as the
separator. Note then that the logical order coincides with the evidential
order, since $x\to y\in S$ if and only if $\top\leq x\to y$, which is
equivalent to $x\leq y$.

Similarly, the logical order $\vdash_{I}$ on
$\operatorname{\mathcal{O}}(X)^{I}$ reduces to the pointwise order, which
makes so that the arrow tripos $P_{\operatorname{\mathcal{O}}(X)}$ coincides
with the localic tripos induced by $\operatorname{\mathcal{O}}(X)$, and hence
$\mathsf{AT}({\operatorname{\mathcal{O}}(X)})$ is equivalent to the topos
$\operatorname{Sh}(\operatorname{\mathcal{O}}(X))$ of sheaves over
$\operatorname{\mathcal{O}}(X)$.

###  3.3. Partial combinatory algebras

A main example of arrow algebras arises from partial combinatory algebras,
building blocks of realizability toposes. We review here their theory: as
already in [vdBB23], our treatment closely follows that of [Zoe22], which
allows us for the highest level of generality considered in the literature in
what concerns appropriate notions of morphisms and their connections with
morphisms of the associated toposes. We then warn the reader that the
following definitions and conventions are not entirely standard, but they turn
out to be particularly convenient for our purposes.

######  Definition 3.1.

A _partial applicative poset_ is a poset $(P,\leq)$ endowed with a partial
binary map $\cdot:P\times P\to P$ called _application_ such that if $a\leq
a^{\prime}$ and $b\leq b^{\prime}$ and $a^{\prime}\cdot b^{\prime}$ is
defined, then $a\cdot b$ is defined as well and $a\cdot b\leq a^{\prime}\cdot
b^{\prime}$. $(P,\leq,\cdot)$ is _total_ if $\cdot$ is a total operation, and
it is _discrete_ if $\leq$ is a discrete order.

We denote $a\cdot b$ also as $ab$, and we assume that $\cdot$ associates to
the left. We write ${ab}{\downarrow}$ to indicate that $ab$ is defined; note
that a statement like “${abc}{\downarrow}$” is to be interpreted as
“${ab}{\downarrow}$ and ${(ab)c}{\downarrow}$”.

A _filter_ on a partial applicative poset $(P,\leq,\cdot)$ is a subset
$P^{\\#}\subseteq P$ such that:

  1. i.

it is _upward closed_ , i.e. if $a\in P^{\\#}$ and $a\leq b$ then $b\in
P^{\\#}$;

  2. ii.

it is _closed under defined application_ , i.e. if $a,b\in P^{\\#}$ and
${ab}{\downarrow}$ then $ab\in P^{\\#}$.

A _partial applicative structure_ is the datum $(P,\leq,\cdot,P^{\\#})$ of a
partial applicative poset ${(P,\leq,\cdot)}$ together with a filter $P^{\\#}$
on it. In particular, it is _absolute_ if $P^{\\#}=P$.

A _partial combinatory algebra_ is a partial applicative structure
$(P,\leq,\cdot,P^{\\#})$ such that there exist elements
$\mathbf{k},\mathbf{s}\in P^{\\#}$ satisfying:

  1. i.

${\mathbf{k}ab}{\downarrow}$ and $\mathbf{k}ab\leq a$;

  2. ii.

${\mathbf{s}ab}{\downarrow}$;

  3. iii.

if ${ac(bc)}{\downarrow}$, then ${\mathbf{s}abc}{\downarrow}$ and
$\mathbf{s}abc\leq ac(bc)$,

for all $a,b,c\in P$. A partial combinatory algebra is _total_ or _discrete_
if the underlying partial applicative poset is, and it is _absolute_ if it is
absolute as a partial applicative structure.

######  Notation.

Let $(P,\leq,\cdot)$ be a partial applicative poset. Given two possibly
undefined expressions $e,e^{\prime}$ that, if defined, assume values in $P$,
we write $e\preceq e^{\prime}$ for the following statement: “if
${e^{\prime}}{\downarrow}$, then ${e}{\downarrow}$ and $e\leq
e^{\prime}$”.121212This relation is also called _Kleene inequality_. Instead,
we write $e\leq e^{\prime}$ only if both expressions are always defined.

######  Example 3.2.

The archetypal example of a PCA is _Kleene’s first model_ $\mathcal{K}_{1}$,
underlying Kleene’s original number realizability of [Kle45].
$\mathcal{K}_{1}$ is the absolute and discrete PCA defined on ${\mathbb{N}}$
by letting $n\cdot m$ be the result of the $n$-th partial recursive function
$\varphi_{n}$ on input $m$ whenever defined, fixed an ordering
$\Set{\varphi_{i}}{i\in{\mathbb{N}}}$ of the partial recursive functions
${\mathbb{N}}\to{\mathbb{N}}$.

######  Example 3.3.

Underlying _function realizability_ , a variant of Kleene’s number
realizability introduced in [Kle65], is _Kleene’s second model_
$\mathcal{K}_{2}$, a discrete PCA defined on the set
${\mathbb{N}}^{\mathbb{N}}$ with total recursive functions as the filter.

The _van Oosten model_ $\mathcal{B}$, introduced in [vO97a], generalizes
$\mathcal{K}_{2}$ by considering all _partial_ functions
${\mathbb{N}}\rightharpoonup{\mathbb{N}}$ as its domain, and _partial_
recursive functions as the filter; in that case, we obtain however a _total_
PCA. It can also be ordered by letting $\alpha\leq\beta$ if $\alpha$ extends
$\beta$ as partial functions ${\mathbb{N}}\rightharpoonup{\mathbb{N}}$, in
which case a filter is given by all subfunctions of partial recursive
functions.

Elements of a PCA are usually called _combinators_ ; in particular, the
$\mathbf{k}$ and $\mathbf{s}$ combinators correspond to constants from
Schönfinkel’s _combinatory logic_. Their most important consequence is
_combinatory completeness_ : every partial function obtained by repeatedly
applying the application map is already present as a computation in the PCA
itself.

More formally, let $\mathbb{P}=(P,\leq,\cdot,P^{\\#})$ be a PCA. The set of
_terms_ over $\mathbb{P}$ is defined recursively as follows:

  * –

we assume given a countable set of distinct variables, each of which is a
term;

  * –

we assume given a constant symbol for each element in $P$, each of which is a
term;

  * –

if $t_{0},t_{1}$ are terms, then so is $t_{0}\cdot t_{1}$.

Every term $t=t(x_{1},\dots,x_{n})$ defines a partial function
$P^{n}\rightharpoonup P$ which assigns the obvious, possibly undefined,
interpretation $t(a_{1},\dots,a_{n})$ to an input sequence
$(a_{1},\dots,a_{n})\in P^{n}$. Combinatory completeness can then be expressed
as follows.

######  Proposition 3.4 (Combinatory completeness).

For every nonempty sequence $\underline{x},y$ of distinct variables and every
term $t=t(\underline{x},y)$, there exists an element
$\lambda^{*}\underline{x},y.t\in P$ such that, for every sequence
$\underline{a}$ of the same length as $\underline{x}$ and every $b$ in $P$:

  1. (1)

${(\lambda^{*}\underline{x},y.t)\underline{a}}{\downarrow}$;

  2. (2)

$(\lambda^{*}\underline{x},y.t)\underline{a}b\preceq t(\underline{a},b)$.

Moreover, if all the constants occurring in $t$ are from $P^{\\#}$, then
$\lambda^{*}\underline{x},y.t\in P^{\\#}$ as well.

Combinatory completeness allows us to perform constructions from recursion
theory inside $\mathbb{P}$: let us see some examples which we will make use of
in the following. Since they also correspond to constants of combinatory
logic, they are called combinators as well.

  1. i.

The _identity combinator_ is defined as

$\mathbf{i}\coloneqq\lambda^{*}x.x\in P^{\\#}$

and it satisfies $\mathbf{i}a\leq a$ for all $a\in P$.

  2. ii.

The _constant combinator_ $\mathbf{k}$ can also be defined as
$\lambda^{*}xy.x$; its ‘dual’ $\overline{\mathbf{k}}\in P^{\\#}$ is defined as

$\overline{\mathbf{k}}\coloneqq\mathbf{ki}$

and it satisfies $\overline{\mathbf{k}}ab\leq b$ for all $a,b\in P$.

  3. iii.

The _pairing combinator_ $\mathbf{p}\in P^{\\#}$ and the _unpairing
combinators_ $\mathbf{p}_{0},\mathbf{p}_{1}\in P^{\\#}$ are defined as

$\mathbf{p}\coloneqq\lambda^{*}x,y,z.zxy\qquad\mathbf{p}_{0}\coloneqq\lambda^{*}x.x\mathbf{k}\qquad\mathbf{p}_{1}\coloneqq\lambda^{*}x.x\overline{\mathbf{k}}$

and they satisfy $\mathbf{p}_{0}(\mathbf{p}ab)\leq a$ and
$\mathbf{p}_{1}(\mathbf{p}ab)\leq b$ for all $a,b\in P$.

The most important construction on a PCA, at least in the context of this
paper, is the following.

######  Definition 3.5.

Let $\mathbb{P}=(P,\leq,\cdot,P^{\\#})$ be a PCA. The set $DP$ of downward-
closed subsets of $P$, ordered by inclusion, can be given an application
operation by defining, for $\alpha,\beta\in DP$:

$\alpha\cdot\beta\coloneqq{\downarrow}{\Set{xy}{x\in\alpha,\ y\in\beta}}$

in case ${xy}{\downarrow}$ for all $x\in\alpha$ and $y\in\beta$ – in
particular, this gives ${\alpha\beta}{\downarrow}$ and $\alpha\beta=\emptyset$
in case either $\alpha=\emptyset$ or $\beta=\emptyset$. Then, the family of
downward-closed subsets containing an element from $P^{\\#}$ is a filter on
this partial applicative poset:

$\displaystyle(DP)^{\\#}\coloneqq{}$ $\displaystyle\Set{\alpha\in DP}{\exists
a\in\alpha\cap P^{\\#}}$ $\displaystyle={}$ $\displaystyle\Set{\alpha\in
DP}{\exists a\in P^{\\#}:{\downarrow}{\\{a\\}}\subseteq\alpha}$
$\displaystyle={}$ $\displaystyle\Set{\alpha\in DP}{\exists\beta\in
D(P^{\\#}):\exists b\in\beta\land\beta\subseteq\alpha}$

and two combinators $\mathbf{k},\mathbf{s}\in P^{\\#}$ for $\mathbb{P}$ yield
corresponding combinators
${\downarrow}{\\{\mathbf{k}\\}},{\downarrow}{\\{\mathbf{s}\\}}\in(DP)^{\\#}$
making $(DP,\subseteq,\cdot,(DP)^{\\#})$ into a PCA which we denote as
$D\mathbb{P}$.

######  Remark 3.6.

For future reference, given a discrete and absolute PCA $\mathbb{P}$, we
denote with $\operatorname{Pow}({\mathbb{P}})$ the PCA $D\mathbb{P}$: note
then that the filter is given by the set of inhabited subsets of $P$.

######  Notation.

Following [Zoe22], for $x\in P$ and $\beta\in DP$ we write $x\cdot\beta$
instead of ${\downarrow}{\\{x\\}}\cdot\beta$. Explicitly,
${x\beta}{\downarrow}$ if ${xy}{\downarrow}$ for all $y\in\beta$, in which
case $x\beta={\downarrow}{\Set{xy}{y\in\beta}}$.

Therefore, given $\gamma\in DP$, $x\cdot\beta\subseteq\gamma$ is equivalent to
$xy\in\gamma$ for all $y\in\beta$.

Given a PCA $\mathbb{P}=(P,\leq,\cdot,P^{\\#})$, the _realizability tripos_
$P_{\mathbb{P}}$ is defined as follows.

For any set $X$, we let $P_{\mathbb{P}}(X)\coloneqq DP^{X}$, ordered by
letting $\phi\vdash_{X}\psi$ if there exists an element $r\in P^{\\#}$ such
that $r\cdot\phi(x)\subseteq\psi(x)$131313Recall that this notation
presupposes ${r\cdot\phi(x)}{\downarrow}$. for all $x\in X$. The Heyting
structure is then given by $\top_{X}(x)\coloneqq P$ and
$\bot_{X}(x)\coloneqq\emptyset$ as top and bottom elements, and for
$\phi,\psi\in P_{\mathbb{P}}(X)$:

$\displaystyle(\phi\land\psi)(x)$
$\displaystyle\coloneqq\mathbf{p}\cdot\phi(x)\cdot\psi(x)$
$\displaystyle(\phi\lor\psi)(x)$
$\displaystyle\coloneqq(\mathbf{p}\cdot\mathbf{k}\cdot\phi(x))\cup(\mathbf{p}\cdot\overline{\mathbf{k}}\cdot\psi(x))$
$\displaystyle(\phi\to\psi)(x)$ $\displaystyle\coloneqq\Set{a\in
P}{a\cdot\phi(x)\subseteq\psi(x)}$

For any function $f:X\to Y$, the precomposition map
$f^{*}:P_{\mathbb{P}}(Y)\to P_{\mathbb{P}}(X)$ is then a morphism of Heyting
prealgebras. Adjoints for $f^{*}$ satisfying the Beck-Chevalley condition are
defined by:

$\displaystyle\exists_{f}(\phi)(y)$
$\displaystyle\coloneqq\bigcup_{x\in{f}^{\kern 0.50003pt\text{-}1}(y)}\phi(x)$
$\displaystyle\forall_{f}(\phi)(y)$ $\displaystyle\coloneqq\Set{a\in
A}{\forall b\in P,\ \forall x\in{f}^{\kern 0.70004pt\text{-}1}(y),\
{ab}{\downarrow}\mbox{ and }ab\in\phi(x)}$

while a generic element is trivially given by $\operatorname{id}_{DP}\in
P_{\mathbb{P}}(DP)$.

We denote with $\mathsf{RT}({\mathbb{P}})$ the _realizability topos_
$\operatorname{\mathsf{Set}}[P_{\mathbb{P}}]$.

######  Example 3.7.

$\mathsf{RT}(\mathcal{K}_{1})$ is the _effective topos_ $\mathsf{Eff}$.

With these definitions, we can finally describe arrow algebras arising from
PCAs.

Let $\mathbb{P}=(P,\leq,\cdot,P^{\\#})$ be a PCA and consider the poset $DP$
of downward-closed subsets of $P$. Defining, for $\alpha,\beta\in DP$:

$\alpha\to\beta\coloneqq\Set{a\in P}{{a\cdot\alpha}{\downarrow}\mbox{ and
}a\cdot\alpha\subseteq\beta}$

and letting $S_{DP}$ be the family of downward-closed subsets containing an
element from the filter $P^{\\#}$ – that is, $S_{DP}=(DP)^{\\#}$ –, [vdBB23,
Thm. 3.9] shows how $(DP,\preccurlyeq,\to,S_{DP})$ is an arrow algebra which
is compatible with joins; we denote it with $D\mathbb{P}$ as for the
corresponding PCA.141414Similarly, we let $\operatorname{Pow}({\mathbb{P}})$
be the arrow algebra $D\mathbb{P}$ for a discrete and absolute PCA
$\mathbb{P}$.

This makes so that the arrow tripos $P_{D\mathbb{P}}$ coincides with the
realizability tripos induced by $\mathbb{P}$, and hence
$\mathsf{AT}({D\mathbb{P}})$ coincides with the realizability topos
$\mathsf{RT}({\mathbb{P}})$.

######  Remark 3.8.

In [vdBB23, Thm. 3.10], another construction is identified which yields an
arrow algebra starting from a PCA. Although it will not play any role in this
paper, we here introduce it to use it as an example in section 9.

Let $\mathbb{P}=(P,\leq,\cdot,P^{\\#})$ be a PCA. Then,
$\mathbb{P}\times\mathbb{P}$ is a PCA with pointwise order and application,
and with the filter $P^{\\#}\times P^{\\#}$, which means that
$D(\mathbb{P}\times\mathbb{P})$ is an arrow algebra. Explicitly, its elements
are downward-closed binary relations on $P$ ordered by inclusion, the
implication is defined as:

$R\to S\coloneqq\Set{(a,a^{\prime})\in P\times P}{{(a,a^{\prime})\cdot
R}{\downarrow}\mbox{ and }(a,a^{\prime})\cdot R\subseteq S}$

while a separator is given by:

$S_{D(P\times P)}\coloneqq\Set{R\in D(P\times P)}{\exists(a,a^{\prime})\in
R\cap(P^{\\#}\times P^{\\#})}$

If we restrict to downward-closed binary relations on $P$ which are symmetric
and transitive151515That is, _partial equivalence relations_., we obtain an
arrow algebra which is compatible with joins; we denote it as
$\mathsf{PER}(\mathbb{P})$.

##  4\. Implicative morphisms

In this section, we introduce the first notion of a morphism between arrow
algebras we will see in this paper, namely that of _implicative morphisms_ ,
and we set up some first results which will be useful in the following.

By definition, an arrow algebra is a poset endowed with an implication and a
specified subset: therefore, it would be natural to define morphisms of arrow
algebras as monotone functions preserving implications (in a suitable sense)
and the specified subset. This intuition, obviously also valid for implicative
algebras, is what leads to the definition of _applicative morphisms_ in
[SM17], which partially inspires our definition. However, for reasons which
will become clear in the following, we will not define our morphisms to be
monotone with respect to the evidential order161616As we have already
mentioned, the evidential order is not the most important feature of an arrow
algebra anyway., but we will see how this will not actually be an issue. The
downside is that, in general, we will have to impose a third condition –
automatically satisfied in case of monotonicity – involving both implications
and separators.

###  4.1. Implicative morphisms

Let $\mathcal{A}=(A,\preccurlyeq,\to,S_{A})$ and
$\mathcal{B}=(B,\preccurlyeq,\to,S_{B})$ be two arrow algebras.

######  Definition 4.1.

An _implicative morphism_ $f:\mathcal{A}\to\mathcal{B}$ is a function $f:A\to
B$ satisfying:

  1. i.

$f(a)\in S_{B}$ for all $a\in S_{A}$;

  2. ii.

there exists an element $r\in S_{B}$ such that $r\preccurlyeq f(a\to
a^{\prime})\to f(a)\to f(a^{\prime})$ for all ${a,a^{\prime}\in A}$;

  3. iii.

for any subset $X\subseteq A\times A$,

$\mbox{if
}\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
X}a\to a^{\prime}\in S_{A}\;\mbox{ then
}\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
X}f(a)\to f(a^{\prime})\in S_{B},$

in which case we say that $f$ is _realized_ by $r\in S_{B}$.

An order ‘up to a realizer’ can be defined on implicative morphisms as
follows. Given two implicative morphisms
$f,f^{\prime}:\mathcal{A}\to\mathcal{B}$, we write $f\vdash f^{\prime}$ if
there exists an element $u\in S_{B}$ such that $u\preccurlyeq f(a)\to
f^{\prime}(a)$ for all $a\in A$, in which case we say that $f\vdash
f^{\prime}$ is _realized_ by $u$. In other words, this means that:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}f(a)\to f^{\prime}(a)\in S_{B}$

i.e. $f\vdash_{A}f^{\prime}$ seeing $f$ and $f^{\prime}$ as elements of the
arrow algebra $\operatorname{\mathcal{B}}^{A}$ of 2.19, so in particular it is
also equivalent to $f\phi\vdash_{I}f^{\prime}\phi$ for all sets $I$ and all
functions $\phi:I\to A$.

######  Remark 4.2.

If $f$ happens to be monotone with respect to the evidential order, then (iii)
is a consequence of (i) and (ii).

Indeed, given any $X\subseteq A\times A$ such that
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
X}a\to a^{\prime}\in S_{A}$:

  * –

by (ii) we have:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
X}f(a\to a^{\prime})\to f(a)\to f(a^{\prime})\in S_{B};$

  * –

as
$f(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@P)\preccurlyeq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@f(P)$
for all subsets $P\subseteq A$ by monotonicity, and by (i) and upward-closure
of $S_{B}$:

$f\left(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
X}a\to
a^{\prime}\right)\preccurlyeq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
X}f(a\to a^{\prime})\in S_{B},$

from which
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
X}f(a)\to f(a^{\prime})\in S_{B}$ by 2.2.

Therefore, to prove that a monotone function is an implicative morphism, we
will systematically omit to check condition (iii).

######  Remark 4.3.

Applicative morphisms of [SM17] only satisfy condition (ii) for
$a,a^{\prime}\in A$ such that $a\vdash a^{\prime}$, while they are monotone by
definition. The two notions are hence incomparable in general.

######  Proposition 4.4.

Arrow algebras, implicative morphisms and their order form a preorder-enriched
category $\operatorname{\mathsf{ArrAlg}}$.

###### Proof.

First, let $f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ and
$g:\operatorname{\mathcal{B}}\to\mathcal{C}$ be implicative morphisms; let us
show that $gf:A\to C$ satisfies the definition of an implicative morphism
$\operatorname{\mathcal{A}}\to\mathcal{C}$. Condition (i) and (iii) are
clearly compositional; to show condition (ii), instead, note that by (ii) for
$f$ we know that:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,a^{\prime}}f(a\to
a^{\prime})\to f(a)\to f(a^{\prime})\in S_{B}$

from which, by (iii) for $g$:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,a^{\prime}}gf(a\to
a^{\prime})\to g(f(a)\to f(a^{\prime}))\in S_{C}$

Moreover, by (ii) for $g$ we know that:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,a^{\prime}}g(f(a)\to
f(a^{\prime}))\to gf(a)\to gf(a^{\prime})\in S_{C}$

from which, by intuitionistic reasoning:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,a^{\prime}}gf(a\to
a^{\prime})\to gf(a)\to gf(a^{\prime})\in S_{C}$

Then, for any arrow algebra $\operatorname{\mathcal{A}}$, the identity
function $\operatorname{id}_{A}$ is an implicative morphism
$\operatorname{\mathcal{A}}\to\operatorname{\mathcal{A}}$, trivially realized
by $\mathbf{i}\in S_{A}$ since we know that:

$\mathbf{i}\preccurlyeq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,a^{\prime}\in
A}(a\to a^{\prime})\to a\to a^{\prime}$

This makes $\operatorname{\mathsf{ArrAlg}}$ into a category. The fact that
$\vdash$ is a preorder on each homset
$\operatorname{\mathsf{ArrAlg}}(\operatorname{\mathcal{A}},\operatorname{\mathcal{B}})$
follows immediately as it is the subpreorder of $(B^{A},\vdash_{A})$ on
implicative morphisms. Therefore, to conclude, we simply need to show that
composition of implicative morphisms is order-preserving:

  * –

for $f,f^{\prime}:\mathcal{A}\to\mathcal{B}$ and $g:\mathcal{B}\to\mathcal{C}$
such that $f\vdash f^{\prime}$; explicitly, this means that:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}f(a)\to f^{\prime}(a)\in S_{B}$

from which, by (iii) in 4.1:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\in
A}gf(a)\to gf^{\prime}(a)\in S_{C}$

meaning that $gf\vdash gf^{\prime}$;

  * –

for $f:\mathcal{A}\to\mathcal{B}$ and
$g,g^{\prime}:\mathcal{B}\to\mathcal{C}$, any realizer of $g\vdash g^{\prime}$
also realizes $gf\vdash g^{\prime}f$.

∎

######  Example 4.5.

Let $j:A\to A$ be a nucleus on an arrow algebra $\mathcal{A}$. Then, (i), (ii)
and (vi) in 2.6 immediately imply that $j$ is an implicative morphism
$\operatorname{\mathcal{A}}\to\operatorname{\mathcal{A}}$.

######  Example 4.6.

In a constructive metatheory, truth values are arranged in the frame $\Omega$
given by the powerset of the singleton $\\{*\\}$171717$\Omega$ is the initial
object in the category of frames, and coincides with
$2\coloneqq\\{\bot\leq\top\\}$ in a classical metatheory., which we can see as
an arrow algebra in the canonical way. For any arrow algebra
$\operatorname{\mathcal{A}}=(A,\preccurlyeq,\to,S)$, we can then consider the
characteristic function of the separator, which is defined constructively as:

$\chi:A\to\Omega\qquad\chi(a)\coloneqq\Set{*}{a\in S}$

Note that, by upward closure of the separator, $\chi$ is monotone. Indeed, if
$a\preccurlyeq a^{\prime}$, to show that $\chi(a)\subseteq\chi(a^{\prime})$
suppose that $*\in\chi(a)$; then, $a\in S$, hence $a^{\prime}\in S$ as well,
i.e. $*\in\chi(a^{\prime})$.

We then have that $\chi$ is an implicative morphism
$\operatorname{\mathcal{A}}\to\Omega$.

  1. i.

If $a\in S$, then by definition $*\in\chi(a)$, which means that
$\chi(a)=\\{*\\}$.

  2. ii.

Let $a,a^{\prime}\in A$. Then, $\\{*\\}\subseteq\chi(a\to
a^{\prime})\to\chi(a)\to\chi(a^{\prime})$ is equivalent to $\chi(a\to
a^{\prime})\subseteq\chi(a)\to\chi(a^{\prime})$. To show this, suppose
$*\in\chi(a\to a^{\prime})$, meaning that $a\to a^{\prime}\in S$. So,
$\chi(a\to a^{\prime})=\\{*\\}$, which means that we can show equivalently
that $\chi(a)\subseteq\chi(a^{\prime})$. Suppose then $*\in\chi(a)$ as well,
meaning that $a\in S$; by modus ponens, it follows that $a^{\prime}\in S$,
i.e. $*\in\chi(a^{\prime})$.

The definition of an implicative morphism can be restated purely in terms of
the logical order.

######  Lemma 4.7.

Let $\operatorname{\mathcal{A}}=(A,\preccurlyeq,\to,S_{A})$ and
$\operatorname{\mathcal{B}}=(B,\preccurlyeq,\to,S_{B})$ be arrow algebras. A
function $f:A\to B$ is an implicative morphism
$\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ if and only if it
satisfies:

  1. (1)

$\top\vdash f(\top)$;

  2. (2)

$f(\pi_{1}\to\pi_{2})\vdash_{A\times A}f\pi_{1}\to f\pi_{2}$, where
$\pi_{1},\pi_{2}:A\times A\to A$ are the two projections;

  3. (3)

$f\phi\vdash_{I}f\psi$ for any set $I$ and all $\phi,\psi:I\to A$ such that
$\phi\vdash_{I}\psi$.

###### Proof.

Condition (2) is a rewriting of condition (ii) recalling that the Heyting
implication in $\operatorname{\mathcal{A}}^{A\times A}$ is computed pointwise,
and condition (3) is a rewriting of condition (iii).

Suppose now $f$ satisfies (i), (ii) and (iii). Then, $f(\top)\in S_{B}$ since
$\top\in S_{A}$, which means that $\top\vdash f(\top)$.

Conversely, suppose that $f$ satisfies (1), (2) and (3). Note that condition
(3) implies that $f$ is monotone with respect to the logical order: therefore,
for $a\in S_{A}$ we have that $\top\vdash a$, and hence $f(\top)\vdash f(a)$.
Then, $\top\vdash f(\top)$ implies by modus ponens that $f(\top)\in S_{B}$,
from which $f(a)\in S_{B}$ as well. ∎

######  Corollary 4.8.

If $f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ is an
implicative morphism and $f^{\prime}:A\to B$ is such that
$f\dashv\vdash_{A}f^{\prime}$ in $\operatorname{\mathcal{B}}^{A}$, then
$f^{\prime}$ is an implicative morphism
$\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ as well.

Many implicative morphisms we will see in the following are monotone with
respect to the evidential order: as it turns out, this can always be assumed
up to isomorphism. Therefore, in principle, we could substitute
$\operatorname{\mathsf{ArrAlg}}$ for an equivalent category where all
morphisms are monotone; however, we will not go in this direction, for reasons
which will become clear in the next sections.

Recall that, for any arrow algebra $\operatorname{\mathcal{A}}$, we can
consider the nucleus $\partial x\coloneqq\top\to x$, which satisfies
$\operatorname{id}_{A}\dashv\vdash_{A}\partial$.

######  Lemma 4.9.

Every implicative morphism is isomorphic to a monotone one.

###### Proof.

Let $f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ be an
implicative morphism and consider the monotone function:

$f^{\prime}:A\to B\qquad
f^{\prime}(a)\coloneqq\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\preccurlyeq
a^{\prime}}\partial f(a^{\prime})$

Let us show that $f\dashv\vdash_{A}f^{\prime}$, which in particular implies
that $f^{\prime}$ is an implicative morphism
$\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ by the previous
corollary.

On one hand, $\partial\vdash_{B}\operatorname{id}_{B}$ gives:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a}(\partial
f(a))\to f(a)\in S_{B}$

from which, since
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\preccurlyeq
a^{\prime}}\partial f(a^{\prime})\preccurlyeq\partial f(a)$ and by upward-
closure of $S_{B}$:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a}(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\preccurlyeq
a^{\prime}}\partial f(a^{\prime}))\to f(a)\in S_{B}$

i.e. $f^{\prime}\vdash_{A}f$.

On the other hand, $f\vdash_{A}f^{\prime}$ explicitly reads as:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a}f(a)\to\left(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\preccurlyeq
a^{\prime}}\partial f(a^{\prime})\right)\in S_{B}$

Note that, since $\mathbf{a}\in S_{B}$:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a}\left(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\preccurlyeq
a^{\prime}}f(a)\to\top\to f(a^{\prime})\right)\to
f(a)\to\left(\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a\preccurlyeq
a^{\prime}}\top\to f(a^{\prime})\right)\in S_{B}$

Therefore, $f\vdash_{A}f^{\prime}$ is ensured by 2.2 if we show:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
I}f(a)\to\partial f(a^{\prime})\in S_{B}$

where $I\coloneqq\Set{(a,a^{\prime})\in A\times A}{a\preccurlyeq a^{\prime}}$.
By intuitionistic reasoning, this is ensured by:

(1)
$\displaystyle\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
I}f(a)\to f(a^{\prime})\in S_{B}$ (2)
$\displaystyle\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
I}f(a^{\prime})\to\partial f(a^{\prime})\in S_{B}$

where (1) follows since $f$ is an implicative morphism and $\mathbf{i}\in
S_{A}$ witnesses the fact that
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(a,a^{\prime})\in
I}a\to a^{\prime}\in S_{A}$, and (2) follows since
$\operatorname{id}_{B}\vdash_{B}\partial$. ∎

######  Remark 4.10.

Let $Mf\coloneqq f^{\prime}$ be the monotone implicative morphism defined
above. Then, $f\mapsto Mf$ is immediately seen to be a pseudofunctor
$M:\operatorname{\mathsf{ArrAlg}}\to\operatorname{\mathsf{ArrAlg}}$ since
$Mf\dashv\vdash f$.

##  5\. Examples of implicative morphisms I

Besides the easy examples seen above, let us see the two main classes of
implicative morphisms, corresponding to the examples of arrow algebras seen in
section 3: those arising from frame homomorphisms, and those arising from
morphisms of PCAs.

###  5.1. Frames

As we know, every frame can be canonically seen as an arrow algebra by
choosing $\\{\top\\}$ as the separator. Then, any morphism of frames
$f:\operatorname{\mathcal{O}}(Y)\to\operatorname{\mathcal{O}}(X)$, a
(necessarily monotone) function preserving finite meets and arbitrary joins,
is also an implicative morphism. Indeed:

  1. i.

$f(\top)=\top$ as $f$ preserves finite meets;

  2. ii.

for $y,y^{\prime}\in\operatorname{\mathcal{O}}(Y)$ we know that $y\land(y\to
y^{\prime})\leq y^{\prime}$, so by monotonicity and meet-preservation
$f(y)\land f(y\to y^{\prime})\leq f(y^{\prime})$, meaning that $f(y\to
y^{\prime})\leq f(y)\to f(y^{\prime})$ and therefore $\top\leq f(y\to
y^{\prime})\to f(y)\to f(y^{\prime})$.

######  Remark 5.1.

As emerges from the above reasoning, more generally we have that any monotone
function $f:\operatorname{\mathcal{O}}(Y)\to\operatorname{\mathcal{O}}(X)$
which preserves finite meets is an implicative morphism.

Recall moreover that $\operatorname{\mathsf{Frm}}$ is preorder-enriched with
respect to the pointwise order: therefore, given two frame homomorphisms
$f,f^{\prime}:\operatorname{\mathcal{O}}(Y)\to\operatorname{\mathcal{O}}(X)$,
$f\leq f^{\prime}$ in
$\operatorname{\mathsf{Frm}}(\operatorname{\mathcal{O}}(Y),\operatorname{\mathcal{O}}(X))$
if and only if $f\vdash f^{\prime}$ in
$\operatorname{\mathsf{ArrAlg}}(\operatorname{\mathcal{O}}(Y),\operatorname{\mathcal{O}}(X))$,
since $\vdash_{I}$ coincides with the pointwise order for any set $I$. In
other words, the inclusion determines a 2-functor
$\operatorname{\mathsf{Frm}}\to\operatorname{\mathsf{ArrAlg}}$ with the
additional property that each map
$\operatorname{\mathsf{Frm}}(\operatorname{\mathcal{O}}(Y),\operatorname{\mathcal{O}}(X))\hookrightarrow\operatorname{\mathsf{ArrAlg}}(\operatorname{\mathcal{O}}(Y),\operatorname{\mathcal{O}}(X))$
(preserves and) reflects the order.

While obviously faithful, this inclusion is far from being full. Indeed,
consider the initial frame $\Omega$ and let $\operatorname{\mathcal{O}}(X)$ be
a frame such that $\bot\neq\top$: then, the unique frame homomorphism
$\Omega\to\operatorname{\mathcal{O}}(X)$ is given by
$p\mapsto\bigvee\Set{\top}{*\in p}$, whereas the constant function of value
$\top$ is an implicative morphism $\Omega\to\operatorname{\mathcal{O}}(X)$. As
we will see in section 7, frame homomorphisms coincide with _computationally
dense_ implicative morphisms, while implicative morphisms between frames
coincide simply with monotone functions preserving finite meets – thus
reversing the previous remark.

###  5.2. Partial combinatory algebras

Let $\operatorname{\mathbb{A}}=(A,\leq,\cdot,A^{\\#})$ and
$\operatorname{\mathbb{B}}=(B,\leq,\cdot,B^{\\#})$ be two PCAs. Let us start
by reviewing the theory of morphisms between PCAs, again following [Zoe22].

######  Definition 5.2.

A _morphism of PCAs_ $\mathbb{A}\to\mathbb{B}$ is a function $f:A\to B$
satisfying:

  1. i.

$f(a)\in B^{\\#}$ for all $a\in A^{\\#}$;

  2. ii.

there exists an element $t\in B^{\\#}$ such that if
${aa^{\prime}}{\downarrow}$ then ${tf(a)f(a^{\prime})}{\downarrow}$ and
$tf(a)f(a^{\prime})\leq f(aa^{\prime})$;

  3. iii.

there exists an element $u\in B^{\\#}$ such that if $a\leq a^{\prime}$ then
${uf(a)}{\downarrow}$ and $uf(a)\leq f(a^{\prime})$,

in which case we say that $f$ is _realized_ by $t,u\in B^{\\#}$, or that it
preserves application up to $t$ and order up to $u$.

An order ‘up to a realizer’ can be defined on morphisms of PCAs as follows.
Given two morphisms $f,f^{\prime}:\mathbb{A}\to\mathbb{B}$, we write $f\leq
f^{\prime}$ if there exists some $s\in B^{\\#}$ such that
${sf(a)}{\downarrow}$ and $sf(a)\leq f^{\prime}(a)$ for all $a\in A$, in which
case we say that $f\leq f^{\prime}$ is _realized_ by $s$.

######  Proposition 5.3.

PCAs, morphisms of PCAs and their order form a preorder-enriched category
$\operatorname{\mathsf{OPCA}}$.

Let’s also introduce here the notion of _computational density_ , which we
will make use of in the following section.

######  Definition 5.4.

A morphism of PCAs $f:\mathbb{A}\to\mathbb{B}$ is _computationally dense_ if
there exists an element $m\in B^{\\#}$ with the property that for all $s\in
B^{\\#}$ there is some $r\in A^{\\#}$ such that $mf(ra)\preceq sf(a)$ for all
$a\in A$.

Let us now note that the construction of 3.5 determine pseudomonads on
$\operatorname{\mathsf{OPCA}}$. Indeed, given a morphism of PCAs
$f:\mathbb{A}\to\mathbb{B}$, we can define a morphism $Df:D\mathbb{A}\to
D\mathbb{B}$ by letting:

$\displaystyle Df(\alpha)\coloneqq{}$ $\displaystyle{\downarrow}{(f(\alpha))}$
$\displaystyle={}$ $\displaystyle{\downarrow}{\Set{f(x)}{x\in\alpha}}$

and this makes the association $\operatorname{\mathbb{A}}\mapsto
D\operatorname{\mathbb{A}}$ pseudofunctorial. Then, a pseudomonad structure is
defined considering:

  * –

as unit $\delta$, the pseudonatural transformation
$:\operatorname{id}_{\operatorname{\mathsf{OPCA}}}\Rightarrow D$ of components
$\delta_{\mathbb{A}}:\mathbb{A}\to D\mathbb{A}$ given by the (computationally
dense) morphisms of PCAs sending $a\in A$ to the _principal downset_
${\downarrow}{\\{a\\}}\in DA$;

  * –

as multiplication $\bigcup$, the pseudonatural transformation $DD\Rightarrow
D$ of components
$\bigcup_{\operatorname{\mathbb{A}}}:DD\operatorname{\mathbb{A}}\to
D\operatorname{\mathbb{A}}$ given by the (computationally dense) morphisms of
PCAs sending $\alpha\in DDA$ to its union $\bigcup\alpha$.181818In this case,
naturality actually holds on the nose.

Through this pseudomonad we can define two new notions of morphism of PCAs.

######  Definition 5.5.

Let $\operatorname{\mathsf{OPCA}}_{D}$ be the preorder-enriched bicategory
defined as the Kleisli bicategory of the pseudomonad
$\left(D,\delta,\bigcup\right)$. Explicitly,
$\operatorname{\mathsf{OPCA}}_{D}$ is the category having PCAs as objects, and
morphisms of PCAs $\operatorname{\mathbb{A}}\to D\operatorname{\mathbb{B}}$ as
morphisms $\operatorname{\mathbb{A}}\to\operatorname{\mathbb{B}}$, which we
call _partial applicative morphisms_.

A morphism in $\operatorname{\mathsf{OPCA}}_{D}$ is computationally dense if
it is so as a morphism of PCAs. Explicitly, a partial applicative morphism
$f:\operatorname{\mathbb{A}}\to\operatorname{\mathbb{B}}$ is then
computationally dense if there exists an element $m\in B^{\\#}$ with the
property that for all $s\in B^{\\#}$ there is some $r\in A^{\\#}$ satisfying
${mf(ra)}{\downarrow}$ and $mf(ra)\subseteq sf(a)$ for any $a\in A$ such that
${sf(a)}{\downarrow}$.

######  Remark 5.6.

As $D$ is a pseudomonad, $\operatorname{\mathsf{OPCA}}_{D}$ is not strictly a
(preorder-enriched) category but only a bicategory. The only axiom of an
ordinary category that does not hold, however, is $f\circ\operatorname{id}=f$.
Since it can be shown that $f$ satisfies $f\circ\operatorname{id}=f$ if and
only if it preserves the order on the nose, $f$ can therefore be replaced up
to isomorphism with $f\circ\operatorname{id}$ which preserves the order on the
nose: under this identification, $\operatorname{\mathsf{OPCA}}_{D}$ can then
be treated as a preorder-enriched category.

######  Remark 5.7.

A partial applicative morphism
$f:\operatorname{\mathbb{A}}\to\operatorname{\mathbb{B}}$ is _total_ if
$\operatorname{dom}{f}=A$, where:

$\operatorname{dom}{f}\coloneqq\Set{a\in A}{\exists b\in f(a)}$

######  Example 5.8.

The map $h(\alpha)\coloneqq\Set{e\in{\mathbb{N}}}{\varphi_{e}=\alpha}$ is a
partial applicative morphism ${\mathcal{K}_{2}\to\mathcal{K}_{1}}$.

Let us now move to the level of arrow algebras. We warn the reader here that
we will see $D\operatorname{\mathbb{A}}$ and $D\operatorname{\mathbb{B}}$
simultaneously as PCAs as in 3.5 and as arrow algebras as described in section
3. Both structures possess a notion of application, and in general the two do
_not_ coincide: for example, given $\alpha,\beta\in DA$, the inequality

$(\alpha\to\beta)\cdot\alpha\subseteq\beta$

only holds with respect to the application defining the partial applicative
structure on $D\operatorname{\mathbb{A}}$, while it does not hold for the
arrow-algebraic application of 2.10.191919For this other application, we only
have the inequality
$(\alpha\to\partial\beta)\cdot\alpha\subseteq\partial\beta$, where
$\partial\beta\coloneqq A\to\beta$. In this paper, we will not make any use of
the latter form of application when dealing with arrow algebras of the form
$D\operatorname{\mathbb{A}}$; hence, the application considered will always be
the one defining the partial applicative structure.

First, let us show how every morphism of PCAs $D\operatorname{\mathbb{A}}\to
D\operatorname{\mathbb{B}}$ is an implicative morphism with respect to the
canonical arrow structures on $D\operatorname{\mathbb{A}}$ and
$D\operatorname{\mathbb{B}}$.

######  Lemma 5.9.

Let $f:D\operatorname{\mathbb{A}}\to D\operatorname{\mathbb{B}}$ be a morphism
of PCAs. Then, $f$ is also an implicative morphism
$D\operatorname{\mathbb{A}}\to D\operatorname{\mathbb{B}}$.

###### Proof.

Let us verify the three conditions in 4.1.

  1. i.

Condition (i) is ensured by (i) in 5.2 since $S_{DA}=(DA)^{\\#}$ and
$S_{DB}=(DB)^{\\#}$.

  2. ii.

To show condition (ii), we need to find some $\rho\in(DB)^{\\#}$ such that
$\rho\subseteq{f}(\alpha\to\beta)\to{f}(\alpha)\to{f}(\beta)$ for all
$\alpha,\beta\in DA$. By definition, recall that:

     * –

there exists $\tau\in(DB)^{\\#}$ such that if
${\alpha\alpha^{\prime}}{\downarrow}$, then ${\tau
f(\alpha)f(\alpha^{\prime})}{\downarrow}$ and $\tau
f(\alpha)f(\alpha^{\prime})\subseteq f(\alpha\alpha^{\prime})$;

     * –

there exists $\upsilon\in(DB)^{\\#}$ such that if
$\alpha\subseteq\alpha^{\prime}$ then ${\upsilon f(\alpha)}{\downarrow}$ and
$\upsilon f(\alpha)\subseteq f(\alpha^{\prime})$.

By combinatory completeness, consider then:

$\rho\coloneqq(\lambda^{*}v,w.\upsilon(\tau vw))\in(DB)^{\\#}$

Since ${(\alpha\to\beta)\cdot\alpha}{\downarrow}$, we know that:

${\tau\ f(\alpha\to\beta)\ f(\alpha)}{\downarrow}\quad\mbox{and}\quad\tau\
f(\alpha\to\beta)\ f(\alpha)\subseteq f((\alpha\to\beta)\cdot\alpha)$

Since moreover $(\alpha\to\beta)\cdot\alpha\subseteq\beta$, we also know that:

${\upsilon\
f((\alpha\to\beta)\cdot\alpha)}{\downarrow}\quad\mbox{and}\quad\upsilon\
f((\alpha\to\beta)\cdot\alpha)\subseteq f(\beta)$

So, by downward-closure of the domain of the application:

${\upsilon(\tau\ f(\alpha\to\beta)\
f(\alpha))}{\downarrow}\quad\mbox{and}\quad\upsilon(\tau\ f(\alpha\to\beta)\
f(\alpha))\subseteq f(\beta)$

Therefore:

${\rho\ f(\alpha\to\beta)\ f(\alpha)}{\downarrow}\quad\mbox{and}\quad\rho\
f(\alpha\to\beta)\ f(\alpha)\subseteq f(\beta)$

or, in other words:

$\rho\subseteq f(\alpha\to\beta)\to f(\alpha)\to f(\beta)$

  3. iii.

Let $X\subseteq DA\times DA$ be such that there exists some
$\sigma\in(DA)^{\\#}$ satisfying $\sigma\subseteq\alpha\to\beta$ for all
$(\alpha,\beta)\in X$. To show condition (iii), we need to find some
$\rho\in(DB)^{\\#}$ such that $\rho\subseteq f(\alpha)\to f(\beta)$ for all
$(\alpha,\beta)\in X$.

By combinatory completeness, since $f(\sigma)\in(DB)^{\\#}$ by condition (i),
consider then:

$\rho\coloneqq(\lambda^{*}w.\upsilon(\tau f(\sigma)w))\in(DB)^{\\#}$

Since ${\sigma\cdot\alpha}{\downarrow}$ and $\sigma\cdot\alpha\subseteq\beta$,
exactly as above we have that:

${\upsilon(\tau\ f(\sigma)\
f(\alpha))}{\downarrow}\quad\mbox{and}\quad\upsilon(\tau\ f(\sigma)\
f(\alpha))\subseteq f(\beta)$

Therefore:

${\rho\ f(\alpha)}{\downarrow}\quad\mbox{and}\quad\rho\ f(\alpha)\subseteq
f(\beta)$

or, in other words:

$\rho\subseteq f(\alpha)\to f(\beta)$

∎

######  Remark 5.10.

The two orders also coincide, by definition of the implication in downsets
PCAs: given two morphisms of PCAs $f,f^{\prime}:D\operatorname{\mathbb{A}}\to
D\operatorname{\mathbb{B}}$, then $f\leq f^{\prime}$ in
${\operatorname{\mathsf{OPCA}}}({D\operatorname{\mathbb{A}}},{D\operatorname{\mathbb{B}}})$
if and only if $f\vdash f^{\prime}$ in
${\operatorname{\mathsf{ArrAlg}}}({D\operatorname{\mathbb{A}}},{D\operatorname{\mathbb{B}}})$.

Let now $f:\operatorname{\mathbb{A}}\to\operatorname{\mathbb{B}}$ be a partial
applicative morphism, i.e. a morphism of PCAs $\operatorname{\mathbb{A}}\to
D\operatorname{\mathbb{B}}$. Then, $f$ corresponds to an essentially unique
$D$-algebra morphism $\widetilde{f}:D\operatorname{\mathbb{A}}\to
D\operatorname{\mathbb{B}}$ which, up to isomorphism, we can describe as:

$\widetilde{f}(\alpha)\coloneqq\bigcup_{a\in\alpha}f(a)$

The association $f\mapsto\widetilde{f}$ is 2-functorial202020As noted in 5.6,
$\operatorname{\mathsf{OPCA}}_{D}$ is only a bicategory, but compositions are
defined on the nose so we can still speak of 2-functors rather than
pseudofunctors. on $\operatorname{\mathsf{OPCA}}_{D}$, and it realizes an
equivalence of preorder categories between partial applicative morphisms
$\operatorname{\mathbb{A}}\to\operatorname{\mathbb{B}}$ and $D$-algebra
morphisms $D\operatorname{\mathbb{A}}\to D\operatorname{\mathbb{B}}$. Together
with the previous lemma and remark, this immediately implies the following.

######  Proposition 5.11.

The assignment $f\mapsto\widetilde{f}$ determines a $2$-functor:

$\widetilde{D}:\leavevmode\hbox to105.93pt{\vbox
to16.31pt{\pgfpicture\makeatletter\hbox{\hskip 52.96541pt\lower-8.204pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-52.96541pt}{-8.10416pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
21.3543pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.04875pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\operatorname{\mathsf{OPCA}}_{D}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
21.3543pt\hfil&\hfil\hskip 43.6111pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.30559pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\operatorname{\mathsf{ArrAlg}}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
19.61113pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-10.05682pt}{-5.60416pt}\pgfsys@lineto{13.14319pt}{-5.60416pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.34317pt}{-5.60416pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

Moreover, for any PCAs $\operatorname{\mathbb{A}}$ and
$\operatorname{\mathbb{B}}$, the map:

${{\operatorname{\mathsf{OPCA}}_{D}}({\operatorname{\mathbb{A}}},{\operatorname{\mathbb{B}}})}$${{\operatorname{\mathsf{ArrAlg}}}({D\operatorname{\mathbb{A}}},{D\operatorname{\mathbb{B}}})}$

(preserves and) reflects the order.

######  Remark 5.12.

The maps
${\operatorname{\mathsf{OPCA}}_{D}}({\operatorname{\mathbb{A}}},{\operatorname{\mathbb{B}}})\to{\operatorname{\mathsf{ArrAlg}}}({D\operatorname{\mathbb{A}}},{D\operatorname{\mathbb{B}}})$
defined by $\widetilde{D}$ are obviously not essentially surjective, meaning
that $\widetilde{D}$ is not 2-fully faithful. Indeed, any morphism of PCAs
$D\operatorname{\mathbb{A}}\to D\operatorname{\mathbb{B}}$ is an implicative
morphism $D\operatorname{\mathbb{A}}\to D\operatorname{\mathbb{B}}$, but
obviously only those which are union-preserving are $D$-algebra morphisms and
therefore arise as $\widetilde{D}f$ for some partial applicative morphism
$f:\operatorname{\mathbb{A}}\to\operatorname{\mathbb{B}}$. We will see more
about the interplay of these notions in section 7.

######  Question.

How does the $\operatorname{PER}(-)$ construction behave with respect to
(partial applicative) morphisms of PCAs and implicative morphisms?

##  6\. Transformations of arrow triposes

We have finally arrived at the heart of this paper. In this section, we
further the study of implicative morphisms and their relations with
transformations of arrow triposes, lifting the association
$\operatorname{\mathcal{A}}\mapsto P_{\operatorname{\mathcal{A}}}$ to a
2-functor defined on a suitable category of arrow algebras. The main goals, in
this perspective, are the following.

  1. i.

First, we will characterize implicative morphisms
$\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ as those functions
$A\to B$ which induce by postcomposition a cartesian transformation of arrow
triposes $P_{\operatorname{\mathcal{A}}}\to P_{\operatorname{\mathcal{B}}}$.

  2. ii.

Then, we will determine a suitable notion of _computational density_ which
characterizes those implicative morphisms
$\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ such that the
induced transformation $P_{\operatorname{\mathcal{A}}}\to
P_{\operatorname{\mathcal{B}}}$ has a right adjoint, hence corresponding to
geometric morphism of triposes $P_{\operatorname{\mathcal{B}}}\to
P_{\operatorname{\mathcal{A}}}$.

To motivate this, let us reconsider the classes of examples seen in the
previous section.

######  Example (Localic triposes).

The localic tripos $P_{\operatorname{\mathcal{O}}(X)}$ induced by a frame
$\operatorname{\mathcal{O}}(X)$ coincides with the arrow tripos obtained
seeing $\operatorname{\mathcal{O}}(X)$ as an arrow algebra in the canonical
way.

By [Pit81] we know that any frame homomorphism
$f^{*}:\operatorname{\mathcal{O}}(X)\to\operatorname{\mathcal{O}}(Y)$ induces
a geometric morphism of triposes $P_{\operatorname{\mathcal{O}}(Y)}\to
P_{\operatorname{\mathcal{O}}(X)}$ whose inverse image is given by
postcomposition with $f^{*}$ at each component; as we have shown in the
previous section, $f^{*}$ is an implicative morphism
$\operatorname{\mathcal{O}}(X)\to\operatorname{\mathcal{O}}(Y)$.

Moreover, the direct image is given by postcomposition with
$f_{*}:\operatorname{\mathcal{O}}(Y)\to\operatorname{\mathcal{O}}(X)$ at each
component, where $f_{*}$ is the right adjoint of $f^{*}$ as maps of posets –
which always exists for frame homomorphisms.

######  Example (Realizability triposes).

The realizability tripos $P_{\operatorname{\mathbb{A}}}$ induced by a PCA
$\operatorname{\mathbb{A}}$ coincides with the arrow tripos
$P_{D\operatorname{\mathbb{A}}}$ obtained seeing $D\operatorname{\mathbb{A}}$
as an arrow algebra in the canonical way.

By [Zoe22] we know that any partial applicative morphism
$f:\operatorname{\mathbb{A}}\to\operatorname{\mathbb{B}}$ induces a cartesian
transformation of triposes $P_{\operatorname{\mathbb{A}}}\to
P_{\operatorname{\mathbb{B}}}$ given by postcomposition with
$\widetilde{f}:DA\to DB$ at each component; as we’ve shown in the previous
chapter, $\widetilde{f}$ is an implicative morphism
$D\operatorname{\mathbb{A}}\to D\operatorname{\mathbb{B}}$.

Moreover, the induced cartesian transformation admits a right adjoint making
it the inverse image of a geometric morphism $P_{\operatorname{\mathbb{B}}}\to
P_{\operatorname{\mathbb{A}}}$ if and only if $f$ is computationally dense, in
which case the direct image is given by postcomposition with
$h:D\operatorname{\mathbb{B}}\to D\operatorname{\mathbb{A}}$, where $h$ is the
right adjoint of $\widetilde{f}$ in $\operatorname{\mathsf{OPCA}}$ – which
[Zoe22] showed to be equivalent to the computational density of $f$.

###  6.1. Cartesian transformations of arrow triposes

Let us start with a lemma we will make use of in the following. Recall that,
given any two arrow algebras
$\operatorname{\mathcal{A}}=(A,\preccurlyeq,\to,S_{A})$ and
$\operatorname{\mathcal{B}}=(B,\preccurlyeq,\to,S_{B})$, for every set $I$ we
can consider the arrow algebras
$\operatorname{\mathcal{A}}^{I}=(A^{I},\preccurlyeq,\to,S_{A}^{I})$ and
$\operatorname{\mathcal{B}}^{I}=(B^{I},\preccurlyeq,\to,S_{B}^{I})$ as in
2.19.

######  Lemma 6.1.

Let $f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ be an
implicative morphism.

For any set $I$, $f^{I}\coloneqq f\circ-$ is an implicative morphism
$\operatorname{\mathcal{A}}^{I}\to\operatorname{\mathcal{B}}^{I}$.

###### Proof.

Let us verify the three conditions in 4.1.

  1. i.

To show condition (i), recall that we can equivalently prove that
$f^{I}(\top_{I})\in S_{B}^{I}$, where $\top_{I}:I\to A$ is the constant
function of value $\top\in A$. Note then that by condition (i) for $f$ we
have:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i}f(\top_{I}(i))=\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i}f(\top)=f(\top)\in
S_{B}$

meaning that $f^{I}(\top)\in S^{I}_{B}$.

  2. ii.

Let $r\in S_{B}$ be a realizer for $f$ and let $\rho:I\to B$ be the constant
function at $r$; as
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i}\rho(i)=r\in
S_{B}$, we know that $\rho\in S^{I}_{B}$.

Then, for any $\phi,\phi^{\prime}\in A^{I}$:

$r\preccurlyeq f(\phi(i)\to\phi^{\prime}(i))\to f\phi(i)\to
f\phi^{\prime}(i)\quad\forall i\in I$

i.e., since the order and implications are defined pointwise in
$\operatorname{\mathcal{B}}^{I}$:

$\rho\preccurlyeq f^{I}(\phi\to\phi^{\prime})\to f^{I}\phi\to
f^{I}\phi^{\prime}$

meaning that $\rho$ realizes $f^{I}$.

  3. iii.

Let $X\subseteq A^{I}\times A^{I}$ be such that
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{(\phi,\psi)\in
X}\phi\to\psi\in S_{A}^{I}$. For the sake of notation, assume
$X=\Set{(\phi_{j},\psi_{j})}{j\in J}$; then, since the order (hence meets) and
implications are defined pointwise in $\operatorname{\mathcal{A}}^{I}$, we
have:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i}\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{j}\phi_{j}(i)\to\psi_{j}(i)\in
S_{A}$

from which, by (iii) for $f$:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{i}\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{j}f\phi_{j}(i)\to
f\psi_{j}(i)\in S_{A}$

meaning that
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{j}f^{I}\phi_{j}\to
f^{I}\psi_{j}\in S_{A}^{I}$.

∎

Fix now an implicative morphism
$f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ and define the
transformation:

$\Phi_{f}^{+}:P_{\operatorname{\mathcal{A}}}\to
P_{\operatorname{\mathcal{B}}}\qquad(\Phi_{f}^{+})_{I}(\phi)\coloneqq
f^{I}\phi=f\circ\phi$

Indeed, monotonicity of each component
$(\Phi_{f}^{+})_{I}:P_{\operatorname{\mathcal{A}}}(I)\to
P_{\operatorname{\mathcal{B}}}(I)$ precisely corresponds to condition (iii) in
4.1, while naturality is obvious.

Let us now show that, for every set $I$,
$(\Phi_{f}^{+})_{I}:P_{\operatorname{\mathcal{A}}}(I)\to
P_{\operatorname{\mathcal{B}}}(I)$ preserves finite meets up to isomorphism.
As $f^{I}(\top_{I})\in S_{B}^{I}$ we know that
$f^{I}(\top_{I})\dashv\vdash_{I}\top_{I}$, so we only have to show that for
any $\phi,\psi\in A^{I}$:

$f^{I}(\phi\times\psi)\dashv\vdash_{I}f^{I}\phi\times f^{I}\psi$

where $f^{I}\phi\times f^{I}\psi$ is the meet of $f^{I}\phi$ and $f^{I}\psi$
in $P_{\operatorname{\mathcal{B}}}(I)$ which, we recall from 2.21, can be
assumed to be defined pointwise.

Of course $f^{I}(\phi\times\psi)\vdash_{I}f^{I}\phi\times f^{I}\psi$ follows
simply by monotonicity of $f^{I}$ with respect to the logical order; on the
other hand, $f^{I}\phi\times f^{I}\psi\vdash_{I}f^{I}(\phi\times\psi)$ is
ensured by the following lemma applied to
$f^{I}:\operatorname{\mathcal{A}}^{I}\to\operatorname{\mathcal{B}}^{I}$.

######  Lemma 6.2.

Let $f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ be an
implicative morphism. Then:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}(f(a)\times f(b))\to f(a\times b)\in S_{B}$

###### Proof.

First, recall that:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}a\to b\to(a\times b)\in S_{A}$

from which, by (iii) in 4.1:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}f(a)\to f(b\to(a\times b))\in S_{B}$

whereas, by (ii):

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}f(b\to(a\times b))\to f(b)\to f(a\times b)\in S_{B}$

so by intuitionistic reasoning we conclude:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}f(a)\to f(b)\to f(a\times b)\in S_{B}$

which means:

$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{8.50015pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\curlywedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\curlywedge$}}}}}\slimits@_{a,b\in
A}(f(a)\times f(b))\to f(a\times b)\in S_{B}$

∎

Summing up, we have shown the following.

######  Proposition 6.3.

Let $f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ be an
implicative morphism. Then:

$\Phi_{f}^{+}:P_{\operatorname{\mathcal{A}}}\to
P_{\operatorname{\mathcal{B}}}\qquad(\Phi_{f}^{+})_{I}(\phi)\coloneqq
f\circ\phi$

is a cartesian transformation of triposes.

As promised above, we can also prove the converse: up to isomorphism, every
cartesian transformation of arrow triposes is induced in the sense of the
previous proposition by an implicative morphism which is unique up to
isomorphism.

######  Proposition 6.4.

The association $f\mapsto\Phi_{f}^{+}$ determines a 2-fully faithful
2-functor:

${\operatorname{\mathsf{ArrAlg}}}$${\mathsf{Trip}_{\mathsf{cart}}({\operatorname{\mathsf{Set}}})}$

Explicitly, this means that for any arrow algebras
$\operatorname{\mathcal{A}}$ and $\operatorname{\mathcal{B}}$ there is an
equivalence of preorder categories:

${{\operatorname{\mathsf{ArrAlg}}}({\operatorname{\mathcal{A}}},{\operatorname{\mathcal{B}}})}\simeq{{\mathsf{Trip}_{\mathsf{cart}}({\operatorname{\mathsf{Set}}})}({P_{\operatorname{\mathcal{A}}}},{P_{\operatorname{\mathcal{B}}}})}$

###### Proof.

By the previous discussion, we have a functor
$\operatorname{\mathsf{ArrAlg}}\to\mathsf{Trip}_{\mathsf{cart}}({\operatorname{\mathsf{Set}}})$;
2-functoriality amounts to showing that given any two implicative morphisms
$f,f^{\prime}:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ such
that $f\vdash f^{\prime}$, then $\Phi^{+}_{f}\leq\Phi^{+}_{f^{\prime}}$. By
definition, $f\vdash f^{\prime}$ means that $f\phi\vdash_{I}f^{\prime}\phi$
holds for any set $I$ and any $\phi:I\to A$, i.e.
$(\Phi^{+}_{f})_{I}(\phi)\vdash_{I}(\Phi^{+}_{f^{\prime}})_{I}(\phi)$ holds in
$P_{\operatorname{\mathcal{B}}}(I)$, which means that
$\Phi^{+}_{f}\leq\Phi^{+}_{f^{\prime}}$. Note then that the converse also
holds: if $\Phi_{f}^{+}\leq\Phi_{f^{\prime}}^{+}$, then in particular we have
that
$(\Phi^{+}_{f})_{A}(\operatorname{id}_{A})\vdash_{A}(\Phi^{+}_{f^{\prime}})_{A}(\operatorname{id}_{A})$,
which means that $f\vdash f^{\prime}$.

Let now $\Phi^{+}:P_{\operatorname{\mathcal{A}}}\to
P_{\operatorname{\mathcal{B}}}$ be any cartesian transformation of arrow
triposes. Recall that, up to isomorphism, $\Phi^{+}$ is given by
postcomposition with the function:

$f\coloneqq(\Phi^{+})_{A}(\operatorname{id}_{A}):A\to B$

Let us now verify that $f$ satisfies the three conditions212121If we assumed
implicative morphisms to be monotone, we would not be able to prove that $f$
is one. in 4.1.

  1. i.

To show condition (i), recall that we can equivalently prove that $f(\top)\in
S_{B}$. By preservation of finite meets, we know that
$(\Phi^{+})_{I}(\top_{I})\dashv\vdash_{I}\top_{I}$, which for $I\coloneqq 1$
means that $f(\top)\dashv\vdash\top$, i.e. $f(\top)\in S_{B}$.

  2. ii.

Let $I\coloneqq A\times A$; recall that condition (ii) can be rewritten as:

$f(\pi_{1}\to\pi_{2})\vdash_{I}f\pi_{1}\to f\pi_{2}$

where $\pi_{1},\pi_{2}:I\to A$ are the two projections. In terms of
$\Phi^{+}$, this means that we have to show:

$(\Phi^{+})_{I}(\pi_{1}\to\pi_{2})\vdash_{I}(\Phi^{+})_{I}(\pi_{1})\to(\Phi^{+})_{I}(\pi_{2})$

Through the Heyting adjunction in $P_{\operatorname{\mathcal{B}}}(I)$, the
previous is equivalent to:

$(\Phi^{+})_{I}(\pi_{1}\to\pi_{2})\times(\Phi^{+})_{I}(\pi_{1})\vdash_{I}(\Phi^{+})_{I}(\pi_{2})$

i.e., by preservation of finite meets:

$(\Phi^{+})_{I}(\pi_{1}\to\pi_{2}\times\pi_{1})\vdash_{I}(\Phi^{+})_{I}(\pi_{2})$

which is ensured by monotonicity since
$\pi_{1}\to\pi_{2}\times\pi_{1}\vdash_{I}\pi_{2}$.

  3. iii.

Condition (iii) precisely corresponds to the monotonicity of each component
$(\Phi^{+})_{I}$.

Therefore, the association
$\Phi^{+}\mapsto(\Phi^{+})_{A}(\operatorname{id}_{A})$ realizes the desired
inverse equivalence since obviously
$(\Phi^{+}_{f})_{A}(\operatorname{id}_{A})=f$ for all implicative morphisms
$f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$. ∎

######  Remark 6.5.

Recall from [Miq20b] that every $\operatorname{\mathsf{Set}}$-based tripos is
isomorphic to an implicative one, and hence to an arrow one. Therefore, at
least assuming the Axiom of Choice, the 2-functor
$\operatorname{\mathsf{ArrAlg}}\to\mathsf{Trip}_{\mathsf{cart}}({\operatorname{\mathsf{Set}}})$
is actually a 2-equivalence of 2-categories.

###  6.2. Geometric morphisms of arrow triposes

Let us now move to geometric morphisms: as we will see in a moment, the
existence of a right adjoint at the level of transformations of triposes can
exactly be characterized by the existence of a right adjoint in
$\operatorname{\mathsf{ArrAlg}}$.

######  Definition 6.6.

An implicative morphism
$f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ is
_computationally dense 222222The name is obviously taken from the theory of
PCAs, and it is also used in [SM17] in the context of applicative morphisms._
if it admits a right adjoint in $\operatorname{\mathsf{ArrAlg}}$, that is, if
there exists an implicative morphism
$h:\operatorname{\mathcal{B}}\to\operatorname{\mathcal{A}}$ such that
$fh\vdash\operatorname{id}_{B}$ and $\operatorname{id}_{A}\vdash hf$.

For any arrow algebra $\operatorname{\mathcal{A}}$, the identity
$\operatorname{id}_{A}:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{A}}$
is computationally dense, as it is trivially right adjoint to itself. As the
existence of a right adjoint in the preorder-enriched sense is clearly
compositional, we can define the wide subcategory
$\operatorname{\mathsf{ArrAlg}_{\mathsf{cd}}}$ of
$\operatorname{\mathsf{ArrAlg}}$ on computationally dense morphisms.

Fix now a computationally dense implicative morphism
$f:\operatorname{\mathcal{A}}\to\operatorname{\mathcal{B}}$ with right adjoint
$h:\operatorname{\mathcal{B}}\to\operatorname{\mathcal{A}}$ and consider the
cartesian transformation induced by $h$ as in 6.3:

$\Phi_{+}:P_{\operatorname{\mathcal{B}}}\to
P_{\operatorname{\mathcal{A}}}\qquad(\Phi_{+})_{I}(\phi)\coloneqq h\circ\phi$

######  Lemma 6.7.

For every set $I$, $(\Phi_{+})_{I}:P_{\operatorname{\mathcal{B}}}(I)\to
P_{\operatorname{\mathcal{A}}}(I)$ is right adjoint to the map
$(\Phi_{f}^{+})_{I}:\psi\mapsto f\circ\psi$.

###### Proof.

By the universal property of the counit of the adjunction, it suffices to show