The fact that $\vf$ is exact is equivalent, through ZZ, to a condition LI of local initiality or to a condition LF of local finality:
- (local initiality) $x\in X_0$, $x\downarrow S \to Ux\downarrow V$ is initial [this is the functor sending $(x\to Sa)$ into $(Ux \to USa \xto{\vf} VTa)$, TN];
- (local finality) $y\in Y_0$, $T\downarrow y \to U\downarrow Vy$ is final [this is the functor sending $(Ta\to y)$ into $(USa \xto{\vf} VTa \to Vy)$, TN].
For every $P,Q, x : P \to X, y : Q \to Y$ we consider the diagram of comma objects, where $x \tdown_\vf y$ is a strict pullback, and $x\btdown y : x \tdown_\vf y \to Ux\downarrow Vy$ [the dotted arrow, TN] is the functor induced by the universal property of said comma object.
If $\pi_0(x\btdown y)$ is a bijection we say that $\vf$ is exact at $\smat{x \\ y}$ and we write $\smat{x \\ y}\vDash \vf$. So, $\vf$ exact equals the following condition ($\pi_0\tdown$): for all $P,Q, x : P \to X, y : Q \to Y$, we have $\smat{x \\ y}\vDash\vf$.
The proof is by inspection of the strict pullback $x \tdown_\vf y$ and of the functor $x\btdown y$; $x \tdown_\vf y$ is the subcategory of the product on objects of the form $\left\{ p,a,q \mid \nbsmat{ Xp &\overset{f}\to& Sa \\ Ta &\underset{g}\to& Yq } \right\}$, and $x\btdown y$ is defined sending such an object to $\left\{ p,q \mid \nbsmat{UXp &\overset{f}\to& USa \\ &\swarrow&\\ VTa &\underset{g}\to& VYq } \right\}$.