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

Jetze Zoethout

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

We consider two preorder-enriched categories of ordered partial combinatory algebras: OPCA, where the arrows are functional (i.e., projective) morphisms, and OPCA†, where the arrows are applicative morphisms. We show that OPCA has small products and finite biproducts, and that OPCA† has finite coproducts, 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 a realizability topos. In contrast, we show that nontrivial subtoposes of realizability toposes are closed under pushouts over Set.
Original languageEnglish
Pages (from-to)214-233
Number of pages20
JournalMathematical Structures in Computer Science
Volume31
Issue number2
DOIs
Publication statusPublished - 13 Feb 2021

Keywords

  • Partial combinatory algebra
  • realizability
  • toposes

Fingerprint

Dive into the research topics of 'On (co)products of partial combinatory algebras, with an application to pushouts of realizability toposes'. Together they form a unique fingerprint.

Cite this