Coherent topology (source code)

= Coherent topology
{title2=$J_{\rm coh}$}

The coherent topology on a small <coherent category> is generated by finite families of arrows whose image subobjects have union equal to the whole target. Pullback stability of images and unions and closure under composition make these a coverage. On a <coherent syntactic category>, this is the site topology used to construct the <classifying topos> of its <coherent theory>.