also subtraction.

-   the *adjunction property* holds if whenever $\phi\colon A\rat B$ is a mono, then

    -   $\mathcal{A}_\phi\colon \mathcal{A}(A)\to \mathcal{A}(B)$ has a right adjoint $\mathit{red}_\phi\colon \mathcal{A}(B)\to \mathcal{A}(A)$, i.e., $\mathit{red}_\phi$ is monotone and satisfies $a \le \mathit{red}_\phi(\mathcal{A}_\phi(a))$ for $a\in \mathcal{A}(A)$ and $\mathcal{A}_\phi(\mathit{red}_\phi(b))\le b$ for $b\in \mathcal{A}(B)$.

    -   $\mathit{red}_\phi$ is a monoid homomorphism that preserves subtraction.

    -   it holds that $\mathit{red}_\phi(s_B) = s_A$, where $s_A,s_B$ are standard annotations.

Furthermore, assuming that $\mathcal{A}_\phi$ has a right adjoint $\mathit{red}_\phi$, we say that

-   the *pushout property* holds, whenever for each pushout as shown in the diagram to the right, with all arrows monos where $\eta = \psi_1 \circ \phi_1 = \psi_2 \circ \phi_2$, it holds that for every $d\in \mathcal{A}(D)$: $$d = \mathcal{A}_{\psi_1}(\mathit{red}_{\psi_1}(d)) +
            (\mathcal{A}_{\psi_2}(\mathit{red}_{\psi_2}(d)) -
            \mathcal{A}_{\eta}(\mathit{red}_{\eta}(d))).$$

    $$\xymatrix{ A \ar@{>->}[r]^{\phi_2} \ar@{>.>}[dr]_{\eta}
              \ar@{>->}[d]_{\phi_1} & C
              \ar@{>->}[d]^{\psi_2} \\
              B \ar@{>->}[r]_{\psi_1} & D }$$  

    We say that the *pushout property for standard annotations* holds if we replace $d$ by $s_D$, $\mathit{red}_\eta(d)$ by $s_A$, $\mathit{red}_{\psi_1}(d)$ by $s_B$ and $\mathit{red}_{\psi_2}(d)$ by $s_C$.

-   the *Beck-Chevalley property* holds if whenever the square shown to the right is a pullback with $\phi_1$, $\psi_2$ mono, then it holds for every $b\in\mathcal{A}(B)$ that $$\mathcal{A}_{\phi_2}(\mathit{red}_{\phi_1}(b)) =
          \mathit{red}_{\psi_2}(\mathcal{A}_{\psi_1}(b)).$$

    $$\xymatrix{
              A \ar[r]^{\phi_2} \ar@{>->}[d]_{\phi_1} & C \ar@{>->}[d]^{\psi_2} 