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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## Standard

**The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation.** / Escardo, Martin; Xu, Chuangjie.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## Harvard

*13th International Conference on Typed Lambda Calculi and Applications, Proceedings.*LIPICS - Leibniz International Proceedings in Informatics, vol. 38, Schloss Dagstuhl, pp. 153-164, 13th International Conference on Typed Lambda Calculi and Applications, Warsaw, Poland, 1/07/15. https://doi.org/10.4230/LIPIcs.TLCA.2015.153

## APA

*13th International Conference on Typed Lambda Calculi and Applications, Proceedings*(pp. 153-164). (LIPICS - Leibniz International Proceedings in Informatics; Vol. 38). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.TLCA.2015.153

## Vancouver

## Author

## Bibtex

}

## RIS

TY - GEN

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

AU - Escardo, Martin

AU - Xu, Chuangjie

PY - 2015/7/1

Y1 - 2015/7/1

N2 - 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.

AB - 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.

U2 - 10.4230/LIPIcs.TLCA.2015.153

DO - 10.4230/LIPIcs.TLCA.2015.153

M3 - Conference contribution

SN - 9783939897873

T3 - LIPICS - Leibniz International Proceedings in Informatics

SP - 153

EP - 164

BT - 13th International Conference on Typed Lambda Calculi and Applications, Proceedings

A2 - Altenkirch, Thorsten

PB - Schloss Dagstuhl

T2 - 13th International Conference on Typed Lambda Calculi and Applications

Y2 - 1 July 2015 through 3 July 2015

ER -