A functor between coherent categories is coherent when it preserves finite limits, image factorizations and finite unions of subobjects, including the empty union. It consequently preserves the interpretation of every coherent formula. A coherent functor from a coherent syntactic category to a topos is equivalent to a model of the corresponding coherent theory; natural transformations correspond to ordinary model homomorphisms.
New to topics? Read the docs here!