We show that a fully faithful and covering regular functor between regular categories induces a fully faithful (and covering) functor between their respective effectivizations. Such a functor between effective categories is known to be an equivalence. We exploit this result in order to give a constructive proof of conceptual completeness for regular logic. We also use it in analyzing what it means for a morphism between effective categories to be a quotient in the 2-category of effective categories and regular functors between them.
Keywords: regular category, effectivization, pretopos, conceptual completeness, quotient
2010 MSC: 18C20, 18F20, 03G30
Theory and Applications of Categories, Vol. 32, 2017, No. 22, pp 769-779.
Published 2017-07-25.
TAC Home