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:

- The free topos is the initial object in the category of toposes & logical morphisms / nLab
- Logical morphisms preserve truth of sentences in the internal language of toposes. / nLab
- Brouwer's theorem is false in the topos of sets $\mathbf{Set}$.
- 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.

4more comments