A category of arrow algebras for modified realizability

TL;DR

This paper advances the theory of arrow algebras by defining morphisms, characterizing subtriposes via nuclei, and applying these concepts to lift and establish the functoriality of modified realizability.

Contribution

It introduces morphisms between arrow algebras, characterizes subtriposes through nuclei, and extends modified realizability within this algebraic framework.

Findings

Morphisms between arrow algebras correspond to tripos morphisms.

Subtriposes are characterized by nuclei on arrow algebras.

Modified realizability is shown to be functorial in this setting.

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.