A property of effectivization and its uses in categorical logic

Vasileios Aravantinos-Sotiropoulos and Panagis Karazeris

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.

http://www.tac.mta.ca/tac/volumes/32/22/32-22.pdf

TAC Home