Gaëtan Gilbert
ABSTRACT
Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. In this case, the limit of a Cauchy sequence of Cauchy reals is defined through lifting it to a sequence of Cauchy sequences of rationals.
This lifting requires the axiom of countable choice or excluded middle, neither of which is available in homotopy type theory. To address this, the Univalent Foundations Program uses a higher inductive-inductive type to define the Cauchy reals as the free Cauchy complete metric space generated by the rationals.
We generalize this construction to define the free Cauchy complete metric space generated by an arbitrary metric space. This forms a monad in the category of metric spaces with Lipschitz functions. When applied to the rationals it defines the Cauchy reals. Finally, we can use Altenkirch and Danielson (2016)'s partiality monad to define a semi-decision procedure comparing a real number and a rational number.
The entire construction has been formalized in the Coq proof assistant. It is available at https://github.com/SkySkimmer/HoTTClasses/tree/CPP2017 .
- The Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics, first edition. http://homotopytypetheory.org/book/ (2013) Bas Spitters and Eelis van der Weegen. Type Classes for Mathematics in Type Theory. https://math-classes.github.io/ (2011) T. Altenkirch and N. A. Danielsson and N. Kraus. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. ArXiv e-prints (2016). https://arxiv.org/abs/1610.Google Scholar
- 09254 Russell O’Connor. A Monadic, Functional Implementation of Real Numbers. Mathematical Structures in Computer Science 17(1): 129-159 (2007) Introduction Context Premetric Spaces Continuity Notions The Premetric Space of Functions Cauchy Completion Definition and Eliminators Properties of the Completion Monadic Structure of the Completion Cauchy Reals Addition and Order Relations Multiplication Multiplicative Inverse A Partial Function on Cauchy Reals The Partiality Monad The Sierpinski Space Interleaving Partial Comparison of Real Numbers with Rational Numbers Conclusion Acknowledgements Google ScholarDigital Library
Index Terms
- Formalising real numbers in homotopy type theory
Recommendations
The HoTT library: a formalization of homotopy type theory in Coq
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and ProofsWe report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic ...
Finite sets in homotopy type theory
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsWe study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type ...
The real projective spaces in homotopy type theory
LICS '17: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer ScienceHomotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct ...
Comments