Article contents
Iterated realizability as a comma construction
Published online by Cambridge University Press: 01 January 2008
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 φ: A → B 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
- Information
- Mathematical Proceedings of the Cambridge Philosophical Society , Volume 144 , Issue 1 , January 2008 , pp. 39 - 51
- Copyright
- Copyright © Cambridge Philosophical Society 2008
References
REFERENCES
- 4
- Cited by