The category of PERs over a partial combinatory algebra is a particularly concrete and simple subcategory of its realizability topos, which is especially well-suited to modelling “computable” objects relative to .
It is based on the idea that a “computable set” relative to is specified by saying which elements of are “codes” representing which elements of , such that no element of can code for more than one element of (but not all elements of need to code for any element of ). Thus this sort of “computable set” (sometimes called a modest set) is equivalently a partition of a subset of , i.e. a partial equivalence relation on .
Let be a partial combinatory algebra. If is a partial equivalence relation on , we write for its set of equivalence classes. Now the category has:
as objects, the partial equivalence relations on .
as morphisms , for PERs and , the set-theoretic functions with the property of being “tracked”, i.e. such that there exists an element such that whenever we have (hence in particular ). Equivalently, it is the quotient of the set of elements such that implies by the relation meaning that whenever .
is a locally cartesian closed category and a Heyting category.
is a full subcategory of the category of assemblies over , which is in turn a full subcategory of the realizability topos over .
Last revised on April 28, 2019 at 00:39:51. See the history of this page for a list of all contributions to it.