I clarify my previous question with a simple example. It is also a simpler (and more general) question whose resolution resolves the previous question on interpreting a theory in another.
The reference is the book [CDM] ``Algebraic foundations of Many-valued Reasoning’’ Kluver Academic Publishers (2000)
Consider the theory of MV-algebras. By a standard choice argument we have:
1) Every MV-algebra is a subalgebra of a product of MV-chains with the pointwise structure.
Corollary. Given any two terms $p(x, y, \ldots z),\; q(x, y, \ldots z)$, the equation $p(x, y, \ldots z) = q(x, y, \ldots z)$ holds in every MV-algebra if and only if it holds in every MV-chain.
2) $x \oplus y < 1 \Rightarrow x \odot y = 0$ holds in any MV-chain (very easy, [CDM] 1.6.1 page 27).
3) $x \oplus 0 = x$ (axiom, [CDM] page 7), $\hspace{2ex}$ $1 \oplus x = 1$ (very easy, [CDM] page 9).
4) The equation (a): $(x \oplus y) \oplus (x \odot y) = x \oplus y$ holds in any MV-algebra.
proof: By 1) it is enough to prove it for MV-chains:
case $(x \oplus y) = 1$, we have $(1 \oplus (x \odot y) = x \oplus y$
case $(x \oplus y) < 1$, we have $(x \oplus y) \oplus 0 = x \oplus y$
both cases hold by 3).
5) By the completeness theorem the equation (a) follows from the axioms of the theory,
(intuicionistically or classically ?)
thus the equation should hold in (the internal language) for any MV-algebra object in any Grothendieck topos ?
5) Also we can argue via the presheaf classifying topos of the theory of MV-algebras and come to the same conclusion ?
Is 5) valid ?
Notice that, besides the use of choice in 1), we are using an exclude middle in 4) (invalid for example in the MV-chain [0, 1], the real interval in the object of reals of the topos).