On the Existence of Pushouts of Realizability Toposes

TL;DR

This paper investigates the categorical properties of ordered PCAs and shows that certain pushouts of realizability toposes over Set cannot be realizability toposes, revealing limitations in their categorical constructions.

Contribution

It establishes the existence of small products and finite biproducts in OPCA, finite coproducts in PCA, and proves the non-existence of certain pushouts of realizability toposes.

Findings

OPCA has small products and finite biproducts.

PCA has finite coproducts.

Pushouts of two nontrivial realizability toposes over Set are not realizability toposes.

Abstract

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