preprint: Ordered PCA's and Realizability Toposes

[<jvoosten@math.uu.nl>]

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.