Graphs in a regular category

Question

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.

Answer 1

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.