A coherent category has finite limits, pullback-stable regular-epi/mono image factorizations, and finite unions of subobjects stable under pullback. Each subobject lattice is distributive. These structures interpret all constructors of coherent logic.
New to topics? Read the docs here!