category of partial equivalence relations

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)$ where $X$ is a sort in the first-order theory and $R$ is a binary predicate which the theory proves to be a partial equivalence relation on $X$. A morphism between objects $(X, R)$ and $(Y, S)$ can be taken to be a binary predicate $F \in P(X \times Y)$ such that the theory proves $F$ 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).

Revised on February 23, 2010 22:27:46
by Sridhar Ramesh
(67.180.31.171)