Brouwer's Theorem in the free topos?

Question

In Introduction to Higher-Order Categorical Logic, Lambek & Scott remark that Brouwer's Theorem (all functions $\mathbb{R}\to\mathbb{R}$ are continuous) holds in the free topos $\mathcal{T}$.

EDIT: L&S do not say that it holds in the free topos, they are incorrectly quoted as saying this in the nLab.

Let me present a naïve syllogism which is bothering me:

1. The free topos is the initial object in the category of toposes & logical morphisms / nLab
2. Logical morphisms preserve truth of sentences in the internal language of toposes. / nLab
3. Brouwer's theorem is false in the topos of sets $\mathbf{Set}$.
4. By (1) there is a logical morphism $\mathcal{T}\to\mathbf{Set}$ whence by (2) Brouwer's theorem should hold in $\mathbf{Set}$, which is not the case.

Therefore, I think I have misinterpreted something. Is the claimed theorem (attributed to Joyal by Lambek & Scott) really that Brouwer's Theorem holds internally to $\mathcal{T}$ (i.e. as a statement in the internal language of $\mathcal{T}$)?

Or could it be that it holds externally of the functions defined in $\mathcal{T}$ or something? The latter case sounds plausible, because we can certainly show that the definable functions in extensional type theory are continuous, but we cannot do this internally for certain important reasons (I believe Beeson's Foundations of Constructive Mathematics explains why—later, Escardó and Xu have established this also for intensional type theory).

Thanks to anyone who can help demystify this for me.

Answer 1

To summarize, the Lambek and Scott book actually says that functions on the reals in the free topos represent continuous functions. The nLab previously made the stronger claim that Brouwer's Theorem holds in the free topos (which is not the case for the reasons I described), but I have edited the page appropriately.

Answer 2

Dear All: you must be precise on what you mean by Brouwer's theorem. The free topos is closed under many rules, but unlike the realizability topos, it is seldom closed under the internal implicative statement. Thus the free topos is closed under Church's rule (see the original paper by Lambek and me, Intuitionist type theory and the free topos, JPAA 19 (1980) doi:10.1016/0022-4049(80)90102-4), but obviously not the internal Church's theorem. The statement about Brouwer's principle (an original beautiful sketch of a proof, due to Joyal, but never published) is in LS, p. viii (Introduction). Here is the version you would want: using an appropriate version of the reals, if $\vdash f\colon \mathbb{R}\to \mathbb{R}$ (is provable in higher order int. logic) then $\vdash$ "$f$ is continuous". And, by the way, of course this is formalizable in the internal logic. For a reasonable proof, similar continuity rules were formalized and proved by Susumu Hayashi for second order logics and type theories in the 1970's. There are some versions of this also in Troelstra's Metamathematical Investigation of Intuitionistic Arithmetic and Analysis SLNM 344 (doi:10.1007/BFb0066739) (the "bible" of such formalizations). Phil Scott