Models of Intuitionistic Set Theory in Subtoposes of Nested Realizability Toposes

Abstract

With every pca $\mathcal{A}$ and subpca ${\mathcal{A}}_{\#}$ we associate the nested realizability topos $\mathsf{RT}(\mathcal{A},{\mathcal{A}}_{\#})$ within which we identify a class of small maps $\mathcal{S}$ giving rise to a model of intuitionistic set theory within $\mathsf{RT}(\mathcal{A},{\mathcal{A}}_{\#})$. For every subtopos $\mathcal{E}$ of such a nested realizability topos we construct an induced class ${\mathcal{S}}_{\mathcal{E}}$ of small maps in $\mathcal{E}$ giving rise to a model of intuitionistic set theory within $\mathcal{E}$. This covers relative realizability toposes, modified relative realizability toposes, the modified realizability topos and van den Berg's recent Herbrand topos.