# 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.)

$$[\![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$$.