preprint: Ordered PCA's and Realizability Toposes
Paper available: P.J.W. Hofstra and J. van Oosten, Ordered PCA's and Realizability Toposes http://www.math.uu.nl/people/jvoosten/papers.html Abstract: The concept of Ordered PCA (Partial Combinatory Algebra) is defined; it is a generalization of ordinary PCA's. The construction of Realizability Toposes for OPCA's is straightforward. Two 2-categories OPCA and OPCA+ are defined, OPCA+ being a lluf subcategory of OPCA. Both have a 2-monad I on them. It is shown that the category of realizability triposes over opca's with Set-indexed exact functors is equivalent to the Kleisli category of I on OPCA, whereas the category of realizabiloity triposes with geometric morphisms is the Kleisli category for I on OPCA+. This extends and analyzes results in the theses of Pitts and Longley. As an application we obtain an elegant tripos presentation of Menni's chain of toposes, constructed as exact completions.
participants (1)
-
jvoosten@math.uu.nl