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. A morphism from (X0, X1, x0, x1) to (Y0, Y1, y0, y1) in Cex is given by an equivalence class of morphisms f0 from X0 to Y0 such that there exists a morphism f1 from X1 to Y1 such that y0f1 = f0x0 and y1f1 = f0x1, with two such morphisms f0 and g0 being equivalent if there exists a morphism e from X0 to Y1 such that y0e = f0 and y1e = g0.