We identify yet another category equivalent to that of Kleene–Kreisel continuous functionals. Reasoning constructively and predicatively, all functions from the Cantor space to the natural numbers are uniformly continuous in this category. We do not need to assume Brouwerian continuity axioms to prove this, but, if we do, then we can show that the full type hierarchy is equivalent to our manifestation of the continuous functionals. We construct this manifestation within a category of concrete sheaves, called C-spaces, which form a locally cartesian closed category, and hence can be used to model system T and dependent types. We show that this category has a fan functional and validates the uniform continuity axiom in these theories. Our development is within informal constructive mathematics, along the lines of Bishop mathematics. However, in order to extract concrete computational content from our constructions, we formalized it in intensional Martin-Löf type theory, in Agda notation.
|Number of pages||3|
|Publication status||Published - 2014|
|Event||11th International Conference on Computability and Complexity in Analysis, CCA 2014 - Darmstadt, Germany|
Duration: 21 Jul 2014 → 24 Jul 2014
|Conference||11th International Conference on Computability and Complexity in Analysis, CCA 2014|
|Period||21/07/14 → 24/07/14|
Bibliographical notePublisher Copyright:
© CCA 2014 - 11th International Conference on Computability and Complexity in Analysis, Proceedings. All rights reserved.
ASJC Scopus subject areas
- Computer Networks and Communications
- Computer Science Applications