TY - JOUR
T1 - On (co)products of partial combinatory algebras, with an application to pushouts of realizability toposes
AU - Zoethout, Jetze
N1 - Publisher Copyright:
©
PY - 2021/2/13
Y1 - 2021/2/13
N2 - 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.
AB - 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.
KW - Partial combinatory algebra
KW - realizability
KW - toposes
UR - http://www.scopus.com/inward/record.url?scp=85113161509&partnerID=8YFLogxK
U2 - 10.1017/S096012952100013X
DO - 10.1017/S096012952100013X
M3 - Article
SN - 0960-1295
VL - 31
SP - 214
EP - 233
JO - Mathematical Structures in Computer Science
JF - Mathematical Structures in Computer Science
IS - 2
ER -