nLab category of PERs

The category of PERs

The category of PERs


The category of PERs over a partial combinatory algebra AA is a particularly concrete and simple subcategory of its realizability topos, which is especially well-suited to modelling “computable” objects relative to AA.

It is based on the idea that a “computable set” XX relative to AA is specified by saying which elements of AA are “codes” representing which elements of XX, such that no element of AA can code for more than one element of XX (but not all elements of AA need to code for any element of XX). Thus this sort of “computable set” (sometimes called a modest set) is equivalently a partition of a subset of AA, i.e. a partial equivalence relation on AA.


Let AA be a partial combinatory algebra. If EE is a partial equivalence relation on AA, we write A/EA/E for its set of equivalence classes. Now the category PER(A)PER(A) has:

  • as objects, the partial equivalence relations on AA.

  • as morphisms EEE\to E', for PERs EE and EE', the set-theoretic functions ϕ:A/EA/E\phi:A/E \to A/E' with the property of being “tracked”, i.e. such that there exists an element fAf\in A such that whenever (a,a)E(a,a)\in E we have ϕ([a])=[fa]\phi([a]) = [f\cdot a] (hence in particular (fa,fa)E(f\cdot a,f\cdot a)\in E'). Equivalently, it is the quotient of the set of elements fAf\in A such that (a,b)E(a,b)\in E implies (fa,fb)E(f\cdot a,f\cdot b)\in E' by the relation fgf\sim g meaning that (fa,ga)E(f\cdot a,g\cdot a)\in E' whenever (a,a)E(a,a)\in E.


In first-order logic

Given a theory in first-order logic with equality (categorically, this can be taken as a first-order hyperdoctrine), its category of partial equivalence relations represents all the subquotients the theory can “see” of its given sorts and all the functions the theory can “see” between them.

Specifically, the objects of this category are pairs (X,R)(X, R) where XX is a sort in the first-order theory and RR is a binary predicate which the theory proves to be a partial equivalence relation on XX. A morphism between objects (X,R)(X, R) and (Y,S)(Y, S) can be taken to be a binary predicate FP(X×Y)F \in P(X \times Y) such that the theory proves FF is essentially the graph of a function between the specified subquotients (In detail: …). Composition is given in the obvious way (In detail: …).

In the case where the original hyperdoctrine was in fact a tripos, the resulting category of PERs will be a topos (while the converse isn’t quite true, the condition of being a tripos is just slightly stronger than necessary for this to happen).

Last revised on December 7, 2023 at 17:27:38. See the history of this page for a list of all contributions to it.