Hostname: page-component-cd9895bd7-p9bg8 Total loading time: 0 Render date: 2024-12-28T04:17:55.323Z Has data issue: false hasContentIssue false
  • English
  • Français

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

Published online by Cambridge University Press:  13 August 2021

Jetze Zoethout Open the ORCID record for Jetze Zoethout [Opens in a new window]
Jetze Zoethout*
Affiliation:
Mathematical Institute, Utrecht University, Utrecht, Netherlands Email: [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Keywords

Partial combinatory algebrarealizabilitytoposes
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 31 , Issue 2 , February 2021 , pp. 214 - 233
Check for updates
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Faber, E. and van Oosten, J. (2014). More on geometric morphisms between realizability toposes. Theory and Applications of Categories 29 (30) 874–895.Google Scholar
Hofstra, P. (2006). All realizability is relative. Mathematical Proceedings of the Cambridge Philosophical Society 141 (2) 239–264.CrossRefGoogle Scholar
Hofstra, P. and van Oosten, J. (2003). Ordered partial combinatory algebras. Mathematical Proceedings of the Cambridge Philosophical Society 134 (3) 445–463.CrossRefGoogle Scholar
Hyland, J. M. E. (1982). The effective topos. In: Troelstra, A. S. and van Dalen, D. (eds.), The L. E. J. Brouwer Centenary Symposium, Studies in Logic and the Foundations of Mathematics, vol. 110, North Holland Publishing Company, 165–216.CrossRefGoogle Scholar
Hyland, J. M. E., Johnstone, P. T. and Pitts, A. M. (1980). Tripos theory. Mathematical Proceedings of the Cambridge Philosophical Society 88 (2) 205–232.CrossRefGoogle Scholar
Johnstone, P. T. (1977). Topos Theory, Academic Press. Paperback edition: Dover reprint 2014.Google Scholar
Johnstone, P. T. (2013). Geometric morphisms of realizability toposes. Theory and Applications of Categories 28 (9) 241–249.Google Scholar
Kleene, S. C. (1945). On the interpretation of intuitionistic number theory. Journal of Symbolic Logic 10 (4) 109–124.CrossRefGoogle Scholar
Lee, S. and van Oosten, J. (2013). Basis subtoposes of the effective topos. Annals of Pure and Applied Logic 164 (9) 335–347.CrossRefGoogle Scholar
Longley, J. (1994). Realizability Toposes and Language Semantics. Phd thesis, University of Edinburgh.Google Scholar
van Oosten, J. (2008). Realizability: An Introduction to its Categorical Side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier.Google Scholar
Zoethout, J. (2020). Internal partial combinatory algebras and their slices. Theory and Applications of Categories 35 (52) 1907–1952.Google Scholar