Some intuitionist principles in the free topos

Abstract

Brouwer's principle/theorem states that all total functions R→R are continuous. Obviously not classically true this result was a theorem of Brouwer in his intuitionistic setting. The formalization(s) of intuitionistic logic provides us with systems of logic in which to ask is this principle provable? In a higher order setting (e.g. higher order type theory) one has two ways of expressing this principle. First is simply the statement ⊢∀f&parl0;f:R&rarrr; R⇒'' fiscontinuous'' &parr0; Second is as a meta theorem ⊢f:R→R⊢'' fis continuous'' In this work we present a categorical proof that the second formulation holds in higher order Heyting arithmetic (HAH). Our proof is general enough however to obtain the same continuity principle with R replaced by a "sufficiently nice" space S, a notion which is made precise.