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 where is a sort in the first-order theory and is a binary predicate which the theory proves to be a partial equivalence relation on . A morphism between objects and can be taken to be a binary predicate such that the theory proves 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).