The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Colleges, School and Institutes


If all functions (N -> N) -> N are continuous then 0 = 1. We establish this in intensional (and hence also in extensional) intuitionistic dependent-type theories, with existence in the formulation of continuity expressed as a Sigma type via the Curry-Howard interpretation. But with an intuitionistic notion of anonymous existence, defined as the propositional truncation of Sigma, it is consistent that all such functions are continuous. A model is Johnstone’s topological topos. On the other hand, any of these two intuitionistic conceptions of existence give the same, consistent, notion of uniform continuity for functions (N -> 2) -> N, again valid in the topological topos. It is open whether the consistency of (uniform) continuity extends to homotopy type theory. The theorems of type theory informally proved here are also formally proved in Agda, but the development presented here is self-contained and doesn't show Agda code.


Original languageEnglish
Title of host publication13th International Conference on Typed Lambda Calculi and Applications, Proceedings
EditorsThorsten Altenkirch
Publication statusPublished - 1 Jul 2015
Event13th International Conference on Typed Lambda Calculi and Applications - Warsaw, Poland
Duration: 1 Jul 20153 Jul 2015

Publication series

NameLIPICS - Leibniz International Proceedings in Informatics
PublisherDagstuhl Publishing
ISSN (Print)1868-8969


Conference13th International Conference on Typed Lambda Calculi and Applications