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_ex) 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 C_ex thus consists of two objects X₀ and X₁ and two parallel morphisms x₀ and x₁ from X₁ to X₀ such that there exist a reflexivity morphism r from X₀ to X₁ such that x₀r = x₁r = 1_X0; a symmetry morphism s from X₁ to itself such that x₀s = x₁ and x₁s = x₀; and a transitivity morphism t from X₁ × _{x1, X0, x0} X₁ to X₁ such that x₀t = x₀p and x₁t = x₁q, where p and q are the two projections of the aforementioned pullback. A morphism from (X₀, X₁, x₀, x₁) to (Y₀, Y₁, y₀, y₁) in C_ex is given by an equivalence class of morphisms f₀ from X₀ to Y₀ such that there exists a morphism f₁ from X₁ to Y₁ such that y₀f₁ = f₀x₀ and y₁f₁ = f₀x₁, with two such morphisms f₀ and g₀ being equivalent if there exists a morphism e from X₀ to Y₁ such that y₀e = f₀ and y₁e = g₀.

• If the axiom of choice holds, then Set_ex is equivalent to Set.
• More generally, let C be a small category with finite limits. Then the category of presheaves Set^Cop is equivalent to the exact completion of the coproduct completion of C.^[2]
• The effective topos is the exact completion of the category of assemblies.^[2]

• If C is an additive category, then C_ex is an abelian category.^[3]
• If C is cartesian closed or locally cartesian closed, then so is C_ex.^[4]

• setoid

• Shulman, Michael. "The derivator of setoids." arXiv preprint arXiv:2105.08152 (2021). [1]

• Exact completion at the nLab