# Brouwer's Theorem in the free topos?

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.

• Do you have a page no for Lambek/Scott? – Jonas Frey Mar 15 '17 at 3:24
• My guess is that Brouwer's theorem is not a statement in the internal language. – Qiaochu Yuan Mar 15 '17 at 3:24
• @JonasFrey It is mentioned (attributed to Joyal, apparently unpublished) in the preface on page viii, but I cannot find a statement of the theorem or proof elsewhere in the book. – Jonathan Sterling Mar 15 '17 at 3:27
• I think it is what you write in the last paragraph. LS do not say that that the statement "all endomorphisms on R are continuous" holds, but that all arrows on R "represent continuous functions", which is a more external statement. – Jonas Frey Mar 15 '17 at 3:34
• Jonathan, thanks for asking! Please also consider making a note of your edit at the nForum: nforum.ncatlab.org/discussions/?CategoryID=0 – Todd Trimble Mar 15 '17 at 3:57

• Hello @PhilipScott! You can't meant that the meta-theorem "if $\vdash f : R \to R$ then $\vdash \text{$f$continuous}$ is formalizable in the internal logic. It's not an internal statement. – Andrej Bauer Mar 15 '17 at 20:32