I am starting to learn about regular categorical logic as an application of what we learned in class about regular categories. After reading through the definitions of the representation of terms, formulas, etc. I am trying to understand a simple proposition:
Let $f:S\rightarrow T$ be a function symbol and $S,T$ sorts of a many-sorted logic $L$.
$f(x^s)=f(y^s)\vdash_{x^s,y^s}x^s=y^s$ is true iff $[f]$ is mono.
I am unable to prove this. This I simply explicitly wrote down the definitions involved and tried to relate them to the conclusion, but with no success: (I'll write $x$ and $y$ omitting the superscript $s$)
Calling $\phi$ the left side of the sequent, we know that the representation of $\phi$ in our regular category is the subobject of $[FV(\phi)]=[(x,y)]=[S]\times [S]$ represented by the equalizer of the following equalizer diagram:
$$ [\phi]\rightarrow[S]\times[S]\underset{[f(y)]p_2}{\overset{[f(x)]p_1}{\rightrightarrows}}[S] $$
Similarly, calling $\psi$ the right side of the sequent:
$$ [\psi]\rightarrow[S]\times[S]\underset{p_2}{\overset{p_1}{\rightrightarrows}}[S] $$
Now, the sequent $\phi\vdash_{x,y}\psi$ is true iff $p^*_\phi([\phi])\le p^*_\psi([\psi])$, i.e $p^*_\phi([\phi])$ factors trough $p^*_\psi([\psi])$. I wrote down the diagrams associated with these pullbacks and tried to play with what I get from them to extract information about $[f]$, but couldn't. Any hints would be appreciated.
Consider the following diagram:
where $p_i$ is the projection onto the $i$th co-ordinate, $e_1$ is the equalizer of $p_1$ and $p_2$, and $e_2$ is the equalizer of $[f]p_1$ and $[f]p_2$.
Suppose first that $[f]$ is a monomorphism. Since $e_2$ equalizes $[f]p_1$ and $[f]p_2$ we have that $[f]p_1e_2 = [f]p_2e_2$ and so $p_1e_2 = p_2e_2$ as $[f]$ is mono. Therefore $e_2$ equalizes $p_1$ and $p_2$, so it factors through $e_1$ by the universal property of the equalizer $e_1$; hence $\ [(x, y) : f(x) = f(y)] \leq [(x, y) : x = y ]$ as subobjects of $[S] \times [S]$, so $\left( f(x) = f(y)\right) \vdash_{x,y} \left(x=y\right)$ is true in our regular category.
Conversely, suppose that $\left( f(x) = f(y)\right) \vdash_{x,y} \left(x=y\right)$ holds in our regular category, so that $e_2$ factors through $e_1$, and let $g, h : R \rightrightarrows [S]$ be two parallel arrows such that $[f]g = [f]h$. Then the arrow $\langle g,h \rangle : R \to [S] \times [S]$ equalizes $[f]p_1$ and $[f]p_2$, so by the universal property of the equalizer $e_2$, $\langle g,h\rangle$ factorises through $e_2$. An easy diagram chase now shows that $g=h$, since both $g$ and $h$ factor through $e_1$ and $e_1$ equalises $p_1$ and $p_2$.