For every P,Q,x:P→X,y:Q→Y we consider the diagram
of comma objects, where x▽φy is a strict pullback, and x▼y:x▽φy→Ux↓Vy [the dotted arrow, TN] is the functor induced by the universal property of said comma object.
If π0(x▼y) is a bijection we say that φ is exact at (xy) and we write (xy)⊨φ. So, φ exact equals the following condition (π0▽): for all P,Q,x:P→X,y:Q→Y, we have (xy)⊨φ.
The proof is by inspection of the strict pullback x▽φy and of the functor x▼y; x▽φy is the subcategory of the product on objects of the form {p,a,q∣XpTa→fg→SaYq}, and x▼y is defined sending such an object to {p,q∣UXpVTa→f↙g→USaVYq}.