The idea of working in additive categories with exact squares instead of exact sequences dates back to Lambek, Mac Lane, Puppe, and a large part of what can be done is exposed in Hilton (Hilton, 1966). About te use of exact squares in non-additive categories, and the relation with the problem of embedding the ambient category in various categories with involution, we advise the reader to consult (Grandis, 1977) or other references (for example Čalenko and Conte).

The advantage of this point of view lies in the following key observation: we can obtain the composition of two relations-spans $A\leftarrow X\to B$ and $B\leftarrow Y\to C$ as follows: where $*$ is any exact square (see (Guitart, 1975), p. 35 and (Guitart, 1982), p 22). As a consequence, the study of formation laws for exact squares in a category of the form $\Set^{C^\op}$ allows to understand the calculus of relations of $\Set^{C^\op}$ and as a consequence the deductive logic of this topos.

However, since we know that the logics of categories like $\Set^{C^\op}$ “are” the natural semantics for intuitionistic logic, we see that the method of exact squares is, in fact, larger than intuitionism. Intuitionism is, in some sense, the discrete or 1-dimensional part of fibered exact logic introduced in (Guitart, 1982) as a principal part of categorical logic. Fibered exact logic in a category $C$ is the study of formation laws of exact squares in the 2-categories $\Cat^{C^\op}$, $\Fib(C)$, $\underline{D}(C)$, $\Cat/C$,… (the second principal part of categorical logic on $C$ is the study of fibered monads on $C$, i.e. of monads in $\Cat^{C^\op}$, $\Fib(C)$, $\underline{D}(C)$, $\Cat/C$,…)