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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Awodey, S., Bauer, A.: Propositions as [types]. Journal of Logic and Computation 14(4), 447–471 (2004)
Baez, J.C., Hoffnung, A.E.: Convenient categories of smooth spaces (2008)
Bauer, A., Birkedal, L., Scott, D.: Equilogical spaces. Theoret. Comput. Sci. 315(1), 35–59 (2004)
Bauer, A., Simpson, A.: Continuity begets continuity. Presented at Trends in Constructive Mathematics in Germany (2006)
Beeson, M.J.: Foundations of Constructive Mathematics. Springer (1985)
Bove, A., Dybjer, P.: Dependent types at work. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) LerNet 2008. LNCS, vol. 5520, pp. 57–99. Springer, Heidelberg (2009)
Community. Agda wiki, http://wiki.portal.chalmers.se/agda/
Coquand, T., Jaber, G.: A note on forcing and type theory. Fundamenta Informaticae 100(1-4), 43–52 (2010)
Coquand, T., Jaber, G.: A computational interpretation of forcing in type theory. In: Epistemology Versus Ontology, vol. 27, pp. 203–213. Springer, Netherlands (2012)
Curien, P.-L.: Substitution up to isomorphism. Fundamenta Informaticae 19(1/2), 51–85 (1993)
Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 120–134. Springer, Heidelberg (1996)
Escardó, M., Lawson, J., Simpson, A.: Comparing Cartesian closed categories of (core) compactly generated spaces. Topology Appl. 143(1-3), 105–145 (2004)
Fourman, M.P.: Notions of choice sequence. In: The L. E. J. Brouwer Centenary Symposium Proceedings of the Conference Held in Noordwijkerhout, vol. 110, pp. 91–105 (1982)
Fourman, M.P.: Continuous truth I, non-constructive objects. In: Proceedings of Logic Colloquium, Florence 1982, vol. 112, pp. 161–180. Elsevier (1984)
Hofmann, M.: On the interpretation of type theory in locally Cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 427–441. Springer, Heidelberg (1995)
Johnstone, P.T.: On a topological topos. Proceedings of the London Mathematical Society 38(3), 237–271 (1979)
Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford University Press (2002)
Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer (1992)
Normann, D.: Recursion on the countable functionals. Lec. Not. Math, vol. 811. Springer (1980)
Normann, D.: Computing with functionals—computability theory or computer science? Bull. Symbolic Logic 12(1), 43–59 (2006)
Seely, R.A.G.: Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society 95(1), 33–48 (1984)
Spanier, E.H.: Quasi-topologies. Duke Mathematical Journal 30(1), 1–14 (1963)
van der Hoeven, G., Moerdijk, I.: Sheaf models for choice sequences. Annals of Pure and Applied Logic 27(1), 63–107 (1984)
Xu, C., Escardó, M.H.: A constructive model of uniform continuity, developed in Agda. Available at the Authors’ Institutional Web Pages (2012-2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xu, C., Escardó, M. (2013). A Constructive Model of Uniform Continuity. In: Hasegawa, M. (eds) Typed Lambda Calculi and Applications. TLCA 2013. Lecture Notes in Computer Science, vol 7941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38946-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-38946-7_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38945-0
Online ISBN: 978-3-642-38946-7
eBook Packages: Computer ScienceComputer Science (R0)