同伦类型论中实数的形式化
Formalising Real Numbers in Homotopy Type Theory
摘要：
柯西实数可以定义为有理数的柯西序列的商。通过将柯西实数序列提升为有理数柯西序列，定义了柯西实数序列的极限。这种提升需要可数选择公理或排中律公理，而这两个公理在同伦类型论中都不存在。为了解决这个问题，单叶基础计划使用了一个更高的归纳-归纳类型来定义柯西实数作为由有理数生成的自由柯西完备度量空间。我们推广这个构造来定义由任意度量空间生成的自由Cauchy完备度量空间。这就形成了具有Lipschitz函数的度量空间范畴中的单子。当应用于有理数时，它定义了柯西实数。最后，我们可以使用Altenkirch和Danielson（2016）的多项式来定义一个比较实数和有理数的半决策过程。整个建筑已正式在科克证明助手。可在https://github.com/SkySkimmer/HoTTClasses/tree/CPP2017上查阅。
英文摘要：
Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. 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 .
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
