极简主义基础与同伦类型论的兼容性
The Compatibility of the Minimalist Foundation with Homotopy Type Theory
AI总结：
本文证明MF的内涵与外延两个层次均与HoTT兼容，关键在于HoTT借助单价公理和高归纳商类型统一内涵与外延特征，从而使MF获得全新可计算模型。
摘要：
极简主义基础（Minimalist Foundation，简称MF）是由Maietti和Sambin于2005年构想、随后由Maietti于2009年完全形式化的一个构造性数学的两层基础。MF充当文献中最相关数学基础之间的共同核心：对每种基础，选择MF的适当层次，并以兼容的方式进行翻译，即保留逻辑构造子和集合论构造子的含义。这种两层结构由一个内涵层次、一个外延层次，以及后者到前者的解释组成，以便从涉及日常数学实践中使用的外延构造的数学证明里提取内涵计算内容。2013年，文献中出现了一个全新的构造性数学基础，称为同伦类型论（Homotopy Type Theory，简称HoTT），它是Voevodsky的具有计算性质的单价基础的一个例子。迄今为止，MF的任何层次都尚未被证明与文献中的任何单价基础兼容。在此，我们证明MF的两个层次都与HoTT兼容。这一结果之所以成为可能，得益于HoTT的独特之处：它通过假定Voevodsky的单价公理和高归纳商类型，将类型论的内涵特征与外延特征结合起来。作为一个相关结果，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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
