Pretopos completion sends every coherent category into a pretopos, called its pretopos completion; the operation is idempotent. It is a “higher-ary” version of the exact completion of a regular category.
More generally, pretoposes form a full reflective sub-2-category of the 2-category of finitary sites, which in turn includes coherent categories (with their coherent topologies) as a full sub-2-category.
According to the observation of Mihály Makkai from around 1980, the pretopos completion of the syntactic category of a first-order theory corresponds to the operation invented by Saharon Shelah. is a universal extension of which admits elimination of imaginaries.
For any an arity class , there is a corresponding version of -pretopos completion; see (Shulman). The version for is the exact completion, while classical pretopos completion is the version for . The version for the size of the universe includes the topos of sheaves.
Panagis Karazeris, Notions of flatness relative to a Grothendieck topology,
Mihály Makkai, G. E. Reyes, First order categorical logic, Lecture Notes in Math. 611, Springer 1977
David Ballard, William Boshuck, Definability and descent, The Journal of Symbolic Logic 63:2 (Jun., 1998), pp. 372-378, jstor
Victor Harnik, Model theory vs. categorical logic: two approaches to pretopos completion (a.k.a. ), in: Models, logics, and higher-dimensional categories, 79–106 (Makkai volume), CRM Proc. Lecture Notes 53, Amer. Math. Soc. 2011; gBooks
Saharon Shelah, Classification theory and the number of non-isomorphic models, Studies in Logic and the Foundations of Mathematics 92, North Holland, Amsterdam 1978