On (co)products of partial combinatory algebras, with an application to pushouts of realizability toposes

摘要

We consider two preorder-enriched categories of ordered partial combinatory algebras: OPCA, wherethe arrows are functional (i.e., projective) morphisms, and OPCA†, where the arrows are applicativemorphisms. We show that OPCA has small products and finite biproducts, and that OPCA† has finitecoproducts, all in a suitable 2-categorical sense. On the other hand, OPCA† lacks all nontrivial binary products.We deduce from this that the pushout, over Set, of two nontrivial realizability toposes is never arealizability topos. In contrast, we show that nontrivial subtoposes of realizability toposes are closed underpushouts over Set.