# A category of arrow algebras for modified realizability

Umberto Tarantino

► To cite this version:

Umberto Tarantino. A category of arrow algebras for modified realizability. Theory and Applications of Categories, 2025, 44 (4), pp.132-180. hal-05480729

HAL Id: hal-05480729

https://hal.science/hal-05480729v1

Submitted on 27 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# A CATEGORY OF ARROW ALGEBRAS FOR MODIFIED REALIZABILITY

UMBERTO TARANTINO

**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.

## Introduction

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 [25], of which this paper can be seen as a follow-up, generalizing Alexandre Miquel’s *implicative algebras* [18, 19] as algebraic structures which induce triposes and then toposes through the tripos-to-topos construction. The weakening of the axiom that distinguishes implicative algebras from arrow algebras allows the latter to perfectly factor through the construction of realizability triposes coming from partial combinatory algebras – from now on, PCAs – which are actually *partial*, whereas implicative algebras are the intermediate structure only in the case of *total* combinatory algebras. Indeed, in [25] it is shown how every frame can be seen as an arrow algebra in such a way that the induced *arrow tripos* coincides with the usual localic tripos; similarly, every PCA gives rise to an arrow algebra in such a way that the induced arrow tripos coincides with the usual realizability tripos. 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 as to determine a category of arrow algebras factoring through the construction of both realizability and localic triposes in a 2-functorial way.

Earlier work in this area includes Hofstra’s *basic combinatory objects* (BCOs) [7], fundamental in advocating for the study of *relative* realizability which is implemented by the theory of both implicative and arrow algebras through the *separator*. The notion of a BCO appears quite different and more combinatorial in nature than the more algebraic

Thanks to Benno van den Berg who supervised this work as part of the author’s Master Thesis.

Received by the editors 2024-07-01 and, in final form, 2025-01-14.

Transmitted by Matias Menni. Published on 2025-01-16.

2020 Mathematics Subject Classification: 03G30, 18B25.

Key words and phrases: arrow algebras, topos theory, geometric morphisms, realizability.

© Umberto Tarantino, 2025. Permission to copy for private use granted.
notion of an arrow algebra, and we do not yet see how exactly the two structures relate: we
hope to investigate this further in the future, possibly showing how to endow every arrow
algebra with the structure of a BCO inducing the same tripos. A further generalization in
this direction is given by Frey's *uniform preorders* [23, 24]. Closely related to implicative
algebras are instead Cohen, Miquey and Tate's *evidenced frames* [3]. We leave for further
research the question of how exactly arrow algebras compare with these other structures
– now also with respect to morphisms.

The contents of this paper are as follows. In Section 1 we briefly review the theory of triposes and their morphisms. In Section 2 we summarize the theory of arrow algebras from [25] and we describe the two main examples: those coming from frames, and those coming from partial combinatory algebras. In Section 3 we introduce a first notion of morphism between arrow algebras, and in Section 4 we specialize it to the two main classes of arrow algebras described above recovering familiar notions in both cases. In Section 5, we show how these morphisms correspond to appropriate transformations of the associated triposes, and we introduce the notion of *computational density* characterizing geometric morphisms of triposes; in Section 6, we specialize once again to the two main examples. In Section 7, we focus on geometric inclusions, characterizing subtriposes of triposes arising from arrow algebras as arrow triposes themselves. This recovers and extends [25, Sec. 6], in particular by proving the converse of [25, Prop. 6.3], and relies on a particularly simple construction on arrow algebras which does not seem to work for implicative algebras. 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. Finally, in Section 8 we apply the previous machinery to the study of Kreisel's modified realizability on the level of arrow algebras, rephrasing and extending results partially known in the literature at the level of PCAs.

2-CATEGORICAL NOTATION. Following [29], 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 invertible 2-cells.

A *preorder-enriched category*, i.e. a category enriched over the category *Preord* of
preordered sets and monotone functions, can then be seen as a locally small 2-category
with at most one 2-cell between any pair of 1-cells. *Preord* is itself preorder-enriched
with respect to the pointwise order. We refer to weak 2-functors and strict 2-functors as
*pseudofunctors* and *2-functors*, respectively. *Pseudonatural transformations* are defined
in the usual way. With *pseudomonad* on a preorder-enriched category, we will refer to a
(fully) weak 2-monad, that is, an endo-pseudofunctor endowed with pseudonatural unit
and multiplication satisfying the usual monad axioms up to isomorphism. For more details
on 2-categories and 2-monads, we refer the reader to [13].

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 $\mathrm{id}_X \leq gf$ and $fg \leq \mathrm{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 \cong g$.
# 1. Preliminary on tripos theory

We begin by reviewing the necessary background on tripos theory, mainly drawing on the account given in [28] on the basis of [8, 21]; the reader is instead assumed to be familiar with topos theory, for which standard references are [20, 1, 9].

## 1.1. TRIPOSES.
In this paper, we will only consider Set-based triposes.

Recall that a Heyting prealgebra is a preorder whose poset reflection is a Heyting algebra, and a morphism of Heyting prealgebras is a monotone function which is a morphism of Heyting algebras between the poset reflections of domain and codomain. The category HeytPre of Heyting prealgebras is preorder-enriched with respect to the pointwise order.

## 1.2. DEFINITION.
A (Set-)tripos is a pseudofunctor $P : \mathbf{Set}^{\mathrm{op}} \to \mathbf{HeytPre}$ satisfying the following axioms.

i. For every function $f : X \to Y$, the map $f^* := P(f) : P(Y) \to P(X)$ has both a left adjoint $\exists_f$ and a right adjoint $\forall_f$ in Preord,<fnref n="1" /> and they satisfy the Beck-Chevalley condition.

ii. There exists a generic element in $P$, i.e. 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$ and $P(f)$ acts by precomposing with $f$ is said to be canonically presented.

## 1.3. EXAMPLE.
Let $H$ be a complete Heyting algebra. We define the Set-tripos of $H$-valued predicates $P_H$ as follows.

For every set $X$, we let $P_H(X) := H^X$, which is a Heyting algebra under pointwise order and operations; for every 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) := \bigvee_{x \in f^{-1}(y)} \phi(x) \quad \forall_f(\phi)(y) := \bigwedge_{x \in f^{-1}(y)} \phi(x) $$

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

## 1.4. DEFINITION.
Let $P$ and $Q$ be triposes. A transformation $\Phi : P \to Q$ is a pseudonatural transformation $P \Rightarrow Q$, seeing $P$ and $Q$ as pseudofunctors $\mathbf{Set}^{\mathrm{op}} \to \mathbf{Preord}$; explicitly, 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.

<footnote n="1">¹That is, $\exists_f$ and $\forall_f$ need not preserve the Heyting structure.</footnote>
Transformations $P \to Q$ can be ordered by letting $\Phi \le \Psi$ if $\Phi_X \le \Psi_X$ pointwise for every set $X$, therefore making triposes and transformations into a preorder-enriched category which we denote as Trip$(\mathbf{Set})$.

A transformation $\Phi : P \to Q$ is an equivalence if there exists another transformation $\Psi : Q \to P$ such that $\Phi \circ \Psi \cong \mathrm{id}_Q$ and $\Psi \circ \Phi \cong \mathrm{id}_P$.

Every tripos $P$ gives rise to a topos $\mathbf{Set}[P]$ through 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 [28].

**1.5. EXAMPLE.** For a complete Heyting algebra $H$, $\mathbf{Set}[P_H]$ is the topos of $H$-valued sets, proved in [5] to be equivalent to the topos $\mathrm{Sh}(H)$ of sheaves over $H$.

**1.6. 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 what we will need in the following.

**1.7. DEFINITION.** 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 $\mathrm{Trip}_{\mathrm{cart}}(\mathbf{Set})$ the wide subcategory of $\mathrm{Trip}(\mathbf{Set})$ on cartesian transformations.

A transformation is geometric if it is cartesian and admits a right adjoint in $\mathrm{Trip}(\mathbf{Set})$, that is, if there exists another transformation $\Phi_+ : Q \to P$ such that $(\Phi^+)_X \dashv (\Phi_+)_X$ in $\mathrm{Preord}$ for every set $X$. We denote with $\mathrm{Trip}_{\mathrm{geom}}(\mathbf{Set})$ the wide subcategory of $\mathrm{Trip}_{\mathrm{cart}}(\mathbf{Set})$ on geometric transformations.

In this language, a geometric morphism of triposes $(\Phi^+, \Phi_+)$ : $Q \to P$ is a geometric transformation $\Phi^+ : P \to Q$ with right adjoint $\Phi_+ : Q \to P$, of which they constitute respectively the inverse and direct image.<fnref n="2" />

**1.8. REMARK.** Cartesian transformations preserve the interpretation of *cartesian logic*, the fragment of finitary first-order logic defined by $\top$ and $\land$.

Geometric transformations preserve the interpretation of *geometric logic*, the fragment of infinitary first-order logic defined by $\top$, $\bot$, finitary $\land$, infinitary $\lor$ and $\exists$.

We will not go into details on the internal logic of triposes as it will not play any role in the paper; once again, we refer the reader to [28].

**1.9. REMARK.** Let $\Phi : P \to Q$ be an equivalence and let $\Psi : Q \to P$ be such that $\Phi \circ \Psi \cong \mathrm{id}_Q$ and $\Psi \circ \Phi \cong \mathrm{id}_P$. Then, $(\Phi, \Psi) : Q \to P$ and $(\Psi, \Phi) : P \to Q$ are both geometric morphisms.

**1.10. THEOREM.** Every geometric morphism of triposes $Q \to P$ induces a geometric morphism $\mathbf{Set}[Q] \to \mathbf{Set}[P]$.

<footnote n="2">²The direction is conventional and agrees with the definition of geometric morphisms of toposes.</footnote>
1.11. **REMARK.** The converse is not true in general: a geometric morphism $\mathbf{Set}[Q] \to \mathbf{Set}[P]$ is induced by a geometric morphism of triposes $Q \to P$ if and only if its inverse image part *preserves constant objects*.

1.12. **EXAMPLE.** 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^*: \mathcal{O}(Y) \to \mathcal{O}(X)$ and letting $f_*: \mathcal{O}(X) \to \mathcal{O}(Y)$ be its right adjoint, $\Phi^+$ is given by postcomposition with $f^*$ and $\Phi_+$ is given by postcomposition with $f_*$.

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

1.14. **DEFINITION.** A geometric morphism of triposes $\Phi = (\Phi^+, \Phi_+): Q \to P$ is an inclusion, in which case we also write $\Phi : Q \twoheadrightarrow P$, if either of the following equivalent conditions hold:

- for every set $X$, $(\Phi_+)_X$ reflects the order;

- $\Phi^+ \circ \Phi_+ \cong \mathrm{id}_Q$,

Dually, $\Phi$ is a surjection, in which case we also write $\Phi : Q \twoheadrightarrow P$, if either of the following equivalent conditions hold:

- for every set $X$, $(\Phi^+)_X$ reflects the order;

- $\Phi_+ \circ \Phi^+ \cong \mathrm{id}_P$.

1.15. **PROPOSITION.** Every geometric inclusion (resp. surjection) of triposes $Q \to P$ induces a geometric inclusion (resp. surjection) $\mathbf{Set}[Q] \to \mathbf{Set}[P]$.

1.16. **DEFINITION.** Let $\mathbf{SubTrip}(P)$ be the set of subtriposes of $P$, that is, triposes endowed with a geometric inclusions into $P$.<fnref n="3" /> Given two geometric inclusions $\Phi : Q \to P$ and $\Psi : R \to P$, we write $\Phi \subseteq \Psi$ if there exists a geometric morphism $\Theta : Q \to R$ such that $\Phi \cong \Psi \circ \Theta$ – meaning that $\Phi_+ \cong \Psi_+ \circ \Theta_+$ or equivalently $\Phi^+ \cong \Theta^+ \circ \Psi^+$ –, in which case $\Theta$ is an inclusion itself. This relation obviously makes $\mathbf{SubTrip}(P)$ into a preorder.

Two subtriposes $\Phi : Q \to P$ and $\Psi : R \to P$ are equivalent if they are isomorphic elements of $\mathbf{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 \cong \Psi \circ \Theta$.

As it is known, subtoposes of a topos $E$ correspond up to equivalence to local operators in $E$, that is, morphisms $j : \Omega \to \Omega$ such that, in the internal logic of $E$:

i. $j(\top) = \top$;

<footnote n="3">³For practical reasons, we identify a subtripos with the inclusion itself.</footnote>
ii. $jj = j$;

iii. $j(a \wedge b) = j(a) \wedge j(b)$,

In a topos of the form $\mathbf{Set}[P]$ for a tripos $P$, such a morphism corresponds to an essentially unique transformation $\Phi_j : P \to P$ which is:

i. cartesian;

ii. inflationary, that is, $\mathrm{id}_P \leq \Phi_j$;

iii. idempotent, that is, $\Phi_j\Phi_j \cong \Phi_j$.

Such $\Phi_j$ is called a closure transformation on $P$; conversely, every closure transformation on $P$ determines a local operator on $\mathbf{Set}[P]$.

These correspondences lead to the following result.

**1.17. THEOREM.** Let $P$ be a tripos and let $\mathrm{CITrans}(P)$ be the set of closure transformations on $P$, ordered as above.

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

$$ \mathrm{SubTrip}(P) \simeq \mathrm{CITrans}(P)^{\mathrm{OP}} $$

2. Every geometric inclusion of toposes into $\mathbf{Set}[P]$ is, up to equivalence, of the form $\mathbf{Set}[Q] \dashrightarrow \mathbf{Set}[P]$, induced by an essentially unique geometric inclusion of triposes $Q \dashrightarrow P$; in particular, there is an equivalence of preorder categories:

$$ \mathrm{SubTop}(\mathbf{Set}[P]) \simeq \mathrm{SubTrip}(P) $$

**1.18. REMARK.** Note then that the poset reflection of $\mathrm{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 := \Sigma^-$, we can even give an explicit description of the inclusion $Q \dashrightarrow P$ inducing a geometric inclusion into $\mathbf{Set}[P]$.

Let $(\mathbf{Set}[P])_j$ be the subtopos of $\mathbf{Set}[P]$ corresponding to a closure transformation $\Phi_j : P \to P$ and let $J := (\Phi_j)_{\Sigma}(\mathrm{id}_{\Sigma}) : \Sigma \to \Sigma$. Then, $(\mathbf{Set}[P])_j$ is equivalent over $\mathbf{Set}$ to $\mathbf{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 \xrightarrow{\mathrm{id}_{\Sigma} \times J} \Sigma \times \Sigma \xrightarrow{\to} \Sigma $$

while $\top, \bot, \wedge, \vee$ remain unchanged.<fnref n="4" />

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

<footnote n="4">⁴Left and right adjoints for $f^*$ can then be defined as $\phi \mapsto \exists_f(\phi)$ and $\phi \mapsto \forall_f(J\phi)$.</footnote>
1.19. **COROLLARY.** Let $P$ be a canonically presented tripos.

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

<figure><img src="image_2.png" /></figure>

for some $J : \Sigma \to \Sigma$ corresponding as above to a closure transformation $\Phi_j$ on $P$.

1.20. **EXAMPLE.** 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 *sublokales* of $X$, defined dually as quotient frames of closed elements.

Another important notion from topos theory which can be recovered at the level of triposes is that of *open* and *closed* subtriposes.

1.21. **DEFINITION.** A subtripos $\Phi : Q \to P$ is open if there exists an element $\alpha \in P(1)$ such that, for every set $I$ and every $\phi \in P(I)$:

$$ \Phi_+ \Phi^+(\phi) \cong P!(\alpha) \to \phi $$

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

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

$$ \Psi_+ \Psi^+(\phi) \cong \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.

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

1.23. **EXAMPLE.** Let $X$ be a complete Heyting algebra regarded as a locale. Then, open (resp. closed) subtriposes of $P_X$ correspond to *open* (resp. *closed*) *sublokales* of $X$.

## 2. Arrow algebras

2.1. **ARROW ALGEBRAS.** We now briefly review part of the theory of arrow algebras presented in [25] so as to fix notations and make some remarks.

An arrow algebra $\mathcal{A} = (A, \llcorner, \to, S)$ is the datum of a complete meet-semilattice $(A, \llcorner)$, a binary operation $\to: A \times A \to A$ called *implication* which is monotone in the second component and antitone in the first component, and a specified subset $S \subseteq A$ called
separator which is upward closed, closed under modus ponens, and contains appropriate
combinators **k**, **s**, **a**.

Although an arrow algebra $\mathcal{A}$ is defined in terms of the *evidential order* ≲, there is another order that can be defined in terms of implications and separators, that is, the *logical* order:

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

$(A, \vdash)$ is a Heyting prealgebra, with $\to$ being the Heyting implication. Through the logical order, we can also recover the separator as $\{a \in A \mid \top \vdash a\}$: in hindsight, this characterizes the separator as what Pitts calls the set of *designated truth values* of the induced arrow tripos.

For every set $I$, the set $A^I$ of functions $I \to A$ can be made into an arrow algebra $\mathcal{A}^I$ by choosing pointwise order and implication, and with the separator:

$$S^I := \{ \phi : I \longrightarrow A \mid \bigwedge_{i \in I} \phi(i) \in S \}$$

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

$$\phi \vdash_I \psi \iff \bigwedge_{i \in I} \phi(i) \to \psi(i) \in S$$

In general, note then that $\vdash_I$ is stronger than the pointwise version of $\vdash$: the two orders coincide only if the separator is closed under arbitrary meets. However, it is easy to see that meets, joins and implications in $(A^I, \vdash_I)$ are computed pointwise as meets, joins and implications in $(A, \vdash)$. Given a nucleus $j$ on $\mathcal{A}$, we denote with $\vdash_I^j$ the logical order in $A^I_j$: again by the properties of nuclei and separators, $\phi \vdash_I^j \psi$ explicitly means $\phi \vdash_I j\psi$.

$\mathcal{A}$ induces the *arrow tripos*:

<figure><img src="image_3.png" /></figure>

We denote with $\mathrm{AT}(\mathcal{A})$ the corresponding *arrow topos* $\mathrm{Set}[P_{\mathcal{A}}]$.

2.2. **REMARK.** In the following, we will make use of a form of reasoning internal to an arrow algebra $\mathcal{A} = (A, \prec, \to, S)$, which is given by a combination of [25, Prop. 3.5] and [25, Lem. 3.6] and which we will refer to as *intuitionistic reasoning*.

Suppose we want to prove that $\Lambda_{a_1, \dots, a_n \in A} \psi(a_i/p_i) \to \chi(a_i/p_i) \in S$ for some propositional formulas $\psi, \chi$ built from propositional variables $p_1, \dots, p_n$ using implications only. Then, we will look for a propositional formula $\phi$ also built from the same propositional variables using implications only, such that

1. $\phi \to \psi \to \chi$ is an intuitionistic tautology,
2. and $\mathcal{A}_{a_1, \dots, a_n \in A} \phi(a_i/p_i) \in S$.

If such a $\phi$ can be found, then by [25, Prop. 3.5] and (1) it will follow that:

$$ \mathcal{A}_{a_1, \dots, a_n \in A} \phi(a_i/p_i) \to \psi(a_i/p_i) \to \chi(a_i/p_i) \in S $$

and hence, by [25, Lem. 3.6] and (2):

$$ \mathcal{A}_{a_1, \dots, a_n \in A} \psi(a_i/p_i) \to \chi(a_i/p_i) \in S $$

Let us now introduce the two main classes of arrow algebras that we will keep on analyzing throughout the paper.

2.3. **FRAMES.** Every frame $\mathcal{O}(X)$ can be canonically seen as an arrow algebra$^5$ 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 \le x \to y$, which is equivalent to $x \le y$.

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

2.4. **PARTIAL COMBINATORY ALGEBRAS.** A main example of arrow algebras arises from PCAs, building blocks of realizability toposes. In this paper, we will continue with the not-entirely-standard definitions and conventions about PCAs given in [25], which closely follow those of [29]. This means that, with PCA, we will always mean Hofstra's notion of a filtered ordered partial combinatory algebra [7]. This allows us for the highest level of generality considered in the literature for what concerns appropriate notions of morphisms and their connections with morphisms of realizability triposes and toposes, as we will see in the next sections.

Let $\mathbb{P} = (P, \leq, \cdot, P^\#)$ be a PCA and consider the poset $DP$ of downward-closed subsets of $P$. Recall from [29, Ex. 2.1.7] that $DP$ can be given an application operation by defining, for $\alpha, \beta \in DP$:

$$ \alpha \cdot \beta := \downarrow\{xy \mid x \in \alpha, y \in \beta\} $$

in case $xy\downarrow$ for all $x \in \alpha$ and $y \in \beta$. Then, as seen in [29, Ex. 2.1.18], the family of downward-closed subsets containing an element from $P^\#$ is a filter on this partial applicative poset:

$$ \begin{align*} (DP)^\# &:= \{ \alpha \in DP \mid \exists a \in \alpha \cap P^\# \} \\ &= \{ \alpha \in DP \mid \exists a \in P^\# : \downarrow\{a\} \subseteq \alpha \} \\ &= \{ \alpha \in DP \mid \exists \beta \in D(P^\#) : \exists b \in \beta \wedge \beta \subseteq \alpha \} \end{align*} $$

<footnote>$^5$In particular, compatible with joins.</footnote>

<footnote>$^6$We will see in Proposition 5.18 how this property characterizes frames among arrow algebras up to equivalence of the induced triposes.</footnote>
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 $DP$. In particular, for a discrete and absolute PCA $\mathbb{P}$, we denote $DP$ also as $\mathrm{Pow}(\mathbb{P})$.

Defining, for $\alpha, \beta \in DP$:

$$ \alpha \to \beta := \{ a \in P \mid a \cdot \alpha \downarrow \text{ and } a \cdot \alpha \subseteq \beta \} $$

and letting $S_{DP} = (DP)^{\#}$, [25, Thm. 3.9] shows how $(DP, \subseteq, \cdot, S_{DP})$ is an arrow algebra which is compatible with joins. We denote this arrow algebra as $DP$ as well, and in particular as $\mathrm{Pow}(\mathbb{P})$ in the discrete and absolute case.

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

### 3. A first category of arrow algebras

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 operation and a specified subset: therefore, it would be natural to define morphisms of arrow algebras as monotone functions preserving implications (in some sense) and the specified subset. This intuition, obviously also valid for implicative algebras, is what leads to the definition of *applicative morphisms* in [22], 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 order,<fnref n="7" /> 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.

**3.1. IMPLICATIVE MORPHISMS.** Let $\mathcal{A} = (A, \prec, \to, S_A)$ and $\mathcal{B} = (B, \prec, \to, S_B)$ be two arrow algebras.

**3.2. DEFINITION.** An implicative morphism $f : \mathcal{A} \to \mathcal{B}$ is a function $f : A \to B$ satisfying:

i. $f(a) \in S_B$ for every $a \in S_A$;

ii. there exists an element $r \in S_B$ such that $r \prec f(a \to a') \to f(a) \to f(a')$ for all $a, a' \in A$;

iii. for every subset $X \subseteq A \times A$,

$$ \text{if } \mathop{\mathcal{A}}_{(a,a') \in X} a \to a' \in S_A \text{ then } \mathop{\mathcal{A}}_{(a,a') \in X} f(a) \to f(a') \in S_B, $$

<footnote n="7">⁷In a way, the evidential order is not the most important feature of an arrow algebra: arrow triposes, in fact, are defined by the Heyting prealgebras determined by the logical order.</footnote>
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' : \mathcal{A} \to \mathcal{B}$, we write $f \vdash f'$ if there exists an element $u \in S_B$ such that $u \preccurlyeq f(a) \to f'(a)$ for every $a \in A$, in which case we say that $f \vdash f'$ is realized by $u$. In other words, this means that:

$$ \mathcal{A} f(a) \to f'(a) \in S_B \\ a \in A $$

i.e. $f \vdash_A f'$ seeing $f$ and $f'$ as elements of the arrow algebra $\mathcal{B}^A$, so in particular it is also equivalent to $f \phi \vdash_I f' \phi$ for every set $I$ and every function $\phi : I \to A$.

**3.3. REMARK.** 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 $\lambda_{(a,a') \in X} a \to a' \in S_A$:

- by (ii) we have:

$$ \mathcal{A} f(a \to a') \to f(a) \to f(a') \in S_B; \\ (a,a') \in X $$

- as $f(\mathcal{A} P) \preccurlyeq \mathcal{A} f(P)$ for every subset $P \subseteq A$ by monotonicity, and by (i) and upward-closure of $S_B$:

$$ f \left( \mathcal{A} \quad a \to a' \right) \preccurlyeq \mathcal{A} \quad f(a \to a') \in S_B, \\ (a,a') \in X \qquad (a,a') \in X $$

from which $\lambda_{(a,a') \in X} f(a) \to f(a') \in S_B$ by [25, Lem. 3.6].

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

**3.4. REMARK.** Applicative morphisms of [22] only satisfy condition (ii) for $a, a' \in A$ such that $a \vdash a'$, while they are monotone by definition. The two notions are hence incomparable in general.

**3.5. PROPOSITION.** *Arrow algebras, implicative morphisms and their order form a preorder-enriched category *ArrAlg*.

**PROOF.** First, let $f : \mathcal{A} \to \mathcal{B}$ and $g : \mathcal{B} \to \mathcal{C}$ be implicative morphisms; let us show that $gf : \mathcal{A} \to \mathcal{C}$ satisfies the definition of an implicative morphism $\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:

$$ \mathcal{A} f(a \to a') \to f(a) \to f(a') \in S_B \\ a, a' $$
from which, by (iii) for $g$:

$$ \mathcal{A} \underset{a,a'}{\to} g f(a \to a') \to g(f(a) \to f(a')) \in S_C $$

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

$$ \mathcal{A} \underset{a,a'}{\to} g(f(a) \to f(a')) \to gf(a) \to gf(a') \in S_C $$

from which, by intuitionistic reasoning:

$$ \mathcal{A} \underset{a,a'}{\to} gf(a \to a') \to gf(a) \to gf(a') \in S_C $$

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

$$ \mathbf{i} \preceq \mathcal{A} \underset{a,a' \in A}{\to} (a \to a') \to a \to a' $$

This makes $ArrAlg$ into a category. The fact that $\vdash$ is a preorder on each homset $ArrAlg(\mathcal{A}, \mathcal{B})$ follows immediately as it is the subpreorder of $(\mathcal{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' : \mathcal{A} \to \mathcal{B}$ and $g : \mathcal{B} \to \mathcal{C}$ such that $f \vdash f'$; explicitly, this means that:

$$ \mathcal{A} \underset{a \in A}{\to} f(a) \to f'(a) \in S_B $$

from which, by (iii) in Definition 3.2:

$$ \mathcal{A} \underset{a \in A}{\to} gf(a) \to gf'(a) \in S_C $$

meaning that $gf \vdash gf'$;

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

■
### 3.6. EXAMPLE.
In a constructive metatheory, truth values are arranged in the frame $\Omega$ given by the powerset of the singleton $\{*\}^8$, which we can see as an arrow algebra in the canonical way. For every arrow algebra $\mathcal{A} = (A, \prec, \to, S)$, we can then consider the characteristic function of the separator, defined constructively as:

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

Note that, by upward closure of the separator, $\chi$ is monotone. Indeed, if $a \prec a'$, to show that $\chi(a) \subseteq \chi(a')$ suppose that $* \in \chi(a)$; then, $a \in S$, hence $a' \in S$ as well, i.e. $* \in \chi(a')$. We then have that $\chi$ is an implicative morphism $\mathcal{A} \to \Omega$.

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

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

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

### 3.7. LEMMA.
Let $\mathcal{A} = (A, \prec, \to, S_A)$ and $\mathcal{B} = (B, \prec, \to, S_B)$ be arrow algebras. A function $f : A \to B$ is an implicative morphism $\mathcal{A} \to \mathcal{B}$ if and only if it satisfies:

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

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. $f\phi \vdash_I f\psi$ for every 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 $\mathcal{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. ■

<footnote n="8">⁸Ω is the initial object in the category of frames.</footnote>
3.8. COROLLARY. If $f: \mathcal{A} \to \mathcal{B}$ is an implicative morphism and $f': \mathcal{A} \to \mathcal{B}$ is such that $f \dashv_A f'$ in $\mathcal{B}^A$, then $f'$ is an implicative morphism $\mathcal{A} \to \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 $\text{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.

On any arrow algebra $\mathcal{A}$ we can consider the map:

$$ \partial : A \to A \qquad \partial a := \top \to a $$

By [25, Prop. 5.8] we have that $\partial \dashv_A \text{id}_A$; in particular, by Corollary 3.8, $\partial$ is an implicative morphism $\mathcal{A} \to \mathcal{A}$.

3.9. LEMMA. Every implicative morphism is isomorphic to a monotone one.

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

$$ f' : A \to B \qquad f'(a) := \bigwedge_{a \prec a'} \partial f(a') $$

Let us show that $f \dashv_A f'$, which in particular implies that $f'$ is an implicative morphism $\mathcal{A} \to \mathcal{B}$ by the previous corollary.

On one hand, $\partial \vdash_B \text{id}_B$ gives:

$$ \mathcal{A}(\partial f(a)) \to f(a) \in S_B $$

from which, since $\mathcal{A}_{a \prec a'} \partial f(a') \preceq \partial f(a)$ and by upward-closure of $S_B$:

$$ \mathcal{A}(\mathcal{A} \partial f(a')) \to f(a) \in S_B $$

i.e. $f' \vdash_A f$.

On the other hand, $f \vdash_A f'$ explicitly reads as:

$$ \mathcal{A}_a f(a) \to \left( \mathcal{A}_{a \prec a'} \top \to f(a') \right) \in S_B $$

Note that, since $a \in S_B$:

$$ \mathcal{A}_a \left( \mathcal{A}_{a \prec a'} f(a) \to \top \to f(a') \right) \to f(a) \to \left( \mathcal{A}_{a \prec a'} \top \to f(a') \right) \in S_B $$
Therefore, $f \vdash_A f'$ is ensured by [25, Lem. 3.6] if we show:

$$ \mathfrak{A} f(a) \to \partial f(a') \in S_B \qquad (a,a') \in I $$

where $I := \{ (a, a') \in A \times A \mid a \preceq a' \}$. By intuitionistic reasoning, this is ensured by:

$$ \mathfrak{A} f(a) \to f(a') \in S_B \qquad (a,a') \in I \qquad (1) $$

$$ \mathfrak{A} f(a') \to \partial f(a') \in S_B \qquad (a,a') \in I \qquad (2) $$

where (1) follows since $f$ is an implicative morphism and $\mathbf{i} \in S_A$ witnesses the fact that $\mathfrak{A}_{(a,a') \in I} a \to a' \in S_A$, and (2) follows since $\mathrm{id}_B \vdash_B \partial$. ■

**3.10. REMARK.** Let $Mf := f'$ be the monotone implicative morphism defined above. Then, $Mf \dashv f$ immediately makes the association $f \mapsto Mf$ into a pseudofunctor $M: \mathrm{ArrAlg} \to \mathrm{ArrAlg}$.

## 4. Examples of implicative morphisms I

Let us now consider the two main classes of implicative morphisms, corresponding to two main examples of arrow algebras: those arising from frame homomorphisms, and those arising from morphisms of PCAs.

**4.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: \mathcal{O}(Y) \to \mathcal{O}(X)$, a (necessarily monotone) function which preserves finite meets and arbitrary joins, is also an implicative morphism. Indeed:

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

ii. for $y, y' \in \mathcal{O}(Y)$ we know that $y \wedge (y \to y') \le y'$, so by monotonicity and meet-preservation $f(y) \wedge f(y \to y') \le f(y')$, meaning that $f(y \to y') \le f(y) \to f(y')$ and therefore $\top \le f(y \to y') \to f(y) \to f(y')$.

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

Recall moreover that $\mathrm{Frm}$ is preorder-enriched with respect to the pointwise order: therefore, given two frame homomorphisms $f, f' : \mathcal{O}(Y) \to \mathcal{O}(X)$, we have that $f \le f'$ in $\mathrm{Frm}(\mathcal{O}(Y), \mathcal{O}(X))$ if and only if $f \vdash f'$ in $\mathrm{ArrAlg}(\mathcal{O}(Y), \mathcal{O}(X))$, since $\vdash_I$ coincides with the pointwise order for every set $I$. In other words, the inclusion determines a 2-functor $\mathrm{Frm} \to \mathrm{ArrAlg}$ with the additional property that each map $\mathrm{Frm}(\mathcal{O}(Y), \mathcal{O}(X)) \hookrightarrow \mathrm{ArrAlg}(\mathcal{O}(Y), \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 $\mathcal{O}(X)$ be a frame such that $\perp \neq \top$: then, the unique frame homomorphism $\Omega \to \mathcal{O}(X)$ is given by $p \mapsto \bigvee \{\top | * \in p\}$, whereas the constant function of value $\top$ is an implicative morphism $\Omega \to \mathcal{O}(X)$. As we will see in Section 6, 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.

**4.3. PARTIAL COMBINATORY ALGEBRAS.** The study of morphisms of PCAs in relation with induced morphisms of the associated triposes and toposes was initiated, in the discrete and absolute case, by John Longley in his PhD thesis [17]. The notion of *computational density* was introduced in [6] in the ordered case to characterize geometric morphisms of realizability toposes (see also [10], where computational density was also given a simpler reformulation), and then it was lifted to the ordered and relative case in [7] by considering morphisms of BCOs. We now briefly summarize the definitions we will need, as usual following the account given in [29].

Let $\mathbb{A} = (A, \leq, \cdot, A^\#)$ and $\mathbb{B} = (B, \leq, \cdot, B^\#)$ be two PCAs.

**4.4. DEFINITION.** [29, Def. 2.2.1] A morphism of PCAs $\mathbb{A} \to \mathbb{B}$ is a function $f : A \to B$ satisfying:

i. $f(a) \in B^\# \text{ for every } a \in A^\#;$

ii. there exists an element $t \in B^\#$ such that if $aa' \downarrow$ then $tf(a)f(a') \downarrow$ and $tf(a)f(a') \le f(aa');$

iii. there exists an element $u \in B^\#$ such that if $a \le a'$ then $uf(a) \downarrow$ and $uf(a) \le f(a')$,

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' : \mathbb{A} \to \mathbb{B}$, we write $f \le f'$ if there exists some $s \in B^\#$ such that $sf(a) \downarrow$ and $sf(a) \le f'(a)$ for every $a \in A$, in which case we say that $f \le f'$ is realized by $s$.

PCAs, morphisms of PCAs and their order form a *preorder-enriched category* OPCA.

**4.5. DEFINITION.** [29, Lem. 2.2.12] 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 every $s \in B^\#$ there is some $r \in A^\#$ such that $mf ra) \le sf(a)$ for every $a \in A$.

The construction $\mathbb{P} \mapsto \mathbb{DP}$ lifts to a pseudomonad on OPCA (see [29, Prop. 2.3.1]), through which a new notion of morphism of PCAs can be defined.
4.6. **DEFINITION.** [29, Def. 2.3.2] Let $\mathcal{OPCA}_D$ be the preorder-enriched bicategory defined as the Kleisli bicategory of the pseudomonad $D: \mathcal{OPCA} \to \mathcal{OPCA}$. Explicitly, $\mathcal{OPCA}_D$ is the category having PCAs as objects, and morphisms of PCAs $A \to D\mathbb{B}$ as morphisms $A \to \mathbb{B}$, which we call partial applicative morphisms.

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

Let us now move to the level of arrow algebras.

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

4.7. **LEMMA.** Let $f: D A \to D \mathbb{B}$ be a morphism of PCAs.

Then, $f$ is also an implicative morphism $D A \to D \mathbb{B}$.

**PROOF.** Let us verify the three conditions in Definition 3.2.

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

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 every $\alpha, \beta \in DA$. By definition, recall that:

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

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

By combinatory completeness, consider then:

$$ \rho := (\lambda^*\upsilon, 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 \text{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 \text{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 \text{and} \quad \upsilon(\tau f(\alpha \to \beta) f(\alpha)) \subseteq f(\beta) $$

Therefore:

$$ \rho f(\alpha \to \beta) f(\alpha)\downarrow \quad \text{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) $$
iii. Let $X \subseteq DA \times DA$ be such that there exists some $\sigma \in (DA)^{\#}$ satisfying $\sigma \subseteq \alpha \to \beta$ for every $(\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 every $(\alpha, \beta) \in X$.

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

$$ \rho := (\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 \text{and} \quad \upsilon(\tau f(\sigma) f(\alpha)) \subseteq f(\beta) $$

Therefore:

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

or, in other words:

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

■

4.8. **REMARK.** The two orders also coincide, by definition of the implication in downsets PCAs: given two morphisms of PCAs $f, f' : DA \to DB$, then $f \le f'$ in $OPCA(DA, DB)$ if and only if $f \vdash f'$ in **ArrAlg**(DA, DB).

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

$$ \tilde{f}(\alpha) := \bigcup_{a \in \alpha} f(a) $$

The association $f \mapsto \tilde{f}$ is 2-functorial<fnref n="9" /> on $OPCA_D$, and it realizes an equivalence of pre-order categories between partial applicative morphisms $A \to B$ and $D$-algebra morphisms $DA \to DB$. Together with the previous lemma and remark, this immediately implies the following.

4.9. **PROPOSITION.** *The assignment $f \mapsto \tilde{f}$ determines a 2-functor $\tilde{D} : OPCA_D \to \text{ArrAlg}.$* Moreover, for all PCAs $A$ and $B$, the map $OPCA_D(A, B) \to \text{ArrAlg}(DA, DB)$ (preserves and) reflects the order.

4.10. **REMARK.** The maps $OPCA_D(A, B) \to \text{ArrAlg}(DA, DB)$ defined by $\tilde{D}$ are obviously not essentially surjective, meaning that $\tilde{D}$ is not 2-fully faithful. Indeed, any morphism of PCAs $DA \to DB$ is an implicative morphism $DA \to DB$, but obviously only those which are union-preserving are $D$-algebra morphisms and therefore arise as $\tilde{D}f$ for some partial applicative morphism $f : A \to B$. We will see more about the interplay of these notions in Section 6.

<footnote n="9">⁹As noted in [29, Rem. 2.3.4], $OPCA_D$ is only a bicategory and not a preorder-enriched category, but since compositions are defined on the nose we can still speak of 2-functors rather than pseudofunctors.</footnote>
### 4.11. QUESTION.
How does the PER(-) construction of [25, Thm. 3.10] behave with respect to (partial applicative) morphisms of PCAs and implicative morphisms?

## 5. 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 $\mathcal{A} \mapsto P_A$ to a 2-functor defined on a suitable category of arrow algebras. The main goals, in this perspective, are the following.

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

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

### 5.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 $\mathcal{A} = (A, \prec, \to, S_A)$ and $\mathcal{B} = (B, \prec, \to, S_B)$, for every set $I$ we can consider the arrow algebras $\mathcal{A}^I = (A^I, \prec, \to, S_A^I)$ and $\mathcal{B}^I = (B^I, \prec, \to, S_B^I)$.

### 5.2. LEMMA.
Let $f : \mathcal{A} \to \mathcal{B}$ be an implicative morphism.
For every set $I$, $f^I := f \circ -$ is an implicative morphism $\mathcal{A}^I \to \mathcal{B}^I$.

**PROOF.** Let us verify the three conditions in Definition 3.2.

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:

$$ \mathcal{A}_i f(\top_I(i)) = \mathcal{A}_i f(\top) = f(\top) \in S_B $$

meaning that $f^I(\top) \in S_B^I$.

ii. Let $r \in S_B$ be a realizer for $f$ and let $\rho : I \to B$ be the constant function at $r$; as $\mathcal{A}_i \rho(i) = r \in S_B$, we know that $\rho \in S_B^I$.
Then, for all $\phi, \phi' \in A^I$:

$$ r \prec f(\phi(i) \to \phi'(i)) \to f\phi(i) \to f\phi'(i) \quad \forall i \in I $$

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

$$ \rho \prec f^I(\phi \to \phi') \to f^I\phi \to f^I\phi' $$

meaning that $\rho$ realizes $f^I$.
iii. Let $X \subseteq A^I \times A^I$ be such that $\lambda_{(\phi, \psi) \in X} \phi \to \psi \in S_A^I$. For the sake of notation, assume $X = \{ (\phi_j, \psi_j) | j \in J \}$; then, since order (hence meets) and implications are defined pointwise in $A^I$, we have:

$$ \lambda_i \lambda_j \phi_j(i) \to \psi_j(i) \in S_A $$

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

$$ \lambda_i \lambda_j f\phi_j(i) \to f\psi_j(i) \in S_A $$

meaning that $\lambda_j f^I \phi_j \to f^I \psi_j \in S_A^I$.

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

$$ \Phi_f^+ : P_A \to P_B \quad (\Phi_f^+)_I(\phi) := f^I \phi = f \circ \phi $$

Indeed, monotonicity of each component $(\Phi_f^+)_I : P_A(I) \to P_B(I)$ precisely corresponds to condition (iii) in Definition 3.2, while naturality is obvious.

Let us now show that, for every set $I$, $(\Phi_f^+)_I : P_A(I) \to P_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_I \top_I$, so we only have to show that for all $\phi, \psi \in A^I$:

$$ f^I(\phi \wedge \psi) \dashv_I f^I \phi \wedge f^I \psi $$

where $f^I \phi \wedge f^I \psi$ is the meet of $f^I \phi$ and $f^I \psi$ in $P_B(I)$ which, as we already recalled, can be assumed to be defined pointwise.

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

5.3. LEMMA. Let $f: A \to B$ be an implicative morphism. Then:

$$ \lambda_{a,b \in A} (f(a) \wedge f(b)) \to f(a \wedge b) \in S_B $$

PROOF. First, note that:

$$ \lambda_{a,b \in A} a \to b \to (a \wedge b) \in S_A $$

from which, by (iii) in Definition 3.2:

$$ \lambda_{a,b \in A} f(a) \to f(b \to (a \wedge b)) \in S_B $$
Moreover, by (ii):

$$ \mathcal{A} \underset{a,b \in A}{\to} f(b \to (a \land b)) \to f(b) \to f(a \land b) \in S_B $$

so by intuitionistic reasoning we conclude:

$$ \mathcal{A} \underset{a,b \in A}{\to} f(a) \to f(b) \to f(a \land b) \in S_B $$

which means:

$$ \mathcal{A} \underset{a,b \in A}{\to} (f(a) \land f(b)) \to f(a \land b) \in S_B $$

Summing up, we have shown the following.

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

$$ \Phi_f^+ : P_A \to P_B \qquad (\Phi_f^+)_I(\phi) := 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.

**5.5. PROPOSITION.** The association $f \mapsto \Phi_f^+$ determines a 2-fully faithful 2-functor $\mathrm{ArrAlg} \hookrightarrow \mathrm{Trip}_{\mathrm{cart}}(\mathrm{Set})$.

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

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

**PROOF.** By the previous discussion, we have a functor $\mathrm{ArrAlg} \to \mathrm{Trip}_{\mathrm{cart}}(\mathrm{Set})$; 2-functoriality amounts to showing that, given any two implicative morphisms $f, f' : \mathcal{A} \to \mathcal{B}$ such that $f \vdash f'$, then $\Phi_f^+ \le \Phi_{f'}^+$. By definition, $f \vdash f'$ means that for every set $I$ and every $\phi : I \to A$ then $f\phi \vdash_I f'\phi$ holds, i.e. $(\Phi_f^+)_I(\phi) \vdash_I (\Phi_{f'}^+)_I(\phi)$ holds in $P_B(I)$, which means that $\Phi_f^+ \le \Phi_{f'}^+$. Note then that the converse also holds: if $\Phi_f^+ \le \Phi_{f'}^+$, then in particular we have that $(\Phi_f^+)_A(\mathrm{id}_A) \vdash_A (\Phi_{f'}^+)_A(\mathrm{id}_A)$, which means that $f \vdash f'$.

Let now $\Phi^+ : P_A \to P_B$ be any cartesian transformation of arrow triposes. Recall that, up to isomorphism, $\Phi^+$ is given by postcomposition with the function:

$$ f := (\Phi^+)_A(\mathrm{id}_A) : A \to B $$

Let us now verify that $f$ satisfies the three conditions<fnref n="10" /> in Definition 3.2.

<footnote n="10">¹⁰If we assumed implicative morphisms to be monotone, we would not be able to prove that $f$ is one.</footnote>
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_I \top_I$, which for $I := 1$ means that $f(\top) \dashv \top$, i.e. $f(\top) \in S_B$.

ii. Let $I := 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_B(I)$, the previous is equivalent to:

$$(\Phi^+)_I(\pi_1 \to \pi_2) \wedge (\Phi^+)_I(\pi_1) \vdash_I (\Phi^+)_I(\pi_2)$$

i.e., by preservation of finite meets:

$$(\Phi^+)_I(\pi_1 \to \pi_2 \wedge \pi_1) \vdash_I (\Phi^+)_I(\pi_2)$$

which is ensured by monotonicity since $\pi_1 \to \pi_2 \wedge \pi_1 \vdash_I \pi_2$.

iii. Condition (iii) precisely corresponds to the monotonicity of each component $(\Phi^+)_I$.

Therefore, the association $\Phi^+ \mapsto (\Phi^+)_A(id_A)$ realizes the desired inverse equivalence since obviously $(\Phi^+)_A(id_A) = f$ for every implicative morphism $f: A \to B$. ■

5.6. **REMARK.** In [19] it is shown that every canonically-presented (Set-)tripos is equivalent to an implicative one, and hence to an arrow one.

Therefore, assuming the Axiom of Choice, the 2-functor **ArrAlg** $\to \text{Trip}_{\text{cart}}(\text{Set})$ is actually a 2-equivalence of 2-categories: in fact, under the Axiom of Choice, every tripos is equivalent to a canonically presented one (cfr. [8, Prop. 1.9]), meaning that the above 2-functor is essentially surjective on objects; moreover, under the Axiom of Choice, a 2-functor is a 2-equivalence if and only if it is 2-fully faithful and essentially surjective on objects, see e.g. [13, Thm. 7.4.1].

5.7. **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 **ArrAlg**.

5.8. **DEFINITION.** An implicative morphism $f: A \to B$ is computationally dense<sup>11</sup> if it admits a right adjoint in **ArrAlg**, that is, if there exists an implicative morphism $h: B \to A$ such that $fh \vdash id_B$ and $id_A \vdash hf$.

<footnote n="11"><sup>11</sup>The name is obviously taken from the theory of PCAs, and it is also used in [22] for applicative morphisms.</footnote>
For every arrow algebra $\mathcal{A}$, the identity $\mathrm{id}_\mathcal{A} : \mathcal{A} \to \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 $\mathrm{ArrAlg}_{\mathrm{cd}}$ of $\mathrm{ArrAlg}$ on computationally dense morphisms.

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

$$ \Phi_+ : P_{\mathcal{B}} \to P_{\mathcal{A}} \qquad (\Phi_+)_I(\phi) := h \circ \phi $$

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

**PROOF.** By the universal property of the counit of the adjunction, it suffices to show that for every $\phi : I \to B$:

1. $fh\phi \vdash_I \phi$ in $P_B(I)$;

2. for every $\psi : I \to A$ such that $f\psi \vdash_I \phi$ in $P_B(I)$, then $\psi \vdash_I h\phi$ in $P_A(I)$.

(1) clearly follows since $h$ is right adjoint to $f$. To show (2), instead, suppose $f\psi \vdash_I \phi$; then, $hf\psi \vdash_I h\phi$ as $h$ is an implicative morphism, and hence $\psi \vdash_I h\psi$ since $\mathrm{id}_\mathcal{A} \vdash_A hf$. ■

The previous results then immediately yield the following.

**5.10. THEOREM.** Let $f : \mathcal{A} \to \mathcal{B}$ be a computationally dense implicative morphism with right adjoint $h : \mathcal{B} \to \mathcal{A}$.

Then, $\Phi_f^+ : P_A \to P_B$ is a geometric transformation of triposes, with $\Phi_+ : P_B \to P_A$ defined above as right adjoint: in other words, the pair

<figure><img src="image_4.png" /></figure>

is a geometric morphism $P_B \to P_A$.

As we did for implicative morphisms and cartesian transformations, in this case too we can prove the converse: up to isomorphism, every geometric morphism of arrow triposes is induced by an essentially unique computationally dense implicative morphism.

**5.11. PROPOSITION.** The 2-functor of Proposition 5.5 restricts to a 2-fully faithful 2-functor $\mathrm{ArrAlg}_{\mathrm{cd}} \hookrightarrow \mathrm{Trip}_{\mathrm{geom}}(\mathrm{Set})$.

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

$$ \mathrm{ArrAlg}_{\mathrm{cd}}(\mathcal{A}, \mathcal{B}) \simeq \mathrm{Trip}_{\mathrm{geom}}(\mathrm{Set})(P_{\mathcal{A}}, P_{\mathcal{B}}) $$
PROOF. By the previous discussion, we have a 2-functor $ArrAlg_{cd} \to Trip_{geom}(Set)$ such that, given any two computationally dense implicative morphisms $f, f' : A \to B$, $f \vdash f'$ if and only if $\Phi_f^+ \le \Phi_{f'}^+$.

Let now $\Phi^+$: $P_A \to P_B$ be a geometric transformation of triposes, that is, a cartesian transformation having a right adjoint $\Phi_+$: $P_B \to P_A$. Recall that, up to isomorphism, $\Phi^+$ is given by postcomposition with $f := (\Phi^+)_A(id_A) : A \to B$, which is an implicative morphism $A \to B$ by Proposition 5.5. In the same way, as it is also necessarily cartesian, $\Phi_+$ is given up to isomorphism by postcomposition with the implicative morphism $h := (\Phi_+)_B(id_B) : B \to A$. Moreover, the adjunction between $\Phi^+$ and $\Phi_+$ directly yields $fh \vdash id_B$ and $id_A \vdash hf$, meaning that $h$ is right adjoint to $f$ making it computationally dense. ■

5.12. **REMARK.** As in Remark 5.6, assuming the Axiom of Choice, the above 2-functor $ArrAlg_{cd} \to Trip_{geom}(Set)$ is a 2-equivalence of 2-categories.

5.13. **EQUIVALENCES OF ARROW TRIPOSES.** Finally, let us characterize equivalences of arrow triposes on the level of arrow algebras.

With usual 2-categorical notation, we say that an implicative morphism $f: A \to B$ is an *equivalence* if there exists another implicative morphism $g: B \to A$ such that $fg \dashv\vdash$ id$_B$ in $ArrAlg(B, B)$ and $gf \dashv\vdash$ id$_A$ in $ArrAlg(A, A)$, in which case $g$ is a *quasi-inverse* of $f$. Two arrow algebras are then *equivalent* if there exists an equivalence between them; clearly, equivalent arrow algebras induce equivalent triposes.

5.14. **LEMMA.** Let $f: A \to B$ be an equivalence of arrow algebras.

Then, $f$ is computationally dense, and the induced geometric morphism of triposes $\Phi: P_B \to P_A$ is an equivalence.

PROOF. Let $g: B \to A$ be a quasi-inverse of $f$. As $g$ is in particular right adjoint to $f$ in $ArrAlg$, $f$ is computationally dense, and the induced geometric morphism $\Phi = (\Phi^+, \Phi_+): P_B \to P_A$ is given by:

$$ (\Phi^+)_I(\psi) = f \circ \psi \quad (\Phi_+)_I(\phi) = g \circ \phi $$

In particular, $\Phi^+\Phi_+$ and $\Phi_+\Phi^+$ are isomorphic to identities since $fg \dashv\vdash$ id$_B$ and $gf \dashv\vdash$ id$_A$, meaning that $\Phi$ is an equivalence. ■

By the previous results, we can also easily address the converse.

5.15. **PROPOSITION.** Let $\Phi: P_A \to P_B$ be an equivalence of arrow triposes. Then, $\Phi$ is induced up to isomorphism by an (essentially unique) equivalence of arrow algebras $f: A \to B$.

PROOF. Let $\Psi: P_B \to P_A$ be a quasi-inverse of $\Phi$. Then, $\Phi$ is both left and right adjoint to $\Psi$, which means in particular that the pair $(\Phi, \Psi)$ defines a geometric morphism $P_B \to P_A$. Therefore, by Proposition 5.11, $\Phi$ is induced up to isomorphism by an (essentially unique) computationally dense implicative morphism $f: A \to B$; a right adjoint $g: B \to A$ inducing $\Psi$ up to isomorphism then satisfies $fg \dashv\vdash$ id$_B$ and $gf \dashv\vdash$ id$_A$, making $f$ an equivalence. ■
5.16. **REMARK.** Recall from [25] that an arrow algebra $\mathcal{A} = (A, \prec, \to, S)$ is strong if

$$ \mathcal{A}_{a \in A, B \subseteq A} \left( \mathcal{A}_{b \in B} a \to b \right) \to a \to \mathcal{A}_{b \in B} b \in S $$

[25, Sec. 5] then shows how every arrow algebra $\mathcal{A} = (A, \prec, \to, S)$ is equivalent to a strong one. In fact, recall by [25, Def. 5.4] that an element $a \in A$ is *functional* if

$$ a = \mathcal{A}_{b,c \in A} \{ b \to c \mid a \prec b \to c \} $$

and, letting $A_{\text{fun}}$ be the set of functional elements of $\mathcal{A}$ and $S_{\text{fun}} := S \cap A_{\text{fun}}$, [25, Cor. 5.6] shows how $A_{\text{fun}} := (A_{\text{fun}}, \prec, \to, S_{\text{fun}})$ is a strong arrow algebra. Then, since implications are functional, $\partial \vdash_A \text{id}_A$ implies that $\partial : A \to A$ defines an equivalence $\mathcal{A} \to A_{\text{fun}}$, with right adjoint given by the inclusion $A_{\text{fun}} \hookrightarrow A$.

5.17. **REMARK.** We say that an arrow algebra $\mathcal{A} = (A, \prec, \to, S)$ is *trivial* if $S = A$, or equivalently if $\perp \in S$. It is then immediate to show that $\mathcal{A}$ is trivial if and only if the unique map $\mathcal{A} \to \{\ast\}$ – which is obviously an implicative morphism – is an equivalence. Hence, $\mathcal{A}$ is trivial if and only if $\text{AT}(\mathcal{A})$ is (equivalent to) the trivial topos.

As an example of application of the above correspondence between equivalences, we can easily characterize localic triposes among arrow triposes:<fnref n="12" /> in particular, thanks to [8] we also have an explicit description – up to equivalence in **ArrAlg** – of the frame inducing the tripos.

5.18. **PROPOSITION.** Let $\mathcal{A} = (A, \prec, \to, S)$ be an arrow algebra. Then, the following are equivalent:

1. for every set $I$, the logical order $\vdash_I$ on $\mathcal{A}^I$ coincides with the pointwise version of $\vdash$;

2. the Heyting algebra $(A/\vdash, \vdash, \to)$ is complete, hence a frame which we see as an arrow algebra $\bar{\mathcal{A}}$ in the canonical way, and the projection map $\mathcal{A} \to \bar{\mathcal{A}}$ is an equivalence in **ArrAlg**;

3. $\mathcal{A}$ is equivalent to a frame, seen as an arrow algebra in the canonical way;

4. $\mathcal{A}$ is equivalent to an arrow algebra having $\{\top\}$ as separator;

5. $P_A$ is localic.

<footnote n="12">¹²We thank the referee for suggesting such a characterization.</footnote>
PROOF. (1) ⇔ (2) coincides with (part of) [8, Thm. 4.1] making use of Proposition 5.15.

(2) ⇒ (3) is obvious.

(3) ⇒ (4) is obvious.

To show (4) ⇒ (1), suppose there exists an equivalence $f : \mathcal{A} \to \mathcal{B}$ for some arrow algebra $\mathcal{B} = (B, \prec, \to, \{\top\})$. Then, for every set $I$ and all $\phi, \psi : I \to A$:

$$ \begin{align*} \phi \vdash_I \psi &\iff f \phi \vdash_I f \psi \\ &\iff \top = \mathop{\bigwedge}_{i \in I} f \phi(i) \to f \psi(i) \\ &\iff \forall i \in I, \top = f \phi(i) \to f \psi(i) \\ &\iff \forall i \in I, f \phi(i) \vdash f \psi(i) \\ &\iff \forall i \in I, \phi(i) \vdash \psi(i) \end{align*} $$

Finally, (3) ⇔ (5) follows from Lemma 5.14 and Proposition 5.15. ■

<figure><img src="image_5.png" /></figure>

## 6. Examples of implicative morphisms II

We can finally conclude our analysis of the two main classes of arrow algebras, namely those arising from frames and from PCAs, now studying their morphisms in relation to the transformations between the associated triposes.

6.1. FRAMES. First, recall that frame homomorphisms are implicative morphisms, seeing frames as arrow algebras in the canonical way. More generally, as noted in Remark 4.2, every function between frames which preserves finite meets is an implicative morphisms: we can now easily prove the converse as well. In fact, if $f : \mathcal{O}(Y) \to \mathcal{O}(X)$ is an implicative morphism, then:

- as the separator on a frame is canonically defined as $\{\top\}$, $f(\top) = \top$;

- by Lemma 5.3, $f$ preserves binary logical meets, but the logical order on frames coincides with the evidential order and hence $f$ preserves binary ("evidential") meets.

Moving on, let us see how every frame homomorphism is computationally dense as an implicative morphism.

6.2. PROPOSITION. Let $f^* : \mathcal{O}(Y) \to \mathcal{O}(X)$ be a frame homomorphism. Then, $f^*$ is a computationally dense implicative morphism.

PROOF. Let $f_* : \mathcal{O}(X) \to \mathcal{O}(Y)$ be the right adjoint of $f^*$, i.e. the monotone function:

$$ f_*(x) = \bigvee \{ y \mid f^*(y) \leq x \} $$

As it is monotone and preserves finite meets, $f_*$ is an implicative morphism $\mathcal{O}(X) \to \mathcal{O}(Y)$; in particular, it is clearly right adjoint to $f^*$ in ArrAlg, which is then computationally dense. ■

<figure><img src="image_6.png" /></figure>
The converse is also true: computationally dense implicative morphisms between frames are themselves frame homomorphisms. Indeed, let $f: \mathcal{O}(Y) \to \mathcal{O}(X)$ be a computationally dense implicative morphism between frames and let $h: \mathcal{O}(X) \to \mathcal{O}(Y)$ be right adjoint to it. As above, we know that $f$ and $h$ preserve finite meets, so in particular they are monotone; moreover, as the logical and the evidential order coincide, $h$ is right adjoint to $f$ as monotone maps between the posets underlying $\mathcal{O}(Y)$ and $\mathcal{O}(X)$, which means that $f$ preserves all joins and hence that it is a frame homomorphism. Summing up, we have shown the following.

**6.3. PROPOSITION.** *The canonical inclusion of frames into arrow algebras determines a 2-fully faithful 2-functor $\text{Frm} \hookrightarrow \text{ArrAlg}_{\text{cd}}$.*

*Explicitly, this means that for all frames $\mathcal{O}(Y)$ and $\mathcal{O}(X)$ there is an equivalence of preorder categories:*

$$ \text{Frm}(\mathcal{O}(Y), \mathcal{O}(X)) \simeq \text{ArrAlg}_{\text{cd}}(\mathcal{O}(Y), \mathcal{O}(X)) $$

**6.4. REMARK.** In essence, this makes so that the canonical embedding of locales and their homomorphisms into localic triposes and geometric morphisms factors through (the opposite category of) arrow algebras and computationally dense implicative morphisms. In the 'algebraic' notation we have been using throughout the paper, this gives the following diagram:

<figure><img src="image_7.png" /></figure>

**6.5. PARTIAL COMBINATORY ALGEBRAS.** Let us start by summarizing the theory of transformations of realizability triposes coming from morphisms between PCAs, once again following [29].

First, let us start by linking morphisms of PCAs with cartesian transformations of realizability triposes. Any transformation of realizability triposes $\Phi: P_A \to P_B$ is given up to isomorphism by postcomposition with the function $f := \Phi_{DA}(\text{id}_{DA}) : DA \to DB$ at each component: as shown in [29, Prop. 3.3.16], $\Phi$ is cartesian if and only if $f$ is a morphism of PCAs, and the respective orders agree as well. In other words, we have the following.

**6.6. PROPOSITION.** *The association $f \mapsto f \circ -$ is 2-functorial on downsets PCAs and, for all PCAs $A$ and $B$, it realizes an equivalence of preorder categories:*

$$ \text{OPCA}(D_A, D_B) \simeq \text{Trip}_{\text{cart}}(\text{Set})(P_A, P_B) $$

Instead, partial applicative morphisms $A \to B$ are characterized as those inducing regular transformations of triposes, which we now introduce.
6.7. **DEFINITION.** A transformation of triposes $\Phi^+ : P \to Q$ is regular if it is cartesian and preserves existential quantification, i.e. if:

$$ (\Phi^+)_Y \circ \exists_g \dashv\vdash_Y \exists_g \circ (\Phi^+)_X $$

for every function $g : X \to Y$.

We denote with $\text{Trip}_{\text{reg}}(\text{Set})$ the wide subcategory of $\text{Trip}_{\text{cart}}(\text{Set})$ on regular transformations.

6.8. **REMARK.** Regular transformations preserve the interpretation of regular logic, the fragment of finitary first-order logic defined by $\top$, $\wedge$ and $\exists$.

Consider now a partial applicative morphism $f : A \to B$, that is, a morphism of PCAs $f : A \to D\mathbb{B}$. Recall that $f$ corresponds essentially uniquely to the $D$-algebra morphism:

$$ \tilde{f} : D\mathbb{A} \to D\mathbb{B} \qquad \tilde{f}(\alpha) := \bigcup_{a \in \alpha} f(a) $$

and the 2-functor defined by $f \mapsto \tilde{f}$ realizes an equivalence of preorder categories between partial applicative morphisms $A \to B$ and $D$-algebra morphisms $D\mathbb{A} \to D\mathbb{B}$.

Therefore, the correspondence stated in the previous proposition restricts to partial applicative morphisms and regular transformations: indeed, a cartesian transformation $g \circ - : P_A \to P_B$ is regular if and only if $g : D\mathbb{A} \to D\mathbb{B}$ is a $D$-algebra morphism, i.e. if and only if it is up to isomorphism of the form $g = \tilde{f}$ for an essentially unique partial applicative morphism $f : A \to B$. In other words, we have the following.

6.9. **PROPOSITION.** The association $f \mapsto \tilde{f} \circ -$ determines a 2-fully faithful 2-functor $\text{OPCA}_D \hookrightarrow \text{Trip}_{\text{reg}}(\text{Set})$.

Explicitly, this means that for all PCAs $A$ and $B$ there is an equivalence of preorder categories:

$$ \text{OPCA}_D(A, B) \simeq \text{Trip}_{\text{reg}}(\text{Set})(P_A, P_B) $$

Finally, we can specify the previous correspondence to geometric morphisms by means of computational density. First, note how computational density can be characterized by the existence of right adjoints in OPCA.

6.10. **LEMMA.** [29, Cor. 2.3.15] Let $f : A \to B$ be a partial applicative morphism. Then, $f$ is computationally dense if and only if $\tilde{f} : D\mathbb{A} \to D\mathbb{B}$ has a right adjoint in OPCA.

As the existence of right adjoints in OPCA precisely corresponds to the existence of right adjoints on the level of transformations of triposes, this yields the following.

6.11. **THEOREM.** Let $\text{OPCA}_{D,cd}$ be the wide sub(-bi)category of $\text{OPCA}_D$ on computationally dense partial applicative morphisms.

The association $f \mapsto \tilde{f} \circ -$ determines a 2-fully faithful 2-functor

$$ \text{OPCA}_{D,cd} \hookrightarrow \text{Trip}_{\text{geom}}(\text{Set}). $$
Explicitly, this means that for all PCAs $\mathcal{A}$ and $\mathcal{B}$ there is an equivalence of preorder categories:

$$ \mathrm{OPCA}_{D,cd}(\mathcal{A}, \mathcal{B}) \simeq \mathrm{Trip}_{\mathrm{geom}}(\mathrm{Set})(P_{\mathcal{A}}, P_{\mathcal{B}}) $$

In particular, a right adjoint of $\tilde{f} \circ - : P_{\mathcal{A}} \to P_{\mathcal{B}}$ is given by $h \circ - : P_{\mathcal{B}} \to P_{\mathcal{A}}$, where $h : D\mathcal{B} \to D\mathcal{A}$ is right adjoint to $\tilde{f}$ in $\mathrm{OPCA}$.

Let us now see how arrow algebras fit in the picture.

First, recall by Lemma 4.7 that any morphism of PCAs $D\mathcal{A} \to D\mathcal{B}$, given two PCAs $\mathcal{A} = (A, \leq, \cdot, A^#)$ and $\mathcal{B} = (B, \leq, \cdot, B^#)$, is an implicative morphism between the associated arrow algebras. Proposition 5.5 now allows us to easily address the converse.

**6.12. PROPOSITION.** Let $f : D\mathcal{A} \to D\mathcal{B}$ be an implicative morphism. Then, $f$ is also a morphism of PCAs $D\mathcal{A} \to D\mathcal{B}$.

Therefore:

$$ \mathrm{OPCA}(D\mathcal{A}, D\mathcal{B}) = \mathrm{ArrAlg}(D\mathcal{A}, D\mathcal{B}) $$

**PROOF.** Indeed, $f$ induces by postcomposition the cartesian transformation of realizability triposes $\Phi_f^+ : P_{D\mathcal{A}} \to P_{D\mathcal{B}}$; by Proposition 6.6, therefore, $f$ is a morphism of PCAs $D\mathcal{A} \to D\mathcal{B}$. Recalling that the two orders coincide as well, we conclude that $\mathrm{OPCA}(D\mathcal{A}, D\mathcal{B}) = \mathrm{ArrAlg}(D\mathcal{A}, D\mathcal{B})$. ■

Moving on to partial applicative morphisms $\mathcal{A} \to \mathcal{B}$, recall that they correspond to regular transformations of triposes. The following definition is then obvious.

**6.13. DEFINITION.** Let $\mathcal{A}$ and $\mathcal{B}$ be arrow algebras. An implicative morphism $f : \mathcal{A} \to \mathcal{B}$ is regular if, for every function $g : X \to Y$ and every $\alpha \in P_{\mathcal{A}}(X)$:

$$ f \circ \exists_g(\alpha) \vdash_Y \exists_g(f \circ \alpha) $$

We denote with $\mathrm{ArrAlg}_{\mathrm{reg}}$ the wide subcategory of $\mathrm{ArrAlg}$ on regular implicative morphisms; the 2-functor of Proposition 5.5 obviously restricts to a 2-fully faithful 2-functor $\mathrm{ArrAlg}_{\mathrm{reg}} \hookrightarrow \mathrm{Trip}_{\mathrm{reg}}(\mathrm{Set})$.

**6.14. REMARK.** Note that the inequality $\exists_g(f\alpha) \vdash_Y f\exists_g(\alpha)$ holds for every implicative morphism $f$: indeed, through the adjunction $\exists_g \dashv g^*$ it is equivalent to $f\alpha \vdash_X f\exists_g(\alpha)g$, which is ensured by the properties of $f$ since $\alpha \vdash_X \exists_g(\alpha)g$ by the unit of the same adjunction. Therefore, regularity amounts to the inequality $f\exists_g(\alpha) \vdash_Y \exists_g(f\alpha)$.

**6.15. REMARK.** Computationally dense implicative morphism are regular, since geometric transformations of triposes are regular.

Drawing from the previous results, we conclude that regular implicative morphisms between arrow algebras arising from PCAs arise themselves from partial applicative morphisms.
6.16. **PROPOSITION.** The 2-functor $\tilde{D}$ of Proposition 4.9 restricts to a 2-fully faithful 2-functor $\text{OPCA}_D \hookrightarrow \text{ArrAlg}_{\text{reg}}$.

Explicitly, this means that for all PCAs $\mathsf{A}$ and $\mathsf{B}$, $\tilde{D}$ realizes an equivalence of preorder categories:

$$ \text{OPCA}_D(\mathsf{A}, \mathsf{B}) \simeq \text{ArrAlg}_{\text{reg}}(\mathcal{D}\mathsf{A}, \mathcal{D}\mathsf{B}) $$

**PROOF.** Let $f: \mathcal{D}\mathsf{A} \to \mathcal{D}\mathsf{B}$ be a regular implicative morphism. Then, $f$ induces by postcomposition the regular transformation of realizability triposes $\Phi_f^+: P_{\mathcal{D}\mathsf{A}} \to P_{\mathcal{D}\mathsf{B}}$; by Proposition 6.9, therefore, $f = \tilde{D}g$ for an essentially unique partial applicative morphism $g: \mathsf{A} \to \mathcal{B}^{13}$.

Moreover, for $f, f': \mathsf{A} \to \mathcal{B}$ partial applicative morphisms, we have already shown that $f \leq f'$ in $\text{OPCA}_D(\mathsf{A}, \mathcal{B})$ if and only if $\tilde{D}f \vdash \tilde{D}f'$ in $\text{ArrAlg}(\mathcal{D}\mathsf{A}, \mathcal{D}\mathsf{B})$. ■

6.17. **REMARK.** Alternatively, the proof of the previous can be given by observing that a regular implicative morphism $f: \mathcal{D}\mathsf{A} \to \mathcal{D}\mathsf{B}$ is a union-preserving morphism of PCAs, and hence a $D$-algebra morphism: in fact, $\mathcal{D}\mathsf{A}$ and $\mathcal{D}\mathsf{B}$ are compatible with joins, meaning that existentials can be computed as unions (cfr. [25, Lem. 5.3]).

Finally, let us specialize to the case of computational density. Recall by Lemma 6.10 that a partial applicative morphism $f: \mathsf{A} \to \mathcal{B}$ is computationally dense if and only if $\tilde{f}: \mathcal{D}\mathsf{A} \to \mathcal{D}\mathsf{B}$ has a right adjoint in $\text{OPCA}$. Since $\text{OPCA}(\mathcal{D}\mathsf{A}, \mathcal{D}\mathsf{B})$ coincides as a preorder with $\text{ArrAlg}(\mathcal{D}\mathsf{A}, \mathcal{D}\mathsf{B})$, this is also equivalent to $\tilde{f}: \mathcal{D}\mathsf{A} \to \mathcal{D}\mathsf{B}$ having a right adjoint in $\text{ArrAlg}$, that is, to $\tilde{f}$ being computationally dense as an implicative morphism $\mathcal{D}\mathsf{A} \to \mathcal{D}\mathsf{B}$. In essence, we have shown the following.

6.18. **PROPOSITION.** The 2-functor $\tilde{D}$ of Proposition 4.9 restricts to a 2-fully faithful 2-functor $\text{OPCA}_{D,cd} \hookrightarrow \text{ArrAlg}_{cd}$.

Explicitly, this means that for all PCAs $\mathsf{A}$ and $\mathcal{B}$, $\tilde{D}$ realizes an equivalence of preorder categories:

$$ \text{OPCA}_{D,cd}(\mathsf{A}, \mathcal{B}) \simeq \text{ArrAlg}_{cd}(\mathcal{D}\mathsf{A}, \mathcal{D}\mathcal{B}) $$

6.19. **REMARK.** As for frames, in essence this makes so that the construction of realizability triposes and geometric morphisms from PCAs and partial applicative morphisms factors through arrow algebras and computationally dense implicative morphisms, giving the following diagram:

<figure><img src="image_8.png" /></figure>

<footnote n="13">¹³We can also describe $g$ as $f \circ \delta'_A$.</footnote>
## 7. Inclusions of arrow triposes

In this section, we will specify the previous correspondence between computationally dense implicative morphisms and geometric morphisms of arrow triposes to the case of geometric inclusions into a given arrow tripos $P_A$, and see how they correspond to nuclei on $\mathcal{A}$.

**7.1. INCLUSIONS AND SURJECTIONS.** Recall that a geometric morphism of arrow triposes $\Phi : P_B \to P_A$ is an inclusion if $(\Phi_+)_I$ reflects the order for every set $I$, or equivalently if $(\Phi^+)_I(\Phi_+)_I(\phi) \dashv_I \phi$ for every set $I$ and every $\phi : I \to B$. Dually, $\Phi$ is a surjection if $(\Phi^+)_I$ reflects the order for every set $I$, or equivalently if $(\Phi_+)_I(\Phi^+)_I(\phi) \dashv_I \phi$ for every set $I$ and every $\phi : I \to A$.

Recall moreover that, in any preorder-enriched category $\mathcal{C}$:

- an arrow $f : A \to B$ is a lax epimorphism if, for every $C \in \mathcal{C}$, the map

$$ - \circ f : \mathcal{C}(B, C) \to \mathcal{C}(A, C) $$

is fully-faithful as a functor between preorder categories, which explicitly means that $p \le q$ for all $p, q : B \to C$ such that $pf \le qf$;

- an arrow $f : A \to B$ is a lax monomorphism if, for every $C \in \mathcal{C}$, the map

$$ f \circ - : \mathcal{C}(C, A) \to \mathcal{C}(C, B) $$

is fully-faithful as a functor between preorder categories, which explicitly means that $p \le q$ for all $p, q : C \to A$ such that $fp \le fq$.

Specializing to **ArrAlg**, we can then give the following definition.

**7.2. DEFINITION.** A computationally dense implicative morphism $f : \mathcal{A} \to \mathcal{B}$ is an implicative surjection (resp. implicative injection) if it is a lax epimorphism (resp. lax monomorphism) in **ArrAlg**.

**7.3. PROPOSITION.** Let $f : \mathcal{A} \to \mathcal{B}$ be a computationally dense implicative morphism with right adjoint $h : \mathcal{B} \to \mathcal{A}$ and let $\Phi : P_B \to P_A$ be the induced geometric morphism of arrow triposes. The following are equivalent:

1. $\Phi$ is an inclusion;

2. $fh \dashv_B id_B$;

3. $f$ is an implicative surjection.

Dually, the following are equivalent:

1. $\Phi$ is a surjection;

2. $hf \dashv_A id_A$;

3. $f$ is an implicative injection.
PROOF. For (1) ⇔ (2), recall that the inverse image $\Phi^+$ is given by postcomposition with $f$, and the direct image $\Phi_+$ is given by postcomposition with $h$: therefore, $\Phi$ is an inclusion if and only if $fh\phi \nvdash_I \phi$ for every set $I$ and every $\phi \in P_B(I)$, which is equivalent to $fh \nvdash_B id_B$.

For (2) ⇒ (3), suppose $p, q : \mathcal{B} \to \mathcal{C}$ are such that $pf \vdash qf$. Then, $pfh \vdash qfh$, and hence $p \vdash q$.

For (3) ⇒ (2), of course $fh \vdash id_B$; conversely, to show that $id_B \vdash fh$ it then suffices to show that $f \vdash fhf$, which is ensured by $id_A \vdash hf$.

7.4. COROLLARY. For all arrow algebras $\mathcal{A}$ and $\mathcal{B}$, there are equivalences of preorder categories between:

- implicative surjections $\mathcal{A} \to \mathcal{B}$ and geometric inclusions $P_B \to P_A$;

- implicative injections $\mathcal{A} \to \mathcal{B}$ and geometric surjections $P_B \to P_A$.

PROOF. Combining Proposition 5.11 with the previous proposition.

7.5. REMARK. Of course, an implicative morphism is an equivalence if and only if it is both an implicative surjection and an implicative inclusion.

7.6. NUCLEI AND SUBTRIPOSES. Let $\mathcal{A} = (A, \prec, \to, S)$ be an arrow algebra.

Recall from [25, Def. 3.11] that a *nucleus* on $\mathcal{A}$ is a function $j : A \to A$ such that:

i. if $a \prec b$ then $ja \prec jb$;

ii. $\lambda_{a \in A} a \to ja \in S$;

iii. $\lambda_{a,b \in A} (a \to jb) \to ja \to jb \in S$.

which also imply:

iv. $\lambda_{a \in A} jja \to ja \in S$;

v. $\lambda_{a,b \in A} (a \to b) \to ja \to jb \in S$;

vi. $\lambda_{a,b \in A} j(a \to b) \to ja \to jb \in S$,

and we can even substitute (iii) in the definition with the conjunction of (iv) and (vi). Every nucleus $j$ on $\mathcal{A}$ determines the new arrow algebra $\mathcal{A}_j = (A, \prec, \to_j, S_j)$, where:

$$a \to_j b := a \to jb \qquad S_j := \{ a \in A \mid ja \in S \}$$

We denote with $\vdash^j$ the logical order in $\mathcal{A}_j$: 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$. Note also that $S \subseteq S_j$: in fact, if $a \in S$, then since $\lambda_{a \in A} a \to ja \in S$ by modus ponens it follows that $ja \in S$, which precisely means $a \in S_j$.

With the machinery of the previous sections, [25, Prop. 6.3] can then be reduced to the following observation.
7.7. LEMMA. $\mathrm{id}_A$ is an implicative surjection $\mathcal{A} \to \mathcal{A}_j$, with $j$ as a right adjoint.

PROOF. Let us start by showing that $\mathrm{id}_A$ is an implicative morphism $\mathcal{A} \to \mathcal{A}_j$. As the evidential order is the same in $\mathcal{A}$ and $\mathcal{A}_j$, we only have to verify (i) and (ii) in Definition 3.2.

i. If $a \in S$, then $ja \in S$, meaning that $a \in S_j$.

ii. Condition (ii) explicitly reads as:

$$ \mathcal{A}_{a,a'}(a \to a') \to_j a \to_j a' \in S_j $$

i.e.:

$$ j\left(\mathcal{A}_{a,a'}(a \to a') \to_j j(a \to ja')\right) \in S $$

so, by (ii) in the definition of a nucleus, it suffices to show:

$$ \mathcal{A}_{a,a'}(a \to a') \to_j j(a \to ja') \in S $$

This, in turn, follows by intuitionistic reasoning from:

$$ \mathcal{A}_{a,a'}(a \to a') \to_j a \to_j ja' \in S $$

$$ \mathcal{A}_{a,a'}(a \to ja') \to_j j(a \to ja') \in S $$

both of which follow again from (ii).

Then, let us show that $j$ is an implicative morphism $\mathcal{A}_j \to \mathcal{A}$: again, recall that $j$ is monotone by definition, so we only have to verify (i) and (ii) in Definition 3.2.

i. If $a \in S_j$, then by definition $ja \in S$.

ii. Condition (ii) explicitly reads as:

$$ \mathcal{A}_{a,a'}(j(a \to ja') \to_j ja \to_j ja' \in S) $$

which follows from intuitionistic reasoning from:

$$ \mathcal{A}_{a,a'}(j(a \to ja') \to_j ja \to_j jja' \in S) $$

$$ \mathcal{A}_{a'}(jja' \to_j ja' \in S) $$

Finally, let us show that $j : \mathcal{A}_j \to \mathcal{A}$ is right adjoint to $\mathrm{id}_A : \mathcal{A} \to \mathcal{A}_j$ in ArrAlg.

- On one hand, $j \vdash_A^j \mathrm{id}_A$ explicitly reads as $j \vdash_A j$, which is clearly true.

- On the other, $\mathrm{id}_A \vdash_A j$ is true as $j$ is a nucleus.

Moreover, we also have that $\mathrm{id}_A \vdash_A^j j$ as it explicitly reads as $\mathrm{id}_A \vdash_A jj$, which makes $\mathrm{id}_A$ an implicative surjection by Proposition 7.3. ■
7.8. COROLLARY. Every nucleus $j$ on $\mathcal{A}$ induces a geometric inclusion of triposes $P_{\mathcal{A}_j} \to P_{\mathcal{A}}$, given by:

<figure><img src="image_9.png" /></figure>

However, we are now in the position to do more than that: namely, we can recover and extend Corollary 1.19 to a correspondence between subtoposes of an arrow topos and nuclei on the underlying arrow algebra, hence proving the converse of the previous.

Recall in fact by the discussion in Section 1 that we have an equivalence of preorder categories between subtriposes of $P_{\mathcal{A}}$ and closure transformations on $P_{\mathcal{A}}$, that is, transformations $\Phi_j : P_{\mathcal{A}} \to P_{\mathcal{A}}$ which are cartesian, inflationary and idempotent:

$$ \mathrm{SubTrip}(P_{\mathcal{A}}) \simeq \mathrm{CITrans}(P_{\mathcal{A}})^{\mathrm{op}} $$

By the correspondence in Proposition 5.5, a transformation $\Phi_j : P_{\mathcal{A}} \to P_{\mathcal{A}}$ is a closure transformation on $P_{\mathcal{A}}$, if and only if the function $j := (\Phi_j)_{\mathcal{A}}(\mathrm{id}_{\mathcal{A}}) : A \to A$ inducing it up to isomorphism satisfies the following:

i. $j$ is an implicative morphism $\mathcal{A} \to \mathcal{A}$;

ii. $\mathrm{id}_{\mathcal{A}} \vdash j$;

iii. $jj \dashv\dashv j$.

Assuming up to isomorphism $j$ to be monotone with respect to the evidential order in $\mathcal{A}$ as in Lemma 3.9, note then how this is equivalent to $j$ satisfying (i), (ii), (iv) and (vi) in the definition of a nucleus, which as we've noted is equivalent to asking that $j$ is a nucleus. Since the association $j \mapsto \Phi_j$ also preserves and reflects the order, we conclude with the following.

7.9. PROPOSITION. Let $\mathcal{N}(\mathcal{A})$ be the set of nuclei on $\mathcal{A}$, with the preorder induced by $P_{\mathcal{A}}(\mathcal{A})$. Then, Proposition 5.5 yields an equivalence of preorder categories:

$$ \mathrm{CITrans}(P_{\mathcal{A}}) \simeq \mathcal{N}(\mathcal{A}) $$

so, in particular:

$$ \mathrm{SubTrip}(P_{\mathcal{A}}) \simeq \mathcal{N}(\mathcal{A})^{\mathrm{op}} $$

7.10. COROLLARY. Every geometric inclusion of toposes into $\mathrm{AT}(\mathcal{A})$ is induced, up to equivalence, by a geometric inclusion of triposes of the form:

<figure><img src="image_10.png" /></figure>

for some nucleus $j$ on $\mathcal{A}$.
7.11. **REMARK.** By definition of $\mathcal{A}_j$, note therefore how $P_{\mathcal{A}_j}$ coincides precisely with the tripos $P_j$ described before Corollary 1.19. For this reason, we will usually refer to the subtripos $P_{\mathcal{A}_j} \dashrightarrow P_{\mathcal{A}}$ simply as $P_j \dashrightarrow P_{\mathcal{A}}$.

We conclude this part with the following alternative description of $P_j$, already noted in the general case in [28] and then in the context of arrow algebras in [25, Prop. 6.6]. We record it here to have an explicit description of the corresponding geometric inclusion, which will come back in Section 8.

7.12. **PROPOSITION.** Let $j \in \mathbf{N}(\mathcal{A})$. Then, $P_j \in \mathbf{SubTrip}(P_{\mathcal{A}})$ is equivalent to the subtripos $Q_j \to P_{\mathcal{A}}$ defined by:

$$Q_j(I) := \{ \alpha \in P_{\mathcal{A}}(I) \mid j\alpha \vdash_I \alpha \}$$

with the Heyting prealgebra structure induced by $P_{\mathcal{A}}(I)$.

**PROOF.** Consider the pair of transformations:

$$\Theta^+ := \mathrm{id}_{\mathcal{A}} \circ - : Q_j \to P_j \qquad \Theta_+ := j \circ - : P_j \to Q_j$$

obviously well-defined since so is the geometric morphism $P_j \dashrightarrow P_{\mathcal{A}}$ above, and as $jj \vdash_A j$. Then, $\Theta^+$ and $\Theta_+$ define an equivalence of triposes between $P_j$ and $Q_j$.

- The fact that $\Theta^+\Theta_+ \cong \mathrm{id}_{P_j}$ is equivalent, by Proposition 5.5, to $j \dashv^j_A \mathrm{id}_{\mathcal{A}}$: on one hand, $\mathrm{id}_{\mathcal{A}} \vdash^j_A j$ explicitly means $\mathrm{id}_{\mathcal{A}} \vdash_A jj$, which follows from $\mathrm{id}_{\mathcal{A}} \vdash_A j$; on the other, $j \vdash^j_A \mathrm{id}_{\mathcal{A}}$ explicitly means $j \vdash_A j$, which follows by reflexivity.

- To show that $\Theta_+\Theta^+ \cong \mathrm{id}_{Q_j}$ we need to show that $j\alpha \dashv^I \alpha$ for every set $I$ and every $\alpha \in Q_j(I)$: on one hand, $\alpha \vdash_I j\alpha$ follows by $\mathrm{id}_{\mathcal{A}} \vdash_A j$; on the other, $j\alpha \vdash_I \alpha$ follows by definition of $Q_j(I)$.

Therefore, $Q_j$ is equivalent to $P_j$; through the equivalence, the geometric inclusion of $Q_j$ in $P_{\mathcal{A}}$ is given by:

$$Q_j \underset{j\alpha}{\overset{j\alpha-}{\swarrow}} \perp \underset{j\alpha-}{\searrow} P_{\mathcal{A}}$$

7.13. **A FACTORIZATION THEOREM.** As it is known, every geometric morphism of toposes can be factored as a geometric surjection followed by a geometric inclusion. Generalizing locale theory, let us recover the same result on the level of arrow algebras; in doing so, we will also make the correspondence between subtriposes and nuclei more explicit.

Let $f: \mathcal{A} \to \mathcal{B}$ be a computationally dense implicative morphism with right adjoint $h: \mathcal{B} \to \mathcal{A}$; by Lemma 3.9, up to isomorphism we can assume both $f$ and $h$ to be monotone with respect to the evidential order. First, observe the following.

7.14. **LEMMA.** $hf: \mathcal{A} \to \mathcal{A}$ is a nucleus on $\mathcal{A}$.
PROOF. Let us verify that $hf$ satisfies the three conditions defining nuclei.

i. $hf$ is monotone by composition.

ii. Clearly $\mathrm{id}_A \vdash hf$ as $h$ is right adjoint to $f$.

iii. Let $I := A \times A$; note that condition (iii) can be rewritten as:

$$ \pi_1 \to hf\pi_2 \vdash_I hf\pi_1 \to hf\pi_2 $$

where $\pi_1, \pi_2: I \to A$ are the obvious projections. Through the Heyting adjunction in $P_A(I)$, this is equivalent to:

$$ (\pi_1 \to hf\pi_2) \wedge hf\pi_1 \vdash_I hf\pi_2 $$

and hence, since $h \circ -$ is right adjoint to $f \circ -$, which preserves finite meets, to:

$$ f(\pi_1 \to hf\pi_2) \wedge fhf\pi_1 \vdash_I f\pi_2 $$

Therefore, since $fjf\pi_1 \vdash_I f\pi_1$ as $f \vdash \mathrm{id}_B$, it suffices to show:

$$ f(\pi_1 \to hf\pi_2) \wedge f\pi_1 \vdash_I f\pi_2 $$

i.e., again through the Heyting adjunction in $P_B(I)$:

$$ f(\pi_1 \to hf\pi_2) \vdash_I f\pi_1 \to f\pi_2 $$

which in turn follows since, by (ii) in Definition 3.2:

$$ f(\pi_1 \to hf\pi_2) \vdash_I f\pi_1 \to fhf\pi_2 $$

and again $fjf\pi_2 \vdash_I f\pi_2$.

A natural question is then to relate $f$ to $j := hf$, and in particular the geometric morphism $\Phi_f: P_B \to P_A$ induced by $f$ with the inclusion $\Phi_j: P_j \to P_A$ induced by $j$. To this aim, recall here that $fh \vdash \mathrm{id}_B$ and $\mathrm{id}_A \vdash hf$ imply $fjf \vdash f$ and $fhh \vdash h$.

7.15. **LEMMA.** *f* is an implicative injection *A*<sub>j</sub> —> *B*, with *h* as a right adjoint.

PROOF. Let us start by showing that $f$ is an implicative morphism $A_j \to B$.

i. Let $a \in S_j$; by definition, $hf(a) \in S_A$, so $fjf(a) \in S_B$, and hence $f(a) \in S_B$ since $fh \vdash \mathrm{id}_B$.
ii. Condition (ii) explicitly reads as:

$$ \mathcal{A}_{a,a'} f(a \to ja') \to f(a) \to f(a') \in S_B $$

which follows by intuitionistic reasoning from:

$$ \mathcal{A}_{a,a'} f(a \to ja') \to f(a) \to fj(a') \in S_B $$

$$ \mathcal{A}_{a,a'} (f(a) \to fhf(a')) \to f(a) \to f(a') \in S_B $$

where the latter follows since $fhh \vdash f$.

Note now that $h : B \to A$ is an implicative morphism $B \to A_j$ since it is an implicative morphism $B \to A$ and $\mathrm{id}_A$ is an implicative morphism $A \to A_j$. Then, we have that $h : B \to A_j$ is right adjoint to $f : A_j \to B$:

- clearly $hf \vdash \mathrm{id}_B$;

- on the other hand, $\mathrm{id}_A \vdash^j hf$ explicitly reads as $\mathrm{id}_A \vdash_A hfhf$, which follows from $\mathrm{id}_A \vdash_A hf$.

Moreover, we also have that $hf \vdash^j \mathrm{id}_A$ as it explicitly reads as $hf \vdash_A hf$, which makes $f : A_j \to B$ an implicative surjection by Proposition 7.3. ■

Recalling by Lemma 7.7 that $\mathrm{id}_A$ defines an implicative surjection $A \to A_j$, we have the following.

**7.16. COROLLARY.** Every computationally dense implicative morphism factors as an implicative surjection followed by an implicative inclusion.

On the level of triposes, this means that the geometric morphism $\Phi_f : P_B \to P_A$ induced by $f$ factors through $\Phi_j : P_j \to P_A$ by means of a geometric surjection $\Theta_f : P_B \to P_j$, also induced by $f$ as a morphism $A_j \to B$:

<figure><img src="image_11.png" /></figure>

**7.17. PROPOSITION.** $\Theta_f$ is an equivalence if and only if $\Phi_f$ is an inclusion.

**PROOF.** By Lemma 5.14 and Proposition 5.15, $\Theta_f$ is an equivalence if and only if $f : A_j \to B$ is an equivalence. Since $h : B \to A_j$ is right adjoint to $f : A_j \to B$, this is equivalent to $hf \vdash^j \mathrm{id}_A$ and $\mathrm{id}_B \vdash fh$, and since $hf \vdash^j \mathrm{id}_A$ holds trivially this is equivalent simply to $\mathrm{id}_B \vdash fh$. By Proposition 7.3, $\mathrm{id}_B \vdash fh$ is in turn equivalent to $\Phi_f$ being an inclusion. ■
7.18. **REMARK.** In essence, this gives us a more explicit description of the correspondence given in Proposition 7.9, in perfect generalization of the localic case: indeed, if a subtripos $\Phi: P_B \twoheadrightarrow P_A$ is induced by an implicative surjection $f: A \to B$, then it is equivalent to the subtripos induced by (a nucleus isomorphic to) $hf$, where $h$ is right adjoint to $f$.

## 8. Arrow algebras for modified realizability

In this section, we will apply the theoretical framework developed above to lift the study of *modified realizability* to the level of arrow algebras. Modified realizability is a variant of Kleene's number realizability introduced by Kreisel in 1959 [16]. On the semantical side, a topos for Kreisel's modified realizability was first defined by Greyson in 1981 [4]; see also [27, 2, 12].

The key feature of modified realizability lies in separating between a set of *potential realizers* and a subset thereof of *actual realizers*. On the level of triposes, this amounts to shifting from the ordinary realizability tripos $P_A$ over a (traditionally, discrete and absolute) PCA $A$ to a tripos whose predicates on a set $I$ are functions from $I$ to the set:

$$ \{ (\alpha, \beta) \in DA \times DA \mid \alpha \subseteq \beta \} $$

which are preordered by:

$$ \phi \vdash_I \psi \iff \bigcap_{i \in I} (\phi_1(i) \to \psi_1(i)) \cap (\phi_2(i) \to \psi_2(i)) \in (DA)^# $$

where we denote with $\phi_1(i), \phi_2(i)$ the two components of $\phi(i)$. This idea is what led, in [25], to the definition of the *Sierpiński construction* on arrow algebras, which we will describe below. To do this, and for what follows, we will consider some *ad hoc* notions of arrow algebras which still encompass all the relevant cases and many others. This does not mean that we have counterexamples showing how the presented results may fail for more general classes of arrow algebras, but only that minimal assumptions suffice to ensure the desired properties.

8.1. **DEFINITION.** An arrow algebra $\mathcal{A} = (A, \prec, \to, S)$ is binary implicative if the equality:

$$ a \to (b \to c) = a \to b \to a \to c $$

holds for all $a, b, c \in A$, and it is modifiable if moreover the equality:

$$ \perp \to a = \top $$

holds for every $a \in A$.

We denote with $\text{ArrAlg}_{\text{bi}}$ and $\text{ArrAlg}_{\text{mod}}$ the full subcategories of $\text{ArrAlg}$ on binary implicative and modifiable arrow algebras, respectively.

8.2. **EXAMPLE.** Every frame, seen as an arrow algebra in the canonical way, is modifiable.
8.3. EXAMPLE. For every PCA A, D A is modifiable; in particular, PER A (cfr. [25, Thm. 3.10]) is modifiable.

8.4. THE SIERPIŃSKI CONSTRUCTION. Recall by [25, Prop. 7.2] that, starting from any binary implicative arrow algebra $\mathcal{A} = (A, \prec, \to, S)$, we can define a new arrow algebra $\mathcal{A}^{\to} = (A^{\to}, \prec, \to, S^{\to})$, also binary implicative, by letting:

$$A^{\to} := \{ x = (x_0, x_1) \in A \times A \mid x_0 \prec x_1 \}$$

with pointwise order, implication:

$$x \to y := (x_0 \to y_0 \land x_1 \to y_1, x_1 \to y_1)$$

and separator:

$$S^{\to} := \{ x \in A^{\to} \mid x_0 \in S \}$$

8.5. REMARK. This means that, for every set $I$, the order in $P_{A^{\to}}(I)$ is given by:

$$\phi \vdash_I \psi \iff \bigwedge_{i \in I} \phi_1(i) \to \psi_1(i) \land \phi_2(i) \to \phi_2(i) \in S$$

where we denote with $\phi_1, \phi_2 : I \to A$ the two components of $\phi : I \to A^{\to}$.

Let us now lift the association $\mathcal{A} \mapsto \mathcal{A}^{\to}$ to a (pseudo)functor on $\mathbf{ArrAlg}_{bi}$.

Let $f : \mathcal{A} \to \mathcal{B}$ be an implicative morphism in $\mathbf{ArrAlg}_{bi}$, for the moment assumed to be monotone, and define:

$$f^{\to} : A^{\to} \to B^{\to} \qquad f^{\to}(x_0, x_1) := (f(x_0), f(x_1))$$

8.6. LEMMA. $f^{\to}$ is an implicative morphism $\mathcal{A}^{\to} \to \mathcal{B}^{\to}$.

PROOF. First, note that $f^{\to}$ is well-defined as a function $\mathcal{A}^{\to} \to \mathcal{B}^{\to}$ by monotonicity of $f$, and it is monotone itself with respect to the evidential orders in $\mathcal{A}^{\to}$ and $\mathcal{B}^{\to}$. Let us then verify that $f^{\to}$ satisfies the first two conditions in Definition 3.2.

i. If $x \in S_{\mathcal{A}}^{\to}$, then $x_0 \in S_{\mathcal{A}}$, so $f(x_0) \in S_{\mathcal{B}}$ and hence $f^{\to}(x) \in S_{\mathcal{B}}^{\to}$.

ii. First note that, for all $x, y \in A^{\to}$:

$$\begin{aligned} f^{\to}(x \to y) &= f^{\to}(x_0 \to y_0 \land x_1 \to y_1, x_1 \to y_1) \\ &= (f(x_0 \to y_0 \land x_1 \to y_1), f(x_1 \to y_1)) \end{aligned}$$

whereas:

$$\begin{aligned} f^{\to}(x) \to f^{\to}(y) &= (fx_0, fx_1) \to (fy_0, fy_1) \\ &= (fx_0 \to fy_0 \land fx_1 \to fy_1, fx_1 \to fy_1) \end{aligned}$$
Therefore, by binary implicativity, a realizer for $f \rightarrow$ amounts to an element $r \in S_B$ such that:

$$r \preceq f(x_0 \rightarrow y_0 \lambda x_1 \rightarrow y_1) \rightarrow fx_0 \rightarrow fy_0$$

$$r \preceq f(x_0 \rightarrow y_0 \lambda x_1 \rightarrow y_1) \rightarrow fx_1 \rightarrow fy_1$$

$$r \preceq f(x_1 \rightarrow y_1) \rightarrow fx_1 \rightarrow fy_1$$

for all $x, y \in A \rightarrow$, in which case $(r, r) \in S_B \rightarrow$ realizes $f \rightarrow$. By monotonicity of $f$, note then that it suffices to show that:

$$r \preceq f(x_0 \rightarrow y_0) \rightarrow fx_0 \rightarrow fy_0$$

$$r \preceq f(x_1 \rightarrow y_1) \rightarrow fx_1 \rightarrow fy_1$$

for all $x, y \in A \rightarrow$, which means that $r$ can be taken to be a realizer for $f$.

Therefore, $(-) \rightarrow$ defines a functorial association on binary implicative arrow algebras and monotone implicative morphisms between them. Note moreover that, given two monotone implicative morphisms $f, f' : A \rightarrow B$ in $ArrAlg_{bi}$, if $u \in S_B$ realizes $f \vdash f'$, then $(u, u) \in S_B \rightarrow$ clearly realizes $f \rightarrow \vdash f' \rightarrow$, meaning that $(-) \rightarrow$ is actually 2-functorial. Precomposing with the pseudofunctor $M$ of Remark 3.10, we obtain the following.

**8.7. PROPOSITION.** For every implicative morphism $f : A \rightarrow B$ in $ArrAlg_{bi}$, let:

$$f \rightarrow : A \rightarrow \mathcal{B} \rightarrow \quad f \rightarrow (x_0, x_1) := \left( \mathcal{A} \underset{x_0 \preceq a}{\rightarrow} \partial f(a), \mathcal{A} \underset{x_1 \preceq a}{\rightarrow} \partial f(a) \right)$$

Then, $(-) \rightarrow$ is a pseudofunctor $ArrAlg_{bi} \rightarrow ArrAlg_{bi}$.

Moreover, if $f$ is computationally dense with right adjoint $h : B \rightarrow A$, then $f \rightarrow$ is computationally dense as well, and a right adjoint is given by $h \rightarrow : B \rightarrow A \rightarrow$.

**PROOF.** We only have to show the last part, so let $f$ be computationally dense with right adjoint $h : B \rightarrow A$ and, up to isomorphism, assume both $f$ and $h$ to be monotone, so that $f \rightarrow$ and $h \rightarrow$ can be defined as above in the case of monotonicity. Let us show that $h \rightarrow$ is right adjoint to $f \rightarrow$.

– To show that $f \rightarrow h \rightarrow \vdash \mathrm{id}_{B \rightarrow}$, note that:

$$\mathcal{A} \underset{y \in B \rightarrow}{\rightarrow} f \rightarrow h \rightarrow (y) \rightarrow y \in S_B \rightarrow$$

$$\iff \mathcal{A} \underset{y \in B \rightarrow}{\rightarrow} (fh(y_0), fh(y_1)) \rightarrow (y_0, y_1) \in S_B \rightarrow$$

$$\iff \mathcal{A} \underset{y \in B \rightarrow}{\rightarrow} fh(y_0) \rightarrow y_0 \lambda fh(y_1) \rightarrow y_1 \in S_B$$

which is ensured by $fh \vdash \mathrm{id}_B$.
- Similarly, $\mathrm{id}_{A} \to h \to f \to$ reduces to $\mathrm{id}_{A} \to hf$.

■

8.8. **COROLLARY.** Let $\mathcal{A}$ and $\mathcal{B}$ be binary implicative arrow algebras.
Every geometric morphism $\Phi : P_{\mathcal{B}} \to P_{\mathcal{A}}$ lifts to a geometric morphism $\Phi \to : P_{\mathcal{B}} \to P_{\mathcal{A}}$.

8.9. **QUESTION.** For $\mathcal{A} = \mathrm{Pow}(\mathcal{K}_1)$, we have that $\mathrm{AT}(\mathcal{A}^{\to})$ is the effective topos built on the topos of sheaves over the Sierpiński space, $\mathrm{Eff}_{\to}$. – that is, the result of the construction of $\mathrm{Eff}$ inside the topos $\mathrm{Set}^{\to}$.

Can we develop a theory of arrow algebras over other base toposes, encompassing that of PCAs over other base toposes, so that the same result holds for every (binary implicative) arrow algebra?

8.10. **THE MODIFICATION OF AN ARROW ALGEBRA.** Let us now study the relation between $P_{\mathcal{A}}$ and $P_{\mathcal{A}^{\to}}$. First, generalizing what is shown in [11] for discrete and absolute PCAs, we can note the following.

8.11. **LEMMA.** $P_{\mathcal{A}}$ is a subtripos of $P_{\mathcal{A}^{\to}}$.

**PROOF.** Consider the projection:

$$ \pi_1 : A^{\to} \to A \quad (x_0, x_1) \mapsto x_1 $$

Let us show that $\pi_1$, which is obviously monotone, is an implicative morphism $\mathcal{A}^{\to} \to \mathcal{A}$.

i. If $(x_0, x_1) \in S^{\to}$, then by definition $x_0 \in S$, so $x_1 \in S$ as well since $x_0 \preceq x_1$.

ii. A realizer of $\pi_1$ amounts to an element $r \in S$ such that:

$$ r \preceq (x_1 \to y_1) \to x_1 \to y_1 $$

for all $x, y \in A^{\to}$, so we can take $r := i$.

Consider now the diagonal map:

$$ \delta : A \to A^{\to} \quad a \mapsto (a, a) $$

Let us show that $\delta$, also obviously monotone, is an implicative morphism $\mathcal{A} \to \mathcal{A}^{\to}$.

i. If $a \in S$, then clearly $(a, a) \in S$.

ii. We have:

$$ \mathcal{A} \delta(a \to a') \to \delta(a) \to \delta(a') \in S^{\to} $$

$$ \iff \mathcal{A} (a \to a', a \to a') \to (a, a) \to (a', a') \in S^{\to} $$

$$ \iff \mathcal{A} (a \to a') \to a \to a' \in S $$

which is ensured by $i \in S$.
Finally, let us show that $\delta$ is right adjoint to $\pi_1$ in $\mathbf{ArrAlg}$, making it an implicative surjection.

- On one hand, $\pi_1\delta = \mathrm{id}_A$.

- On the other, we have:

$$ \begin{align*} \mathrm{id}_{A \to A} &\vdash \delta \pi_0 \\ \iff \mathbf{A} &\xrightarrow[x \in A \to]{\phantom{\delta}} (x_0, x_1) \to (x_1, x_1) \in S \xrightarrow{\phantom{\delta}} \\ \iff \mathbf{A} &\xrightarrow[x \in A \to]{\phantom{\delta}} x_1 \to x_1 \in S \end{align*} $$

which is ensured by $\mathbf{i} \in S$.

Therefore, $\pi_1$ induces a geometric inclusion $\Phi_1 : P_A \dashrightarrow P_{A \to}$.

<figure><img src="image_12.png" /></figure>

**8.12. COROLLARY.** $\mathbf{AT}(\mathcal{A})$ is a subtopos of $\mathbf{AT}(\mathcal{A}^{\to})$.

**8.13. QUESTION.** In the case of $\mathcal{A} = \mathrm{Pow}(\mathbb{P})$ for a discrete and absolute PCA $\mathbb{P}$, Johnstone [11, Lem. 3.1] showed that there is another inclusion $P_A \dashrightarrow P_{A \to}$, induced by the projection $\pi_0 : \mathcal{A}^{\to} \to \mathcal{A}$ and disjoint from $\Phi_1$. We have not been able to show that this holds in general for (binary implicative) arrow algebras, nor to find reasonable assumptions under which this may be the case.

At least in the modifiable case, we can say more about the inclusion $\Phi_1 : P_A \dashrightarrow P_{A \to}$.

Specializing Definition 1.21 to the context of arrow algebras, recall that a subtripos of $P_A$ is open if it is induced by a nucleus $o$ on $\mathcal{A}$ of the shape:

$$ o(a) := u \to a $$

for some $u \in A$, in which case the closed nucleus:

$$ c(a) := a \lor u $$

induces its complement in the lattice of subtriposes of $P_A$ considered up to equivalence.

**8.14. DEFINITION.** Given a modifiable arrow algebra $\mathcal{A}$, we define its modification as the arrow algebra $\mathcal{A}^m := (\mathcal{A}^{\to})_c$, where $c$ is the nucleus on $\mathcal{A}^{\to}$ defined by:

$$ c(x) := x \lor (\bot, \top) $$

We denote with $M_A$ the modified arrow tripos $P_{A^m}$, that is, the subtripos $P_{(A^{\to})_c}$ of $P_{A^{\to}}$.
8.15. PROPOSITION. Let $\mathcal{A}$ be a modifiable arrow algebra.

Then, the inclusion $\Phi_1 : P_A \to P_{A^\to}$ is open, induced by the nucleus:

$$o(x) := (\bot, \top) \to x$$

In particular, $M_A$ is the closed complement of $P_A$ in the lattice of subtriposes of $P_{A^\to}$ considered up to equivalence.

PROOF. By Remark 7.18 and the discussion preceding it, we only have to show that $o \vdash \delta\pi_1$.

- To show that $o \vdash_{A^\to} \delta\pi_1$, note that:

$$ \begin{align*} \mathfrak{A}_{x \in A^\to} o(x) \to \delta\pi_1(x) \in S^\to &\iff \mathfrak{A}_{x \in A^\to} ((\bot, \top) \to (x_0, x_1)) \to (x_1, x_1) \in S^\to \\ &\iff \mathfrak{A}_{x \in A^\to} (\bot \to x_0 \mathfrak{A} \top \to x_1, \top \to x_1) \to (x_1, x_1) \in S^\to \\ &\iff \mathfrak{A}_{x \in A^\to} (\bot \to x_0 \mathfrak{A} \top \to x_1) \to x_1 \mathfrak{A} (\top \to x_1) \to x_1 \in S \\ &\iff \mathfrak{A}_{x \in A^\to} (\top \to x_1) \to x_1 \in S \end{align*} $$

which is ensured by the properties of $\partial a := \top \to a$.

- To show that $\delta\pi_1 \vdash_{A^\to} o$ note that, by the hypothesis of modifiability:

$$ \begin{align*} \mathfrak{A}_{x \in A^\to} \delta\pi_1(x) \to o(x) \in S^\to &\iff \mathfrak{A}_{x \in A^\to} (x_1, x_1) \to (\bot, \top) \to (x_0, x_1) \in S^\to \\ &\iff \mathfrak{A}_{x \in A^\to} (x_1, x_1) \to (\bot \to x_0 \mathfrak{A} \top \to x_1, \top \to x_1) \in S^\to \\ &\iff \mathfrak{A}_{x \in A^\to} (x_1, x_1) \to (\top \to x_1, \top \to x_1) \in S^\to \\ &\iff \mathfrak{A}_{x \in A^\to} (x_1 \to \top \to x_1, x_1 \to \top \to x_1) \in S^\to \\ &\iff \mathfrak{A}_{x \in A^\to} x_1 \to \top \to x_1 \in S \end{align*} $$

which is again ensured by the properties of $\partial a := \top \to a$.

■
8.16. EXAMPLE. For $\mathcal{A} = \operatorname{Pow}(\mathcal{K}_1)$, we reobtain what proved in [27]: the effective topos $\operatorname{Eff} \simeq \operatorname{AT}(\mathcal{A})$ is an open subtopos of the effective topos built on the topos of sheaves over the Sierpiński space, $\operatorname{Eff}_{\to}$. $\simeq \operatorname{AT}(\mathcal{A}^{\to})$, and Grayson's modified realizability topos $\operatorname{Mod} -$ characterized in [25] as $\operatorname{AT}(\mathcal{A}^m)$ – is its closed complement.

8.17. EXAMPLE. For $\mathcal{A} = \operatorname{PERN}$, we obtain that the *extensional modified realizability topos* characterized in [25] as $\operatorname{AT}(\mathcal{A}^m)$ is the closed complement of $\operatorname{AT}(\mathcal{A})$ as subtoposes of $\operatorname{AT}(\mathcal{A}^{\to})$.

Let us now see how the construction of the modified arrow tripos can be made pseudofunctorial. In the proof, we will need the following property, which makes use of the hypothesis of modifiability.

8.18. LEMMA. Let $f: \mathcal{A} \to \mathcal{B}$ be an implicative morphism in $\operatorname{ArrAlg}_{\mathrm{mod}}$. Then, $cf \to c \vdash f \to c$.<fnref n="14" />

PROOF. By definition of the nucleus $c \in \mathbb{N}(\mathcal{B}^{\to})$, and using the fact that logical joins are computed pointwise in $(\mathcal{B}^{\to})^{A^{\to}}$, $cf \to c \vdash f \to c$ is equivalent to:

$$ \mathcal{A} (\bot, \top) \to f \to c(x) \in S_B^{\to} \qquad x \in A^{\to} $$

Since $\mathcal{B}$ is modifiable, this reduces to:

$$ \mathcal{A} \top \to Mf((cx)_1) \in S_B \qquad x \in A^{\to} $$

where $M: \operatorname{ArrAlg} \to \operatorname{ArrAlg}$ is the monotonization pseudofunctor of Remark 3.10, and hence since $Mf \dashv f$:

$$ \mathcal{A} \top \to f(((\bot, \top) \lor (x_0, x_1))_1) \in S_B \qquad x \in A^{\to} $$

Note now that, in any arrow algebra of the form $\mathcal{A}^{\to}$, the logical join $a \lor a'$ has $a_1 \lor a'_1$ as its second component. This can be seen using the explicit description of logical joins given in [25, Prop. 5.1] together with Remark 5.16, recalling also that (evidential) meets and implications in $\mathcal{A}^{\to}$ are computed pointwise on the second component. Hence, the previous explicitly reads as:

$$ \mathcal{A} \top \to f(\top \lor x_1) \in S_B \qquad x \in A^{\to} $$

which follows from $\mathcal{A}_{a \in A} \top \to (\top \lor a) \in S_A$ by the properties of implicative morphisms. ■

<footnote n="14">¹⁴Of course, the first $c$ is a nucleus on $\mathcal{A}^{\to}$, while the second one is a nucleus on $\mathcal{B}^{\to}$.</footnote>
8.19. THEOREM. For every implicative morphism $f : \mathcal{A} \to \mathcal{B}$ in $\text{ArrAlg}_{\text{mod}}$, let $f^m : \mathcal{A}^m \to \mathcal{B}^m$ be the composite:

$$ \mathcal{A}^m \xrightarrow{c} \mathcal{A} \xrightarrow{f} \mathcal{B} \xrightarrow{\text{id}_{\mathcal{B}}} \mathcal{B}^m $$

where $f : \mathcal{A} \to \mathcal{B}$ is the implicative morphism defined in Proposition 8.7.

Then, $(-)^m$ is a pseudofunctor $\text{ArrAlg}_{\text{mod}} \to \text{ArrAlg}$.

Moreover, if $f$ is computationally dense with right adjoint $h : \mathcal{B} \to \mathcal{A}$, then $f^m$ is computationally dense as well, and a right adjoint is given by $h^m : \mathcal{B}^m \to \mathcal{A}^m$. Furthermore, the square:

$$ \begin{tikzcd} & \mathcal{B}^m \arrow[r, "h^m"] \arrow[d, "c"] & \mathcal{A}^m \arrow[d, "c"] \\ \mathcal{B}^m \arrow[r, "h"] & \mathcal{A} \arrow[r, "\text{id}_{\mathcal{A}}"] \arrow[d, "c"] & \mathcal{B}^m \arrow[r, "\text{id}_{\mathcal{B}}"] \arrow[d, "c"] \end{tikzcd} $$

commutes up to isomorphism.

PROOF. First, let us show that $(-)^m$ preserves identities and compositions up to isomorphism.

- By definition, $\text{id}_{\mathcal{A}}^m : \mathcal{A}^m \to \mathcal{A}^m$ is given by the composite:

$$ \mathcal{A}^m \xrightarrow{c} \mathcal{A} \xrightarrow{\text{id}_{\mathcal{A}}} \mathcal{A} \xrightarrow{\text{id}_{\mathcal{A}}} \mathcal{A}^m $$

which means that $\text{id}_{\mathcal{A}}^m = c : \mathcal{A}^m \to \mathcal{A}^m$, and obviously $c \vdash c^c \text{id}_{\mathcal{A}}$.

- By definition, for $f : \mathcal{A} \to \mathcal{B}$ and $g : \mathcal{B} \to \mathcal{C}$, $(gf)^m$ is given by the composite:

$$ \mathcal{A}^m \xrightarrow{c} \mathcal{A} \xrightarrow{(gf)} \mathcal{C} \xrightarrow{\text{id}_{\mathcal{C}}} \mathcal{C}^m $$

where of course $(gf) \vdash c^c g \vdash f$, whereas $g^m f^m$ is given by the composite:

$$ \mathcal{A}^m \xrightarrow{c} \mathcal{A} \xrightarrow{f} \mathcal{B} \xrightarrow{\text{id}_{\mathcal{B}}} \mathcal{B}^m \xrightarrow{c} \mathcal{B} \xrightarrow{g} \mathcal{C} \xrightarrow{\text{id}_{\mathcal{C}}} \mathcal{C}^m $$

which means that we need to show that $g \vdash c^c f \vdash c \vdash c^c g \vdash f \vdash c$.

On one hand, using the fact that $\text{id} \vdash c$ both for $c \in \mathcal{N}(\mathcal{B})$ and $c \in \mathcal{N}(\mathcal{C})$:

$$ g \vdash f \vdash c \vdash g \vdash c^c f \vdash c \vdash c^c g \vdash c^c f \vdash c $$

i.e. $g \vdash f \vdash c \vdash c^c g \vdash c^c f \vdash c$.

On the other, by the previous lemma we know that $c f \vdash c \vdash f \vdash c$, which implies $g \vdash c^c f \vdash c \vdash g \vdash f \vdash c$ by the properties of $g$, and hence $g \vdash c^c f \vdash c \vdash c^c g \vdash f \vdash c$ since $\text{id}_{\mathcal{C}} \vdash c$.
The pseudofunctoriality of $f \mapsto f^{\rightarrow}$ then yields the pseudofunctoriality of $f \mapsto f^m$.

Suppose now $h : \mathcal{B} \to \mathcal{A}$ is right adjoint to $f$; let us show that $h^{\rightarrow}c$ is right adjoint to $f^{\rightarrow}c : \mathcal{A}^m \to \mathcal{B}^m$.

- On one hand, $f^{\rightarrow}ch^{\rightarrow}c \vdash_{\mathcal{B}^{\rightarrow}}^c id_{\mathcal{B}^{\rightarrow}}$ explicitly reads as $f^{\rightarrow}ch^{\rightarrow}c \vdash_{\mathcal{B}^{\rightarrow}} c$. By Proposition 8.7, we know that $h^{\rightarrow}$ is right adjoint to $f^{\rightarrow}$, so the previous is equivalent to $ch^{\rightarrow}c \vdash_{\mathcal{B}^{\rightarrow}} h^{\rightarrow}c$, which is ensured by the previous lemma.

- On the other, $id_{A \rightarrow} \vdash_{A \rightarrow}^c h^{\rightarrow}cf^{\rightarrow}c$ explicitly reads as $id_{A \rightarrow} \vdash_{A \rightarrow} ch^{\rightarrow}cf^{\rightarrow}c$. As $id_{A \rightarrow} \vdash c$, this is ensured if $id_{A \rightarrow} \vdash_{A \rightarrow} h^{\rightarrow}cf^{\rightarrow}c$. This is again equivalent to $f^{\rightarrow} \vdash_{A \rightarrow} cf^{\rightarrow}c$ as $h^{\rightarrow}$ is right adjoint to $f^{\rightarrow}$, which follows since $id \vdash c$ both for $c \in \mathcal{N}(\mathcal{A}^{\rightarrow})$ and $c \in \mathcal{N}(\mathcal{B}^{\rightarrow})$.

Finally, to show that the square above commutes up to isomorphism, we need to show that $ch^m \dashv h^{\rightarrow}c$ as morphisms $\mathcal{B}^m \to \mathcal{A}^{\rightarrow}$. On one hand, $h^{\rightarrow}c \vdash ch^m$ explicitly means $h^{\rightarrow}c \vdash_{\mathcal{B}^{\rightarrow}} ch^{\rightarrow}c$, which follows simply from $id_{A \rightarrow} \vdash c$. On the other, $ch^m \vdash h^{\rightarrow}c$ explicitly means $ch^{\rightarrow}c \vdash_{\mathcal{B}^{\rightarrow}} h^{\rightarrow}c$, which is again ensured by the previous lemma. ■

**8.20. COROLLARY.** Let $\mathcal{A}$ and $\mathcal{B}$ be modifiable arrow algebras.

Then, every geometric morphism $\Phi : P_{\mathcal{B}} \to P_{\mathcal{A}}$ induces a geometric morphism $\Phi^m : M_{\mathcal{B}} \to M_{\mathcal{A}}$ such that the diagram:

<figure><img src="image_13.png" /></figure>

is a pullback square of triposes and geometric morphisms.

In particular, the induced diagram of toposes and geometric morphisms:

<figure><img src="image_14.png" /></figure>

is a pullback square.

**PROOF.** The fact that the square commutes follows directly by the previous proposition. To show that it is a pullback, instead, recall from [12] that, given a closed nucleus $kx := x \lor u$ on $\mathcal{A}^{\rightarrow}$, the pullback of the closed subtripos $P_{\mathcal{A}_k^{\rightarrow}} \twoheadrightarrow P_{\mathcal{A}^{\rightarrow}}$ along $\Phi^{\rightarrow}$ is the closed subtripos of $P_{\mathcal{B}^{\rightarrow}}$ determined by the nucleus $k'y := y \lor (\Phi^{\rightarrow})_{\mathcal{B}^{\rightarrow}}^{+}(u)$. Therefore, the square above is a pullback if and only if $(\Phi^{\rightarrow})_{\mathcal{B}^{\rightarrow}}^{+}(\bot, \top) \dashv (\bot, \top)$ in $\mathcal{B}^{\rightarrow}$.

To prove this, let $f : \mathcal{A} \to \mathcal{B}$ be an implicative morphism with right adjoint $h : \mathcal{B} \to \mathcal{A}$ inducing $\Phi$, so that $\Phi^{\rightarrow}$ is induced by $f^{\rightarrow}$ with right adjoint $h^{\rightarrow}$ as in Proposition 8.7;
then, we need to show that $f^{\rightarrow}(\perp, \top) \dashv\vdash (\perp, \top)$ in $\mathcal{B}^{\rightarrow}$. On one hand, by modifiability of $\mathcal{B}$, $(\perp, \top) \vdash f^{\rightarrow}(\perp, \top)$ reduces simply to $\top \vdash f(\top)$, which is true as $f$ is an implicative morphism. On the other, $f^{\rightarrow}(\perp, \top) \vdash (\perp, \top)$ is equivalent to $(\perp, \top) \vdash h^{\rightarrow}(\perp, \top)$, which is true again as $\mathcal{A}$ is modifiable and $h$ is an implicative morphism. ■

**8.21. REMARK.** In particular, restricting to arrow algebras of the form $\text{Pow}(\mathbb{P})$ for a discrete and absolute PCA $\mathbb{P}$, we reobtain [12, Prop. 2.1].

**8.22. REMARK.** Recall by Proposition 7.12 that we can identify $M_{\mathcal{A}}$ up to equivalence with the subtripos $M'_{\mathcal{A}} \dashrightarrow P_{\mathcal{A}}$ defined by:

$$
\begin{align*}
M'_{\mathcal{A}}(I) &:= \{ \alpha \in P_{\mathcal{A}}(I) \mid c\alpha \vdash_I \alpha \} \\
&= \{ \alpha \in P_{\mathcal{A}}(I) \mid \mathfrak{A}(\perp, \top) \xrightarrow{i} \alpha(i) \in S_{\mathcal{A}}^{\rightarrow} \} \\
&= \{ \alpha \in P_{\mathcal{A}}(I) \mid \mathfrak{A} \top \rightarrow_i \alpha_1(i) \in S_{\mathcal{A}} \} \\
&= \{ \alpha \in P_{\mathcal{A}}(I) \mid \top_I \vdash_I \alpha_1 \}
\end{align*}
$$

and in the same way we can identify $M_{\mathcal{B}}$ up to equivalence with the subtripos $M'_{\mathcal{B}} \dashrightarrow P_{\mathcal{B}}$ defined by:

$$M'_{\mathcal{B}}(I) = \{ \beta \in P_{\mathcal{B}}(I) \mid \top_I \vdash_I \beta_1 \}$$

In these terms, $\Phi^m$ can be described explicitly as:

$$M'_{\mathcal{B}} \underset{h \rightarrow \circ -}{\stackrel{f \rightarrow \circ -}{\rightleftharpoons}} \mathfrak{M}'_{\mathcal{A}}$$

that is, exactly the restriction of $\Phi^{\rightarrow}$ in both directions.

The details of the proof of the previous corollary also reveal that a similar result holds for open complements of modified triposes, again generalizing what proved in [12].

**8.23. PROPOSITION.** Let $\mathcal{A}$ and $\mathcal{B}$ be modifiable arrow algebras.

Then, for every geometric morphism $\Phi : P_{\mathcal{B}} \rightarrow P_{\mathcal{A}}$, the diagram:

$$\begin{tikzcd}
& & P_{\mathcal{B}} \arrow[r, "\Phi"] & P_{\mathcal{A}} \\
& & \bigcirc \arrow[u] \arrow[r, "\Phi \rightarrow"] & \bigcirc \\
P_{\mathcal{B}} & & P_{\mathcal{A}}
\end{tikzcd}$$

is a pullback square of triposes and geometric morphisms.
In particular, the induced diagram of toposes and geometric morphisms:

<figure><img src="image_15.png" /></figure>

is a pullback square.

References

[1] F. Borceux, *Handbook of Categorical Algebra*. Cambridge University Press, 1994.

[2] L. Birkedal and J. van Oosten, “Relative and modified relative realizability”, *Annals of Pure and Applied Logic*, vol. 118, no. 1, pp. 115–132, 2002.

[3] L. Cohen, É. Miquey and R. Tate, “Evidenced Frames: A Unifying Framework Broadening Realizability Models”, *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pp. 1-13, 2021.

[4] R. Grayson, “Modified realizability toposes”, handwritten notes from Münster University, 1981.

[5] D. Higgs, “A category approach to boolean-valued set theory”, unpublished, 1973.

[6] P. J. W. Hofstra and J. van Oosten, “Ordered partial combinatory algebras”, *Mathematical Proceedings of the Cambridge Philosophical Society*, vol. 134, no. 3, pp. 445–463, 2003.

[7] P. J. W. Hofstra, “All realizability is relative”, *Mathematical Proceedings of the Cambridge Philosophical Society*, vol. 141, no. 2, pp. 239–264, 2006.

[8] J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts, “Tripos theory”, *Mathematical Proceedings of the Cambridge Philosophical Society*, vol. 88, no. 2, pp. 205–232, 1980.

[9] P. T. Johnstone, *Sketches of an Elephant: a Topos Theory Compendium*, Oxford Logic Guides, Oxford University Press, 2002.

[10] P. T. Johnstone, “Geometric morphisms of realizability toposes”, *Theory and Applications of Categories*, vol. 28, no. 9, pp. 241-249, 2013.

[11] P. T. Johnstone, “The Gleason cover of a realizability topos”, *Theory and Applications of Categories*, vol. 28, no. 32, pp. 1139-1152, 2013.

[12] P. T. Johnstone, “Functoriality of modified realizability”, *Tbilisi Mathematical Journal*, vol. 10, pp. 209-222, 2017.

[13] N. Johnson and D. Yau, *2-Dimensional Categories*, Oxford University Press, 2020.
[14] S. C. Kleene, "On the interpretation of intuitionistic number theory", *Journal of Symbolic Logic*, vol. 10, no. 4, pp. 109-124, 1945.

[15] S. C. Kleene, *The Foundations of Intuitionistic Mathematics*, North-Holland Pub. Co., 1965.

[16] G. Kreisel, "Interpretation of analysis by means of constructive functionals of finite types", in *Constructivity in Mathematics*, A. Heyting, Ed., North-Holland Pub. Co., 1959, pp. 101-128.

[17] J. Longley, "Realizability Toposes and Language Semantics", PhD dissertation, 1995. Available online at: https://era.ed.ac.uk/handle/1842/402

[18] A. Miquel, "Implicative algebras: a new foundation for realizability and forcing", *Mathematical Structures in Computer Science*, vol. 30, no. 5, pp. 458-510, 2020.

[19] A. Miquel, "Implicative algebras II: completeness w.r.t. Set-based triposes", 2020, arXiv:2011.09085.

[20] S. Mac Lane and I. Moerdijk, *Sheaves in Geometry and Logic*, Universitext, Springer, 1992.

[21] A. M. Pitts, "The theory of triposes", Ph.D. dissertation, University of Cambridge, 1981. Available online at: https://www.cl.cam.ac.uk/amp12/papers/thet/thet.pdf

[22] W. Ferrer Santos and O. Malherbe, "The category of implicative algebras and realizability", *Mathematical Structures in Computer Science*, vol. 29, pp. 1575-1606, 2017.

[23] J. Frey, "A fibrational study of realizability toposes", Ph.D. dissertation, Université Paris Diderot, 2013. Available online at: https://arxiv.org/abs/1403.3672

[24] J. Frey, "Uniform Preorders and Partial Combinatory Algebras", 2024, arXiv:2403.17340.

[25] B. van den Berg and M. Briët, "Arrow algebras", 2023, arXiv:2308.14096.

[26] J. van Oosten, "A combinatory algebra for sequential functionals of finite type", in *Models and Computability*, S. B. Cooper and J. K. Truss, Eds., Cambridge University Press, 1997, pp. 389-406.

[27] J. van Oosten, "The modified realizability topos", *Journal of Pure and Applied Algebra*, vol. 116, no. 1, pp. 273-289, 1997.

[28] J. van Oosten, *Realizability: an Introduction to its Categorical Side*, Elsevier Science, 2008.

[29] J. Zoethout, "Computability models and realizability toposes", Ph.D. dissertation, 2022. Available online at: https://dspace.library.uu.nl/handle/1874/416798

IRIF, Université Paris Cité, France

Email: tarantino@irif.fr
THEORY AND APPLICATIONS OF CATEGORIES will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

SUBSCRIPTION INFORMATION Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. Full text of the journal is freely available at http://www.tac.mta.ca/tac/.

INFORMATION FOR AUTHORS LATEX2e is required. Articles may be submitted in PDF by email directly to a Transmitting Editor following the author instructions at http://www.tac.mta.ca/tac/authinfo.html.

MANAGING EDITOR. Geoff Cruttwell, Mount Allison University: gcruttwell@mta.ca

TEXNICAL EDITOR. Michael Barr, McGill University: michael.barr@mcgill.ca

ASSISTANT TEX EDITOR. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne: gavin.seal@fastmail.fm

TRANSMITTING EDITORS.

Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr

Julie Bergner, University of Virginia: jeb2md (at) virginia.edu

Richard Blute, Université d'Ottawa: rblute@uottawa.ca

John Bourke, Masaryk University: bourkej@math.muni.cz

Maria Manuel Clementino, Universidade de Coimbra: mmc@mat.uc.pt

Valeria de Paiva, Topos Institute: valeria.depaiva@gmail.com

Richard Garner, Macquarie University: richard.garner@mq.edu.au

Ezra Getzler, Northwestern University: getzler (at) northwestern(dot)edu

Rune Haugseng, Norwegian University of Science and Technology: rune.haugseng@ntnu.no

Dirk Hofmann, Universidade de Aveiro: dirk@ua.pt

Joachim Kock, Universitat Autònoma de Barcelona: Joachim.Kock (at) uab.cat

Stephen Lack, Macquarie University: steve.lack@mq.edu.au

Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk

Sandra Mantovani, Università degli Studi di Milano: sandra.mantovani@unimi.it

Matias Menni, Conicet and Universidad Nacional de La Plata, Argentina: matias.menni@gmail.com

Giuseppe Metere, Università degli Studi di Palermo: giuseppe.metere (at) unipa.it

Kate Ponto, University of Kentucky: kate.ponto (at) uky.edu

Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

Jiri Rosický, Masaryk University: rosicky@math.muni.cz

Giuseppe Rosolini, Università di Genova: rosolini@unige.it

Michael Shulman, University of San Diego: shulman@sandiego.edu

Alex Simpson, University of Ljubljana: Alex.Simpson@fmf.uni-lj.si

James Stasheff, University of North Carolina: jds@math.upenn.edu

Tim Van der Linden, Université catholique de Louvain: tim.vanderlinden@uclouvain.be

Christina Vasilakopoulou, National Technical University of Athens: cvasilak@math.ntua.gr