Characterization of equality of terms in the internal logic of toposes

This is a nice note explaining the internal logic of a topos. I'll use the notation and terminology defined in that article.

Let $\Sigma$ be a higher-order signature and $M$ an interpretation of $\Sigma$ in an elementary topos $\mathcal E$ (in particular, $M$ assigns to each sort $A$ in $\Sigma$ an object $MA$).

Question: Let $A$ and $B$ be sorts in $\Sigma$, and $t$ and $s$ $\Sigma$-terms of type $B$ in context $x\colon A$. Is it true that $[\![x.t]\!]_M = [\![x.s]\!]_M$ as morphisms $MA\to MB$ if and only if the subobject $[\![\forall x\colon A.t=s]\!]_M\hookrightarrow 1$ is the full subobject?

If yes, does that follow from the definitions in chapter 2 or does one need Kripke-Joyal semantics (chapter 4) to see that? Is it also possible to prove that using Kripke-Joyal semantics (instead of the definitions)? (I want to know both.)

Yes, it follows directly from the definitions.

$[\![x.s]\!] = [\![x.t]\!]$ if and only if their equalizer $[\![x.s=t]\!]$ is the top subobject of $A$. If $[\![x.s=t]\!]$ is the top subobject of $A$, then since $\forall_!$ is a right adjoint, it preserves the top (terminal) subobject, so $[\![\forall x. s=t]\!]$ is the top subobject of $1$. Conversely, if $[\![\forall x. s=t]\!]$ is the top subobject of $1$, then $[\![\top]\!]\leq [\![\forall x.s=t]\!]$, so by adjointness, $[\![x.\top]\!]=!^*[\![\top]\!]\leq [\![x.s=t]\!]$, so the latter is the top subobject of $A$.

I'm not quite sure what it would mean to prove this using Kripke-Joyal semantics, but here's a go. We have $[\![x.s]\!] = [\![x.t]\!]$ if and only if $U\Vdash (s=t)[u/x]$ for all $u\colon U\to A$ (by Theorem 4.6(iii)) if and only if $1\Vdash \forall x.s=t$ (by Theroem 4.6(ix)) if and only if $[\![\forall x. s=t]\!]$ is the top subobject of $1$.