10. $\cate{Sub}$-exact squares and relational calculus [0034]
Many classes $E$ of squares are built starting from a pseudo-functor $S : C^\op\to\Cat$ such that, for each object $X$ in $C$ the category $SX$ is a “category of formal subobjects” of $X$. We define, then, $E_S\subseteq C^\square$ to be the set of commutative squares whose image under $S$ ie exact (i.e. it is “anticommutative” in $\Prof\supseteq\Cat$).
In particular, if $S=\cate{Sub}$ is precisely the subobject functor $C^\op\to\Cat$, where $\cate{Sub}(X)$ is the category (=poset) of subobjects of $X$, the resulting theory of relations $Re(E_\cate{Sub})$ is the calculus of functors between $\cate{Sub}(X), \cate{Sub}(Y)$ that are representable by a path in $C$.
If to every path $c$ we associate the projective limit of $c$ regarded as a diagram, we determine, provided all pullback squares are counted as exact, a representation of relations via spans; if $C$ doesn’t have projective limits we can always consider the limit in the category $\widehat{C}=\Set^{C^\op}$ so that $\varprojlim : \Ch(C) \to\Span(\widehat C).$