I have a question about Johnstone's proof (in either Topos Theory or the Elephant; the accounts are essentially the same, so far as I can tell) that internal equivalence relations in a topos are effective. In particular, I don't yet see why (for $\overline{\phi}$ the exponential transpose of the classifying map $\phi: X \times X \to \Omega$ for the equivalence relation $ R \overset{(a,b)}{\hookrightarrow} X \times X$) the diagram $$ R \overset{a}{\underset{b}{\rightrightarrows}} X \overset{\overline{\phi}}{\to} \Omega^X$$ commutes. Johnstone claims that that subobjects $S_a$ and $S_b$ classified by $\phi(a \times X)$ and $\phi(b \times X)$ are both isomorphic to "the object of $R$-related triples" $T$, which is just the pullback of $R \overset{a}{\to} X$ and $R \overset{b}{\to} X$. In the Elephant, these two squares are claimed to be pullbacks (where $A$ takes the place of $X$, $t$ witnesses transitivity, and $p$ and $q$ are the projections from $T$):
I agree that they commute and that if they are pullbacks, the conclusion follows. How does one see that they are pullbacks? And where exactly do internal symmetry and transitivity come into play when showing this?
A complete and very lucid account is given in Borceux's Handbook of Categorical Algebra, volume 3, 5.9.6, some parts of which I'll use to answer this question.
Notion 1. An internal equivalence relation on an object $X$ of a finitely complete category $\mathbf{C}$ is a pair of maps $R \overset{a}{\underset{b}{\rightrightarrows}} X$ such that:
$R \overset{(a,b)}{\to} X$ is mono.
The diagonal map $X \overset{\Delta}{\to} X \times X$ factors through $(a,b)$.
There exists a map $s: R \to R$ such that $as = b$ and $bs = a$.
There exists a map $t : R \times_X R \to R$ such that for the projections $a', b'$ in the pullback square $$\require{AMScd} \begin{CD} R \times_X R @>a'>> R \\ @Vb'VV @VaVV\\ R@> \hspace{10mm}b \hspace{10mm}>>X\end{CD}$$
$at = ab'$ and $bt = ba'$.
Notion 2. An internal equivalence relation on an object $X$ of a finitely complete category $\mathbf{C}$ is a pair of maps $R \overset{a}{\underset{b}{\rightrightarrows}} X$ such that for each object $U \in \mathbf{C}$, the induced relation $$R_U \overset{\operatorname{df}}{=} \big\{(af,bf) \operatorname{ | } f \in \operatorname{Hom}_{\mathbf{C}}(U,R)\big\}$$ on $\operatorname{Hom}_{\mathbf{C}}(U,X)$ is an equivalence relation in the usual sense.
Proposition 1. The two notions of an internal equivalence relation given above are equivalent.
Proof. Denote the fiber product $R \times_X R$ by $a \times b$. Reflexivity: if $(R,a,b)$ is an ER in the sense of Notion 2, then $\left(\operatorname{id}_X, \operatorname{id}_X)\right) \in R_X$. This means there must exist some $r : X \to R$ which is a section to both $a$ and $b$. Writing out the diagram, one sees that by the uniqueness of cone maps to a limit, $\Delta : X \to X \times X$ factors into $(a,b) \circ r$.
If $(R,a,b)$ is an ER in the sense of Notion 1, then for any $f : U \to X$, $$U \overset{f}{\to} X \overset{r}{\to} R \overset{a}{\underset{b}{\rightrightarrows}} X$$ witnesses that $(f,f) \in R_U$.
Symmetry: similarly, if $(R,a,b)$ is an ER in the sense of Notion 2, then symmetry of $R_R$ implies that $(a,b)$ and $(b,a)$ are in $R_R$, so that in particular there exists some $s : R \to R$ such that $as = b$ and $bs = a$, satisfying Notion 1.
If $(R,a,b)$ is an ER in the sense of Notion 1, then for any $f: U \to R$ which becomes $(a \circ f, b \circ f)$ in $R_U$, $$U \overset{f}{\to} R \overset{s}{\to} R$$ becomes $(b \circ f, a \circ f)$ in $R_U$.
Transitivity: Now we must use the finite completeness of $\mathbf{C}$. (In Borceux, it's shown that we can weaken finite completeness to just the existence of pullbacks of strong epimorphisms.) If $(R, a,b)$ is an ER in the sense of Notion 2, consider the diagrams $$a \times b \overset{a'}{\to} R \overset{a}{\underset{b}{\rightrightarrows}} X$$ and $$a \times b \overset{b'}{\to} R \overset{a}{\underset{b}{\rightrightarrows}} X,$$ which tell us that $(aa',ba')$ and $(ab',bb')$ are in $R_{a \times b}$. By definition, $aa' = bb'$, so by the transitivity of $R_{a \times b}$, $(ba', ab') \in R_{a \times b}$, which must be witnessed by some $t$ satisfying the requirements of Notion 1.
On the other hand, if $(R,a,b)$ is an ER in the sense of Notion 1, and we have $f,g : U \to R$ such that $(af, bf)$ and $(ag,bg)$ are in $R_U$, with $bf = ag$, then we can form the commutative diagram
where $u$ is the unique cone map into $a \times b$. Forming $$U \overset{u}{\to} a \times b \overset{t}{\to} R \overset{a}{\underset{b}{\rightrightarrows}} X$$ yields $(ab'u, ba'u) = (af,bf) \in R_U$, so $(R,a,b)$ is transitive in the sense of Notion 2, as required. $\square$
Now we can show:
Proposition 2. The diagram $$R \overset{a}{\underset{b}{\rightrightarrows}} X \overset{\overline{\phi}}{\to} \Omega^X$$ as in the above question commutes.
Proof. Taking product-exponential transposes, this is equivalent to showing that $\phi(b \times X)$ and $\phi (a \times X)$ classify the same subobject of $R \times X$. By the above, $R$ induces equivalence relations $R_U$ on $\operatorname{Hom}_{\mathbf{C}}(U,X)$ for each $U \in \mathbf{C}$. Composing by $(a,b) \times X$, we see that a map $U \to R \times X$ is equivalent to specifying three morphisms $f_1, f_2 f_3 \in \operatorname{Hom}_{\mathbf{C}}(U,X)$ such that $f_1 \sim_{R_U} f_2$. Examining the diagram
(respectively, the one with $S_a$ switched for $S_b$ and $\pi_2$ switched for $\pi_1$), we see that a map $U \to R \times X$ factors through $S_a$ (resp. $S_b$) precisely when $f_1 \sim_{R_U} f_3$ (resp. $f_2 \sim_{R_U} f_3$.) By symmetry and transitivity of $R_U$, $S_a$ and $S_b$ factor through each other and so are the same subobject. $\square$