Univalent Foundations Project ( a modified version of an NSF grant application )
Univalent Foundations Project ( a modified version of an NSF grant application )
复制标题
Univalent 基金会项目（NSF 拨款申请的修改版本）
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
V. Voevodsky
中科院分区：
文献类型：
--
作者：
V. Voevodsky
在完成Bloch-Kato猜想的证明的过程中，我思考了很多下一步该做什么。最终，我确信当前数学中最有趣和最重要的方向是那些与过渡到一个新时代有关的方向，这个新时代的特点是广泛使用自动化工具来构建证明和验证。我从2003/04学年开始积极学习相关科目。几年前，我提出了一个关于依赖类型理论（在编程语言理论中广泛使用的形式系统）的新语义的想法。与通常将类型解释为集合的语义不同，这种“一元语义”将类型解释为同伦类型。单价解释的关键性质是它满足单价公理，这是一个新的公理，它使得在由适当定义的弱等价连接的类型之间自动传递构造和证明成为可能。在2009/2010年，我做了一些关于一元解释的演讲，引起了类型理论界的极大兴趣。到目前为止，已经计划了两个特别活动来进一步讨论相关的想法——一个是2011年3月在奥伯沃尔法赫举行的研讨会，另一个是2012-2013年在高等研究院举行的为期一年的特别项目。最终，我明白了，单价语义只是第一步，我正在研究数学的新基础。这些“单价基础”的主要特征如下：一元基础自然包括范畴思维和更高范畴思维的“公理化”。2. 使用一类称为依赖类型系统的语言，可以方便地形式化单价基础。3. 一元基础是基于同伦类型“世界”的直接公理化，而不是基于集合世界。4. 一元基础既可用于构造数学，也可用于非构造数学。为了了解同伦理论与数学基础的关系，请考虑通常同伦范畴中的以下定义：如果A（同伦）类型T可缩并，则称其为h级0；如果对于T的任意两点，这两点之间的路径空间…
1 General outline of the proposed project While working on the completion of the proof of the Bloch-Kato conjecture I have thought a lot about what to do next. Eventually I became convinced that the most interesting and important directions in current mathematics are the ones related to the transition into a new era which will be characterized by the widespread use of automated tools for proof construction and verification. I have started to actively learn about the related subjects around 2003/04. A few years ago I have come up with an idea for a new semantics for dependent type theories-the class of formal systems which are widely used in the theory of programming languages. Unlike the usual semantics which interpret types as sets this " univalent semantics " interprets types as homotopy types. The key property of the univalent interpretation is that it satisfies the univalence axiom a new axiom which makes it possible to automatically transport constructions and proofs between types which are connected by appropriately defined weak equivalences. In 2009/2010 I made a number of presentations on the univalent interpretation which were received with great interest by the type theoretic community. As of today two special events have been planned for the further discussion of the related ideas-a workshop in Oberwolfach in March 2011 and a year long special program at the Institute for Advanced Study in 2012-2013. Eventually it became clear to me that the univalent semantics is just a first step and that I am really working on new foundations of mathematics. The key features of these " univalent foundations " are as follows: 1. Univalent foundations naturally include " axiomatization " of the categorical and higher categorical thinking. 2. Univalent foundations can be conveniently formalized using the class of languages called dependent type systems. 3. Univalent foundations are based on direct axiomatization of the " world " of homotopy types instead of the world of sets. 4. Univalent foundations can be used both for constructive and for non-constructive mathematics. To see what homotopy theory has to do with foundations of mathematics consider the following definitions which take place in the usual homotopy category: A (homotopy) type T is said to be of h-level 0 if it is contractible, A (homotopy) type T is said to be of h-level 1 if for any two points of T the space of paths between these two points …