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

摘要

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-Howa