A constructive manifestation of the Kleene–Kreisel continuous functionals

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 principle 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, and we discuss the main technical aspects of this at the end of the paper.