A category of arrow algebras for modified realizability
Umberto Tarantino
TL;DR
The paper develops arrow algebras as a concrete algebraic lens on realizability and localic toposes by defining implicative morphisms that correspond to tripos morphisms. It establishes a robust 2-categorical bridge: arrow algebras map to arrow triposes, and computationally dense morphisms induce geometric morphisms, with subtriposes corresponding to nuclei and factorization mirroring locale theory. The results specialize cleanly to frames and PCAs, recovering known realizability and localic phenomena within the arrow-algebra framework, and extend to modified realizability via the Sierpiński construction and a canonical modification operation. The framework yields functorial behavior across triposes, enabling a unified treatment of inclusions, subtoposes, and open/closed subtoposes within realizability and modified realizability settings, with concrete consequences for the corresponding toposes.
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.