arXiv · 2407.02836
A category of arrow algebras for modified realizability
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.
Explore related subjects
Keep this discovery
Umberto Tarantino. 2024-07-03. A category of arrow algebras for modified realizability. https://arxiv.org/abs/2407.02836
Cite the original work for its findings. Save a collection to share your selection of sources.