More on Geometric Morphisms between Realizability Toposes

TL;DR

This paper investigates the structure of geometric morphisms between realizability toposes, characterizing the conditions on partial combinatory algebras that induce such morphisms and their relation to the effective topos.

Contribution

It provides a new characterization of morphisms between realizability toposes via partial combinatory algebras and explores their connection to the effective topos.

Findings

Morphisms are induced by computationally dense pca morphisms with right adjoints.

Characterization of topos inclusions related to relative computability.

Identification of pcas whose realizability toposes map to the effective topos.

Abstract

Geometric morphisms between realizability toposes are studied in terms of morphisms between partial combinatory algebras (pcas). The morphisms inducing geometric morphisms (the {\em computationally dense\/} ones) are seen to be the ones whose `lifts' to a kind of completion have right adjoints. We characterize topos inclusions corresponding to a general form of relative computability. We characterize pcas whose realizability topos admits a geometric morphism to the effective topos.