A constructive model of uniform continuity

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

Authors

Colleges, School and Institutes

Abstract

We construct a continuous model of Gödel's system T and its logic HAω in which all functions from the Cantor space 2 to the natural numbers are uniformly continuous. Our development is constructive, and has been carried out in intensional type theory in Agda notation, so that, in particular, we can compute moduli of uniform continuity of T-definable functions 2 → ℕ. Moreover, the model has a continuous Fan functional of type (2 → ℕ) → ℕ that calculates moduli of uniform continuity. We work with sheaves, and with a full subcategory of concrete sheaves that can be presented as sets with structure, which can be regarded as spaces, and whose natural transformations can be regarded as continuous maps.

Details

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
Publication statusPublished - 2013
Event11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Netherlands
Duration: 26 Jun 201328 Jun 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7941 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
Country/TerritoryNetherlands
CityEindhoven
Period26/06/1328/06/13

Keywords

  • Constructive mathematics, Fan functional, Gödel's system T, HA, intuitionistic type theory, sheaves, topological models, topos theory, uniform continuity