Hostname: page-component-78c5997874-xbtfd Total loading time: 0 Render date: 2024-11-05T21:11:13.315Z Has data issue: false hasContentIssue false

Iterated realizability as a comma construction

Published online by Cambridge University Press:  01 January 2008

PIETER J. W. HOFSTRA*
Affiliation:
University of Ottawa, Department of Mathematics and Statistics, 585 King Edward Avenue, Ottawa, ON, K1N 6N5, Canada. e-mail: [email protected]

Abstract

We show that the 2-category of partial combinatory algebras, as well as various related categories, admit a certain type of lax comma objects. This not only reveals some of the properties of such categories, but it also gives an interpretation of iterated realizability, in the following sense. Let φ: AB be a morphism of PCAs, giving a comma object AφB. In the realizability topos RT(B) over B, the object (A, φ) is an internal PCA, so we can construct the realizability topos over (A, φ). This topos is equivalent to the realizability topos over the comma-PCA AφB. This result is both an analysis and a generalization of a special case studied by Pitts in the context of the effective monad.

Type
Research Article
Copyright
Copyright © Cambridge Philosophical Society 2008

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

REFERENCES

[Hof03a]Hofstra, P. J. W. and Oosten, J. van. Ordered partial combinatory algebras. Math. Proc. Camb. Phil. Soc. 134 (2003), 445463.CrossRefGoogle Scholar
[Hof03b]Hofstra, P. J. W.. Completions in realizability. Ph.D. thesis, Utrecht University (2003).Google Scholar
[Hof05]Hofstra, P. J. W.. All realizability is relative. Accepted for publication in Math. Proc. Camb. Phil. Soc.Google Scholar
[Lon94]Longley, J.. Realizability toposes and language semantics. Ph.D. thesis, University of Edinburgh (1994).Google Scholar
[Pit81]Pitts, A. M.. The theory of triposes. Ph.D. thesis, University of Cambridge (1981).Google Scholar