Brouwer's Theorem in the free topos?

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.

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 on Intuitionist type theory and the free topos, JPAA (1980), 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 |-- f: R-->R (is provable in higher order int. logic) then |-- "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 SLN344 (the "bible" of such formalizations). Phil Scott