@ykm: "Corepresents", since we're discussing a property of maps out of $X \wedge Y$.

@HeinrichD: By "$K = e^{1/x}$ on $x \neq 0$" I mean the subsheaf of the sheaf of continuous functions whose sections on an open subset $U\subseteq\mathbb{R}^1$ are given by $\{e^{1/x}\}$ if $0 \not\in U$ and $\emptyset$ otherwise. The reason why the condition fails for this choice of $K$ is that $e^{1/x}$, and also no product of $e^{1/x}$ with an arbitrarily high power of $x$, can be extended to a global continuous function. You can read some details (about the situation with schemes, not with manifolds) in Section 9 of these notes.

@HeinrichD: I'm sorry for the late reply. $K$ is only a set of global sections from the point of view of the internal language. From the external point, $K$ is a subsheaf of $\mathcal{O}_X$. The internal condition "$f$ is invertible $\Rightarrow$ $K$ is a singleton" means that on the open subset $D(f)$, the sheaf $K$ contains only a single section. The gist of the statement is that any such section can be extended to a global one, after clearing denominators. It is satisfied for affine schemes since the maps $\Gamma(X,\mathcal{O}_X)[f^{-1}] \to \Gamma(D(f),\mathcal{O}_X)$ are bijective.

You probably mean $2^\mathbb{N}$ instead of $\mathbb{N}$, right? (As $\mathbb{N}$ is not compact.) Also momentarily I fail to see how the Kleene tree gives a problem for $\mathsf{all}$, could you elaborate on that? I see it for the related function $\mathsf{max} : \mathbb{N}^{2^\mathbb{N}} \to \mathbb{N}$ which calculates the maximal value of a given function $2^\mathbb{N} \to \mathbb{N}$, since the Kleene tree gives rise to an unbounded such function.

For anyone looking for a counterexample let me remark that the most naive example does not work: Let $f : \mathbb{R} \to \mathbb{R}$ be a fixed continuous function. Let $X$ be a metric space. The object of Dedekind real numbers in the sheaf topos $\mathrm{Sh}(X)$ is the sheaf $\mathcal{C}_X$ of continuous functions on $X$. The function $f$ induces a morphism $\mathcal{C}_X \to \mathcal{C}_X$ by postcomposition, that is internally a function $\mathbb{R} \to \mathbb{R}$. From the internal point of view, this function is continuous and verifies the strong IVT.

I agree. Just a remark: In (one of the flavours of) realizability theory, a realizer for a formula like $\forall a \exists b$ is precisely a Turing machine which calculates a suitable $b$ when given an arbitrary $a$ as input.

@HeinrichD: Indeed. And this field property has many consequences, for instance generic freeness. I just added a further property to the answer, one which is sufficiently strong to distinguish schemes from manifolds.

@HeinrichD: Just saw (part of) your deleted question on characterization of Zariski toposes in my mail feed. If you drop me a mail ([email protected]), I can try to give a (very partial) answer. Also I'd be interested in the full text of your question!

I wholeheartedly with your answer. Two small additions: Firstly, one can prove "$\forall n,m \in \mathbb{N}: n = m \vee n \neq m" by induction. Secondly, a rather large and nice field which has decidable equality is the field of algebraic numbers. The extra information coming with an algebraic number, that is a polynomial with rational coefficient which has the given number as a zero, is enough to intuitionistically verify whether the number is zero or not zero.

@HeinrichD: It depends on how you actually verify the "easy case" in the proof of the corollary in my answer. If you do it by (somewhat needlessly) employing Lemma 6.4 (using the basis as generating family), then my proof unravels to Shin's proof. I don't know yet what my proof unravels to if you verify the "easy case" by employing the standard isomorphism $R^n \otimes_R B \cong B^n$. I'll report when I know more!

Shin's proof is very nice! I wonder whether the explicit proof given in my answer is actually "the same" as his. In my proof lots of universal quantifications appear, but not all of thee might actually be needed.

Shin's proof can be salvaged as follows. We assume that $R$ is reduced and induct over the length $n$ of a generating family $(a_1,\ldots,a_n)$ of $A$. The case $n=0$ is trivial. For $n\geq1$ write $\alpha(r)=\sum_ir_ia_i$. Lemma 6.4 yields elements $h_{ij}\in R$ and $c_j\in B$ such that $r_i\beta(1)=\sum_jh_{ij}c_j$ for all $i$ and $\sum_ih_{ij}a_i=0$ for all $j$. We can apply the induction hypothesis to each of the rings $R[h_{ij}^{-1}]$, showing that $r=0$ there. Thus $h_{ij}r=0\in R$ for all $i,j$. Thus $\beta(rr_i)=0$, therefore $rr_i=0$ for all $i$. Finally $\alpha(r^2)=0$, so $r=0$.

@HeinrichD: Just as an aside, the literal translation of "Any finitely generated module is not not finite free" is very similar to your lemma: "Let $M$ be a finitely generated $R$-module where $R$ is reduced. Assume that for all $f \in R$ such that the localized module $M_f$ is projective as an $R_f$-module we have $f = 0$. Then $R = 0$." (This is because an $R$-module $A$ is projective and finitely generated if and only if $A^\sim$ is finite free from the internal point of view of the Zariski topos of $R$.)