On the Existence of Pushouts of Realizability Toposes

Abstract

We consider two preorder-enriched categories of ordered PCAs: OPCA, where the arrows are functional morphisms, and PCA, where the arrows are applicative morphisms. We show that OPCA has small products and finite biproducts, and that PCA has finite coproducts, all in a suitable 2-categorical sense. On the other hand, PCA lacks all nontrivial binary products. We deduce from this that the pushout, over Set, of two nontrivial realizability toposes is never a realizability topos.