English

On the Existence of Pushouts of Realizability Toposes

Category Theory 2020-12-07 v2

Abstract

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

Keywords

Cite

@article{arxiv.2011.08561,
  title  = {On the Existence of Pushouts of Realizability Toposes},
  author = {Jetze Zoethout},
  journal= {arXiv preprint arXiv:2011.08561},
  year   = {2020}
}

Comments

19 pages; revised argument in Section 6, added remarks and references