Hostname: page-component-78c5997874-xbtfd Total loading time: 0 Render date: 2024-11-13T01:08:30.737Z Has data issue: false hasContentIssue false
  • English
  • Français

Regular functors and relative realisability categories

Published online by Cambridge University Press:  18 April 2013

WOUTER PIETER STEKELENBURG
WOUTER PIETER STEKELENBURG*
Affiliation:
Utrecht University, Department of Mathematics, P.O. Box 80010, 3508 TA Utrecht, The Netherlands Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The relative realisability toposes introduced by Awodey, Birkedal and Scott in Awodey et al. (2002) satisfy a universal property involving regular functors to other categories. We use this universal property to define what relative realisability categories are when they are based on categories other than the topos of sets. This paper explains the property and gives a construction for relative realisability categories that works for arbitrary base Heyting categories. The universal property also provides some new geometric morphisms to relative realisability toposes.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 23 , Issue 5 , October 2013 , pp. 1082 - 1110
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Awodey, S., Birkedal, L. and Scott, D. S. (2002) Local realizability toposes and a modal logic for computability. Mathematical Structures in Computer Science 12 (3)319–334.CrossRefGoogle Scholar
Bauer, A. (2000) The realizability approach to computable analysis and topology, Ph.D. Thesis, Carnegie Mellon University.Google Scholar
Birkedal, L. (2000) Developing theories of types and computability via realizability. Electronic Notes in Theoretical Computer Science 34.CrossRefGoogle Scholar
Birkedal, L. and van Oosten, J. (2002) Relative and modified relative realizability. Annals of Pure and Applied Logic 118 (1–2)115–132.CrossRefGoogle Scholar
Carboni, A. (1995) Some free constructions in realizability and proof theory. Journal of Pure and Applied Algebra 103 (2)117–148.CrossRefGoogle Scholar
Carboni, A. and Celia Magno, R. (1982) The free exact category on a left exact one. Journal of the Australian Mathematical Society, Series A 33 (3)295–301.CrossRefGoogle Scholar
Carboni, A. and Vitale, E. M. (1998) Regular and exact completions. Journal of Pure and Applied Algebra 125 (1–3)79–116.CrossRefGoogle Scholar
Carboni, A., Freyd, P. J. and Scedrov, A. (1988) A categorical approach to realizability and polymorphic types. In: Main, M., Melton, A., Mislove, M. and Schmidt, D. (eds.) Mathematical foundations of programming language semantics: Proceedings, 3rd Workshop Tulane University, New Orleans, Louisiana. Springer-Verlag Lecture Notes in Computer Science 298 23–42.CrossRefGoogle Scholar
Feferman, S. (1975) A language and axioms for explicit mathematics. In: Crossley, J. N. (ed.) Algebra and logic: Papers from the 1974 Summer Research Institute of the Australian Mathematical Society, Monash University, Australia. Springer-Verlag Lecture Notes in Mathematics 450 87–139.CrossRefGoogle Scholar
Frey, J. (2011) A 2-categorical analysis of the tripos-to-topos construction. (Preprint avaialable at arXiv:1104.2776 [math.CT].)Google Scholar
Hofstra, P. J. W. (2004) Relative completions. Journal of Pure and Applied Algebra 192 (1–3)129–148.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
Hofstra, P. J. W. (2006) All realizability is relative. Mathematical Proceedings of the Cambridge Philosophical Society 141 (2)239–264.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 (Noordwijkerhout, 1981), Studies in Logic and the Foundations of Mathematics 110, North-Holland165–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–231.CrossRefGoogle Scholar
Kleene, S. C. and Vesley, R. E. (1965) The foundations of intuitionistic mathematics, especially in relation to recursive functions, North–Holland.Google Scholar
Longley, J. R. (1994) Realizability Toposes and Language Semantics, Ph.D. thesis, University of Edinburgh.Google Scholar
Medvedev, Y. T. (1955) Degrees of difficulty of the mass problem. Doklady Akademii Nauk SSSR (N.S.) 104 501–504.Google Scholar
Menni, M. (2000) Exact Completions and Toposes, Ph.D. thesis, University of Edinburgh.Google Scholar
Menni, M. (2002) More exact completions that are toposes. Annals of Pure and Applied Logic 116 (1–3) 187–203.CrossRefGoogle Scholar
Pitts, A. M. (1981) The Theory of Triposes, Ph.D. thesis, University of Cambridge.Google Scholar
Robinson, E. and Rosolini, G. (1990) Colimit completions and the effective topos. Journal of Symbolic Logic 55 (2)678–699.CrossRefGoogle Scholar
Terwijn, S. A. (2006) Constructive logic and the Medvedev lattice. Notre Dame Journal of Formal Logic 47 (1)73–82 (electronic).CrossRefGoogle Scholar
van Oosten, J. (2008) Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics 152, Elsevier.Google Scholar