自由格函子弱保持满射拉回

设$p(x,y,z)$与$q(x,y,z)$为项。若存在公共“祖先”项$s(z_{1},z_{2},z_{3},z_{4})$，通过识别某些变量分别特化为$p$与$q$\begin{align*} p(x,y,z) & \approx s(x,y,z,z)\\ q(x,y,z) & \approx s(x,x,y,z), \end{align*}则方程$$p(x,x,z)\approx q(x,z,z)$$可由$s(x,y,z,z)$与$s(x,x,y,z)$的语法合一平凡得到。在本注记中我们证明，对格项，更一般地对格序代数的项，其逆亦真。给定项$p,q$及方程\begin{equation} p(u_{1},\ldots,u_{m})\approx q(v_{1},\ldots,v_{n})\label{eq:p_eq_q} \end{equation}其中$\{u_{1},\ldots,u_{m}\}=\{v_{1},\ldots,v_{n}\}$，总存在“祖先项”$s(z_{1},\ldots,z_{r})$使得$p(x_{1},\ldots,x_{m})$与$q(y_{1},\ldots,y_{n})$作为$s$的代换实例，其合一给出原方程。在范畴论术语中，上述命题限于格时有更简洁的表述：自由格函子弱保持满射的拉回。