Exact completion

In category theory, a branch of mathematics, the exact completion constructs a Barr-exact category from any finitely complete category.

It is used to form the effective topos and other realizability toposes.

Let C be a category with finite limits.

Then the exact completion of C (denoted Cex) has for its objects pseudo-equivalence relations in C.[1] A pseudo-equivalence relation is like an equivalence relation except that it need not be jointly monic.

An object in Cex thus consists of two objects X0 and X1 and two parallel morphisms x0 and x1 from X1 to X0 such that there exist a reflexivity morphism r from X0 to X1 such that x0r = x1r = 1X0; a symmetry morphism s from X1 to itself such that x0s = x1 and x1s = x0; and a transitivity morphism t from X1 × x1, X0, x0 X1 to X1 such that x0t = x0p and x1t = x1q, where p and q are the two projections of the aforementioned pullback.