Question about Lemma D1.4.4(iii) in the Elephant - possible typo?

Question

Given a morphism $[\theta] \colon \lbrace \bar{x}.\phi \rbrace \rightarrow \lbrace \bar{y}. \psi \rbrace$ in the syntactic category $\mathcal{C}_{\mathbb{T}}$ of a (cartesian) theory, we are told, in the proof of D1.4.4(iii), that the kernel pair of $[\theta]$ is the object $\lbrace \bar{x}, \bar{x'}. \theta \wedge \theta[\bar{x'}/\bar{x}] \rbrace$.

However, $\bar{x}, \bar{x'}$ is not a suitable context for $\theta \wedge \theta[\bar{x'}/\bar{x}]$ since the free variables of $\theta$ also include $\bar{y}$. So as far as my understanding goes this is not a well-formed object of $\mathcal{C}_{\mathbb{T}}$.

Is this a typo? Is the formula for the kernel pair correct, but $\bar{y}$ should be added to the context? Or is the formula wrong and it should be instead $\phi \wedge \phi[\bar{x'}/\bar{x}]$ with the context as is? Or is it all correct and I'm missing something?

Also, if it's not too much trouble could someone actually write down explicitly the diagonal map referred to in the proof, since my understanding of syntactic categories gives me little confidence that I can write these things down accurately? Is the idea of the proof that $[\theta]$ is a mono iff the diagonal is an iso iff (by (i) the diagonal is functional in both directions iff the sequent stated in (iii) holds?

Answer 1

1. The (underlying object of the) kernel pair is $\{ \bar{x}', \bar{x}'', y . \theta[\bar{x}'' / \bar{x}] \land \theta [\bar{x}' / \bar{x}] \}$.
2. The diagonal morphism $\{ \bar{x} . \phi \} \to \{ \bar{x}', \bar{x}'', y . \theta[\bar{x}'' / \bar{x}] \land \theta [\bar{x}' / \bar{x}] \}$ is given by $[ \theta \land \bar{x} = \bar{x}' \land \bar{x} = \bar{x}'' ]$.

It's best not to worry too much about the details about syntactic categories: otherwise one gets bogged down with all kinds of obvious but tedious details like renaming variables and checking contexts and so on.