I have read a lecture note by Jaap van Oosten and I am stuck on the exercise 84 in the article.
A functor between two regular categories is regular if it preserves finite limits and regular epimorphisms.
For a regular category $\mathcal{E}$ and $T$ a theory, show that a regular functor $\mathcal{C}(T)\to \mathcal{E}$ gives an interpretation which makes all sequents in $T$ true.
Conversely, show that any interpretation of $T$ in $\mathcal{E}$ arises the unique (up to natural isomorphism) regular functor $\mathcal{C}(T)\to\mathcal{E}$ with the property that it maps the standard interpretation of $T$ in $\mathcal{C}(T)$ to the given one in $\mathcal{E}$.
Proving converse in detail comes hard to me. The problem is how to define a functor on a set of arrows of $\mathcal{C}(T)$, since the standard interpretation merely interpret $\chi$ as an object, not a function. Thus I need to find an arrow corrsponding to $[\chi]$ in $\mathcal{E}$.
My attempt is as follows: for an interpretation $[\![\cdot]\!]_\mathcal{E}$ of $T$ in $\mathcal{E}$ and an arrow $[\chi(x,y)]:\varphi(x)\to\psi(y)$ in $\mathcal{C}(T)$, find the arrow $\phi : [\![\varphi]\!]_\mathcal{E} \to [\![\chi]\!]_\mathcal{E}$ (and I guess that it is an isomorphism.) Intuitively, $\phi$ sends an element of a domain to the pair $(x,f(x))$ of the graph. Now the consider the composition $$[\![\varphi]\!]_\mathcal{E}\overset{\phi}{\longrightarrow}[\![\chi]\!]_\mathcal{E}\hookrightarrow [\![\varphi]\!]_\mathcal{E}\times [\![\psi]\!]_\mathcal{E} \twoheadrightarrow [\![\psi]\!]_\mathcal{E}.$$
(An injection at the middle exists, because the sequent $\chi(x,y)\vdash_{x,y} \varphi(x)\land \psi(y)$ is in $T$.)
The problem is that I don't know how to find $\phi$. I would appreciate your help, thanks!
An arrow of $\mathcal{C}(T)$, $[\chi(x,y)] : \varphi(x) \to \psi(y)$ is a(n equivalence class of) formula(s) $\chi(x,y)$ from a formula $\varphi(x)$ to a formula $\psi(y)$. An interpretation of $T$ interprets all of these as subobjects, that is (equivalence classes of) monomorphisms (Definition 4.7). Let's say $x$ has sort $X$ and $y$ has sort $Y$. Then $[\![\varphi(x)]\!] : [\![\varphi(x)]\!] \hookrightarrow [\![X]\!]$, $[\![\psi(y)]\!] : [\![\psi(y)]\!] \hookrightarrow [\![Y]\!]$, and $[\![\chi(x,y)]\!] : [\![\chi(x,y)]\!] \hookrightarrow [\![X\times Y]\!]$. Definition 4.8 explaining what it means for a labelled sequent to hold for an interpretation lets us use the sequents defining $\chi$ as a functional relation.
As you've pointed out, the first condition lets us factor the subobject $[\![\chi(x,y)]\!]$ giving $[\![\chi(x,y)]\!]\hookrightarrow [\![\varphi(x)\land\psi(y)]\!]\hookrightarrow [\![\varphi(x)]\!]\times[\![\psi(y)]\!]$. The third condition gives a subobject $[\![\varphi(x)]\!]\hookrightarrow[\![\exists y.\chi(x,y)]\!]$. Now you could use the image operation to interpret this existential, but using the second condition which ensures that there's at most one such $y$ we see that we really have $\exists! y$, that is, "there exists a unique $y$". It turns out this sort of existential can sometimes be interpreted as just a pullback meaning that this definition of $\mathcal{C}(T)$ would work just as well for categories with only finite limits. In particular, you can show that $\pi_1 \circ [\![\chi(x,y)]\!]$ is a monomorphism and is reasonably interpreted as $[\![\exists y.\chi(x,y)]\!]$ assuming we (internally) know that $y$ is unique. Another way to put it is, under these assumptions, an image exists for this morphism even if images don't exist in general. At any rate, the factorization of $[\![\exists y.\chi(x,y)]\!]$ leads to $[\![\varphi(x)]\!]\hookrightarrow[\![\chi(x,y)]\!]\hookrightarrow[\![\varphi(x)]\!]\times[\![\psi(y)]\!]\to[\![\psi(y)]\!]$.