Extensional PERs

A class of Partial Equivalence Relations (PERs) is described such that the resulting full subcategory of the realizability universe has the expected properties of a good category of CPOs; that is, it is a Cartesian closed category and every endomorphism has a canonical fixed point. Moreover, the reflection functor into the subcategory of strict maps (usually called the “lifting operation”) yields a good notion of “partial map, ” a necessary condition if one wishes to maintain a connection between strict maps and partial maps. It is shown that all functors that arise in practice have canonical invariant objects; hence a host of domain equations are guaranteed to have solutions.

Authors

• P. Freyd
• P. Mulry
• G. Rosolini
• D. Scott

Keywords

No keywords are indexed for this paper.