Abstract

Conceptual completeness for coherent categories (due to M. Makkai and G. Reyes) says that if a coherent functor F: C → D induces an equivalence COH → COH between their categories of Set-valued models, then the induced functor P(F): P© → P(D) between the associated pretoposes is an equivalence. Their arguments are model-theoretic (involving compactness and the method of diagrams). Later A. Pitts gave a constructive version of that theorem, allowing models in (an adequate class of) toposes (and relaxing the notion of equivalence to mean fully faithful and essentially surjective on objects). A similar result by Makkai for regular logic says that if a regular functor F: C → D induces an equivalence REG → REG , then the induced E(F): E© → E(D) between the respective effectivizations of the regular categories is an equivalence. The latter comes as a corollary to a more general duality result of his that, again, uses model-theoretic methods. We exploit the result of Pitts, along with a (seemingly) hitherto unnoticed property of effectivization, to give a direct and constructive proof of that result of Makkai.