Graphs in a regular category Let $\mathcal{C}$ be a regular category, and let $X,Y,Z\in Ob(\mathcal{C})$. Let $g:Z\to Y$ be a regular epi, and let $R\in Sub(X\times Y)$ (subobjects of $X\times Y$). Define $S:=(id_X\times g)^\ast(R)\in Sub(X\times Z)$, and assume that the sequents
\begin{align}
\vdash_x\exists zS(x,z) \\
S(x,z)\wedge S(x,z^\prime)\vdash_{x,z,z^\prime}z=z^\prime
\end{align}
are true.
I am trying to prove that there is an arrow $f:X\to Y$ such that $R$ is the graph of $f$ (i.e. the subobject of $X\times Y$ represented by $\left<id_X,f\right>$). I am a little bit lost. I am informally reading the two sequents as "for all $x\in X$, there exists $z\in Z$ such that $(x,z)\in Z$" (which of course makes no sense in general), and the second sequent then adds that this $z$ is unique. In http://www.brics.dk/LS/98/2/BRICS-LS-98-2.pdf this file, which I am reading alongside, there is a Lemma 2.8 on page 9 which is very similar to my statement, but this proof is also very unclear to me. If someone could provide some hints/explanation/whatever, that would be very much appreciated.
Edit: some explanation on what these sequents actually mean would already be helpful.
Edit1:
Let $\pi_X:X\times Z\to X$ and $\pi_Z:X\times Z\to Z$ be the projections. Let $r:R_0\to X\times Y$ represent $R$, and let $s:S_0\to X\times Z$ represent $S$. Then the pullback diagram (which exists because $\mathcal{C}$ is regular?)
$\require{AMScd}$
\begin{CD}
    S_0\times_XS_0 @>p_2>> S_0\\
    @V p_1 V V @VV \pi_Xs V\\
    S_0 @>>\pi_Xs> X
\end{CD}
has a coequalizer (because $\mathcal{C}$ is regular!), and apparently the coequalizer is $\pi_Xr$ itself, because of the first sequent (but I do not see this).
Edit2: for the category Set:
Let $X,Y,Z$ be sets, let $g:Z\to Y$ be a surjective function, and $R$ a subset of $X\times Y$. Consider $S=(id\times g)^{-1}(R)\subset X\times Z$. We need to find a function $f:X\to Y$ such that $R=graph(f)$, assuming that for all $x\in X$ there exists a unique $z\in Z$ such that $(x,z)\in S$. Well define $f:X\to Y$ be sending $x$ to $g(z)$. Well-defined by the existence-unicity condition, and clearly $R=graph(f)$, since $g$ is surjective.
 A: Logic: Let $R:X\looparrowright Y$ and $Q:Z\looparrowright Y$ be binary relations. Suppose that $Q$ is surjective and functional:
$$\begin{align}\top&\vdash_{y:Y}\exists_{z:Z}Q(y,z)\\
Q(y,z)\land Q(y',z)&\vdash_{y,y':Y;z:Z}y=y'\text{.}
\end{align}$$
Let $S:X\looparrowright Z$ be the binary relation
$$S(z,x)\equiv \exists_{y:Y}(Q(y,z)\land R(y,x))\text{.}$$
Suppose that $S$ is total and functional:
$$\begin{align}\top &\vdash_{x:X}\exists_{z:Z}S(z,x)\\
S(z,x)\land S(z',x)&\vdash_{x:X;z,z':Z}z=z'\text{.}
\end{align}$$
Then you need to prove that $R$ is total and functional using only the deduction rules allowed in regular logic:
$$\begin{align}
\top&\vdash_{x:X}\exists_{y:Y}R(y,x)\\
R(y,x)\land R(y',x)&\vdash_{x:X;y,y':Y}y=y'\text{.}
\end{align}$$
Basically, this amounts to careful bookkeeping of the usual proof in $\mathbf{Set}$.
Semantics: Interpret


*

*each side of each sequent (i.e., proposition or formula) as a subobject (e.g., $Q(x,y)$ as a subobject of $X\times Y$),

*each sequent as an inequality between subobjects (e.g., $\top \vdash_{x:X}\exists_{z:Z}S(z,x)$ as "the direct image of the subobject of $X\times Z$ interpreting $S$ under the projection onto $X$ is the largest subobject of $X$"), and

*each derivation rule in the sequent calculus as a lemma about inequalities between subobjects of objects in regular categories (e.g., $\exists$-introduction and $\exists$-elimination as the adjunction between pullback and taking direct images). 


Then you'll have a statement and proof of the following:

Let $Q$ be a subobject of $Z\times Y$, and let $R$ be a subobject of $X\times Y$. Let $S$ be the subobject of $X\times Z$ given by the pullback of the tabulations of $Q$ and $R$. Suppose that
  
  
*
  
*the direct image of $S$ under the projection onto $X$ is $1_X$,
  
*the direct image of $Q$ under the projection onto $Y$ is $1_Y$,
  
*the canonical map $S\times_X S\to Z\times Z\times X$ factors through $(\delta_Z,1_X)$,
  
*and $Q\times_Z Q\to Y\times Y\times Z$ factor through $(\delta_Y,1_Z)$.
  
  
  Then
  
  
*
  
*the direct image of $R$ under projection onto $X$ is $1_X$, and
  
*the canonical map $R\times_X R\to Y\times Y\times X$ factors through $(\delta_Y,1_X)$.
  

From there, you should be able to apply Lemma 2.8.
