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.
Construction.
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". 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"0 and "X"1 and two parallel morphisms "x"0 and "x"1 from "X"1 to "X"0 such that there exist a reflexivity morphism "r" from "X"0 to "X"1 such that "x"0"r" = "x"1"r" = 1"X"0; a symmetry morphism "s" from "X"1 to itself such that "x"0"s" = "x"1 and "x"1"s" = "x"0; and a transitivity morphism "t" from "X"1 × "x"1, "X"0, "x"0 "X"1 to "X"1 such that "x"0"t" = "x"0"p" and "x"1"t" = "x"1"q", where "p" and "q" are the two projections of the aforementioned pullback. A morphism from ("X"0, "X"1, "x"0, "x"1) to ("Y"0, "Y"1, "y"0, "y"1) in "C""ex" is given by an equivalence class of morphisms "f"0 from "X"0 to "Y"0 such that there exists a morphism "f"1 from "X"1 to "Y"1 such that "y"0"f"1 = "f"0"x"0 and "y"1"f"1 = "f"0"x"1, with two such morphisms "f"0 and "g"0 being equivalent if there exists a morphism "e" from "X"0 to "Y"1 such that "y"0"e" = "f"0 and "y"1"e" = "g"0.