In the positive finite-limit convention, a Horn theory uses atomic finite-conjunction sequents; uniquely witnessed existential extensions remain Cartesian. Its models are the finite-limit-preserving functors out of its Cartesian syntactic category. This convention does not insert arbitrary existential witnesses or falsity as Cartesian constructors. Its classifier is the presheaf classifier of a Horn theory.
New to topics? Read the docs here!