论文标题
极简主义基础与同质类型理论的兼容性
The Compatibility of the Minimalist Foundation with Homotopy Type Theory
论文作者
论文摘要
极简主义的基础是短MF，是Maietti和Sambin在2005年构思的建设性数学的两级基础设置理论构造函数。两级结构由一个强度级别，延伸的结构组成，以及对后者的解释，以便从涉及日常数学实践中使用的扩展结构的数学证据中提取强度计算内容。 2013年，对于简短的霍特（Short Hott）而言，文献中出现了一个全新的建设性数学基础，这是Voevodsky具有计算本质的单价基础的一个例子。到目前为止，尚未证明MF水平与文献中的任何单价基础都兼容。在这里，我们表明两个MF级别都与Hott兼容。通过假设Voevodsky的Univalence Axiom和更高的电感商类型，将HOTT的特殊性与扩展理论结合在一起，这使得该结果成为可能。作为一个相关结果，MF继承了全新的可计算模型。
The Minimalist Foundation, for short MF, is a two-level foundation for constructive mathematics ideated by Maietti and Sambin in 2005 and then fully formalized by Maietti in 2009. MF serves as a common core among the most relevant foundations for mathematics in the literature by choosing for each of them the appropriate level of MF to be translated in a compatible way, namely by preserving the meaning of logical and set-theoretical constructors. The two-level structure consists of an intensional level, an extensional one, and an interpretation of the latter in the former in order to extract intensional computational contents from mathematical proofs involving extensional constructions used in everyday mathematical practice. In 2013 a completely new foundation for constructive mathematics appeared in the literature, called Homotopy Type Theory, for short HoTT, which is an example of Voevodsky's Univalent Foundations with a computational nature. So far no level of MF has been proved to be compatible with any of the Univalent Foundations in the literature. Here we show that both levels of MF are compatible with HoTT. This result is made possible thanks to the peculiarities of HoTT which combines intensional features of type theory with extensional ones by assuming Voevodsky's Univalence Axiom and higher inductive quotient types. As a relevant consequence, MF inherits entirely new computable models.
