In fact, exact modifications are “strict” proofs in the sense that if, in an ordinary proof/derivation $H \to A \to B\to C \to\dots\to T$ we agree to repeat at each step the preceding assumptions in the conclusion, we obtain a chain of equivalences of exact modifications of $H$:

Working inside an object of the form $PZ$, this means avoiding to use $A\subseteq B$ and replace it with $A\cup B=B$ or equivalently $A\cap B=A$.

If now the relations are paths, using exact squares we can define what it means $R\iff S$ or $R\To T$: in this last situation, it must exist $Q$ such that $R\lor Q\iff T$. But it is unclear how to define $\lor$: this boils down to define $\To$. And consequently, one defines $R\iff S$ by $R\To S$ and $S\To R$.

This leads to the concept of a deductive square, standing in the same relation $\To$ stands to $\iff$, as I define them in §13.