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 C<sub>ex</sub>) has for its objects pseudo-equivalence relations in C. A pseudo-equivalence relation is like an equivalence relation except that it need not be jointly monic. An object in C<sub>ex</sub> thus consists of two objects X<sub>0</sub> and X<sub>1</sub> and two parallel morphisms x<sub>0</sub> and x<sub>1</sub> from X<sub>1</sub> to X<sub>0</sub> such that there exist a reflexivity morphism r from X<sub>0</sub> to X<sub>1</sub> such that x<sub>0</sub>r = x<sub>1</sub>r = 1<sub>X<sub>0</sub></sub>; a symmetry morphism s from X<sub>1</sub> to itself such that x<sub>0</sub>s = x<sub>1</sub> and x<sub>1</sub>s = x<sub>0</sub>; and a transitivity morphism t from X<sub>1</sub> ÃÂ <sub>x<sub>1</sub>, X<sub>0</sub>, x<sub>0</sub></sub> X<sub>1</sub> to X<sub>1</sub> such that x<sub>0</sub>t = x<sub>0</sub>p and x<sub>1</sub>t = x<sub>1</sub>q, where p and q are the two projections of the aforementioned pullback. A morphism from (X<sub>0</sub>, X<sub>1</sub>, x<sub>0</sub>, x<sub>1</sub>) to (Y<sub>0</sub>, Y<sub>1</sub>, y<sub>0</sub>, y<sub>1</sub>) in C<sub>ex</sub> is given by an equivalence class of morphisms f<sub>0</sub> from X<sub>0</sub> to Y<sub>0</sub> such that there exists a morphism f<sub>1</sub> from X<sub>1</sub> to Y<sub>1</sub> such that y<sub>0</sub>f<sub>1</sub> = f<sub>0</sub>x<sub>0</sub> and y<sub>1</sub>f<sub>1</sub> = f<sub>0</sub>x<sub>1</sub>, with two such morphisms f<sub>0</sub> and g<sub>0</sub> being equivalent if there exists a morphism e from X<sub>0</sub> to Y<sub>1</sub> such that y<sub>0</sub>e = f<sub>0</sub> and y<sub>1</sub>e = g<sub>0</sub>.